From 36548d6634864a131cc83ce21491c797163de305 Mon Sep 17 00:00:00 2001 From: QGarchery Date: Mon, 3 Dec 2018 08:08:56 +0100 Subject: verit also works when it doesn't use the conclusion (#24) Fixes issue #20 --- unit-tests/Tests_verit.v | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'unit-tests') diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index f39e904..ba69110 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -1045,6 +1045,12 @@ Lemma lcongr3 (P:Z -> Z -> bool) x y z: x =? y -> P z x -> P z y. Proof. intros eqxy pzx. verit_base eqxy pzx; vauto. Qed. +Lemma test20 : forall x, (forall a, a 0 <=? x = false. +Proof. intros x H. verit_base H; vauto. Qed. + +Lemma test21 : forall x, (forall a, negb (x <=? a)) -> negb (0 <=? x). +Proof. intros x H. verit_base H; vauto. Qed. + Lemma un_menteur (a b c d : Z) dit: dit a =? c -> dit b =? d -> @@ -1123,8 +1129,8 @@ Section mult3. Hypothesis mult3_Sn : forall n, mult3 (n+1) =? mult3 n + 3. Add_lemmas mult3_0 mult3_Sn. - Lemma mult3_21 : mult3 14 =? 42. - Proof. verit. Qed. (* very slow to verify with standard coq *) + Lemma mult3_21 : mult3 4 =? 12. + Proof. verit. Qed. (* slow to verify with standard coq *) Clear_lemmas. End mult3. -- cgit