added Knaster - Tarski theorem.

1 files changed, 29 insertions, 0 deletions

diff --git a/coq/KnasterTarski.v b/coq/KnasterTarski.v
new file mode 100644
index 00000000..c377c1a3
--- /dev/null
+++ b/coq/KnasterTarski.v
@@ -0,0 +1,29 @@
+(* 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.
+
+Theorem Tarski_lemma : Eq M (f M).
+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.