Skip to content

Instantly share code, notes, and snippets.

@siraben
Created January 17, 2019 23:42
Show Gist options
  • Save siraben/d8f8bda58d38aee0b8de467e82f212a2 to your computer and use it in GitHub Desktop.
Save siraben/d8f8bda58d38aee0b8de467e82f212a2 to your computer and use it in GitHub Desktop.
First steps in coq.
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment