First steps in coq.

logical foundations.v

Inductive day : Type :=
 | monday
 | tuesday
 | wednesday
 | thursday
 | friday
 | saturday
 | sunday.

Definition next_weekday (d:day) : day :=
  match d with
  | monday  => tuesday
  | tuesday  => wednesday
  | wednesday  => thursday
  | thursday  => friday
  | friday  => monday
  | saturday  => monday
  | sunday  => monday
  end.


Compute (next_weekday friday).
(* ==> monday : day *)
Compute (next_weekday (next_weekday saturday)).
(* ==> tuesday : day *)

Example test_next_weekday:
  (next_weekday (next_weekday saturday)) = tuesday.
Proof. simpl; reflexivity. Qed.

Inductive bool : Type :=
  | true
  | false.

Definition negb (b:bool) : bool :=
  match b with
  | true => false
  | false => true
  end.

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.

Example test_orb1: (orb true false) = true.
Proof. simpl; reflexivity. Qed.
Example test_orb2: (orb false false) = false.
Proof. simpl; reflexivity. Qed.
Example test_orb3: (orb false true) = true.
Proof. simpl; reflexivity. Qed.
Example test_orb4: (orb true true) = true.
Proof. simpl; reflexivity. Qed.

Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).

Example test_orb5: false || false || true = true.
Proof. simpl; reflexivity. Qed.

Definition nandb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true => negb b2
  | false => true
  end.
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *)
Example test_nandb1: (nandb true false) = true.
Proof. simpl; reflexivity. Qed.
Example test_nandb2: (nandb false false) = true.
Proof. simpl; reflexivity. Qed.
Example test_nandb3: (nandb false true) = true.
Proof. simpl; reflexivity. Qed.
Example test_nandb4: (nandb true true) = false.
Proof. simpl; reflexivity. Qed.

Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool :=
  match b1 with
  | true => andb b2 b3
  | false => false
  end.
Example test_andb31: (andb3 true true true) = true.
Proof. simpl; reflexivity. Qed.
Example test_andb32: (andb3 false true true) = false.
Proof. simpl; reflexivity. Qed.
Example test_andb33: (andb3 true false true) = false.
Proof. simpl; reflexivity. Qed.
Example test_andb34: (andb3 true true false) = false.
Proof. simpl; reflexivity. Qed.

Check true.
(* ===> true : bool *)
Check (negb true).
(* ===> negb true : bool *)

Check negb.

Inductive rgb : Type :=
  | red
  | green
  | blue.

Inductive color : Type :=
  | black
  | white
  | primary (p : rgb).

Definition monochrome (c : color) : bool :=
  match c with
  | black => true
  | white => true
  | primary q => false
  end.


Inductive bit : Type :=
  | B0
  | B1.
Inductive nybble : Type :=
  | bits (b0 b1 b2 b3 : bit).
Check (bits B1 B0 B1 B0).


Definition all_zero (nb : nybble) : bool :=
  match nb with
    | (bits B0 B0 B0 B0) => true
    | (bits _ _ _ _) => false
  end.
Compute (all_zero (bits B1 B0 B1 B0)).

Compute (all_zero (bits B0 B0 B0 B0)).

Module NatPlayground.

Inductive nat : Type :=
  | O
  | S (n : nat).

Definition pred (n : nat) : nat :=
  match n with
  | O => O
  | S n' => n'
  end.

End NatPlayground.


Check (S (S (S (S O)))).
  (* ===> 4 : nat *)
Definition minustwo (n : nat) : nat :=
  match n with
    | O => O
    | S O => O
    | S (S n') => n'
  end.
Compute (minustwo 4).
(* ===> 2 : nat *)

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

Definition oddb (n:nat) : bool := negb (evenb n).
Example test_oddb1: oddb 1 = true.
Proof. simpl; reflexivity. Qed.
Example test_oddb2: oddb 4 = false.
Proof. simpl; reflexivity. Qed.

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

Compute (plus 3 2).


Fixpoint mult (n m : nat) : nat :=
  match n with
    | O => O
    | S n' => plus m (mult n' m)
  end.
Example test_mult1: (mult 3 3) = 9.
Proof. simpl; reflexivity. Qed.

Fixpoint minus (n m:nat) : nat :=
  match n, m with
  | O , _ => O
  | S _ , O => n
  | S n', S m' => minus n' m'
  end.
End NatPlayground2.

