From a6ea9f91f82c216b9ce756b7323c456eeb80658c Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 13 Aug 2010 10:26:17 +0000 Subject: Renamed file --- coq/KnasterTarski.v | 34 ------------- coq/ex-ssreflect.v | 136 ------------------------------------------------- coq/ex/KnasterTarski.v | 34 +++++++++++++ coq/ex/example-utf8.v | 26 ++++++++++ coq/example-utf8.v | 26 ---------- coq/root2.v | 135 ------------------------------------------------ 6 files changed, 60 insertions(+), 331 deletions(-) delete mode 100644 coq/KnasterTarski.v delete mode 100644 coq/ex-ssreflect.v create mode 100644 coq/ex/KnasterTarski.v create mode 100644 coq/ex/example-utf8.v delete mode 100644 coq/example-utf8.v delete mode 100644 coq/root2.v diff --git a/coq/KnasterTarski.v b/coq/KnasterTarski.v deleted file mode 100644 index 5ca030c5..00000000 --- a/coq/KnasterTarski.v +++ /dev/null @@ -1,34 +0,0 @@ -(* A sample tarski theorem proof, for f: A -> A. - Syntax is for coq v8. *) - -Parameter A : Set. -Variable R : A -> A -> Prop. -Variable Eq : A -> A -> Prop. - -Axiom Assym : forall x y : A, R x y -> R y x -> Eq x y. -Axiom Trans : forall x y z : A, R x y -> R y z -> R x z. - -Variable f : A -> A. -Axiom Incr : forall x y : A, R x y -> R (f x) (f y). - -Variable M : A. -Hypothesis Up : forall x : A, R x (f x) -> R x M. -Hypothesis Least : forall x : A, (forall y : A, R y (f y) -> R y x) -> R M x. - -Hint Resolve Up Assym Incr Least Incr Up Trans : db. - -Theorem Tarski_lemma : Eq M (f M). -(* We can prove the theorem in one line: *) -(* eauto 15 with db. *) -(* But we rather use basic tactics in this sample file: *) - cut (R M (f M)). - intro. - apply Assym; trivial. - apply Up. - apply Incr; trivial. - apply Least. - intros. - apply Trans with (f y); trivial. - apply Incr. - apply Up; trivial. -Qed. 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 "/generic/proof-site.el") -(load-file "/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/ex/KnasterTarski.v b/coq/ex/KnasterTarski.v new file mode 100644 index 00000000..5ca030c5 --- /dev/null +++ b/coq/ex/KnasterTarski.v @@ -0,0 +1,34 @@ +(* A sample tarski theorem proof, for f: A -> A. + Syntax is for coq v8. *) + +Parameter A : Set. +Variable R : A -> A -> Prop. +Variable Eq : A -> A -> Prop. + +Axiom Assym : forall x y : A, R x y -> R y x -> Eq x y. +Axiom Trans : forall x y z : A, R x y -> R y z -> R x z. + +Variable f : A -> A. +Axiom Incr : forall x y : A, R x y -> R (f x) (f y). + +Variable M : A. +Hypothesis Up : forall x : A, R x (f x) -> R x M. +Hypothesis Least : forall x : A, (forall y : A, R y (f y) -> R y x) -> R M x. + +Hint Resolve Up Assym Incr Least Incr Up Trans : db. + +Theorem Tarski_lemma : Eq M (f M). +(* We can prove the theorem in one line: *) +(* eauto 15 with db. *) +(* But we rather use basic tactics in this sample file: *) + cut (R M (f M)). + intro. + apply Assym; trivial. + apply Up. + apply Incr; trivial. + apply Least. + intros. + apply Trans with (f y); trivial. + apply Incr. + apply Up; trivial. +Qed. diff --git a/coq/ex/example-utf8.v b/coq/ex/example-utf8.v new file mode 100644 index 00000000..4cba17c8 --- /dev/null +++ b/coq/ex/example-utf8.v @@ -0,0 +1,26 @@ +(* -*- coding: utf-8; -*- *) + +(* utf8 notations: You can (re)use the version here, + or a compiled version distributed with Coq IDE: + Add LoadPath "/usr/lib/coq/ide". + Require Import utf8. +*) +Load "utf8". + +(* Printing of unicode notation, in *goals* *) +Lemma test : ∀ A:Prop, A -> A. +auto. +Qed. + +(* Parsing of unicode notation here, printing in *goals* *) +Lemma test2 : ∀ A:Prop, A → A. +intro. +intro. +auto. +Qed. + +(* Printing of unicode notation, in *response* *) +Check (fun (X:Set)(x:X) => x). + +(* Parsing of unicode notation here, printing in *response* *) +Check (∀A, A→A). \ No newline at end of file diff --git a/coq/example-utf8.v b/coq/example-utf8.v deleted file mode 100644 index 4cba17c8..00000000 --- a/coq/example-utf8.v +++ /dev/null @@ -1,26 +0,0 @@ -(* -*- coding: utf-8; -*- *) - -(* utf8 notations: You can (re)use the version here, - or a compiled version distributed with Coq IDE: - Add LoadPath "/usr/lib/coq/ide". - Require Import utf8. -*) -Load "utf8". - -(* Printing of unicode notation, in *goals* *) -Lemma test : ∀ A:Prop, A -> A. -auto. -Qed. - -(* Parsing of unicode notation here, printing in *goals* *) -Lemma test2 : ∀ A:Prop, A → A. -intro. -intro. -auto. -Qed. - -(* Printing of unicode notation, in *response* *) -Check (fun (X:Set)(x:X) => x). - -(* Parsing of unicode notation here, printing in *response* *) -Check (∀A, A→A). \ No newline at end of file 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. -- cgit v1.2.3