Coq

Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.
  intros n. simpl. reflexivity. Qed.

(* The _l suffix in the names of these theorems is pronounced "on the left." *)

Theorem plus_1_l : forall n:nat, 1 + n = S n.
Proof.
  intros n. reflexivity. Qed.

Theorem mult_0_l : forall n:nat, 0 * n = 0.
Proof.
  intros n. reflexivity. Qed.

(* The arrow symbol is pronounced "implies." *)

Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.

(* assumptions: hypothèses *)

Proof.
  (* move both quantifiers into the context: *)
  intros n m.
  (* move the hypothesis into the context: *)
  intros H.
  (* rewrite the goal using the hypothesis: *)
  rewrite <- H.
  reflexivity. Qed.

(* (The arrow symbol in the rewrite has nothing to do with implication: it tells Coq to
apply the rewrite from left to right. To rewrite from right to left, you can use rewrite
<-. Try making this change in the above proof and see what difference it makes.) *)

Theorem plus_id_exercise : forall n m o : nat,
  n = m -> m = o -> n + m = m + o.
Proof.
  intros n m o.
  intros H.
  intros H0.
  rewrite -> H.
  rewrite -> H0.
  reflexivity. Qed.

(* every time you say Admitted you are leaving a door open for total nonsense to enter
Coq's nice, rigorous, formally checked world! *)

Theorem mult_0_plus : forall n m : nat,
  (0 + n) * m = n * m.
Proof.
  intros n m.
  rewrite -> plus_O_n.
  reflexivity. Qed.



Theorem mult_S_1 : forall n m : nat,
  m = S n ->
  m * (1 + n) = m * m.
Proof.
  intros n m.
  intros H.
  rewrite -> H.
  reflexivity. Qed.

Fixpoint eqb (n m : nat) : bool :=
  match n with
  | O => match m with
         | O => true
         | S m' => false
         end
  | S n' => match m with
            | O => false
            | S m' => eqb n' m'
            end
  end.

Notation "x =? y" := (eqb x y) (at level 70) : nat_scope.

Theorem plus_1_neq_0_firsttry : forall n : nat,
  (n + 1) =? 0 = false.
Proof.
  intros n.
  simpl. (* does nothing! *)
Abort.

Theorem plus_1_neq_0 : forall n : nat,
  (n + 1) =? 0 = false.
Proof.
  intros n. destruct n as [| n'] eqn:E.
  - reflexivity.
  - reflexivity. Qed.

(* The - signs on the second and third lines are called bullets
and they mark the parts of the proof that correspond to each generated subgoal. *)

(* One reasonable convention is to limit yourself to 80-character lines. *)

Theorem negb_involutive : forall b : bool,
  negb (negb b) = b.
Proof.
  intros b. destruct b eqn:E.
  - reflexivity.
  - reflexivity. Qed.

(* Qed. is required to make the function defined *)

Theorem andb_commutative : forall b c, andb b c = andb c b.
Proof.
  intros b c. destruct b eqn:Eb.
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
Qed.

(* Besides - and +, we can use * (asterisk) as a third kind of bullet. or *)

Theorem andb_commutative' : forall b c, andb b c = andb c b.
Proof.
  intros b c. destruct b eqn:Eb.
  { destruct c eqn:Ec.
    { reflexivity. }
    { reflexivity. } }
  { destruct c eqn:Ec.
    { reflexivity. }
    { reflexivity. } }
Qed.

Theorem andb3_exchange :
  forall b c d, andb (andb b c) d = andb (andb b d) c.
Proof.
  intros b c d. destruct b eqn:Eb.
  - destruct c eqn:Ec.
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
  - destruct c eqn:Ec.
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
Qed.


Theorem plus_1_neq_0' : forall n : nat,
  (n + 1) =? 0 = false.
Proof.
  intros [|n].
  - reflexivity.
  - reflexivity. Qed.

Theorem andb_commutative'' :
  forall b c, andb b c = andb c b.
Proof.
  intros [] [].
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
Qed.

Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros b c.
  intros H.

  destruct b eqn:Eb.
  { destruct c eqn:Ec.
    { reflexivity. }
    { rewrite <- H. reflexivity. } }
  { destruct c eqn:Ec.
    { rewrite <- H. reflexivity. }
    { rewrite <- H. reflexivity. } }
Qed.

Theorem zero_nbeq_plus_1 : forall n : nat,
  0 =? (n + 1) = false.
Proof.
  intros n. destruct n as [| n'] eqn:E.
  - reflexivity.
  - reflexivity. Qed.

Notation "x + y" := (plus x y)
                       (at level 50, left associativity)
                       : nat_scope.
Notation "x * y" := (mult x y)
                       (at level 40, left associativity)
                       : nat_scope.

(*

Coq tries to guess what scope is meant from context, so when it sees S(O*O) it guesses
nat_scope, but when it sees the cartesian product (tuple) type bool*bool (which we'll
see in later chapters) it guesses type_scope. Occasionally, it is necessary to help it
out with percent-notation by writing (x*y)%nat, and sometimes in what Coq prints it will
use %nat to indicate what scope a notation is in.

0%nat, which means O (the natural number 0 that we're using in this chapter), or 0%Z,
which means the Integer zero

*)

Fixpoint plus' (n : nat) (m : nat) : nat :=
  match n with
  | O => m
  | S n' => S (plus' n' m)
  end.

(*

Coq demands that some argument of every Fixpoint definition is "decreasing."
This requirement is a fundamental feature of Coq's design: In particular, it guarantees
that every function that can be defined in Coq will terminate on all inputs. However,
because Coq's "decreasing analysis" is not very sophisticated, it is sometimes necessary
to write functions in slightly unnatural ways.

*)

(*Fixpoint plus'' (n : nat) (m : nat) : nat :=
  match n with
  | O => m
  | S n' => S (plus'' (S n') m)
  end.

Compute  (plus'' 1 4).*)

(* only wants: Cannot guess decreasing argument of fix. ? *)


Theorem identity_fn_applied_twice :
  forall (f : bool -> bool),
  (forall(x : bool), f x = x) ->
  forall(b : bool), f (f b) = b.
Proof.
  intros f b.
  intros H.
  rewrite -> b. rewrite -> b.
  reflexivity.
  Qed. (*what did you expect ?*)

Theorem negation_fn_applied_twice :
  forall (f : bool -> bool),
  (forall(x : bool), f x = negb x) ->
  forall(b : bool), f (f b) = b.
Proof.
  intros f b.
  intros H.
  rewrite -> b. rewrite -> b.
  rewrite -> negb_involutive.
  reflexivity.
  Qed.

Definition andb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true => b2
  | false => false
  end.
Definition orb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true => true
  | false => b2
  end.

Compute (andb true false = orb true false).

Theorem andb_eq_orb :
  forall (b c : bool),
    (andb b c = orb b c) -> b = c.
Proof.
  intros b c.
  destruct b eqn:Eb.
  { destruct c eqn:Ec.
    { reflexivity. }
    { simpl. intros H. rewrite -> H. reflexivity. } } (* why nope ? *)
  { destruct c eqn:Ec.
    { simpl. intros H. rewrite -> H. reflexivity. }
    { simpl. reflexivity. } }
Qed.

Inductive bin : Type :=
  | Z
  | A (n : bin)
  | B (n : bin).

Fixpoint incr (m:bin) : bin := match m with
  | Z => B Z
  | A n => B n
  | B n => A (B n)
  end.

Example test_incr0: incr Z = B Z.
Proof. reflexivity. Qed.

Example test_incr1: incr (B Z) = A (B Z).
Proof. reflexivity. Qed.

Example test_incr2: incr (A (B Z)) = B (B Z).
Proof. reflexivity. Qed.

(* Example test_incr3: incr (B (B Z)) = A (A (B Z)).
Proof. reflexivity. Qed. *)

Fixpoint bin_to_nat (m:bin) : nat (* unary *)
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Theorem andb_true_elim2' : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros b c.
  intros H.

  destruct b eqn:Eb.
  { destruct c eqn:Ec.
    { reflexivity. }
    { rewrite <- H. reflexivity. } }
  { destruct c eqn:Ec.
    { rewrite <- H. reflexivity. }
    { rewrite <- H. reflexivity. } }
Qed.

Theorem andb_eq_orb :
  forall (b c : bool),
  (andb b c = orb b c) ->
  b = c.
Proof.
  intros b c.

  reflexivity.
Qed.

(* TODO last exercise *)

Theorem plus_n_O : forall n:nat, n = n + 0.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *) reflexivity.
  - (* n = S n' *) simpl. rewrite <- IHn'. reflexivity. Qed.

Theorem plus_n_O_bis : forall n:nat, n + 0 = n.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *) reflexivity.
  - (* n = S n' *) simpl. rewrite -> IHn'. reflexivity. Qed.

Theorem minus_diag : forall n,
  minus n n = 0.
Proof.
  (* WORKED IN CLASS *)
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *)
    simpl. reflexivity.
  - (* n = S n' *)
    simpl. rewrite -> IHn'. reflexivity. Qed.

Theorem mult_0_r : forall n:nat,
  n * 0 = 0.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *)
    simpl. reflexivity.
  - (* n = S n' *)
    simpl. rewrite -> IHn'. reflexivity. Qed.

Theorem plus_n_Sm : forall n m : nat,
  S (n + m) = n + (S m).
Proof.
  intros n m.
  (*induction n as [| n' IHn'].
  - (* n = 0 *)
    simpl. reflexivity.
  - (* n = S n' *)
    simpl. rewrite -> IHn'. reflexivity.
    induction m as [| m' IHm'].
    - (* m = 0 *)
      simpl. reflexivity.
    - (* m = S m' *)
      simpl. rewrite -> IHm'. reflexivity.*)
  (*induction n as [|n'].
  match m with
    | O => reflexivity
    | S n' => ( simpl. rewrite <- IHn'. reflexivity.)
  end*)
  induction n. (* how is that working ? *)
  - simpl. reflexivity.
  - simpl. rewrite -> IHn. reflexivity.
Qed.

Theorem plus_comm : forall n m : nat,
  n + m = m + n.
Proof.
  intros n m.
  induction n.
  - simpl. rewrite-> plus_n_O_bis. reflexivity.
  - simpl. rewrite <- plus_n_Sm. rewrite -> IHn. reflexivity.
Qed.

(*Theorem assoc : forall n m p : nat,
  n + m + p = n + (m + p).
Proof.

Qed.*)

(* "S (n + m + p)" with "S (n + (m + p))". *)

Theorem plus_assoc : forall n m p : nat,
  n + (m + p) = (n + m) + p.
Proof.
  intros n m p.
  induction n.
  - simpl. reflexivity.
  - simpl. rewrite -> IHn. reflexivity.
Qed.

Fixpoint double (n:nat) :=
  match n with
  | O => O
  | S n' => S (S (double n'))
  end.

Lemma double_plus : forall n, double n = n + n .
Proof.
  intros n.
  induction n.
  - simpl. reflexivity.
  - simpl. rewrite -> IHn. rewrite -> plus_n_Sm. reflexivity.
Qed.

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O => true
  | S O => false
  | S (S n') => evenb n'
  end.

Theorem evenb_S : forall n : nat,
  evenb (S n) = negb (evenb n).
Proof.
  intros n.
  induction n.
  - simpl. reflexivity.
  - rewrite -> IHn. simpl. rewrite negb_involutive. reflexivity.
Qed.

(*  Briefly explain the difference between the tactics destruct and induction.
Answer: Both are used to perform case analysis on an element of an inductively defined type; induction
also generates an induction hypothesis, while destruct does not
*)

Theorem plus_comme : forall n m : nat,
  n + m = m + n.
Proof.
  intros n m.
  induction n.
  - simpl. rewrite-> plus_n_O_bis. reflexivity.
  - simpl. rewrite <- plus_n_Sm. rewrite -> IHn. reflexivity.
(* S (n + m) = n + (S m). *)
Qed.

Theorem plus_rearrange_firsttry : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  assert (H: n + m = m + n). { rewrite -> plus_comm. reflexivity. }
  rewrite -> H.
  reflexivity. Qed.

(* what did they except as informal ? (there isn't any exemple
Oh I believe they want some Enlish instead of ! *)

(*

Assume n = 0:
  We've 0 + m = m + 0
  Which is clear by the definition of the + operation
Assume n a non null natural number
  We've (S n') + m = m + (S n')
  Which is clear by hypothetical hypothesis (* this name *)
Conclude for all n
*)

(* TODO other one *)

Inductive natprod : Type :=
| pair (n1 n2 : nat).

Notation "( x , y )" := (pair x y).

Definition swap_pair (p : natprod) : natprod :=
  match p with
  | (x,y) => (y,x)
  end.

Definition fst (p : natprod) : nat :=
  match p with
  | pair x y => x
  end.
Definition snd (p : natprod) : nat :=
  match p with
  | pair x y => y
  end.

Theorem snd_fst_is_swap : forall (p : natprod),
  (snd p, fst p) = swap_pair p.
Proof.
    intros p. destruct p as [n m]. simpl. reflexivity. Qed.

Theorem fst_swap_is_snd : forall (p : natprod),
  fst (swap_pair p) = snd p.
Proof.
  intros p. destruct p as [n m]. simpl. reflexivity. Qed.

Inductive natlist : Type :=
  | nil
  | cons (n : nat) (l : natlist).

Notation "x :: l" := (cons x l)
                     (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

Fixpoint repeat (n count : nat) : natlist :=
  match count with
  | O => nil
  | S count' => n :: (repeat n count')
  end.

Fixpoint length (l:natlist) : nat :=
  match l with
  | nil => O
  | h :: t => S (length t)
  end.

Fixpoint app (l1 l2 : natlist) : natlist :=
  match l1 with
  | nil => l2
  | h :: t => h :: (app t l2)
  end.

Notation "x ++ y" := (app x y)
                     (right associativity, at level 60).
Example test_app1: [1;2;3] ++ [4;5] = [1;2;3;4;5].
Proof. reflexivity. Qed.

Definition hd (default:nat) (l:natlist) : nat :=
  match l with
  | nil => default
  | h :: t => h
  end.
Definition tl (l:natlist) : natlist :=
  match l with
  | nil => nil
  | h :: t => t
  end.
Example test_hd1: hd 0 [1;2;3] = 1.
Proof. reflexivity. Qed.
Example test_hd2: hd 0 [] = 0.
Proof. reflexivity.

Fixpoint nonzeros (l:natlist) : natlist :=
  match l with
  | nil => nil
  | O::t => nonzeros t
  | h::t => h::(nonzeros t)
  end.

Example test_nonzeros:
  nonzeros [0;1;0;2;3;0;0] = [1;2;3].
  Proof. reflexivity. Qed.

Definition oddb (n:nat) : bool :=  (evenb n).

Fixpoint oddmembers (l:natlist) : natlist :=
  match l with
  | nil => nil
  | h::t => match (oddb h) with
    | true => h::(oddmembers t)
    | false => (oddmembers t)
    end
  end.

(*Example test_oddmembers:
  oddmembers [0;1;0;2;3;0;0] = [1;3].
  Proof. reflexivity. Qed.*)

Definition countoddmembers (l:natlist) : nat :=
  length (oddmembers l).

(*Example test_countoddmembers1:
  countoddmembers [1;0;3;1;4;5] = 4.
  Proof. reflexivity. Qed.

Example test_countoddmembers2:
  countoddmembers [0;2;4] = 0.
  Proof. reflexivity. Qed.

Example test_countoddmembers3:
  countoddmembers nil = 0.
  Proof. reflexivity. Qed.*)

Fixpoint alternate (l1 l2 : natlist) : natlist :=
  match l1, l2 with
  | [], _ => l2
  | t::q, y::s => t::y::(alternate q s)
  | _, [] => l1
  end.

Example test_alternate1:
  alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
  Proof. reflexivity. Qed.

Example test_alternate2:
  alternate [1] [4;5;6] = [1;4;5;6].
  Proof. reflexivity. Qed.

Example test_alternate3:
  alternate [1;2;3] [4] = [1;4;2;3].
  Proof. reflexivity. Qed.

Example test_alternate4:
  alternate [] [20;30] = [20;30].
  Proof. reflexivity. Qed.

Definition bag := natlist.

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil => O
  | h::t => match h =? v with
    | false => count v t
    | true => S (count v t)
    end
  end.

Example test_count1: count 1 [1;2;3;1;4;1] = 3.
  Proof. reflexivity. Qed.
Example test_count2: count 6 [1;2;3;1;4;1] = 0.
  Proof. reflexivity. Qed.

Definition sum : bag -> bag -> bag := app.

Example test_sum1: count 1 (sum [1;2;3] [1;4;1]) = 3.
 Proof. reflexivity. Qed.

Definition add (v:nat) (s:bag) : bag :=
  v::s. (* left or right, not precised *)

Example test_add1: count 1 (add 1 [1;4;1]) = 3.
 Proof. reflexivity. Qed.
Example test_add2: count 5 (add 1 [1;4;1]) = 0.
 Proof. reflexivity. Qed.

(* Definition member (v:nat) (s:bag) : bool :=
  match s with
  | [] => false
  | h::t => match h =? v with
    | true => true
    | false => member v t
    end
  end. *)

Definition member (v:nat) (s:bag) : bool :=
  match count v s with
  | 0 => false
  | _ => true
  end.

Example test_member1: member 1 [1;4;1] = true.
 Proof. reflexivity. Qed.
Example test_member2: member 2 [1;4;1] = false.
 Proof. reflexivity. Qed.

(* impossible not to supply v argument when calling remove_on *)

Fixpoint remove_one (v:nat) (s:bag) : bag :=
  match s with
  | [] => []
  | h::t => match h =? v with
    | true => t
    | false => h::(remove_one v t)
    end
  end.

(* Compute (remove_one []). *)

Example test_remove_one1:
  count 5 (remove_one 5 [2;1;5;4;1]) = 0.
 Proof. reflexivity. Qed.

Example test_remove_one2:
  count 5 (remove_one 5 [2;1;4;1]) = 0.
 Proof. reflexivity. Qed.

Example test_remove_one3:
  count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.
 Proof. reflexivity. Qed.

Example test_remove_one4:
  count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.
 Proof. reflexivity. Qed.


Fixpoint remove_all (v:nat) (s:bag) : bag :=
  match s with
  | [] => []
  | h::t => match h =? v with
    | true => remove_all v t
    | false => h::(remove_all v t)
    end
  end.

(* count verification isn't the right way to do --' *)
Example test_remove_all1: count 5 (remove_all 5 [2;1;5;4;1]) = 0.
 Proof. reflexivity. Qed.

Example test_remove_all2: count 5 (remove_all 5 [2;1;4;1]) = 0.
 Proof. reflexivity. Qed.

Example test_remove_all3: count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
 Proof. reflexivity. Qed.

(* Compute (remove_all 5 [2;1;5;4;5;1;4;5;1;4]). *)

Example test_remove_all4: count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.
 Proof. reflexivity. Qed.

(* Fixpoint subset (s1:bag) (s2:bag) : bool :=
  match (length s1) with
  | 0 => true
  | _ => match (count (hd 0 s1) s2) with
    | 0 => false
    | _ => subset (tl s1) (remove_one (hd 0 s1) s2)
    end
  end. *) (* why nope ? *)

(* Fixpoint subset (s1:bag) (s2:bag) : bool :=
  match s1 with
    | [] => true
    | h::t => if (member h s2) then (subset t (remove_one h s2)) else false (* don't know this syntax at this point *)
  end. *)

Fixpoint subset (s1:bag) (s2:bag) : bool :=
  match s1 with
  | [] => true
  | x :: xs => andb (member x s2)
                    (subset xs (remove_one x s2))
  end.

Example test_subset1: subset [1;2] [2;1;4;1] = true.
 Proof. reflexivity. Qed.

Example test_subset2: subset [1;2;2] [2;1;4;1] = false.
 Proof. reflexivity. Qed.

(* TODO *)

Notation "x ++ y" := (app x y)
                     (right associativity, at level 60).

Theorem nil_app : forall l:natlist,
  [] ++ l = l.
Proof. reflexivity. Qed.

Theorem tl_length_pred : forall l:natlist,
  pred (length l) = length (tl l).
Proof.
  intros l. destruct l as [| n l'].
  - (* l = nil *)
    reflexivity.
  - (* l = cons n l' *)
    reflexivity. Qed.

Theorem app_assoc : forall l1 l2 l3 : natlist,
  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
  intros l1 l2 l3. induction l1 as [| n l1' IHl1'].
  - (* l1 = nil *)
    reflexivity.
  - (* l1 = cons n l1' *)
    simpl. rewrite -> IHl1'. reflexivity. Qed.

Fixpoint rev (l:natlist) : natlist :=
  match l with
  | nil => nil
  | h :: t => rev t ++ [h]
  end.

Example test_rev1: rev [1;2;3] = [3;2;1].
Proof. reflexivity. Qed.
Example test_rev2: rev nil = nil.
Proof. reflexivity. Qed.

Theorem app_length : forall l1 l2 : natlist,
  length (l1 ++ l2) = (length l1) + (length l2).
Proof.
  (* WORKED IN CLASS what does it mean ? *)
  intros l1 l2. induction l1 as [| n l1' IHl1'].
  - (* l1 = nil *)
    reflexivity.
  - (* l1 = cons *)
    simpl. rewrite -> IHl1'. reflexivity. Qed.

Theorem rev_length : forall l : natlist,
  length (rev l) = length l.
Proof.
  intros l. induction l as [| n l' IHl'].
  - (* l = nil *)
    reflexivity.
  - (* l = cons *)
    simpl. rewrite -> app_length, plus_comm.
    simpl. rewrite -> IHl'. reflexivity. Qed.

Search rev. (* list theorems with rev *)

Theorem app_nil_r : forall l : natlist,
  l ++ [] = l.
Proof.
  intros l. induction l as [| n l' IHl'].
  - (* l = nil *)
    reflexivity.
  - (* l = cons *)
    simpl. rewrite -> IHl'. reflexivity. Qed.

(*Theorem rev_lemna: forall l1 l2 : natlist,
  rev ()*)

Theorem rev_app_distr: forall l1 l2 : natlist,
  rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
  intros l1 l2. induction l1.
  - (* l = nil *)
    simpl. rewrite -> app_nil_r. reflexivity.
  - (* l = cons *)
    simpl. rewrite -> IHl1. rewrite -> app_assoc.  reflexivity. Qed.

Theorem rev_involutive : forall l : natlist,
  rev (rev l) = l.
Proof.
   intros l. induction l.
  - (* l = nil *)
    reflexivity.
  - (* l = cons *)
    simpl. rewrite -> rev_app_distr. rewrite -> IHl. reflexivity. Qed.

Theorem app_assoc4 : forall l1 l2 l3 l4 : natlist,
  l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
    intros l1 l2 l3 l4.
    rewrite -> app_assoc.
    rewrite -> app_assoc.
    reflexivity.
Qed.

Lemma nonzeros_app : forall l1 l2 : natlist,
  nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
Proof.
  intros l1 l2. induction l1 as [| n1 l1']. (* what is n1 *)
  - (* l = nil *)
    reflexivity.
  - (* l = cons *)
    simpl. destruct n1 as [|n1']. (* quite lost here... *)
    + simpl. rewrite <- IHl1'. reflexivity.
    + simpl. rewrite <- IHl1'. reflexivity.
Qed.

Fixpoint eqblist (l1 l2 : natlist) : bool
  := match l1, l2 with
| t0::q0, t1::q1 => andb (t0 =? t1) (eqblist q0 q1)
| [], [] => true
| _, _ => false
end.

Example test_eqblist1 :
  (eqblist nil nil = true).
 Proof. reflexivity. Qed.

Example test_eqblist2 :
  eqblist [1;2;3] [1;2;3] = true.
Proof. reflexivity. Qed.

Example test_eqblist3 :
  eqblist [1;2;3] [1;2;4] = false.
 Proof. reflexivity. Qed.

Theorem eqb_refl : forall n:nat,
  true = (n =? n).
Proof.
  intros n. induction n.
  - simpl. reflexivity.
  - simpl. rewrite <- IHn. reflexivity.
Qed.

Theorem eqblist_refl : forall l:natlist,
  true = eqblist l l.
Proof.
  intros l. induction l.
  - simpl. reflexivity.
  - rewrite -> IHl. simpl. rewrite <- eqb_refl. reflexivity.
Qed.

Theorem silly1 : forall(n m o p : nat),
     n = m ->
     [n;o] = [n;p] ->
     [n;o] = [m;p].
Proof.
  intros n m o p eq1 eq2.
  rewrite <- eq1.
apply eq2. Qed.

Theorem silly2 : forall (n m o p : nat),
    n = m ->
    (n = m -> [n;o] = [m;p]) ->
    [n;o] = [m;p].
Proof.
  intros n m o p eq1 eq2.
  apply eq2. apply eq1. Qed.

Theorem silly2a : forall (n m : nat),
     (n,n) = (m,m) ->
     (forall (q r : nat), (q,q) = (r,r) -> [q] = [r]) ->
     [n] = [m].
Proof.
  intros n m eq1 eq2.
  apply eq2. apply eq1. Qed.

Theorem silly3_firsttry : forall(n : nat),
     true = (n =? 5) ->
     (S (S n)) =? 7 = true.
Proof.
  intros n H.
  symmetry.
   apply H. Qed.

Theorem trans_eq : forall (X:Type) (n m o : X),
  n = m -> m = o -> n = o.
Proof.
  intros X n m o eq1 eq2. rewrite -> eq1. rewrite <- eq2.
  reflexivity. Qed.

Example trans_eq_example' : forall (a b c d e f : nat),
     [a;b] = [c;d] ->
     [c;d] = [e;f] ->
     [a;b] = [e;f].
Proof.
  intros a b c d e f eq1 eq2.
apply trans_eq with (m:=[c;d]).
  apply eq1. apply eq2. Qed.

Theorem S_injective : forall (n m : nat),
  S n = S m ->
  n = m.
Proof.
  intros n m H1.
  assert (H2: n = pred (S n)). { reflexivity. }
  rewrite H2. rewrite H1. reflexivity.
Qed.

Theorem injection_ex1 : forall (n m o : nat),
  [n; m] = [o; o] ->
  [n] = [m].
Proof.
  intros n m o H.
  injection H. intros H1 H2.
  rewrite H1. rewrite H2. reflexivity.
Qed.

Theorem injection_ex2 : forall(n m : nat),
  [n] = [m] ->
  n = m.
Proof.
  intros n m H.
  injection H as Hnm. rewrite Hnm.
  reflexivity. Qed.

Theorem eqb_0_l : forall n,
   0 =? n = true -> n = 0.
Proof.
  intros n.
  destruct n as [| n'] eqn:E.
  - (* n = 0 *)
    intros H. reflexivity.
  - (* n = S n' *)
    simpl.
    intros H. discriminate H.
Qed.

Theorem discriminate_ex1 : forall (n : nat),
  S n = O ->
  2 + 2 = 5.
Proof.
  intros n contra. discriminate contra. Qed.

Theorem discriminate_ex2 : forall (n m : nat),
  false = true ->
  [n] = [m].
Proof.
  intros n m contra. discriminate contra. Qed.

Theorem S_inj : forall (n m : nat) (b : bool),
     (S n) =? (S m) = b ->
     n =? m = b.
Proof.
  intros n m b H. simpl in H. apply H. Qed.

Theorem silly3'' : forall (n : nat),
  (n =? 5 = true -> (S (S n)) =? 7 = true) ->
  true = (n =? 5) ->
  true = ((S (S n)) =? 7).
Proof.
  intros n eq H.
  symmetry in H. apply eq in H. symmetry in H.
  apply H. Qed.

Theorem silly3' : forall (n : nat),
  (n =? 5 = true -> (S (S n)) =? 7 = true) ->
  true = (n =? 5) ->
  true = ((S (S n)) =? 7).
Proof.
  intros n eq H.
  symmetry. apply eq. symmetry.
  apply H. Qed.

Fixpoint double' (n:nat) :=
  match n with
  | O => O
  | S n' => S (S (double n'))
  end.

Theorem double_injective_FAILED : forall n m,
     double n = double m ->
     n = m.
Proof.
  intros n m. induction n as [| n' IHn'].
  - (* n = O *) simpl. intros eq. destruct m as [| m'] eqn:E.
    + (* m = O *) reflexivity.
    + (* m = S m' *) discriminate eq.
  - (* n = S n' *) intros eq. destruct m as [| m'] eqn:E.
    + (* m = O *) discriminate eq.
    + (* m = S m' *) apply f_equal. Abort.

Theorem double_injective : forall n m,
     double n = double m ->
     n = m.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = O *) simpl. intros m eq. destruct m as [| m'] eqn:E.
    + (* m = O *) reflexivity.
    + (* m = S m' *) discriminate eq.
  - (* n = S n' *) simpl.
    intros m eq.
    destruct m as [| m'] eqn:E.
    + (* m = O *) simpl.
      discriminate eq.
    + (* m = S m' *)
      apply f_equal.
      apply IHn'. injection eq as goal. apply goal. Qed.

(* HW: ex where we were *)

Fixpoint leb (n m : nat) : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => leb n' m'
      end
  end.

Notation "x <=? y" := (leb x y) (at level 70) : nat_scope.

Definition lesb (n m : nat) : bool := andb (leb n m) (negb (n =? m)).

Definition gtb (n m : nat) : bool := negb (lesb n m).


Notation "x >=? y" := (gtb x y) (at level 70) : nat_scope.


Theorem count_member_nonzero : forall (s : bag),
  1 <=? (count 1 (1 :: s)) = true.
Proof.
  intros s. induction s.
  - simpl. reflexivity.
  - simpl. reflexivity.
Qed.

Theorem leb_n_Sn : forall n,
  n <=? (S n) = true.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* 0 *)
    simpl. reflexivity.
  - (* S n' *)
    simpl. rewrite IHn'. reflexivity. Qed.

(* Theorem remove_does_not_increase_count: forall (s : bag),
  (count 0 (remove_one 0 s)) <=? (count 0 s) = true.
Proof.
  intros s. induction s.
  - simpl. reflexivity.
  - simpl. rewrite -> leb_n_Sn. rewrite IHs.
Qed. *)

Inductive natoption : Type :=
  | Some (n : nat)
  | None.

Definition hd_error (l : natlist) : natoption :=
  match l with
  | t::q => Some t
  | [] => None
  end.

Example test_hd_error1 : hd_error [] = None.
 Proof. reflexivity. Qed.

Example test_hd_error2 : hd_error [1] = Some 1.
 Proof. reflexivity. Qed.

Example test_hd_error3 : hd_error [5;6] = Some 5.
 Proof. reflexivity. Qed.

Definition option_elim (d : nat) (o : natoption) : nat :=
  match o with
  | Some n' => n'
  | None => d
  end.

Theorem option_elim_hd : forall (l:natlist) (default:nat),
  hd default l = option_elim default (hd_error l).
Proof.
  intros l default. induction l.
  - simpl. reflexivity.
  - simpl. reflexivity.
Qed.

Inductive id : Type :=
  | Id (n : nat).

Definition eqb_id (x1 x2 : id) :=
  match x1, x2 with
  | Id n1, Id n2 => n1 =? n2
  end.

Theorem eqb_id_refl : forall x, true = eqb_id x x.
Proof.
  intros x. destruct x. simpl. rewrite <- eqb_refl. reflexivity.
Qed.

Inductive partial_map : Type :=
  | empty
  | record (i : id) (v : nat) (m : partial_map).

Fixpoint find (x : id) (d : partial_map) : natoption :=
  match d with
  | empty => None
  | record y v d' => if eqb_id x y
                     then Some v
                     else find x d'
  end.

Definition update (d : partial_map)
                  (x : id) (value : nat)
                  : partial_map :=
  record x value d.

(* Theorem update_eq : forall (d : partial_map) (x : id) (v: nat),
  find x (update d x v) = Some v.
Proof.
  intros d x v. induction d.
  - simpl. rewrite <- eqb_id_refl. reflexivity.
  - rewrite <- IHd. simpl.
Qed.

Theorem update_neq :
  forall (d : partial_map) (x y : id) (o: nat),
    eqb_id x y = false -> find x (update d y o) = find x d.
Proof.

Qed. *)

Notation "( x , y )" := (pair x y).
Notation "X * Y" := (prod X Y) : type_scope.

Notation "x :: y" := (cons x y)
                     (at level 60, right associativity).

Notation "[ ]" := nil.

(*Fixpoint combine {X Y : Type} (lx : list X) (ly : list Y)
           : list (X*Y) :=
  match lx, ly with
  | [], _ => []
  | _, [] => []
  | x :: tx, y :: ty => (x, y) :: (combine tx ty)
  end.

Check @combine.*)

Notation "[ x ; .. ; y ]" := (cons x .. (cons y []) ..).

(*Compute (combine [1;2] [false;false;true;true]).

Fixpoint split {X Y : Type} (l : list (X*Y))
               : (list X) * (list Y) :=
  match l with
  | [] => ([], [])
  | (a, b)::q => (a::(fst (split q)), b::(snd (split q)))
  end.

Example test_split:
  split [(1,false);(2,false)] = ([1;2],[false;false]).
Proof. reflexivity. Qed.*)

(*Definition hd_error {X : Type} (l : list X) : option X :=
match l with
| [] => None
| t::q => Some t
end.

Check @hd_error.
Example test_hd_error1 : hd_error [1;2] = Some 1.
  Proof. reflexivity. Qed.
Example test_hd_error2 : hd_error [[1];[2]] = Some [1].
  Proof. reflexivity. Qed.

Fixpoint filter {X:Type} (test: X->bool) (l:list X)
                : (list X) :=
  match l with
  | [] => []
  | h :: t => if test h then h :: (filter test t)
                        else filter test t
  end.

Definition filter_even_gt7 (l : list nat) : list nat :=
  filter (fun l => andb (evenb l) (l >=? 7)) l.

Example test_filter_even_gt7_1 :
  filter_even_gt7 [1;2;6;9;10;3;12;8] = [10;12;8].
  Proof. reflexivity. Qed.

Example test_filter_even_gt7_2 :
  filter_even_gt7 [5;2;6;19;129] = [].
  Proof. reflexivity. Qed.

(*Fixpoint filterneg {X:Type} (test: X->bool) (l:list X)
                : (list X) :=
  match l with
  | [] => []
  | h :: t => if negb (test h) then h :: (filter test t)
                        else filter test t
  end.

Definition partition {X : Type}
                     (test : X -> bool)
                     (l : list X)
                   : list X * list X :=
  ((filter test l), (filterneg test l)).*)

Definition partition {X : Type}
                     (test : X -> bool)
                     (l : list X)
                   : list X * list X :=
  (filter test l, filter (fun x => negb (test x)) l).

(* Example test_partition1: partition oddb [1;2;3;4;5] = ([1;3;5], [2;4]).
  Proof. simpl. reflexivity. Qed.

Example test_partition2: partition (fun x => false) [5;9;0] = ([], [5;9;0]).
  Proof. reflexivity. Qed.*)

Fixpoint map {X Y: Type} (f:X->Y) (l:list X) : (list Y) :=
  match l with
  | [] => []
  | h :: t => (f h) :: (map f t)
  end.

(*

*)

Fixpoint rev {X:Type} (l:list X) : list X :=
  match l with
  | nil => nil
  | cons h t => app (rev t) (cons h nil)
  end.

(* Theorem map_rev : forall (X Y : Type) (f : X -> Y) (l : list X),
  map f (rev l) = rev (map f l).
Proof.
  intros X Y f l. induction l.
  - simpl. reflexivity.
  - simpl. rewrite <- IHl. simpl. reflexivity.
Qed. *)

Fixpoint flat_map {X Y: Type} (f: X -> list Y) (l: list X)
                   : (list Y) :=
  match l with
  | t::q => (f t)++(flat_map f q)
  | [] => []
  end.

Example test_flat_map1:
  flat_map (fun n => [n;n;n]) [1;5;4]
  = [1; 1; 1; 5; 5; 5; 4; 4; 4].*)

(* Theorem eqb_true : forall n m,
    n =? m = true -> n = m.
Proof.
  intros m n H. (*Print eqb.*) generalize dependent m.
  induction n.
  - intros m H.  simpl in H. destruct m.
    + reflexivity.
    + discriminate H.
  - intros m H.  simpl in H. destruct m.
    + discriminate H.
    + f_equal.
Qed. *)

(*

intros
simpl
reflexivity
rewrite <-/-> H
destruct x as ...
induction x as ...

simpl [in H]
symmetry [in H]
rewrite [in H]
apply [in H]
injection H [as ?]
discriminate H
generalize dependent
unfold [in H]
split
left/right

(apply) f_equal ?

*)

(*Definition square n := n * n.*)

(*Lemma square_mult : forall n m, square (n * m) = square n * square m.
Proof.
  intros n m.
 unfold square.
rewrite mult_assoc.
  assert (H : n * m * n = n * n * m).
    { rewrite mult_comm. apply mult_assoc. }
  rewrite H. rewrite mult_assoc. reflexivity.
Qed.*)

(*Fixpoint fold {X Y: Type} (f: X->Y->Y) (l: list X) (b: Y)
                         : Y :=
  match l with
  | nil => b
  | h :: t => f h (fold f t b)
  end.

Definition fold_length {X : Type} (l : list X) : nat :=
  fold (fun _ n => S n) l 0.

Example test_fold_length1 : fold_length [4;7;0] = 3.
Proof. reflexivity. Qed.

(* "to solve the goal" *)

Definition foo (x: nat) := 5.

Fact silly_fact_1 : forall m, foo m + 1 = foo (m + 1) + 1.
Proof.
  intros m.
  simpl.
  reflexivity.
Qed.

Definition bar x :=
  match x with
  | O => 5
  | S _ => 5
  end.

Fact silly_fact_2_FAILED : forall m, bar m + 1 = bar (m + 1) + 1.
Proof.
  intros m.
  simpl. (* Does nothing! *)
Abort.

Fact silly_fact_2 : forall m, bar m + 1 = bar (m + 1) + 1.
Proof.
  intros m.
  destruct m eqn:E.
  - simpl. reflexivity.
  - simpl. reflexivity.
Qed.

Fact silly_fact_2' : forall m, bar m + 1 = bar (m + 1) + 1.
Proof.
  intros m.
  unfold bar.
   destruct m eqn:E.
  - reflexivity.
  - reflexivity.
Qed.

Definition sillyfun1 (n : nat) : bool :=
  if n =? 3 then true
  else if n =? 5 then true
  else false.

Theorem sillyfun1_odd_FAILED : forall (n : nat),
     sillyfun1 n = true ->
     oddb n = true.
Proof.
  intros n eq. unfold sillyfun1 in eq.
  destruct (n =? 3).
  (* stuck... *)
Abort.

(*Theorem sillyfun1_odd : forall (n : nat),
     sillyfun1 n = true ->
     oddb n = true.
Proof.
  intros n eq. unfold sillyfun1 in eq.
  destruct (n =? 3) eqn:Heqe3.
  (* Now we have the same state as at the point where we got
     stuck above, except that the context contains an extra
     equality assumption, which is exactly what we need to
     make progress. *)
    - (* e3 = true *) apply eqb_true in Heqe3.
      rewrite -> Heqe3. reflexivity.
    - (* e3 = false *)
     (* When we come to the second equality test in the body
        of the function we are reasoning about, we can use
        eqn: again in the same way, allowing us to finish the
        proof. *)
      destruct (n =? 5) eqn:Heqe5.
        + (* e5 = true *)
          apply eqb_true in Heqe5.
          rewrite -> Heqe5. reflexivity.
        + (* e5 = false *) discriminate eq. Qed.*)

(*Theorem fold_length_correct : forall X (l : list X),
  fold_length l = length l.
Proof.
  intros l l0. induction l0.
  - simpl.
Qed.*)

Lemma zero_or_succ :
  forall n : nat, n = 0 \/ n = S (pred n).
Proof.
  (* WORKED IN CLASS *)
  intros [|n].
  - left. reflexivity.
  - right. reflexivity.
Qed.

Theorem ex_falso_quodlibet : forall (P:Prop),
  False -> P.
Proof.
  (* WORKED IN CLASS *)
  intros P contra.
  destruct contra. Qed.


Theorem contradiction_implies_anything : forall P Q : Prop,
  (P /\ ~P) -> Q.
Proof.
  (* WORKED IN CLASS *)
  intros P Q [HP HNA]. unfold not in HNA.
  apply HNA in HP. destruct HP. Qed.

Theorem silly1 : forall (n m o p : nat),
     n = m ->
     [n;o] = [n;p] ->
     [n;o] = [m;p].
Proof.
  intros n m o p eq1 eq2.
  rewrite <- eq1.
  apply eq2. Qed.

Theorem silly2 : forall (n m o p : nat),
     n = m ->
     (forall (q r : nat), q = r -> [q;o] = [r;p]) ->
     [n;o] = [m;p].
Proof.
  intros n m o p eq1 eq2.
  apply eq2. apply eq1. Qed.

Theorem silly2a : forall (n m : nat),
     (n,n) = (m,m) ->
     (forall (q r : nat), (q,q) = (r,r) -> [q] = [r]) ->
     [n] = [m].
Proof.
  intros n m eq1 eq2.
  apply eq2. apply eq1. Qed.

Theorem silly_ex :
     (forall n, evenb n = true -> oddb (S n) = true) ->
     oddb 3 = true ->
     evenb 4 = true.
Proof.
  intros n.
  simpl. discriminate.
Qed.

Theorem silly3_firsttry : forall (n : nat),
     true = (n =? 5) ->
     (S (S n)) =? 7 = true.
Proof.
  intros n H.
  symmetry.
  apply H. Qed.*)

(*Fixpoint rev (l:list nat) : list nat :=
  match l with
  | nil => nil
  | h :: t => rev t ++ [h]
  end.

Theorem rev_exercise1 : forall (l l' : list nat),
     l = rev l' ->
     l' = rev l.
Proof.
  intros l l' H.
  (*rewrite -> H.
  Search rev.*)
Qed.*)

Example trans_eq_example : forall (a b c d e f : nat),
     [a;b] = [c;d] ->
     [c;d] = [e;f] ->
     [a;b] = [e;f].
Proof.
  intros a b c d e f eq1 eq2.
  rewrite -> eq1. rewrite -> eq2. reflexivity. Qed.

Theorem trans_eq' : forall(X:Type) (n m o : X),
  n = m -> m = o -> n = o.
Proof.
  intros X n m o eq1 eq2. rewrite -> eq1. rewrite -> eq2.
  reflexivity. Qed.

Example trans_eq_example'' : forall (a b c d e f : nat),
     [a;b] = [c;d] ->
     [c;d] = [e;f] ->
     [a;b] = [e;f].
Proof.
  intros a b c d e f eq1 eq2.
  apply trans_eq' with (m:=[c;d]).
  apply eq1. apply eq2. Qed.

Theorem S_injective' : forall(n m : nat),
  S n = S m ->
  n = m.
Proof.
  intros n m H1.
  assert (H2: n = pred (S n)). { reflexivity. }
  rewrite H2. rewrite H1. reflexivity.
Qed.

Theorem S_injective'' : forall (n m : nat),
  S n = S m ->
  n = m.
Proof.
  intros n m H.
  injection H. intros Hnm. apply Hnm.
Qed.

Theorem injection_ex1' : forall (n m o : nat),
  [n; m] = [o; o] ->
  [n] = [m].
Proof.
  intros n m o H.
  injection H. intros H1 H2.
  rewrite H1. rewrite H2. reflexivity.
Qed.

Theorem injection_ex2' : forall (n m : nat),
  [n] = [m] ->
  n = m.
Proof.
  intros n m H.
  injection H as Hnm. rewrite Hnm.
  reflexivity. Qed.

Example injection_ex3 : forall (x y z : nat) (l j : list nat),
  x :: y :: l = z :: j ->
  y :: l = x :: j ->
  x = y.
Proof.
  intros x y z l j.
Qed.