Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 240 insertions, 0 deletions

diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
new file mode 100644
index 00000000..883a82ab
--- /dev/null
+++ b/test-suite/success/Tauto.v
@@ -0,0 +1,240 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: Tauto.v,v 1.10.8.1 2004/07/16 19:30:59 herbelin Exp $ *)
+
+(**** 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 intuitionistic tautologies ****)
+Parameter A,B,C,D,E,F: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 took 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.
+
+(* This example took very much time (about 3mn on a PIII 450MHz in bytecode)
+   with the old Tauto. Now, it's immediate (less than 1s). *)
+Lemma critical_example2:(~A<->B)->(~B<->A)->(~~A<->A).
+Proof.
+  Tauto.
+Save.
+
+(* This example was a bug *)
+Lemma old_bug0:(~A<->B)->(~(C\/E)<->D/\F)->~(C\/A\/E)<->D/\B/\F.
+Proof.
+  Tauto.
+Save.
+
+(* Another bug *)
+Lemma old_bug1:((A->B->False)->False) -> (B->False) -> False.
+Proof.
+  Tauto.
+Save.
+
+(* A bug again *)
+Lemma old_bug2:
+  ((((C->False)->A)->((B->False)->A)->False)->False) ->
+  (((C->B->False)->False)->False) ->
+  ~A->A.
+Proof.
+  Tauto.
+Save.
+
+(* A bug from CNF form *)
+Lemma old_bug3:
+  ((~A\/B)/\(~B\/B)/\(~A\/~B)/\(~B\/~B)->False)->~((A->B)->B)->False.
+Proof.
+  Tauto.
+Save.
+
+(* sometimes, the behaviour of Tauto depends on the order of the hyps *)
+Lemma old_bug3bis:
+  ~((A->B)->B)->((~B\/~B)/\(~B\/~A)/\(B\/~B)/\(B\/~A)->False)->False.
+Proof.
+  Tauto.
+Save.
+
+(* A bug found by Freek Wiedijk <freek@cs.kun.nl> *)
+Lemma new_bug:
+ ((A<->B)->(B<->C)) ->
+ ((B<->C)->(C<->A)) ->
+ ((C<->A)->(A<->B)) ->
+ (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 intu0:(((x:nat)(P x)) /\ B) ->
+              (((y:nat)(P y)) /\ (P O)) \/ (B /\ (P O)).
+Proof.
+  Intuition.
+Save.
+
+Lemma intu1:((A:Prop)A\/~A)->(x,y:nat)(x=y\/~x=y).
+Proof.
+  Intuition.
+Save.
+