Fixpoint exp (base power : nat) : nat :=
  match power with
    | O => S O
    | S p => mult base (exp base p)
  end.

Fixpoint factorial (n:nat) : nat :=
  match n with
    | O => S O
    | S n => mult (S n) (factorial n)
  end.

Example test_factorial1: (factorial 3) = 6.
Proof. simpl; reflexivity. Qed.
Example test_factorial2: (factorial 5) = (mult 10 12).
Proof. simpl; reflexivity. Qed.

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

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.

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.


Example test_leb1: (leb 2 2) = true.
Proof. simpl; reflexivity. Qed.
Example test_leb2: (leb 2 4) = true.
Proof. simpl; reflexivity. Qed.
Example test_leb3: (leb 4 2) = false.
Proof. simpl; reflexivity. Qed.

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

Example test_leb3': (4 <=? 2) = false.
Proof. simpl; reflexivity. Qed.
Definition exp2 (n : nat) : nat :=
  exp 2 n.

Fixpoint fib (n : nat) : nat :=
  match n with
    | 0 => 0
    | S n' => match n' with
                | 0 => 1
                | S n'' => fib n' + fib n''
              end
  end.

Example fib5: (fib 5) = 5.
Proof. simpl; reflexivity. Qed.


Definition ltb (x y : nat) : bool :=
  andb (x <=? y) (negb (x =? y)).
Notation "x <? y" := (ltb x y) (at level 70) : nat_scope.
Example test_ltb1: (ltb 2 2) = false.
Proof. simpl; reflexivity. Qed.
Example test_ltb2: (ltb 2 4) = true.
Proof. simpl; reflexivity. Qed.
Example test_ltb3: (ltb 4 2) = false.
Proof. simpl; reflexivity. Qed.

Theorem ex1 : forall n : nat, (fib n) <? (exp2 n) = true.
Admitted.

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

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.

Theorem plus_id_example : forall n m : nat, n = m -> n + n = m + m.
Proof.
  intros n m.
  intros H.
  rewrite <- H.
  reflexivity.
Qed.

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


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

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

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

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

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.
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.
Qed.

Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros b c H.
  destruct c.
  reflexivity.
  rewrite <- H.
  destruct b;
  reflexivity.
Qed.


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

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

Theorem andb_eq_orb :
  forall (b c : bool),
  (andb b c = orb b c) ->
  b = c.
Proof.
  destruct b, c;
  intro H;
  inversion H;
  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 (incr n)
  end.

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

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

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

Fixpoint bin_to_nat (m:bin) : nat :=
  match m with
  | Z => 0
  | A n => (2 * (bin_to_nat n))
  | B n => S (2 * (bin_to_nat n))
  end.


Fixpoint nat_to_bin (n:nat) : bin :=
  match n with
  | 0 => Z
  | S n' => incr (nat_to_bin n')
  end.

Recursive Extraction nat_to_bin bin_to_nat.

Example test_bin_to_nat1: bin_to_nat (A (A (B Z))) = 4.
Proof. reflexivity. Qed.


Example test_bin_to_nat2: bin_to_nat (B (A (B Z))) = 5.
Proof. reflexivity. Qed.


Example test_nat_to_bin1: nat_to_bin 5 = (B (A (B Z))).
Proof. reflexivity. Qed.

Lemma incr_to_succ_eqv:
  forall n : nat,
    (nat_to_bin (S n)) = incr (nat_to_bin n).
Proof.
  intros n.
  induction n.
  - reflexivity.
  - simpl. reflexivity.
Qed.

Lemma succ_to_inc_eqv :
  forall n : bin,
    S (bin_to_nat n) = (bin_to_nat (incr n)).
Proof.
  intros n.
  induction n.
  - reflexivity.
  - simpl. reflexivity.
  - simpl. rewrite <- IHn.
Abort.

Theorem succ_exchange_over_id :
  forall n : nat,
    bin_to_nat (nat_to_bin (S (S n))) = S (bin_to_nat (nat_to_bin (S n))).
Proof.
  intros n.
  induction n.
  - reflexivity.
  - simpl. rewrite <- incr_to_succ_eqv.
Abort.
Theorem nat_to_bin_ex_succ :
  forall n : nat,
    (bin_to_nat (nat_to_bin (S n))) = S (bin_to_nat (nat_to_bin n)).
Proof.
  intros n.
  induction n.
  - simpl. reflexivity.
  - simpl. rewrite <- incr_to_succ_eqv. rewrite <- incr_to_succ_eqv.
