commented the new tarski example for coq.

1 files changed, 15 insertions, 10 deletions

diff --git a/coq/KnasterTarski.v b/coq/KnasterTarski.v
index c377c1a3..5ca030c5 100644
--- a/coq/KnasterTarski.v
+++ b/coq/KnasterTarski.v
@@ -15,15 +15,20 @@ 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).
-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.
+(* 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.