blob: 5e88a0bde77f98e14d8a254bd6e9efdffa0037d1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2022 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
Require Import Bool ZArith.
Require Import State SMT_classes.
(** Handling quantifiers with veriT **)
(* verit silently transforms an <implb a b> into a <or (not a) b> when
instantiating a quantified theorem with <implb> *)
Lemma impl_split a b:
implb a b = true -> orb (negb a) b = true.
Proof.
intro H.
destruct a; destruct b; trivial.
(* alternatively we could do <now verit_base H.> but it forces us to have veriT
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.
intro H.
destruct a; destruct b; trivial.
(* alternatively we could do <now verit_base H.> but it forces us to have veriT
installed when we compile SMTCoq. *)
Qed.
Lemma impl_split211 a b1 b2 c1 c2 :
implb a ((b1 && b2) || (c1 && c2)) = true -> (negb a) || b1 || c1 = true.
Proof.
intro H.
destruct a; destruct b1; destruct b2; destruct c1; destruct c2; trivial.
Qed.
Lemma impl_split212 a b1 b2 c1 c2 :
implb a ((b1 && b2) || (c1 && c2)) = true -> (negb a) || b1 || c2 = true.
Proof.
intro H.
destruct a; destruct b1; destruct b2; destruct c1; destruct c2; trivial.
Qed.
Lemma impl_split221 a b1 b2 c1 c2 :
implb a ((b1 && b2) || (c1 && c2)) = true -> (negb a) || b2 || c1 = true.
Proof.
intro H.
destruct a; destruct b1; destruct b2; destruct c1; destruct c2; trivial.
Qed.
Lemma impl_split222 a b1 b2 c1 c2 :
implb a ((b1 && b2) || (c1 && c2)) = true -> (negb a) || b2 || c2 = true.
Proof.
intro H.
destruct a; destruct b1; destruct b2; destruct c1; destruct c2; trivial.
Qed.
(** verit silently transforms an <implb (a || b) c> into a <or (not a) c>
or into a <or (not b) c> when instantiating such a quantified theorem *)
Lemma impl_or_split_right a b c:
implb (a || b) c = true -> negb b || c = true.
Proof.
intro H.
destruct a; destruct c; intuition.
Qed.
Lemma impl_or_split_left a b c:
implb (a || b) c = true -> negb a || c = true.
Proof.
intro H.
destruct a; destruct c; intuition.
Qed.
(** same for Boolean equivalence, modulo symmetry *)
Lemma eqb_sym_or_split_right a b c:
Bool.eqb c (a || b) = true -> negb b || c = true.
Proof.
intro H.
destruct a; destruct c; intuition.
Qed.
Lemma eqb_sym_or_split_left a b c:
Bool.eqb c (a || b) = true -> negb a || c = true.
Proof.
intro H.
destruct a; destruct c; intuition.
Qed.
Lemma eqb_or_split_right a b c:
Bool.eqb (a || b) c = true -> negb b || c = true.
Proof.
intro H.
destruct a; destruct c; intuition.
Qed.
Lemma eqb_or_split_left a b c:
Bool.eqb (a || b) c = true -> negb a || c = true.
Proof.
intro H.
destruct a; destruct c; intuition.
Qed.
Lemma eqb_or_split a b c:
Bool.eqb c (a || b) = true -> negb c || a || b = true.
Proof.
intro H.
destruct a; destruct b; destruct c; intuition.
Qed.
(** verit silently transforms an <implb a (b && c)> into a <or (not a)
b> or into a <or (not a) c> when instantiating such a quantified
theorem. *)
Lemma impl_and_split_right a b c:
implb a (b && c) = true -> negb a || c = true.
Proof.
intro H.
destruct a; destruct c; intuition.
now rewrite andb_false_r in H.
Qed.
Lemma impl_and_split_left a b c:
implb a (b && c) = true -> negb a || b = true.
Proof.
intro H.
destruct a; destruct b; intuition.
Qed.
(** verit considers equality modulo its symmetry, so we have to recover the
right direction in the instances of the theorems *)
(* TODO: currently incomplete *)
(* An auxiliary lemma to rewrite an eqb_of_compdec into its the symmetrical version *)
Lemma eqb_of_compdec_sym (A:Type) (HA:CompDec A) (a b:A) :
eqb_of_compdec HA b a = eqb_of_compdec HA a b.
Proof. apply eqb_sym2. Qed.
(* Strategy: change or not the order of each equality in the goal
Complete but exponential in some cases *)
Definition hidden_eq_Z (a b : Z) := (a =? b)%Z.
Definition hidden_eq_U (A:Type) (HA:CompDec A) (a b : A) := eqb_of_compdec HA a b.
Ltac apply_sym H :=
lazymatch goal with
| [ |- context [ (?A =? ?B)%Z ] ] =>
first [ change (A =? B)%Z with (hidden_eq_Z A B); apply_sym H
| replace (A =? B)%Z with (hidden_eq_Z B A); [apply_sym H | now rewrite Z.eqb_sym] ]
| [ |- context [ @eqb_of_compdec ?A ?HA ?a ?b ] ] =>
first [ change (eqb_of_compdec HA a b) with (hidden_eq_U A HA a b); apply_sym H
| replace (eqb_of_compdec HA a b) with (hidden_eq_U A HA b a); [apply_sym H | now rewrite eqb_of_compdec_sym] ]
| _ => apply H
end.
(* An automatic tactic that takes into account all those transformations *)
Ltac vauto :=
try (unfold is_true;
let H := fresh "H" in
intro H;
first [ apply_sym H
| match goal with
| [ |- (negb ?A || ?B) = true ] =>
first [ eapply impl_split; apply_sym H
| eapply impl_or_split_right; apply_sym H
| eapply impl_or_split_left; apply_sym H
| eapply eqb_sym_or_split_right; apply_sym H
| eapply eqb_sym_or_split_left; apply_sym H
| eapply eqb_or_split_right; apply_sym H
| eapply eqb_or_split_left; apply_sym H
| eapply impl_and_split_right; apply_sym H
| eapply impl_and_split_left; apply_sym H
]
| [ |- (negb ?A || ?B || ?C) = true ] =>
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
| eapply impl_split221; apply_sym H
| eapply impl_split222; apply_sym H
]
end
]
);
auto with smtcoq_core.
(*
Local Variables:
coq-load-path: ((rec "." "SMTCoq"))
End:
*)
|
