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
|
From elpi Require Import elpi.
(** Abstract a term over something, like the generalize tactic *)
Elpi Command generalize.
Elpi Accumulate lp:{{
% we add a new constructor to terms to represent terms to be abstracted
type abs int -> term.
% bind back abstracted subterms
pred bind i:int, i:term, o:term.
bind M T T1 :- M > 0,
T1 = {{ fun x => lp:(B x) }}, % we build a Coq "fun .. => "
N is M - 1,
pi x\ % we allocate the fresh symbol for (abs M)
(copy (abs M) x :- !) ==> % we schedule the replacement (abs M) -> x
bind N T (B x).
bind 0 T T1 :- copy T T1. % we perform all the replacements
main [trm T] :- std.do! [
% example rule, abstracts all 1s.
((pi N M\ fold-map {{ 1 }} N (abs M) M :- !, M is N + 1) ==> fold-map T 0 T1 NVars),
bind NVars T1 T2,
coq.say {coq.term->string T} "becomes" {coq.term->string T2},
].
}}.
Elpi generalize (3 + 7).
(* prints:
(3 + 7) becomes (fun (x : ?e) (x0 : ?e0) => S (S x0) + S (S (S (S (S (S x))))))
*)
|
