blob: 14ff0f7af1371fd94613414f27c18409e088a3e7 (
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
210
211
212
213
214
215
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2019 *)
(* *)
(* 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.
Hint Resolve impl_split : smtcoq_core.
(** 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.
(** 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.
destruct (@eq_dec _ (@Decidable _ HA) a b) as [H|H].
- now rewrite H.
- case_eq (eqb_of_compdec HA a b).
+ now rewrite <- !(@compdec_eq_eqb _ HA).
+ intros _. case_eq (eqb_of_compdec HA b a); auto.
intro H1. elim H. symmetry. now rewrite compdec_eq_eqb.
Qed.
(* First strategy: change the order of all equalities in the goal or the
hypotheses
Incomplete: all or none of the equalities are changed, whereas we may
need to change some of them but not all of them *)
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_hyp T :=
repeat match T with
| context [ (?A =? ?B)%Z] =>
change (A =? B)%Z with (hidden_eq_Z A B) in T
end;
repeat match T with
| context [ @eqb_of_compdec ?A ?HA ?a ?b ] =>
change (eqb_of_compdec HA a b) with (hidden_eq_U A HA a b) in T
end;
repeat match T with
| context [ hidden_eq_Z ?A ?B] =>
replace (hidden_eq_Z A B) with (B =? A)%Z in T;
[ | now rewrite Z.eqb_sym]
end;
repeat match T with
| context [ hidden_eq_U ?A ?HA ?a ?b] =>
replace (hidden_eq_U A HA a b) with (eqb_of_compdec HA b a) in T;
[ | now rewrite eqb_of_compdec_sym]
end.
Ltac apply_sym_goal :=
repeat match goal with
| [ |- context [ (?A =? ?B)%Z] ] =>
change (A =? B)%Z with (hidden_eq_Z A B)
end;
repeat match goal with
| [ |- context [ @eqb_of_compdec ?A ?HA ?a ?b ] ] =>
change (eqb_of_compdec HA a b) with (hidden_eq_U A HA a b)
end;
repeat match goal with
| [ |- context [ hidden_eq_Z ?A ?B] ] =>
replace (hidden_eq_Z A B) with (B =? A)%Z;
[ | now rewrite Z.eqb_sym]
end;
repeat match goal with
| [ |- context [ hidden_eq_U ?A ?HA ?a ?b] ] =>
replace (hidden_eq_U A HA a b) with (eqb_of_compdec HA b a);
[ | now rewrite eqb_of_compdec_sym]
end.
Ltac strategy1 H :=
first [ apply H
| apply_sym_goal; apply H
| apply_sym_hyp H; apply H
| apply_sym_goal; apply_sym_hyp H; apply H
].
(* Second strategy: find the order of equalities
Incomplete: does not work if the lemma is quantified *)
Ltac order_equalities g TH :=
match g with
| eqb_of_compdec ?HC ?a1 ?b1 =>
match TH with
| eqb_of_compdec _ ?a2 _ =>
first [ constr_eq a1 a2 | replace (eqb_of_compdec HC a1 b1) with (eqb_of_compdec HC b1 a1) by now rewrite eqb_of_compdec_sym ]
| _ => idtac
end
| Z.eqb ?a1 ?b1 =>
match TH with
| Z.eqb ?a2 _ =>
first [ constr_eq a1 a2 | replace (Z.eqb a1 b1) with (Z.eqb b1 a1) by now rewrite Z.eqb_sym ]
| _ => idtac
end
| ?f1 ?t1 =>
match TH with
| ?f2 ?t2 => order_equalities f1 f2; order_equalities t1 t2
| _ => idtac
end
| _ => idtac
end.
Ltac strategy2 H :=
match goal with
| [ |- ?g ] =>
let TH := type of H in
order_equalities g TH;
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 [ strategy1 H
| strategy2 H
| match goal with
| [ |- (negb ?A || ?B) = true ] =>
first [ eapply impl_or_split_right;
first [ strategy1 H
| strategy2 H ]
| eapply impl_or_split_left;
first [ strategy1 H
| strategy2 H ]
| eapply eqb_sym_or_split_right;
first [ strategy1 H
| strategy2 H ]
| eapply eqb_sym_or_split_left;
first [ strategy1 H
| strategy2 H ]
| eapply eqb_or_split_right;
first [ strategy1 H
| strategy2 H ]
| eapply eqb_or_split_left;
first [ strategy1 H
| strategy2 H ]
]
end
]
);
auto with smtcoq_core.
(*
Local Variables:
coq-load-path: ((rec "." "SMTCoq"))
End:
*)
|
