diff options
| author | QGarchery <QGarchery@users.noreply.github.com> | 2018-12-03 08:08:56 +0100 |
|---|---|---|
| committer | ckeller <ckeller@users.noreply.github.com> | 2018-12-03 08:08:56 +0100 |
| commit | 36548d6634864a131cc83ce21491c797163de305 (patch) | |
| tree | 283b642e4cdb593ee6add5c4bdeb0ccec1a9258d /unit-tests | |
| parent | 3fdc107b26f475c8fe8b7052de826405b88c14b3 (diff) | |
| download | smtcoq-36548d6634864a131cc83ce21491c797163de305.tar.gz smtcoq-36548d6634864a131cc83ce21491c797163de305.zip | |
verit also works when it doesn't use the conclusion (#24)
Fixes issue #20
Diffstat (limited to 'unit-tests')
| -rw-r--r-- | unit-tests/Tests_verit.v | 10 |
1 files changed, 8 insertions, 2 deletions
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 <? x) -> 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. |