Abort.
Theorem nat_to_bin_and_back :
  forall n : nat,
    (bin_to_nat (nat_to_bin n)) = n.
Proof.
Admitted.

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 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'].
  - reflexivity.
  - simpl. rewrite -> IHn'. reflexivity.
Qed.

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

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

Theorem plus_assoc : forall n m p : nat,
  n + (m + p) = (n + m) + p.
Proof.
  intros.
  induction n.
  - 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, plus_n_Sm. reflexivity.
Qed.

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

Module NatList.

Set Warnings "-notation-overridden,-parsing".

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

Check (pair 3 5).

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.

Compute (fst (pair 3 5)).

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

Compute (fst (3,5)).
Definition fst' (p : natprod) : nat :=
  match p with
  | (x,y) => x
  end.

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

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

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

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

Theorem fst_swap_is_snd : forall (p : natprod),
  fst (swap_pair p) = snd p.
Proof.
  intros p. destruct p as [a b]. 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 append (l1 l2 : natlist) : natlist :=
  match l1 with
  | nil => l2
  | h :: t => h :: (append t l2)
  end.


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

Definition head (default:nat) (l:natlist) : nat :=
  match l with
  | nil => default
  | h :: t => h
  end.
Definition tail (l:natlist) : natlist :=
  match l with
  | nil => nil
  | h :: t => t
  end.
Example test_head1: head 0 [1;2;3] = 1.
Proof. reflexivity. Qed.
Example test_head2: head 0 [] = 0.
Proof. reflexivity. Qed.
Example test_tail: tail [1;2;3] = [2;3].
Proof. reflexivity. Qed.


Fixpoint filter (f : nat -> bool) (l : natlist) : natlist :=
  match l with
  | nil => nil
  | (cons car cdr) => if (f car)
                     then
                       (cons car (filter f cdr))
                     else
                       (filter f cdr)
  end.


Definition nonzeros (l:natlist) : natlist :=
  filter (fun x => negb (x =? 0)) l.

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

Fixpoint oddmembers (l:natlist) : natlist :=
  filter (fun x => negb (evenb x)) l.
                                    
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 with
  | nil => l2
  | (cons x y) => match l2 with
                 | nil => l1
                 | (cons x' y') => (cons x (cons x' (alternate y y')))
                 end
  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 :=
  (length (filter (fun x => v =? x) s)).

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.

Fixpoint make_unique (l : bag) :=
  match l with
  | nil => nil
  | (cons car cdr) => (cons car (filter (fun x => negb (x =? car)) cdr))
  end.

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

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.
  

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 :=
  negb ((length (filter (fun x => (v =? x)) s)) =? 0).

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

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

Fixpoint remove_one (v:nat) (s:bag) : bag :=
  match s with
  | nil => nil
  | (cons car cdr) => if (v =? car)
                     then
                       cdr
                     else
                       (cons car (remove_one v cdr))
  end.

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.


