From 6e3262ce968a436bda303f1022e9d5a46a61098d Mon Sep 17 00:00:00 2001 From: delahaye Date: Mon, 5 Feb 2001 15:25:01 +0000 Subject: Ajout du test de Tauto git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1321 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/success/Tauto.v | 170 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 170 insertions(+) create mode 100644 test-suite/success/Tauto.v (limited to 'test-suite/success/Tauto.v') 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. -- cgit v1.2.3