(* Test 1 with solution - COSC 5V90 Fall 2016*)

Require Import List.
Import ListNotations.
Require Import PeanoNat.
Import Nat.

(* Question 1 (6 marks):
Write a function myRemove that myRemoves all occurance of a natural number from a list, i.e.,
myRemove l n is the list l in the same order without any occurances of n. For example
myRemove [1;2;3;4;3;2;1] 2 = [1;3;4;3;1].
Hint: 
- Use n =? m two compare two natural numbers (returns bool).
*)

Fixpoint myRemove (l : list nat)  (n : nat) : list nat :=
  match l with
   | [] => []
   | m::l' => if n =? m then myRemove l' n else m::myRemove l' n
  end.

(* Question 2 (10 marks):
Prove the lemma below.
Hints: 
- Use induction on l.
- A goal ~False can be solved using the tactic intuition.
- Use a case distinction on the Boolean condition of the if-statement in your program.
- You may want to use the lemmas:
   + not_in_cons : forall (A : Type) (x a : A) (l : list A), ~ In x (a :: l) <-> x <> a /\ ~ In x l
   + eqb_neq : forall x y : nat, (x =? y) = false <-> x <> y
*)

Lemma L1 : forall (l : list nat) (n : nat), ~In n (myRemove l n).
intros.
induction l; intros; simpl.
intuition.
case_eq (n =? a); intros.
trivial.
rewrite not_in_cons.
split.
rewrite eqb_neq in H; trivial.
trivial.
Qed.

(* Question 3 (14 marks):
Prove the lemma below.
Hints: 
- Use induction on l.
- Use the tactic contradiction if your assumptions are contradictory.
- Use a case distinction on the Boolean condition of the if-statement in your program.
- Use simpl on statements (assumption or goal) of the form In n (a::l) or In n [].
- Use destruct on assumption of the form A \/ B.
- left/right if the left/right part of a goal of the form A \/ B is actually true.
- You may want to use the lemmas:
   + eqb_eq : forall n m : nat, (n =? m) = true <-> n = m
*)

Lemma L2 : forall (l : list nat) (m n : nat), m <> n -> In m l -> In m (myRemove l n).
intros.
induction l; intros; simpl.
simpl in H0.
contradiction.
case_eq (n =? a); intros; simpl.
apply eqb_eq in H1. 
simpl in H0; destruct H0.
rewrite H0 in H1; symmetry in H1.
contradiction.
apply IHl in H0; trivial.
simpl in H0; destruct H0.
left; trivial.
apply IHl in H0.
right; trivial.
Qed.

(* Question 4 (10 marks):
Prove the lemma below.
Hints: 
- Use induction on l1.
- Use a case distinction on the Boolean condition of the if-statement in your program.
*)

Lemma L3 :  forall (l1  l2 : list nat) (n : nat), myRemove (l1 ++ l2) n = myRemove l1 n ++ myRemove l2 n.
intros.
induction l1; simpl.
trivial.
case_eq (n =? a); intros.
trivial.
simpl.
rewrite IHl1; trivial.
Qed.