147 lines
3.0 KiB
Coq
147 lines
3.0 KiB
Coq
(* From Chapter-5 of mathcomp book *)
|
|
From mathcomp Require Import all_ssreflect.
|
|
|
|
Lemma test_reflect (b: bool) (P: Prop):
|
|
reflect P b -> P \/ ~P.
|
|
Proof.
|
|
case.
|
|
by move=> H; left.
|
|
by move=> H; right. (* ✓ *)
|
|
Restart.
|
|
by case; [left | right].
|
|
Qed.
|
|
|
|
Lemma andP (b1 b2: bool): reflect (b1 /\ b2) (b1 && b2).
|
|
Proof.
|
|
case: b1.
|
|
case b2.
|
|
by left.
|
|
right.
|
|
move=> [l r].
|
|
by [].
|
|
case b2.
|
|
right.
|
|
by move=> [l r].
|
|
right.
|
|
move=> [l _].
|
|
by []. (* ✓ *)
|
|
Restart.
|
|
case: b1; case b2.
|
|
by left.
|
|
by right; by move=>[l r].
|
|
by right; by move=>[l r].
|
|
by right; by move=>[l r]. (* ✓ *)
|
|
Restart.
|
|
case: b1; case b2.
|
|
by left.
|
|
all: by right; by move=>[l r]. (* ✓ *)
|
|
(* Restart. *)
|
|
(* by case: b1; case b2; *)
|
|
(* [left | right => //= [l r]]. *)
|
|
Qed.
|
|
|
|
Lemma orP (b1 b2: bool): reflect (b1 \/ b2) (b1 || b2).
|
|
Proof.
|
|
case: b1; case b2.
|
|
by left; left.
|
|
by left; left.
|
|
by left; right.
|
|
right.
|
|
move=> [l | r].
|
|
by case b2.
|
|
by case b2. (* ✓ *)
|
|
(* Restart. *)
|
|
(* case: b1; case b2; [ [left; [left | right]] | right]. *)
|
|
(* Restart. *)
|
|
(* case: b1; case b2; *)
|
|
(* [left; by [move | left | right]]. *)
|
|
Qed.
|
|
|
|
Lemma implyP (b1 b2: bool): reflect (b1 -> b2) (b1 ==> b2).
|
|
Proof.
|
|
case b1; case b2.
|
|
by left.
|
|
right.
|
|
Search (_ -> _).
|
|
apply/Bool.ReflectT.
|
|
apply/Bool.ReflectT.
|
|
apply/Bool.ReflectT.
|
|
apply/Bool.ReflectT.
|
|
apply/Bool.ReflectT.
|
|
apply/Bool.ReflectT.
|
|
apply/Bool.ReflectT.
|
|
apply/Bool.ReflectT.
|
|
apply/Bool.ReflectT.
|
|
apply/Bool.ReflectT.
|
|
move => H.
|
|
|
|
rewrite /(_ isT).
|
|
Abort.
|
|
|
|
Lemma nat_inj_eq {A: Type} (f: A -> nat) (x y: A):
|
|
injective f -> reflect (x=y) (eqn (f x) (f y)).
|
|
Proof.
|
|
move=> f_inj.
|
|
Check eqnP.
|
|
Check iffP.
|
|
Check iffP eqnP.
|
|
apply: (iffP eqnP).
|
|
apply: f_inj.
|
|
Search (_ = _ -> _ = _).
|
|
(* congruence. *)
|
|
apply: congr1. (* ✓ *)
|
|
Restart.
|
|
move => f_inj; apply: (iffP eqnP); [apply: f_inj | apply: congr1].
|
|
Qed.
|
|
|
|
Lemma eqnP (n m: nat): reflect (n = m) (eqn n m).
|
|
Proof.
|
|
apply: (iffP idP).
|
|
Abort. (* TODO *)
|
|
|
|
Lemma example1 (n m k: nat):
|
|
k <= n ->
|
|
(n <= m) && (m <= k) ->
|
|
n = k.
|
|
Proof.
|
|
move=> lekn.
|
|
Undo.
|
|
move=> lekn /andP [lenm lemk].
|
|
Undo.
|
|
move=> lekn /andP [/eqnP lenm lemk].
|
|
Abort. (* TODO *)
|
|
|
|
Lemma leq_total (n m: nat): (n <= m) || (n >= m).
|
|
Proof.
|
|
Abort.
|
|
|
|
Locate "_ -> _ ".
|
|
|
|
Lemma example2 (a b: bool): a && b ==> (a == b).
|
|
Proof.
|
|
case: andP => [ab | nab].
|
|
Search (reflect (_ = _) _).
|
|
apply/addbP.
|
|
Abort.
|
|
|
|
(* Euclidean division example *)
|
|
Definition edivn_rec (d: nat): nat -> nat -> nat * nat :=
|
|
fix loop (m q: nat): nat * nat :=
|
|
if m-d is m'.+1 then loop m' q.+1
|
|
else (q, m).
|
|
Definition edivn (m d: nat): nat*nat :=
|
|
if d>0 then edivn_rec d.-1 m 0
|
|
else (0, m).
|
|
|
|
(* Follows from definition but useful to have better control over level of
|
|
* unfolding in later proof *)
|
|
Lemma edivn_recE (d m q: nat):
|
|
edivn_rec d m q =
|
|
if m-d is m'.+1 then edivn_rec d m' q.+1
|
|
else (q, m).
|
|
Proof. by case: m. Qed.
|
|
|
|
Lemma edivnP (m d: nat) (ed := edivn m d):
|
|
((d>0) ==> (ed.2 < d)) && (m == ed.1 * d + ed.2).
|
|
Proof.
|