Ajout du test de Tauto

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1321 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 170 insertions, 0 deletions

diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
new file mode 100644
index 000000000..be51b63ec
--- /dev/null
+++ b/test-suite/success/Tauto.v
@@ -0,0 +1,170 @@
+(**** Tactics Tauto and Intuition ****)
+
+(**** Tauto:
+  Tactic for automating proof in Intuionnistic Propositional Calculus, based on
+  the contraction-free LJT of Dickhoff ****)
+
+(**** Intuition:
+  Simplifications of goals, based on LJT calcul ****)
+
+(**** Examples of intuitionistics tautologies ****)
+Parameter A,B,C:Prop.
+Parameter even:nat -> Prop.
+Parameter P:nat -> Prop.
+
+Lemma Ex_Wallen:(A->(B/\C)) -> ((A->B)\/(A->C)).
+Proof.
+  Tauto.
+Save.
+
+Lemma Ex_Klenne:~(~(A \/ ~A)).
+Proof.
+  Tauto.
+Save.
+
+Lemma Ex_Klenne':(n:nat)(~(~((even n) \/ ~(even n)))).
+Proof.
+  Tauto.
+Save.
+
+Lemma Ex_Klenne'':~(~(((n:nat)(even n)) \/ ~((m:nat)(even m)))).
+Proof.
+  Tauto.
+Save.
+
+Lemma tauto:((x:nat)(P x)) -> ((y:nat)(P y)).
+Proof.
+  Tauto.
+Save.
+
+Lemma tauto1:(A -> A).
+Proof.
+  Tauto.
+Save.
+
+Lemma tauto2:(A -> B -> C) -> (A -> B) -> A -> C.
+Proof.
+  Tauto.
+Save.
+
+Lemma a:(x0: (A \/ B))(x1:(B /\ C))(A -> B).
+Proof.
+  Tauto.
+Save.
+
+Lemma a2:((A -> (B /\ C)) -> ((A -> B) \/ (A -> C))).
+Proof.
+  Tauto.
+Save.
+
+Lemma a4:(~A -> ~A).
+Proof.
+  Tauto.
+Save.
+
+Lemma e2:~(~(A \/ ~A)).
+Proof.
+  Tauto.
+Save.
+
+Lemma e4:~(~((A \/ B) -> (A \/ B))).
+Proof.
+  Tauto.
+Save.
+
+Lemma y0:(x0:A)(x1: ~A)(x2:(A -> B))(x3:(A \/ B))(x4:(A /\ B))(A -> False).
+Proof.
+  Tauto.
+Save.
+
+Lemma y1:(x0:((A /\ B) /\ C))B.
+Proof.
+  Tauto.
+Save.
+
+Lemma y2:(x0:A)(x1:B)(C \/ B).
+Proof.
+  Tauto.
+Save.
+
+Lemma y3:(x0:(A /\ B))(B /\ A).
+Proof.
+  Tauto.
+Save.
+
+Lemma y5:(x0:(A \/ B))(B \/ A).
+Proof.
+  Tauto.
+Save.
+
+Lemma y6:(x0:(A -> B))(x1:A) B.
+Proof.
+  Tauto.
+Save.
+
+Lemma y7:(x0 : ((A /\ B) -> C))(x1 : B)(x2 : A) C.
+Proof.
+  Tauto.
+Save.
+
+Lemma y8:(x0 : ((A \/ B) -> C))(x1 : A) C.
+Proof.
+  Tauto.
+Save.
+
+Lemma y9:(x0 : ((A \/ B) -> C))(x1 : B) C.
+Proof.
+  Tauto.
+Save.
+
+Lemma y10:(x0 : ((A -> B) -> C))(x1 : B) C.
+Proof.
+  Tauto.
+Save.
+
+(* This example takes much time with the old version of Tauto *)
+Lemma critical_example0:(~~B->B)->(A->B)->~~A->B.
+Proof.
+  Tauto.
+Save.
+
+(* Same remark as previously *)
+Lemma critical_example1:(~~B->B)->(~B->~A)->~~A->B.
+Proof.
+  Tauto.
+Save.
+
+(*  A private club has the following rules :
+ *
+ *  . rule 1 : Every non-scottish member wears red socks
+ *  . rule 2 : Every member wears a kilt or doesn't wear red socks
+ *  . rule 3 : The married members don't go out on sunday
+ *  . rule 4 : A member goes out on sunday if and only if he is scottish
+ *  . rule 5 : Every member who wears a kilt is scottish and married
+ *  . rule 6 : Every scottish member wears a kilt
+ *
+ *  Actually, no one can be accepted !
+ *)
+
+Section club.
+
+Variable Scottish, RedSocks, WearKilt, Married, GoOutSunday : Prop.
+
+Hypothesis rule1 : ~Scottish -> RedSocks.
+Hypothesis rule2 : WearKilt \/ ~RedSocks.
+Hypothesis rule3 : Married -> ~GoOutSunday.
+Hypothesis rule4 : GoOutSunday <-> Scottish.
+Hypothesis rule5 : WearKilt -> (Scottish /\ Married).
+Hypothesis rule6 : Scottish -> WearKilt.
+
+Lemma NoMember : False.
+Tauto.
+Save.
+
+End club.
+
+(**** Use of Intuition ****)
+Lemma Intu:(((x:nat)(P x)) /\ B) ->
+              (((y:nat)(P y)) /\ (P O)) \/ (B /\ (P O)).
+Intuition.
+Save.