Initial commit

1 files changed, 296 insertions, 0 deletions

diff --git a/mathcomp/attic/tutorial.v b/mathcomp/attic/tutorial.v
new file mode 100644
index 0000000..3326c90
--- /dev/null
+++ b/mathcomp/attic/tutorial.v
@@ -0,0 +1,296 @@
+(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+
+
+Section HilbertSaxiom.
+
+Variables A B C : Prop.
+
+Lemma HilbertS : (A -> B -> C) -> (A -> B) -> A -> C.
+Proof.
+move=> hAiBiC hAiB hA.
+move: hAiBiC.
+apply.
+  by [].
+by apply: hAiB.
+Qed.
+
+Hypotheses (hAiBiC : A -> B -> C) (hAiB : A -> B) (hA : A).
+
+Lemma HilbertS2 : C.
+Proof.
+apply: hAiBiC; first by apply: hA.
+exact: hAiB.
+Qed.
+
+Check (hAiB hA).
+
+Lemma HilbertS3 : C.
+Proof. by apply: hAiBiC; last exact: hAiB. Qed.
+
+Lemma HilbertS4 : C.
+Proof. exact:  (hAiBiC _ (hAiB _)). Qed.
+
+Lemma HilbertS5 : C.
+Proof. exact: hAiBiC (hAiB _). Qed.
+
+Lemma HilbertS6 : C.
+Proof. exact HilbertS5. Qed.
+
+End HilbertSaxiom.
+
+
+
+Section Symmetric_Conjunction_Disjunction.
+
+Print bool.
+
+Lemma andb_sym : forall A B : bool, A && B -> B && A.
+Proof.
+case.
+  by case.
+by [].
+Qed.
+
+Lemma andb_sym2 : forall A B : bool, A && B -> B && A.
+Proof. by case; case. Qed.
+
+Lemma andb_sym3 : forall A B : bool, A && B -> B && A.
+Proof. by do 2! case. Qed.
+
+Variables (C D : Prop) (hC : C) (hD : D).
+Check (and C D).
+Print and.
+Check conj.
+Check (conj hC hD).
+
+Lemma and_sym : forall A B : Prop, A /\ B -> B /\ A.
+Proof. by move=> A1 B []. Qed.
+
+Print or.
+
+Check or_introl.
+
+Lemma or_sym : forall A B : Prop, A \/ B -> B \/ A.
+Proof. by move=> A B [hA | hB]; [apply: or_intror | apply: or_introl]. Qed.
+
+Lemma or_sym2 : forall A B : bool, A \/ B -> B \/ A.
+Proof. by move=> [] [] AorB; apply/orP; move/orP : AorB. Qed.
+
+End Symmetric_Conjunction_Disjunction.
+
+
+
+Section R_sym_trans.
+
+Variables (D : Type) (R : D -> D -> Prop).
+
+Hypothesis R_sym : forall x y, R x y -> R y x.
+
+Hypothesis R_trans : forall x y z, R x y -> R y z -> R x z.
+
+Lemma refl_if : forall x : D, (exists y, R x y) -> R x x.
+Proof.
+move=> x [y Rxy].
+exact: R_trans (R_sym _ y _).
+Qed.
+
+End R_sym_trans.
+
+
+
+Section Smullyan_drinker.
+
+Variables (D : Type) (P : D -> Prop).
+Hypotheses (d : D) (EM : forall A, A \/ ~A).
+
+Lemma drinker : exists x, P x -> forall y, P y.
+Proof.
+(* case: (EM (exists y, ~P y)) => [[y notPy]| nonotPy] *)
+have [[y notPy]| nonotPy] := EM (exists y, ~P y); first by exists y.
+exists d => _ y; case: (EM (P y)) => // notPy.
+by case: nonotPy; exists y.
+Qed.
+
+End Smullyan_drinker.
+
+
+
+Section Equality.
+
+Variable f : nat -> nat.
+Hypothesis f00 : f 0 = 0.
+
+Lemma fkk : forall k, k = 0 -> f k = k.
+Proof. by move=> k k0; rewrite k0. Qed.
+
+Lemma fkk2 : forall k, k = 0 -> f k = k.
+Proof. by move=> k ->. Qed.
+
+Variable f10 : f 1 = f 0.
+
+Lemma ff10 : f (f 1) = 0.
+Proof. by rewrite f10 f00. Qed.
+
+Variables (D : eqType) (x y : D).
+
+Lemma eq_prop_bool : x = y -> x == y.
+Proof. by move/eqP. Qed.
+
+Lemma eq_bool_prop : x == y -> x = y.
+Proof. by move/eqP. Qed.
+
+End Equality.
+
+
+
+Section Using_Definition.
+
+Variable U : Type.
+
+Definition set := U -> Prop.
+
+Definition subset (A B : set) := forall x, A x -> B x.
+
+Definition transitive (T : Type) (R : T -> T -> Prop) :=
+ forall x y z, R x y -> R y z -> R x z.
+
+Lemma subset_trans : transitive set subset.
+Proof.
+rewrite /transitive /subset => x y z subxy subyz t xt.
+by apply: subyz; apply: subxy.
+Qed.
+
+Lemma subset_trans2 : transitive set subset.
+Proof.
+move=> x y z subxy subyz t.
+by move/subxy; move/subyz.
+Qed.
+
+End Using_Definition.
+
+
+Section Basic_ssrnat.
+
+
+Lemma three : S (S (S O)) = 3 /\ 3 = 0.+1.+1.+1.
+Proof. by []. Qed.
+
+Lemma concrete_plus : plus 16 64 = 80.
+Proof. (*simpl.*) by []. Qed.
+
+Lemma concrete_addn : 16 + 64 = 80.
+Proof. (*simpl.*)  by []. Qed.
+
+Lemma concrete_le : le 1 3.
+Proof. by apply: (Le.le_trans _ 2); apply: Le.le_n_Sn. Qed.
+
+Lemma concrete_big_le : le 16 64.
+Proof. by auto 47 with arith. Qed.
+
+Lemma concrete_big_leq : 0 <= 51.
+Proof. by []. Qed.
+
+Lemma semi_concrete_leq : forall n m, n <= m -> 51 + n <= 51 + m.
+Proof. by []. Qed.
+
+Lemma concrete_arith : (50 < 100) && (3 + 4 < 3 * 4 <= 17 - 2).
+Proof. by []. Qed.
+
+Lemma plus_com : forall m1 n1, n1 + m1 = m1 + n1.
+Proof.
+by elim=> [| n IHn m]; [elim | rewrite -[n.+1 + m]/(n + m).+1 -IHn; elim: m].
+Qed.
+
+End Basic_ssrnat.
+
+
+Section Euclidean_division.
+
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Definition edivn_rec d := fix loop (m q : nat) {struct m} :=
+  if m - d is m'.+1 then loop m' q.+1 else (q, m).
+
+Definition edivn m d := if d is d'.+1 then edivn_rec d' m 0 else (0, m).
+
+CoInductive edivn_spec (m d : nat) : nat * nat -> Type :=
+  EdivnSpec q r of m = q * d + r & (d > 0) ==> (r < d) : edivn_spec m d (q, r).
+
+Lemma edivnP : forall m d, edivn_spec m d (edivn m d).
+Proof.
+move=> m [|d] //=; rewrite -{1}[m]/(0 * d.+1 + m).
+elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //=; rewrite ltnS => le_mn.
+rewrite subn_if_gt; case: ltnP => // le_dm.
+rewrite -{1}(subnKC le_dm) -addSn addnA -mulSnr; apply: IHn.
+apply: leq_trans le_mn; exact: leq_subr.
+Qed.
+
+Lemma edivn_eq : forall d q r, r < d -> edivn (q * d + r) d = (q, r).
+Proof.
+move=> d q r lt_rd; have d_gt0: 0 < d by exact: leq_trans lt_rd.
+case: edivnP lt_rd => q' r'; rewrite d_gt0 /=.
+wlog: q q' r r' / q <= q' by case (ltnP q q'); last symmetry; eauto.
+rewrite leq_eqVlt; case: eqP => [-> _|_] /=; first by move/addnI->.
+rewrite -(leq_pmul2r d_gt0); move/leq_add=> Hqr Eqr _; move/Hqr {Hqr}.
+by rewrite addnS ltnNge mulSn -addnA Eqr addnCA addnA leq_addr.
+Qed.
+
+CoInductive edivn_spec_right : nat -> nat -> nat * nat -> Type :=
+  EdivnSpec_right m d q r of m = q * d + r & (d > 0) ==> (r < d) :
+  edivn_spec_right m d (q, r).
+
+CoInductive edivn_spec_left (m d : nat)(qr : nat * nat) : Type :=
+EdivnSpec_left of m = (fst qr) * d + (snd qr) & (d > 0) ==> (snd qr < d) :
+   edivn_spec_left m d qr.
+
+
+Lemma edivnP_left : forall m d, edivn_spec_left m d (edivn m d).
+Proof.
+move=> m [|d] //=; rewrite -{1}[m]/(0 * d.+1 + m).
+elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //=; rewrite ltnS => le_mn.
+rewrite subn_if_gt; case: ltnP => // le_dm.
+rewrite -{1}(subnKC le_dm) -addSn addnA -mulSnr; apply: IHn.
+apply: leq_trans le_mn; exact: leq_subr.
+Qed.
+
+Lemma edivnP_right : forall m d, edivn_spec_right m d (edivn m d).
+Proof.
+move=> m [|d] //=; rewrite -{1}[m]/(0 * d.+1 + m).
+elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //=; rewrite ltnS => le_mn.
+rewrite subn_if_gt; case: ltnP => // le_dm.
+rewrite -{1}(subnKC le_dm) -addSn addnA -mulSnr; apply: IHn.
+apply: leq_trans le_mn; exact: leq_subr.
+Qed.
+
+Lemma edivn_eq_right : forall d q r, r < d -> edivn (q * d + r) d = (q, r).
+Proof.
+move=> d q r lt_rd; have d_gt0: 0 < d by exact: leq_trans lt_rd.
+set m := q * d + r; have: m = q * d + r by [].
+set d' := d; have: d' = d by [].
+case: (edivnP_right m d') => {m d'} m d' q' r' -> lt_r'd' d'd q'd'r'.
+move: q'd'r' lt_r'd' lt_rd; rewrite d'd d_gt0 {d'd m} /=.
+wlog: q q' r r' / q <= q' by case (ltnP q q'); last symmetry; eauto.
+rewrite leq_eqVlt; case: eqP => [-> _|_] /=; first by move/addnI->.
+rewrite -(leq_pmul2r d_gt0); move/leq_add=> Hqr Eqr _; move/Hqr {Hqr}.
+by rewrite addnS ltnNge mulSn -addnA -Eqr addnCA addnA leq_addr.
+Qed.
+
+
+Lemma edivn_eq_left : forall d q r, r < d -> edivn (q * d + r) d = (q, r).
+Proof.
+move=> d q r lt_rd; have d_gt0: 0 < d by exact: leq_trans lt_rd.
+case: (edivnP_left (q * d + r) d) lt_rd; rewrite d_gt0 /=.
+set q':= (edivn (q * d + r) d).1; set r':= (edivn (q * d + r) d).2.
+rewrite (surjective_pairing (edivn (q * d + r) d)) -/q' -/r'.
+wlog: q r q' r' / q <= q' by case (ltnP q q'); last symmetry; eauto.
+rewrite leq_eqVlt; case: eqP => [-> _|_] /=; first by move/addnI->.
+rewrite -(leq_pmul2r d_gt0); move/leq_add=> Hqr Eqr _; move/Hqr {Hqr}.
+by rewrite addnS ltnNge mulSn -addnA Eqr addnCA addnA leq_addr.
+Qed.
+
+
+End Euclidean_division.
\ No newline at end of file