diff options
Diffstat (limited to 'src/QInst.v')
| -rw-r--r-- | src/QInst.v | 10 |
1 files changed, 9 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 |