mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 17:50:22 +00:00
708 lines
14 KiB
Coq
Executable File
708 lines
14 KiB
Coq
Executable File
Inductive day : Type :=
|
|
| monday : day
|
|
| tuesday : day
|
|
| wednesday : day
|
|
| thursday : day
|
|
| friday : day
|
|
| saturday : day
|
|
| sunday : day.
|
|
|
|
Definition next_weekday (d:day) : day :=
|
|
match d with
|
|
| monday => tuesday
|
|
| tuesday => wednesday
|
|
| wednesday => thursday
|
|
| thursday => friday
|
|
| friday => monday
|
|
| saturday => monday
|
|
| sunday => monday
|
|
end.
|
|
|
|
Example test_next_weekday:
|
|
(next_weekday (next_weekday saturday)) = tuesday.
|
|
|
|
Proof. simpl. reflexivity. Qed.
|
|
|
|
Inductive bool : Type :=
|
|
| true : bool
|
|
| false : bool.
|
|
|
|
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.
|
|
|
|
Definition nandb (b1: bool) (b2:bool) : bool :=
|
|
match b1 with
|
|
| true => match b2 with
|
|
| false => true
|
|
| true => false
|
|
end
|
|
| false => true
|
|
end.
|
|
|
|
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
|
|
| false => false
|
|
| true => match b2 with
|
|
| false => false
|
|
| true => b3
|
|
end
|
|
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.
|
|
|
|
Module Playground1.
|
|
|
|
Inductive nat : Type :=
|
|
| O : nat
|
|
| S : nat -> nat.
|
|
|
|
Definition pred (n : nat) : nat :=
|
|
match n with
|
|
| O => O
|
|
| S n' => n'
|
|
end.
|
|
|
|
Definition minustwo (n : nat) : nat :=
|
|
match n with
|
|
| O => O
|
|
| S O => O
|
|
| S (S n') => n'
|
|
end.
|
|
|
|
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 (S O)) = true.
|
|
Proof. reflexivity. Qed.
|
|
Example test_oddb2: (oddb (S (S (S (S O))))) = false.
|
|
Proof. reflexivity. Qed.
|
|
|
|
Fixpoint plus (n : nat) (m : nat) : nat :=
|
|
match n with
|
|
| O => m
|
|
| S n' => S (plus n' m)
|
|
end.
|
|
|
|
Fixpoint mult (n m : nat) : nat :=
|
|
match n with
|
|
| O => O
|
|
| S n' => plus m (mult n' m)
|
|
end.
|
|
|
|
Fixpoint minus (n m : nat) : nat :=
|
|
match n, m with
|
|
| O, _ => n
|
|
| S n', O => S n'
|
|
| S n', S m' => minus n' m'
|
|
end.
|
|
|
|
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 n (factorial n')
|
|
end.
|
|
|
|
Example test_factorial1: (factorial (S (S (S O)))) = (S (S (S (S (S (S O)))))).
|
|
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.
|
|
|
|
Fixpoint beq_nat (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' => beq_nat n' m'
|
|
end
|
|
end.
|
|
|
|
Fixpoint ble_nat (n m : nat) : bool :=
|
|
match n with
|
|
| O => true
|
|
| S n' =>
|
|
match m with
|
|
| O => false
|
|
| S m' => ble_nat n' m'
|
|
end
|
|
end.
|
|
|
|
Example test_ble_nat1: (ble_nat (S (S O)) (S (S O))) = true.
|
|
Proof. simpl. reflexivity. Qed.
|
|
Example test_ble_nat2: (ble_nat (S (S O)) (S (S (S (S O))))) = true.
|
|
Proof. simpl. reflexivity. Qed.
|
|
Example test_ble_nat3: (ble_nat (S (S (S (S O)))) (S (S O))) = false.
|
|
Proof. simpl. reflexivity. Qed.
|
|
|
|
Definition blt_nat (n m : nat) : bool :=
|
|
(andb (negb (beq_nat n m)) (ble_nat n m)).
|
|
|
|
Example test_blt_nat1: (blt_nat (S (S O)) (S (S O))) = false.
|
|
Proof. simpl. reflexivity. Qed.
|
|
Example test_blt_nat3: (blt_nat (S (S (S (S O)))) (S (S O))) = false.
|
|
Proof. simpl. reflexivity. Qed.
|
|
Example test_blt_nat2 : (blt_nat (S (S O)) (S (S (S (S O))))) = true.
|
|
Proof. simpl. reflexivity. Qed.
|
|
|
|
Theorem plus_O_n : forall n : nat, O + n = n.
|
|
Proof.
|
|
simpl. reflexivity. Qed.
|
|
|
|
Theorem plus_O_n' : forall n : nat, O + n = n.
|
|
Proof.
|
|
reflexivity. Qed.
|
|
|
|
Theorem plus_O_n'' : forall n : nat, O + n = n.
|
|
Proof.
|
|
intros n. reflexivity. Qed.
|
|
|
|
Theorem plus_1_1 : forall n : nat, (S O) + n = S n.
|
|
Proof.
|
|
intros n. reflexivity. Qed.
|
|
|
|
Theorem mult_0_1: forall n : nat, O * n = O.
|
|
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 -> m = o -> n + m = m + o.
|
|
Proof.
|
|
intros n m o.
|
|
intros H.
|
|
intros H'.
|
|
rewrite -> H.
|
|
rewrite <- H'.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem mult_0_plus : forall n m : nat,
|
|
(O + n) * m = n * m.
|
|
Proof.
|
|
intros n m.
|
|
rewrite -> plus_O_n.
|
|
reflexivity. Qed.
|
|
|
|
Theorem mult_1_plus : forall n m: nat,
|
|
((S O) + n) * m = m + (n * m).
|
|
Proof.
|
|
intros n m.
|
|
rewrite -> plus_1_1.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem mult_1 : forall n : nat,
|
|
n * (S O) = n.
|
|
Proof.
|
|
intros n.
|
|
induction n as [| n'].
|
|
reflexivity.
|
|
simpl.
|
|
rewrite -> IHn'.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem plus_1_neq_0 : forall n : nat,
|
|
beq_nat (n + (S O)) O = false.
|
|
Proof.
|
|
intros n.
|
|
destruct n as [| n'].
|
|
reflexivity.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem zero_nbeq_plus_1 : forall n : nat,
|
|
beq_nat O (n + (S O)) = false.
|
|
Proof.
|
|
intros n.
|
|
destruct n.
|
|
reflexivity.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Require String. Open Scope string_scope.
|
|
|
|
Ltac move_to_top x :=
|
|
match reverse goal with
|
|
| H : _ |- _ => try move x after H
|
|
end.
|
|
|
|
Tactic Notation "assert_eq" ident(x) constr(v) :=
|
|
let H := fresh in
|
|
assert (x = v) as H by reflexivity;
|
|
clear H.
|
|
|
|
Tactic Notation "Case_aux" ident(x) constr(name) :=
|
|
first [
|
|
set (x := name); move_to_top x
|
|
| assert_eq x name; move_to_top x
|
|
| fail 1 "because we are working on a different case" ].
|
|
|
|
Ltac Case name := Case_aux Case name.
|
|
Ltac SCase name := Case_aux SCase name.
|
|
Ltac SSCase name := Case_aux SSCase name.
|
|
Ltac SSSCase name := Case_aux SSSCase name.
|
|
Ltac SSSSCase name := Case_aux SSSSCase name.
|
|
Ltac SSSSSCase name := Case_aux SSSSSCase name.
|
|
Ltac SSSSSSCase name := Case_aux SSSSSSCase name.
|
|
Ltac SSSSSSSCase name := Case_aux SSSSSSSCase name.
|
|
|
|
Theorem andb_true_elim1 : forall b c : bool,
|
|
andb b c = true -> b = true.
|
|
Proof.
|
|
intros b c H.
|
|
destruct b.
|
|
Case "b = true".
|
|
reflexivity.
|
|
Case "b = false".
|
|
rewrite <- H. reflexivity. Qed.
|
|
|
|
Theorem plus_0_r : forall n : nat, n + O = n.
|
|
Proof.
|
|
intros n. induction n as [| n'].
|
|
Case "n = 0". reflexivity.
|
|
Case "n = S n'". simpl. rewrite -> IHn'. reflexivity. Qed.
|
|
|
|
Theorem minus_diag : forall n,
|
|
minus n n = O.
|
|
Proof.
|
|
intros n. induction n as [| n'].
|
|
Case "n = 0".
|
|
simpl. reflexivity.
|
|
Case "n = S n'".
|
|
simpl. rewrite -> IHn'. reflexivity. Qed.
|
|
|
|
|
|
Theorem mult_0_r : forall n:nat,
|
|
n * O = O.
|
|
Proof.
|
|
intros n. induction n as [| n'].
|
|
Case "n = 0".
|
|
reflexivity.
|
|
Case "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'].
|
|
Case "n = 0".
|
|
reflexivity.
|
|
Case "n = S n'".
|
|
simpl. rewrite -> IHn'. reflexivity. Qed.
|
|
|
|
Theorem plus_assoc : forall n m p : nat,
|
|
n + (m + p) = (n + m) + p.
|
|
Proof.
|
|
intros n m p.
|
|
induction n as [| n'].
|
|
reflexivity.
|
|
simpl.
|
|
rewrite -> IHn'.
|
|
reflexivity. Qed.
|
|
|
|
Theorem plus_distr : forall n m: nat, S (n + m) = n + (S m).
|
|
Proof.
|
|
intros n m. induction n as [| n'].
|
|
Case "n = 0".
|
|
reflexivity.
|
|
Case "n = S n'".
|
|
simpl. rewrite -> IHn'. reflexivity. Qed.
|
|
|
|
Theorem mult_distr : forall n m: nat, n * ((S O) + m) = n * (S m).
|
|
Proof.
|
|
intros n m.
|
|
induction n as [| n'].
|
|
reflexivity.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem plus_comm : forall n m : nat,
|
|
n + m = m + n.
|
|
Proof.
|
|
intros n m.
|
|
induction n as [| n'].
|
|
Case "n = 0".
|
|
simpl.
|
|
rewrite -> plus_0_r.
|
|
reflexivity.
|
|
Case "n = S n'".
|
|
simpl.
|
|
rewrite -> IHn'.
|
|
rewrite -> plus_distr.
|
|
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 as [| n'].
|
|
Case "n = 0".
|
|
reflexivity.
|
|
Case "n = S n'".
|
|
simpl. rewrite -> IHn'.
|
|
rewrite -> plus_distr. reflexivity.
|
|
Qed.
|
|
|
|
Theorem beq_nat_refl : forall n : nat,
|
|
true = beq_nat n n.
|
|
Proof.
|
|
intros n. induction n as [| n'].
|
|
Case "n = 0".
|
|
reflexivity.
|
|
Case "n = S n".
|
|
simpl. rewrite <- IHn'.
|
|
reflexivity. Qed.
|
|
|
|
Theorem plus_rearrange: 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).
|
|
Case "Proof by assertion".
|
|
rewrite -> plus_comm. reflexivity.
|
|
rewrite -> H. reflexivity. Qed.
|
|
|
|
Theorem plus_swap : forall n m p: nat,
|
|
n + (m + p) = m + (n + p).
|
|
Proof.
|
|
intros n m p.
|
|
rewrite -> plus_assoc.
|
|
assert(H: m + (n + p) = (m + n) + p).
|
|
rewrite -> plus_assoc.
|
|
reflexivity.
|
|
rewrite -> H.
|
|
assert(H2: m + n = n + m).
|
|
rewrite -> plus_comm.
|
|
reflexivity.
|
|
rewrite -> H2.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem plus_swap' : forall n m p: nat,
|
|
n + (m + p) = m + (n + p).
|
|
Proof.
|
|
intros n m p.
|
|
rewrite -> plus_assoc.
|
|
assert(H: m + (n + p) = (m + n) + p).
|
|
rewrite -> plus_assoc.
|
|
reflexivity.
|
|
rewrite -> H.
|
|
replace (m + n) with (n + m).
|
|
rewrite -> plus_comm.
|
|
reflexivity.
|
|
rewrite -> plus_comm.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem mult_1_distr: forall m n: nat,
|
|
n * ((S O) + m) = n * (S O) + n * m.
|
|
Proof.
|
|
intros n m.
|
|
rewrite -> mult_1.
|
|
rewrite -> plus_1_1.
|
|
simpl.
|
|
induction m as [|m'].
|
|
simpl.
|
|
reflexivity.
|
|
simpl.
|
|
rewrite -> plus_swap.
|
|
rewrite <- IHm'.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem mult_comm: forall m n : nat,
|
|
m * n = n * m.
|
|
Proof.
|
|
intros m n.
|
|
induction n as [| n'].
|
|
Case "n = 0".
|
|
simpl.
|
|
rewrite -> mult_0_r.
|
|
reflexivity.
|
|
Case "n = S n'".
|
|
simpl.
|
|
rewrite <- mult_distr.
|
|
rewrite -> mult_1_distr.
|
|
rewrite -> mult_1.
|
|
rewrite -> IHn'.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem evenb_next : forall n : nat,
|
|
evenb n = evenb (S (S n)).
|
|
Proof.
|
|
intros n.
|
|
Admitted.
|
|
|
|
Theorem negb_negb : forall n : bool,
|
|
n = negb (negb n).
|
|
Proof.
|
|
intros n.
|
|
destruct n.
|
|
reflexivity.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem evenb_n_oddb_Sn : forall n : nat,
|
|
evenb n = negb (evenb (S n)).
|
|
Proof.
|
|
intros n.
|
|
induction n as [|n'].
|
|
reflexivity.
|
|
assert(H: evenb n' = evenb (S (S n'))).
|
|
reflexivity.
|
|
rewrite <- H.
|
|
rewrite -> IHn'.
|
|
rewrite <- negb_negb.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
(*Fixpoint bad (n : nat) : bool :=
|
|
match n with
|
|
| O => true
|
|
| S O => bad (S n)
|
|
| S (S n') => bad n'
|
|
end.*)
|
|
|
|
Theorem ble_nat_refl : forall n:nat,
|
|
true = ble_nat n n.
|
|
Proof.
|
|
intros n.
|
|
induction n as [|n'].
|
|
Case "n = 0".
|
|
reflexivity.
|
|
Case "n = S n".
|
|
simpl.
|
|
rewrite <- IHn'.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem zero_nbeq_S : forall n: nat,
|
|
beq_nat O (S n) = false.
|
|
Proof.
|
|
intros n.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem andb_false_r : forall b : bool,
|
|
andb b false = false.
|
|
Proof.
|
|
intros b.
|
|
destruct b.
|
|
reflexivity.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem plus_ble_compat_1 : forall n m p : nat,
|
|
ble_nat n m = true -> ble_nat (p + n) (p + m) = true.
|
|
Proof.
|
|
intros n m p.
|
|
intros H.
|
|
induction p.
|
|
Case "p = 0".
|
|
simpl.
|
|
rewrite -> H.
|
|
reflexivity.
|
|
Case "p = S p'".
|
|
simpl.
|
|
rewrite -> IHp.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem S_nbeq_0 : forall n:nat,
|
|
beq_nat (S n) O = false.
|
|
Proof.
|
|
intros n.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem mult_1_1 : forall n:nat, (S O) * n = n.
|
|
Proof.
|
|
intros n.
|
|
simpl.
|
|
rewrite -> plus_0_r.
|
|
reflexivity. Qed.
|
|
|
|
Theorem all3_spec : forall b c : bool,
|
|
orb (andb b c)
|
|
(orb (negb b)
|
|
(negb c))
|
|
= true.
|
|
Proof.
|
|
intros b c.
|
|
destruct b.
|
|
destruct c.
|
|
reflexivity.
|
|
reflexivity.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Lemma mult_plus_1 : forall n m : nat,
|
|
S(m + n) = m + (S n).
|
|
Proof.
|
|
intros n m.
|
|
induction m.
|
|
reflexivity.
|
|
simpl.
|
|
rewrite -> IHm.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem mult_mult : forall n m : nat,
|
|
n * (S m) = n * m + n.
|
|
Proof.
|
|
intros n m.
|
|
induction n.
|
|
reflexivity.
|
|
simpl.
|
|
rewrite -> IHn.
|
|
rewrite -> plus_assoc.
|
|
rewrite -> mult_plus_1.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem mult_plus_distr_r : forall n m p:nat,
|
|
(n + m) * p = (n * p) + (m * p).
|
|
Proof.
|
|
intros n m p.
|
|
induction p.
|
|
rewrite -> mult_0_r.
|
|
rewrite -> mult_0_r.
|
|
rewrite -> mult_0_r.
|
|
reflexivity.
|
|
rewrite -> mult_mult.
|
|
rewrite -> mult_mult.
|
|
rewrite -> mult_mult.
|
|
rewrite -> IHp.
|
|
assert(H1: ((n * p) + n) + (m * p + m) = (n * p) + (n + (m * p + m))).
|
|
rewrite <- plus_assoc.
|
|
reflexivity.
|
|
rewrite -> H1.
|
|
assert(H2: (n + (m * p + m)) = (m * p + (n + m))).
|
|
rewrite -> plus_swap.
|
|
reflexivity.
|
|
rewrite -> H2.
|
|
assert(H3: (n * p) + (m * p + (n + m)) = ((n * p ) + (m * p)) + (n + m)).
|
|
rewrite -> plus_assoc.
|
|
reflexivity.
|
|
rewrite -> H3.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem mult_assoc : forall n m p : nat,
|
|
n * (m * p) = (n * m) * p.
|
|
Proof.
|
|
intros n m p.
|
|
induction n.
|
|
simpl.
|
|
reflexivity.
|
|
simpl.
|
|
rewrite -> mult_plus_distr_r.
|
|
rewrite -> IHn.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Inductive bin : Type :=
|
|
| BO : bin
|
|
| D : bin -> bin
|
|
| M : bin -> bin.
|
|
|
|
Fixpoint incbin (n : bin) : bin :=
|
|
match n with
|
|
| BO => M (BO)
|
|
| D n' => M n'
|
|
| M n' => D (incbin n')
|
|
end.
|
|
|
|
Fixpoint bin2un (n : bin) : nat :=
|
|
match n with
|
|
| BO => O
|
|
| D n' => double (bin2un n')
|
|
| M n' => S (double (bin2un n'))
|
|
end.
|
|
|
|
Theorem bin_comm : forall n : bin,
|
|
bin2un(incbin n) = S (bin2un n).
|
|
Proof.
|
|
intros n.
|
|
induction n.
|
|
reflexivity.
|
|
reflexivity.
|
|
simpl.
|
|
rewrite -> IHn.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
End Playground1.
|