diff options
Diffstat (limited to 'test-suite/success/Tauto.v')
| -rw-r--r-- | test-suite/success/Tauto.v | 240 |
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. + |