Definition remove_all (v:nat) (s:bag) : bag :=
  (filter (fun x => negb (x =? v)) s).
  
                                      
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.

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 s1 with
  | nil => true
  | (cons car cdr) => (andb (member car s2) (subset cdr (remove_one car 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.

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

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

Theorem append_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 reverse (l:natlist) : natlist :=
  match l with
  | nil => nil
  | h :: t => reverse t ++ [h]
  end.

Example test_reverse1: reverse [1;2;3] = [3;2;1].
Proof. reflexivity. Qed.
Example test_reverse2: reverse nil = nil.
Proof. reflexivity. Qed.

Theorem app_length : forall l1 l2 : natlist,
    length (l1 ++ l2) = (length l1) + (length l2).
Proof.
  intros l1 l2. induction l1 as [| n l1' IHl1'].
  - reflexivity.
  - simpl. rewrite IHl1'. reflexivity.
Qed.

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

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

Theorem reverse_app_distr: forall l1 l2 : natlist,
    reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
Proof.
  intros l1 l2. induction l1 as [| n l1' IHl1'].
  - simpl. rewrite app_nil_r. reflexivity.
  - simpl.  rewrite IHl1', append_assoc. reflexivity.
Qed.

Theorem reverse_involutive : forall l : natlist,
    reverse (reverse l) = l.
Proof.
  intros l. induction l as [| n l' IHl'].
  - simpl. reflexivity.
  - simpl. rewrite reverse_app_distr. simpl. rewrite IHl'. reflexivity.
Qed.

Theorem append_assoc4 : forall l1 l2 l3 l4 : natlist,
  l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
  intros l1 l2 l3 l4.
  induction l1 as [| n l1' IHl1'].
  - simpl. rewrite append_assoc. reflexivity.
  - simpl. rewrite IHl1'. reflexivity.
Qed.

Lemma nonzeros_app : forall l1 l2 : natlist,
  nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
Proof.
Admitted.

Fixpoint eqblist (l1 l2 : natlist) : bool :=
  match l1, l2 with
  | nil, nil => true
  | x1::y1, x2::y2 => (andb (x1 =? x2) (eqblist y1 y2))
  | _, _ => 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 eqblist_refl : forall l:natlist,
  true = eqblist l l.
Proof.
Admitted.

Theorem count_member_nonzero : forall(s : bag),
  1 <=? (count 1 (1 :: s)) = true.
Proof.
  intros.
  induction s; 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.
Admitted.

End NatList.
 
(* Polymorphic lists. *)
Set Warnings "-notation-overridden,-parsing".
Inductive list (X:Type) : Type :=
  | nil
  | cons (x : X) (l : list X).

Fixpoint repeat (X : Type) (x : X) (count : nat) : list X :=
  match count with
  | 0 => nil X
  | S count' => cons X x (repeat X x count')
  end.


Arguments nil {X}.
Arguments cons {X} _ _.
Arguments repeat {X} x count.

Fixpoint append {X : Type} (l1 l2 : list X)
             : (list X) :=
  match l1 with
  | nil => l2
  | cons h t => cons h (append t l2)
  end.
Fixpoint reverse {X:Type} (l:list X) : list X :=
  match l with
  | nil => nil
  | cons h t => append (reverse t) (cons h nil)
  end.
Fixpoint length {X : Type} (l : list X) : nat :=
  match l with
  | nil => 0
  | cons _ l' => S (length l')
  end.
Example test_reverse1 :
  reverse (cons 1 (cons 2 nil)) = (cons 2 (cons 1 nil)).
Proof. reflexivity. Qed.
Example test_reverse2:
  reverse (cons true nil) = cons true nil.
Proof. reflexivity. Qed.
Example test_length1: length (cons 1 (cons 2 (cons 3 nil))) = 3.
Proof. reflexivity. Qed.

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

Theorem append_nil_r : forall (X:Type), forall l:list X,
  l ++ [] = l.
Proof.
  induction l.
  - reflexivity.
  - simpl. rewrite IHl. reflexivity.
Qed.

Theorem append_assoc : forall A (l m n:list A),
  l ++ m ++ n = (l ++ m) ++ n.
Proof.
  intros. 
  induction l.
  - reflexivity.
  - simpl. rewrite IHl. reflexivity.
Qed.

Lemma append_length : forall (X:Type) (l1 l2 : list X),
  length (l1 ++ l2) = length l1 + length l2.
Proof.
  intros.
  induction l1.
  - reflexivity.
  - simpl. rewrite IHl1. reflexivity.
Qed.

Theorem reverse_append_distr: forall X (l1 l2 : list X),
    reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
Proof.
  intros.
  induction l1.
  - simpl. rewrite append_nil_r. reflexivity.
  - simpl. rewrite IHl1, append_assoc. reflexivity.
Qed.

Theorem reverse_involutive : forall X : Type, forall l : list X,
      reverse (reverse l) = l.
Proof.
  intros.
  induction l.
  - reflexivity.
  - simpl. rewrite reverse_append_distr. rewrite IHl. reflexivity.
Qed.

Inductive prod (X Y : Type) : Type :=
| pair (x : X) (y : Y).
Arguments pair {X} {Y} _ _.
Notation "( x , y )" := (pair x y).
Notation "X * Y" := (prod X Y) : type_scope.

Definition fst {X Y : Type} (p : X * Y) : X :=
  match p with
  | (x, y) => x
  end.

Definition snd {X Y : Type} (p : X * Y) : Y :=
  match p with
  | (x, y) => y
  end.

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.

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



Example test_map1: map (fun x => plus 3 x) [2;0;2] = [5;3;5].
Proof. reflexivity. Qed.

Example test_map2:
  map oddb [2;1;2;5] = [false;true;false;true].
Proof. reflexivity. Qed.


Example test_map3:
  map (fun n => [evenb n;oddb n]) [2;1;2;5]
  = [[true;false];[false;true];[true;false];[false;true]].
Proof. reflexivity. Qed.

    
Fixpoint split {X Y : Type} (l : list (X*Y))
  : (list X) * (list Y) :=
  ((map fst l), (map snd l)).

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

Module MaybePlayground.
Inductive maybe (X:Type) : Type :=
  | Just (x : X)
  | Nothing.
Arguments Just {X} _.
Arguments Nothing {X}.

 Fixpoint nth_error {X : Type} (l : list X) (n : nat)
                   : maybe X :=
  match l with
  | [] => Nothing
  | a :: l' => if n =? O then Just a else nth_error l' (pred n)
  end.
Example test_nth_error1 : nth_error [4;5;6;7] 0 = Just 4.
Proof. reflexivity. Qed.
Example test_nth_error2 : nth_error [[1];[2]] 1 = Just [2].
Proof. reflexivity. Qed.
Example test_nth_error3 : nth_error [true] 2 = Nothing.
Proof. reflexivity. Qed.

Definition hd_error {X : Type} (l : list X) : maybe X :=
  match l with
    | [] => Nothing
    | x::y => Just x
  end.

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

Example test_hd_error2 : hd_error [[1];[2]] = Just [1].
Proof. reflexivity. Qed.

End MaybePlayground.

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.

Example test_filter1: filter evenb [1;2;3;4] = [2;4].
Proof. reflexivity. Qed.

Definition length_is_1 {X : Type} (l : list X) : bool :=
  (length l) =? 1.
Example test_filter2:
    filter length_is_1
           [ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]
  = [ [3]; [4]; [8] ].
Proof. reflexivity. Qed.

Definition doit3times {X:Type} (f:X->X) (n:X) : X :=
  f (f (f n)).

  Check @doit3times.
(* ===> doit3times : forall X : Type, (X -> X) -> X -> X *)
Example test_doit3times: doit3times minustwo 9 = 3.
Proof. reflexivity. Qed.
Example test_doit3times': doit3times negb true = false.
Proof. reflexivity. Qed.


 
Definition countoddmembers' (l:list nat) : nat :=
  length (filter oddb l).
Example test_countoddmembers'1: countoddmembers' [1;0;3;1;4;5] = 4.
Proof. reflexivity. Qed.
Example test_countoddmembers'2: countoddmembers' [0;2;4] = 0.
Proof. reflexivity. Qed.
Example test_countoddmembers'3: countoddmembers' nil = 0.
Proof. reflexivity. Qed.

Example test_anon_fun':
  doit3times (fun n => n * n) 2 = 256.
Proof. reflexivity. Qed.

Check S.
Check pred.
Check minustwo.


Example test_filter2': 
  filter (fun l => (length l) =? 1)
         [ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]
  = [ [3]; [4]; [8] ].
Proof. reflexivity. Qed.

Definition filter_even_gt7 (l : list nat) : list nat :=
  filter (fun x => (andb (negb (x <=? 7)) (evenb x))) 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.

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. reflexivity. Qed.

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

Lemma map_distr_append:
  forall (X Y : Type) (f : X -> Y) (x : list X) (y : X) (l1 : list X) (l2 : list X),
    map f (l1 ++ l2) = (map f l1) ++ (map f l2).
Proof.
  intros.
  induction l1, l2.
  - simpl. reflexivity.
  - induction l2; simpl; reflexivity.
  - simpl. rewrite IHl1. reflexivity.
  - simpl. rewrite IHl1.
    assert (H: map f (x1 :: l2) = f x1 :: map f l2).
    {
      induction l2; simpl; reflexivity.
    }
    rewrite <- H. reflexivity.
Qed.

Theorem map_reverse : forall (X Y : Type) (f : X -> Y) (l : list X),
    map f (reverse l) = reverse (map f l).

Proof.
  intros.
  induction l.
  - simpl. reflexivity.
  - simpl. rewrite <- IHl, map_distr_append.
    assert (H: map f [x] = [f x]).
    {
      simpl. reflexivity.
    }
    rewrite H. reflexivity. apply l. apply x.
Qed.


Fixpoint flatmap {X Y: Type} (f: X -> list Y) (l: list X)
  : (list Y) :=
    match l with
    | nil => nil
    | (cons x xs) => (f x) ++ (flatmap f xs)
    end.

Example test_flat_map1:
  flatmap (fun n => [n;n;n]) [1;5;4]
  = [1; 1; 1; 5; 5; 5; 4; 4; 4].
Proof. reflexivity. Qed.