diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2022-07-29 10:49:00 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2022-07-29 10:49:00 +0200 |
commit | d5697269991500ed1b4b3e6bbec6108ea3a059bb (patch) | |
tree | 89c189decec919ebd852a6a22c974472d52ae673 | |
parent | f36bf11e994cc269c2ec92b061b082e3516f472f (diff) | |
download | smtcoq-d5697269991500ed1b4b3e6bbec6108ea3a059bb.tar.gz smtcoq-d5697269991500ed1b4b3e6bbec6108ea3a059bb.zip |
New case for vauto
-rw-r--r-- | src/QInst.v | 10 | ||||
-rw-r--r-- | unit-tests/Tests_verit_tactics.v | 27 |
2 files changed, 36 insertions, 1 deletions
diff --git a/src/QInst.v b/src/QInst.v index d891fe2..5e88a0b 100644 --- a/src/QInst.v +++ b/src/QInst.v @@ -27,6 +27,13 @@ Proof. installed when we compile SMTCoq. *) Qed. +Lemma impl2_split a b c: + implb a (implb b c) = true -> (negb a) || (negb b) || c = true. +Proof. + intro H. + destruct a; destruct b; destruct c; trivial. +Qed. + Lemma impl_split2 a b c: implb a (b || c) = true -> (negb a) || b || c = true. Proof. @@ -180,7 +187,8 @@ Ltac vauto := | eapply impl_and_split_left; apply_sym H ] | [ |- (negb ?A || ?B || ?C) = true ] => - first [ eapply eqb_or_split; apply_sym H + first [ eapply impl2_split; apply_sym H + | eapply eqb_or_split; apply_sym H | eapply impl_split2; apply_sym H | eapply impl_split211; apply_sym H | eapply impl_split212; apply_sym H diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v index 5164308..7be08d4 100644 --- a/unit-tests/Tests_verit_tactics.v +++ b/unit-tests/Tests_verit_tactics.v @@ -1365,6 +1365,33 @@ Section Vauto. End Vauto. +Require QInst. + +Section Vauto2. + Variable A : Type. + Variable Inv_A : Z -> A -> Prop. + Variable Inv_A_bool : Z -> A -> bool. + Variable y : Z. + Variable l : A. + Variable z : Z. + Variable H : Inv_A y l. + Variable H0 : z <= y. + Variable H2 : forall (H2 : A) (a b : Z), + Inv_A_bool a H2 ---> (b <=? a) ---> Inv_A_bool b H2 = true. + Variable H3 : Inv_A_bool y l = true. + Variable H4 : (z <=? y) = true. + Variable H5 : forall (c : A) (a b : Z), + Inv_A_bool a c ---> (b <=? a) ---> Inv_A_bool b c = true. + Variable CompDec0 : CompDec A. + + Goal + (forall (c : A) (a b : Z), + Inv_A_bool a c ---> (b <=? a) ---> Inv_A_bool b c = true) -> + negb (Inv_A_bool y l) || negb (z <=? y) || Inv_A_bool z l. + Proof. QInst.vauto. Qed. +End Vauto2. + + Section PropToBool. Goal (forall (x x0 : bool) (x1 x2 : list bool), x :: x1 = x0 :: x2 -> x = x0) -> true. Proof. verit. Qed. |