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
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
|
(***************************************************************************)
(* This is part of aac_tactics, it is distributed under the terms of the *)
(* GNU Lesser General Public License version 3 *)
(* (see file LICENSE for more details) *)
(* *)
(* Copyright 2009-2010: Thomas Braibant, Damien Pous. *)
(***************************************************************************)
(** aac_rewrite -- rewriting modulo *)
(* functions to handle the failures of our tactic. Some should be
reported [anomaly], some are on behalf of the user [user_error]*)
let anomaly msg =
Util.anomaly ("aac_tactics: " ^ msg)
let user_error msg =
Util.error ("aac_tactics: " ^ msg)
(* debug and timing functions *)
let debug = false
let printing = false
let time = false
let debug x =
if debug then
Printf.printf "%s\n%!" x
let pr_constr msg constr =
if printing then
( Pp.msgnl (Pp.str (Printf.sprintf "=====%s====" msg));
Pp.msgnl (Printer.pr_constr constr);
)
let time msg tac =
if time then Coq.tclTIME msg tac
else tac
let tac_or_exn tac exn msg =
fun gl -> try tac gl with e -> exn msg e
(* helper to be used with the previous function: raise a new anomaly
except if a another one was previously raised *)
let push_anomaly msg = function
| Util.Anomaly _ as e -> raise e
| _ -> anomaly msg
module M = Matcher
open Term
open Names
open Coqlib
open Proof_type
(** [find_applied_equivalence goal eq] try to ensure that the goal is
an applied equivalence relation, with two operands of the same type.
This function is transitionnal, as we plan to integrate with the
new rewrite features of Coq 8.3, that seems to handle this kind of
things.
*)
let find_applied_equivalence goal : Term.constr -> Coq.eqtype *Term.constr *Term.constr* Coq.goal_sigma = fun equation ->
let env = Tacmach.pf_env goal in
let evar_map = Tacmach.project goal in
match Coq.decomp_term equation with
| App(c,ca) when Array.length ca >= 2 ->
let n = Array.length ca in
let left = ca.(n-2) in
let right = ca.(n-1) in
let left_type = Tacmach.pf_type_of goal left in
(* let right_type = Tacmach.pf_type_of goal right in *)
let partial_app = mkApp (c, Array.sub ca 0 (n-2) ) in
let eq_type = Coq.Classes.mk_equivalence left_type partial_app in
begin
try
let evar_map, equivalence = Typeclasses.resolve_one_typeclass env evar_map eq_type in
let goal = Coq.goal_update goal evar_map in
((left_type, partial_app), equivalence),left, right, goal
with
| Not_found -> user_error "The goal is not an applied equivalence"
end
| _ -> user_error "The goal is not an equation"
(* [find_applied_equivalence_force] brutally decomposes the given
equation, and fail if we find a relation that is not the same as
the one we look for [r] *)
let find_applied_equivalence_force rlt goal : Term.constr -> Term.constr *Term.constr* Coq.goal_sigma = fun equation ->
match Coq.decomp_term equation with
| App(c,ca) when Array.length ca >= 2 ->
let n = Array.length ca in
let left = ca.(n-2) in
let right = ca.(n-1) in
let partial_app = mkApp (c, Array.sub ca 0 (n-2) ) in
let _ = if snd rlt = partial_app then () else user_error "The goal and the hypothesis have different top-level relations" in
left, right, goal
| _ -> user_error "The hypothesis is not an equation"
(** Build a couple of [t] from an hypothesis (variable names are not
relevant) *)
let rec t_of_hyp goal rlt envs e = match Coq.decomp_term e with
| Prod (name,ty,c) -> let x, y = t_of_hyp goal rlt envs c
in x,y+1
| _ ->
let l,r ,goal = find_applied_equivalence_force rlt goal e in
let l,goal = Theory.Trans.t_of_constr goal rlt envs l in
let r,goal = Theory.Trans.t_of_constr goal rlt envs r in
(l,r),0
(** @deprecated: [option_rip] will be removed as soon as a proper interface is
given to the user *)
let option_rip = function | Some x -> x | None -> raise Not_found
let mk_hyp_app conv c env =
let l = Matcher.Subst.to_list env in
let l = List.sort (fun (x,_) (y,_) -> compare y x) l in
let l = List.map (fun x -> conv (snd x)) l in
let v = Array.of_list l in
mkApp (c,v)
(** {1 Tactics} *)
(** [by_aac_reflexivity] is a sub-tactic that closes a sub-goal that
is merely a proof of equality of two terms modulo AAC *)
let by_aac_reflexivity eqt envs (t : Matcher.Terms.t) (t' : Matcher.Terms.t) : Proof_type.tactic = fun goal ->
let maps, reifier,reif_letins = Theory.Trans.mk_reifier eqt envs goal in
let ((x,r),e) = eqt in
(* fold through a term and reify *)
let t = Theory.Trans.reif_constr_of_t reifier t in
let t' = Theory.Trans.reif_constr_of_t reifier t' in
(* Some letins *)
let eval, eval_letin = Coq.mk_letin' "eval_name" (mkApp (Lazy.force Theory.eval, [|x;r; maps.Theory.Trans.env_sym; maps.Theory.Trans.env_prd; maps.Theory.Trans.env_sum|])) in
let _ = pr_constr "left" t in
let _ = pr_constr "right" t' in
let t , t_letin = Coq.mk_letin "left" t in
let t', t_letin'= Coq.mk_letin "right" t' in
let apply_tac = Tactics.apply (
mkApp (Lazy.force Theory.decide_thm, [|x;r;e; maps.Theory.Trans.env_sym; maps.Theory.Trans.env_prd; maps.Theory.Trans.env_sum;t;t'|]))
in
Tactics.tclABSTRACT None
(Tacticals.tclTHENLIST
[
tac_or_exn reif_letins anomaly "invalid letin (1)";
tac_or_exn eval_letin anomaly "invalid letin (2)";
tac_or_exn t_letin anomaly "invalid letin (3)";
tac_or_exn t_letin' anomaly "invalid letin (4)";
tac_or_exn apply_tac anomaly "could not apply the decision theorem";
tac_or_exn (time "vm_norm" (Tactics.normalise_vm_in_concl)) anomaly "vm_compute failure";
Tacticals.tclORELSE Tactics.reflexivity
(Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC"))
])
goal
(** The core tactic for aac_rewrite *)
let core_aac_rewrite ?(l2r = true) envs eqt rew p subst left = fun goal ->
let rlt = fst eqt in
let t = Matcher.Subst.instantiate subst p in
let tr = Theory.Trans.raw_constr_of_t envs rlt t in
let tac_rew_l2r =
if l2r then Equality.rewriteLR rew else Equality.rewriteRL rew
in
pr_constr "transitivity through" tr;
Tacticals.tclTHENSV
(tac_or_exn (Tactics.transitivity tr) anomaly "Unable to make the transitivity step")
[|
(* si by_aac_reflexivity foire (pas un theoreme), il fait tclFAIL, et on rattrape ici *)
tac_or_exn (time "by_aac_refl" (by_aac_reflexivity eqt envs left t)) push_anomaly "Invalid transitivity step";
tac_or_exn (tac_rew_l2r) anomaly "Unable to rewrite";
|] goal
exception NoSolutions
(** Choose a substitution from a
[(int * Terms.t * Env.env Search.m) Search.m ] *)
let choose_subst subterm sol m=
try
let (depth,pat,envm) = match subterm with
| None -> (* first solution *)
option_rip (Matcher.Search.choose m)
| Some x ->
List.nth (List.rev (Matcher.Search.to_list m)) x
in
let env = match sol with
None -> option_rip (Matcher.Search.choose envm)
| Some x -> List.nth (List.rev (Matcher.Search.to_list envm)) x
in
pat, env
with
| _ -> raise NoSolutions
(** rewrite the constr modulo AC from left to right in the
left member of the goal
*)
let aac_rewrite rew ?(l2r=true) ?(show = false) ?strict ?occ_subterm ?occ_sol : Proof_type.tactic = fun goal ->
let envs = Theory.Trans.empty_envs () in
let rew_type = Tacmach.pf_type_of goal rew in
let (gl : Term.types) = Tacmach.pf_concl goal in
let _ = pr_constr "h" rew_type in
let _ = pr_constr "gl" gl in
let eqt, left, right, goal = find_applied_equivalence goal gl in
let rlt = fst eqt in
let left,goal = Theory.Trans.t_of_constr goal rlt envs left in
let right,goal = Theory.Trans.t_of_constr goal rlt envs right in
let (hleft,hright),hn = t_of_hyp goal rlt envs rew_type in
let pattern = if l2r then hleft else hright in
let m = Matcher.subterm ?strict pattern left in
let m = Matcher.Search.sort (fun (x,_,_) (y,_,_) -> x - y) m in
if show
then
let _ = Pp.msgnl (Pp.str "All solutions:") in
let _ = Pp.msgnl (Matcher.pp_all (fun t -> Printer.pr_constr (Theory.Trans.raw_constr_of_t envs rlt t) ) m) in
Tacticals.tclIDTAC goal
else
try
let pat,env = choose_subst occ_subterm occ_sol m in
let rew = mk_hyp_app (Theory.Trans.raw_constr_of_t envs rlt )rew env in
core_aac_rewrite ~l2r envs eqt rew pat env left goal
with
| NoSolutions -> Tacticals.tclFAIL 0
(Pp.str (if occ_subterm = None && occ_sol = None
then "No matching subterm found"
else "No such solution")) goal
let aac_reflexivity : Proof_type.tactic = fun goal ->
let (gl : Term.types) = Tacmach.pf_concl goal in
let envs = Theory.Trans.empty_envs() in
let eqt, left, right, evar_map = find_applied_equivalence goal gl in
let rlt = fst eqt in
let left,goal = Theory.Trans.t_of_constr goal rlt envs left in
let right,goal = Theory.Trans.t_of_constr goal rlt envs right in
by_aac_reflexivity eqt envs left right goal
open Tacmach
open Tacticals
open Tacexpr
open Tacinterp
open Extraargs
(* Adding entries to the grammar of tactics *)
TACTIC EXTEND _aac1_
| [ "aac_reflexivity" ] -> [ aac_reflexivity ]
END
TACTIC EXTEND _aac2_
| [ "aac_rewrite" orient(o) constr(c) "subterm" integer(i) "subst" integer(j)] ->
[ fun gl -> aac_rewrite ~l2r:o ~strict:true ~occ_subterm:i ~occ_sol:j c gl ]
END
TACTIC EXTEND _aac3_
| [ "aac_rewrite" orient(o) constr(c) "subst" integer(j)] ->
[ fun gl -> aac_rewrite ~l2r:o ~strict:true ~occ_subterm:0 ~occ_sol:j c gl ]
END
TACTIC EXTEND _aac4_
| [ "aac_rewrite" orient(o) constr(c) "subterm" integer(i)] ->
[ fun gl -> aac_rewrite ~l2r:o ~strict:true ~occ_subterm:i ~occ_sol:0 c gl ]
END
TACTIC EXTEND _aac5_
| [ "aac_rewrite" orient(o) constr(c) ] ->
[ fun gl -> aac_rewrite ~l2r:o ~strict:true c gl ]
END
TACTIC EXTEND _aac6_
| [ "aac_instances" orient(o) constr(c)] ->
[ fun gl -> aac_rewrite ~l2r:o ~strict:true ~show:true c gl ]
END
TACTIC EXTEND _aacu2_
| [ "aacu_rewrite" orient(o) constr(c) "subterm" integer(i) "subst" integer(j)] ->
[ fun gl -> aac_rewrite ~l2r:o ~occ_subterm:i ~occ_sol:j c gl ]
END
TACTIC EXTEND _aacu3_
| [ "aacu_rewrite" orient(o) constr(c) "subst" integer(j)] ->
[ fun gl -> aac_rewrite ~l2r:o ~occ_subterm:0 ~occ_sol:j c gl ]
END
TACTIC EXTEND _aacu4_
| [ "aacu_rewrite" orient(o) constr(c) "subterm" integer(i)] ->
[ fun gl -> aac_rewrite ~l2r:o ~occ_subterm:i ~occ_sol:0 c gl ]
END
TACTIC EXTEND _aacu5_
| [ "aacu_rewrite" orient(o) constr(c) ] ->
[ fun gl -> aac_rewrite ~l2r:o c gl ]
END
TACTIC EXTEND _aacu6_
| [ "aacu_instances" orient(o) constr(c)] ->
[ fun gl -> aac_rewrite ~l2r:o ~show:true c gl ]
END
|