From a6ea9f91f82c216b9ce756b7323c456eeb80658c Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Fri, 13 Aug 2010 10:26:17 +0000
Subject: Renamed file

---
 coq/ex/KnasterTarski.v | 34 ++++++++++++++++++++++++++++++++++
 coq/ex/example-utf8.v  | 26 ++++++++++++++++++++++++++
 2 files changed, 60 insertions(+)
 create mode 100644 coq/ex/KnasterTarski.v
 create mode 100644 coq/ex/example-utf8.v

(limited to 'coq/ex')

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
-- 
cgit v1.2.3