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
|
Some notes about the use of unification in Coq
----------------------------------------------
There are several applications of unification and pattern-matching
** Unification of types **
- For type inference, inference of implicit arguments
* this basically amounts to solve problems of the form T <= U or T = U
where T and U are types coming from a given typing problem
* this kind of problem has to succeed and all the power of unification is
a priori expected (full beta/delta/iota/zeta/nu/mu, pattern-unification,
pruning, imitation/projection heuristics, ...)
- For lemma application (apply, auto, ...)
* these are also problems of the form T <= U on types but with T
coming from a lemma and U from the goal
* it is not obvious that we always want unification and not matching
* it is not clear which amounts of delta one wants to use
** Looking for subterms **
- For tactics applying on subterms: induction, destruct, rewrite
- As part of unification of types in the presence of higher-order
evars (e.g. when applying a lemma of conclusion "?P t")
----------------------------------------------------------------------
Here are examples of features one may want or not when looking for subterms
A- REWRITING
1- Full conversion on closed terms
1a- Full conversion on closed terms in the presence of at least one evars (meta)
Section A1.
Variable y: nat.
Hypothesis H: forall x, x+2 = 0.
Goal y+(1+1) = 0.
rewrite H.
(* 0 = 0 *)
Abort.
Goal 2+(1+1) = 0.
rewrite H.
(* 0 = 0 *)
Abort.
(* This exists since the very beginning of Chet's unification for tactics *)
(* But this fails for setoid rewrite *)
1b- Full conversion on closed terms without any evars in the lemma
1b.1- Fails on rewrite (because Unification.w_unify_to_subterm_list replaces
unification by check for a syntactic subterm if terms has no evar/meta)
Goal 0+1 = 0 -> 0+(1+0) = 0.
intros H; rewrite H.
(* fails *)
Abort.
1b.2- Works with setoid rewrite
Require Import Setoid.
Goal 0+1 = 0 -> 0+(1+0) = 0.
intros H; rewrite H at 1.
(* 0 = 0 *)
Abort.
2- Using known instances in full conversion on closed terms
Section A2.
Hypothesis H: forall x, x+(2+x) = 0.
Goal 1+(1+2) = 0.
rewrite H.
Abort.
End A2.
(* This exists since 8.2 (HH) *)
3- Pattern-unification on Rels
Section A3a.
Variable F: (nat->nat->nat)->nat.
Goal exists f, F (fun x y => f x y) = 0 -> F (fun x y => plus y x) = 0.
eexists. intro H; rewrite H.
(* 0 = 0 *)
Abort.
End A3a.
(* Works since pattern unification on Meta applied to Rel was introduced *)
(* in unification.ml (8.1, Sep 2006, HH) *)
Section A3b.
Variables x y: nat.
Variable H: forall f, f x y = 0.
Goal plus y x = 0.
rewrite H.
(* 0 = 0 *)
Abort.
End A3b.
(* Works since pattern unification on all Meta was supported *)
(* in unification.ml (8.4, Jun 2011, HH) *)
4- Unification with open terms
Section A4.
Hypothesis H: forall x, S x = 0.
Goal S 0 = 0.
rewrite (H _).
(* 0 = 0 *)
Abort.
End A4.
(* Works since unification on Evar was introduced so as to support rewriting *)
(* with open terms (8.2, MS, r11543, Unification.w_unify_to_subterm_list ) *)
5- Unification of pre-existing evars
5a- Basic unification of pre-existing evars
Section A4.
Variables x y: nat.
Goal exists z, S z = 0 -> S (plus y x) = 0.
eexists. intro H; rewrite H.
(* 0 = 0 *)
Abort.
End A4.
(* This worked in 8.2 and 8.3 as a side-effect of support for rewriting *)
(* with open terms (8.2, MS, r11543) *)
5b- Pattern-unification of pre-existing evars in rewriting lemma
Goal exists f, forall x y, f x y = 0 -> plus y x = 0.
eexists. intros x y H; rewrite H.
(* 0 = 0 *)
Abort.
(* Works since pattern-unification on Evar was introduced *)
(* in unification.ml (8.3, HH, r12229) *)
(* currently governed by a flag: use_evars_pattern_unification *)
5c- Pattern-unification of pre-existing evars in goal
Goal exists f, forall x y, plus x y = 0 -> f y x = 0.
eexists. intros x y H; rewrite H.
(* 0 = 0 *)
Abort.
(* This worked in 8.2 and 8.3 but was removed for autorewrite in 8.4 *)
5d- Mixing pattern-unification of pre-existing evars in goal and evars in lemma
Goal exists f, forall x, (forall y, plus x y = 0) -> forall y:nat, f y x = 0.
eexists. intros x H y. rewrite H.
(* 0 = 0 *)
Abort.
(* This worked in 8.2 and 8.3 but was removed for autorewrite in 8.4 *)
6- Multiple non-identical but convertible occurrences
Tactic rewrite only considers the first one, from left-to-right, e.g.:
Section A6.
Variable y: nat.
Hypothesis H: forall x, x+2 = 0.
Goal (y+(2+0))+(y+(1+1)) = (y+(1+1))+(y+(2+0)).
rewrite H.
(* 0+(y+(1+1)) = y+(1+1)+0 *)
Abort.
End A6.
Tactic setoid rewrite first looks for syntactically equal terms and if
not uses the leftmost occurrence modulo delta.
Require Import Setoid.
Section A6.
Variable y: nat.
Hypothesis H: forall x, x+2 = 0.
Goal (y+(2+0))+(y+2) = (y+2)+(y+(2+0)).
rewrite H at 1 2 3 4.
(* (y+(2+0))+0 = 0+(y+(2+0)) *)
Abort.
Goal (y+(2+0))+(y+(1+1)) = (y+(1+1))+(y+(2+0)).
rewrite H at 1 2 3 4.
(* 0+(y+(1+1)) = y+(1+1)+0 *)
Abort.
End A6.
7- Conversion
Section A6.
Variable y: nat.
Hypothesis H: forall x, S x = 0.
Goal id 1 = 0.
rewrite H.
B- ELIMINATION (INDUCTION / CASE ANALYSIS)
This is simpler because open terms are not allowed and no unification
is involved (8.3).
|
