From 8846e497d6f869191645e18a9e2a8dc68956d679 Mon Sep 17 00:00:00 2001 From: delahaye Date: Mon, 5 Feb 2001 16:23:13 +0000 Subject: D'autres exemples git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1324 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/success/Tauto.v | 24 ++++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v index be51b63ec..fc1ee0fca 100644 --- a/test-suite/success/Tauto.v +++ b/test-suite/success/Tauto.v @@ -2,13 +2,13 @@ (**** Tauto: Tactic for automating proof in Intuionnistic Propositional Calculus, based on - the contraction-free LJT of Dickhoff ****) + the contraction-free LJT* of Dickhoff ****) (**** Intuition: - Simplifications of goals, based on LJT calcul ****) + Simplifications of goals, based on LJT* calcul ****) -(**** Examples of intuitionistics tautologies ****) -Parameter A,B,C:Prop. +(**** Examples of intuitionistic tautologies ****) +Parameter A,B,C,D,E,F:Prop. Parameter even:nat -> Prop. Parameter P:nat -> Prop. @@ -134,6 +134,12 @@ Proof. Tauto. Save. +(* An example which was a bug *) +Lemma old_bug:(~A<->B)->(~(C\/E)<->D/\F)->~(C\/A\/E)<->D/\B/\F. +Proof. + Tauto. +Save. + (* A private club has the following rules : * * . rule 1 : Every non-scottish member wears red socks @@ -164,7 +170,13 @@ Save. End club. (**** Use of Intuition ****) -Lemma Intu:(((x:nat)(P x)) /\ B) -> +Lemma intu0:(((x:nat)(P x)) /\ B) -> (((y:nat)(P y)) /\ (P O)) \/ (B /\ (P O)). -Intuition. +Proof. + Intuition. +Save. + +Lemma intu1:((A:Prop)A\/~A)->(x,y:nat)(x=y\/~x=y). +Proof. + Intuition. Save. -- cgit v1.2.3