aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--coq/ex-ssreflect.v136
-rw-r--r--coq/ex/KnasterTarski.v (renamed from coq/KnasterTarski.v)0
-rw-r--r--coq/ex/example-utf8.v (renamed from coq/example-utf8.v)0
-rw-r--r--coq/root2.v135
4 files changed, 0 insertions, 271 deletions
diff --git a/coq/ex-ssreflect.v b/coq/ex-ssreflect.v
deleted file mode 100644
index 54c4283a..00000000
--- a/coq/ex-ssreflect.v
+++ /dev/null
@@ -1,136 +0,0 @@
-(* An example of customization file for the hightlight of the Coq Mode *)
-
-(*Supposing you .emacs contains the following lines:
-
-(load-file "<proofgeneral-home>/generic/proof-site.el")
-(load-file "<location>/pg-ssr.el")
-
-And that the file my-tacs.el contains for instance:
----
-
-(defcustom coq-user-tactics-db
- '(("nat_congr" "ncongr" "nat_congr" t "nat_congr")
- ("nat_norm" "nnorm" "nat_norm" t "nat_norm")
- ("bool_congr" "bcongr" "bool_congr" t "bool_congr")
- ("prop_congr" "prcongr" "prop_congr" t "prop_congr")
- ("move" "m" "move" t "move")
- ("pose" "po" "pose # := #" t "pose")
- ("set" "set" "set # := #" t "set")
- ("have" "hv" "have # : #" t "have")
- ("congr" "con" "congr #" t "congr")
- ("wlog" "wlog" "wlog : / #" t "wlog")
- ("without loss" "wilog" "without loss #" t "without loss")
- ("unlock" "unlock" "unlock #" t "unlock")
- ("suffices" "suffices" "suffices # : #" t "suffices")
- ("suff" "suff" "suff # : #" t "suff")
-)
- "Extended list of tactics, includings ssr and user defined ones")
-
-
-(defcustom coq-user-commands-db
- '(("Prenex Implicits" "pi" "Prenex Implicits #" t "Prenex\\s-+Implicits")
- ("Hint View for" "hv" "Hint View for #" t "Hint\\s-+View\\s-+for")
- ("inside" "ins" nil f "inside")
- ("outside" "outs" nil f "outside")
-)
- "Extended list of commands, includings ssr and user defined ones")
-
-(defcustom coq-user-tacticals-db
- '(("last" "lst" nil t "last"))
- "Extended list of tacticals, includings ssr and user defined ones")
-
-(defcustom coq-user-reserved-db
- '("is" "nosimpl" "of")
- "Extended list of keywords, includings ssr and user defined ones")
-
-(defcustom coq-user-solve-tactics-db
- '(("done" nil "done" nil "done")
- )
- "Extended list of closing tactic(al)s, includings ssr and user defined ones")
----
-Below is a sample script file coloured by this customised mode:
-
-*)
-
-
-
-Require Import ssreflect.
-Require Import ssrbool.
-Require Import ssrnat.
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-Import Prenex Implicits.
-
-
-Inductive mylist (A : Type) : Type := mynil | mycons of A & mylist A.
-
-(***************** The stack******************)
-
-Goal forall A B : Prop, A -> (A -> B) -> B.
-Proof. move=> A B Ha; exact. Qed.
-
-(***************** Bookkeeping **************)
-
-Lemma my_mulnI : forall x y, mult x y = muln x y.
-Proof. elim=> // m Hrec n /=; congr addn; done. Qed.
-
-
-(* Warning : corecion bool >-> Prop *)
-Lemma demo_bool : forall x y z: bool,
- x && y -> z -> x && y && z.
-Proof. by move=> x y z -> ->. Qed.
-
-(* com + assoc *)
-Lemma my_addnCA : forall m n p, m + (n + p) = n + (m + p).
-Proof.
-by move=> m n; elim: m => [|m Hrec] p; rewrite ?addSnnS -?addnS. Qed.
-
-(*** Rotation of subgoals *)
-Inductive test : nat -> Prop :=
- C1 : forall n, test n | C2 : forall n, test n |
- C3 : forall n, test n | C4 : forall n, test n.
-Goal forall n, test n -> True.
-move=> n t; case: t; last 1 [move=> k| move=> l]; last first.
-Admitted.
-
-(*** Selection of subgoals *)
-Goal forall n, test n -> True.
-move=> n t; case E: t; first 1 last.
-Admitted.
-
-
-(*** Forward chaining *)
-Lemma demo_fwd : forall x y : nat, x = y.
-Proof.
-move=> x y.
- suff [H1 H2] : (x, y) = (x * 1, y + 0).
-Admitted.
-
-Lemma demo_fwd2 : forall x y : nat, x = y.
-Proof.
-move=> x y.
- wlog : x / x <= y.
-Admitted.
-
-
-
-Lemma rwtest1 : let x := 3 in x * 2 = 6.
-Proof. move=> x. rewrite /x //=. Qed.
-(* => unfold + simpl *)
-
-Lemma rwtest2 : forall x, 0 * x = 0.
-Proof. move=> x. rewrite -[0 * x]/0 //. Qed.
-(* => conversion *)
-
-Goal (forall t u, t + u = u + t) -> forall x y, x + y = y + x.
-Proof. by move=> H x y; rewrite (*[x + _ ]H *) [_ + y]H. Qed.
-(* => with patterns *)
-
-Goal (forall t u, t + u = u + t) ->
- forall x y, x + y + (y + x) = y + x.
-move=> H x y; rewrite {2}(H y).
-Admitted.
-(* => occurrence selection *)
-
-
diff --git a/coq/KnasterTarski.v b/coq/ex/KnasterTarski.v
index 5ca030c5..5ca030c5 100644
--- a/coq/KnasterTarski.v
+++ b/coq/ex/KnasterTarski.v
diff --git a/coq/example-utf8.v b/coq/ex/example-utf8.v
index 4cba17c8..4cba17c8 100644
--- a/coq/example-utf8.v
+++ b/coq/ex/example-utf8.v
diff --git a/coq/root2.v b/coq/root2.v
deleted file mode 100644
index ecba1a7f..00000000
--- a/coq/root2.v
+++ /dev/null
@@ -1,135 +0,0 @@
-(******************************************************************************
- * *
- * Proof that sqrt 2 is irrational *
- * *
- * Laurent.Thery@sophia.inria.fr *
- * February 2002 *
- * (Revised April 2004 for coq 8.0) *
- ******************************************************************************)
-
-Require Import ArithRing.
-Require Import Wf_nat.
-Require Import Peano_dec.
-Require Import Div2.
-Require Import Even.
-
-(******************************************************************************
- * *
- * Properties of div2 and double (these theorems should be in Div2.v) *
- * *
- ******************************************************************************)
-
-Theorem double_div2: forall (n : nat), div2 (double n) = n.
-simple induction n; auto with arith.
-intros n0 H.
-rewrite double_S; pattern n0 at 2; rewrite <- H; simpl; auto.
-Qed.
-
-Theorem double_inv: forall (n m : nat), double n = double m -> n = m.
-intros n m H; rewrite <- (double_div2 n); rewrite <- (double_div2 m); rewrite H;
- auto.
-Qed.
-
-Theorem double_mult_l: forall (n m : nat), double (n * m) = double n * m.
-unfold double; auto with arith.
-Qed.
-
-Theorem double_mult_r: forall (n m : nat), double (n * m) = n * double m.
-unfold double; intros; ring.
-Qed.
-
-(******************************************************************************
- * *
- * If the power to the 2 of a number is even, then this number is even *
- * *
- ******************************************************************************)
-
-Theorem even_is_even_times_even: forall (n : nat), even (n * n) -> even n.
-intros n H; (try case (even_or_odd n)); auto.
-intros; apply even_mult_inv_r with (1 := H); auto.
-Qed.
-
-(******************************************************************************
- * *
- * Useful fact 4*(n/2)*(n/2) = n*n if n is even *
- * *
- ******************************************************************************)
-
-Theorem main_thm_aux:
- forall (n : nat), even n -> double (double (div2 n * div2 n)) = n * n.
-intros; rewrite double_mult_l; rewrite double_mult_r;
- (repeat rewrite <- even_double); auto.
-Qed.
-
-(******************************************************************************
- * Main theorem *
- * We do the proof of the theorem by well founded induction: *
- * Suppose that we have n*n = 2*p*p *
- * if n=0 then p = O *
- * if n<>0 then *
- * - n is even (n=2n') and p is even (p=2p') *
- * - we have n'*n'=2*p'*p' and n' < n *
- * - by the induction hypothesis we have p'=O *
- * - so p=O *
- ******************************************************************************)
-
-Theorem main_thm: forall (n p : nat), n * n = double (p * p) -> p = 0.
-intros n; pattern n; apply lt_wf_ind; clear n.
-intros n H p H0.
-case (eq_nat_dec n 0); intros H1.
-generalize H0; rewrite H1; case p; auto; intros; discriminate.
-assert (H2: even n).
-apply even_is_even_times_even.
-apply double_even; rewrite H0; rewrite double_div2; auto.
-assert (H3: even p).
-apply even_is_even_times_even.
-rewrite <- (double_inv (double (div2 n * div2 n)) (p * p)).
-apply double_even; rewrite double_div2; auto.
-rewrite main_thm_aux; auto.
-assert (H4: div2 p = 0).
-apply (H (div2 n)).
-apply lt_div2; apply neq_O_lt; auto.
-apply double_inv; apply double_inv; (repeat rewrite main_thm_aux); auto.
-rewrite (even_double p); auto; rewrite H4; auto.
-Qed.
-
-
-
-(******************************************************************************
- * *
- * Coercions from nat and Z to R *
- * *
- ******************************************************************************)
-
-Require Import Reals.
-Require Import Field.
-Coercion INR : nat >-> R.
-Coercion IZR : Z >-> R.
-
-(******************************************************************************
- * *
- * Definition of irrational *
- * *
- ******************************************************************************)
-
-Definition irrational (x : R) : Prop :=
- forall (p : Z) (q : nat), q <> 0 -> x <> (p / q)%R.
-
-(******************************************************************************
- * *
- * Final theorem *
- * *
- ******************************************************************************)
-
-Theorem irrational_sqrt_2: irrational (sqrt 2%nat).
-intros p q H H0; case H.
-apply (main_thm (Zabs_nat p)).
-replace (Div2.double (q * q)) with (2 * (q * q));
- [idtac | unfold Div2.double; ring].
-case (eq_nat_dec (Zabs_nat p * Zabs_nat p) (2 * (q * q))); auto; intros H1.
-case (not_nm_INR _ _ H1); (repeat rewrite mult_INR).
-rewrite <- (sqrt_def (INR 2)); auto with real.
-rewrite H0; auto with real.
-assert (q <> 0%R :> R); auto with real.
-field; auto with real; case p; simpl; intros; ring.
-Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 22:15:55 +0000