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
|
From elpi Require Import elpi.
(* Tactics
The entry point of a tactic is called solve
and the goal is made of a proof context, a type
to inhabit and the corresponding evar to assign *)
Elpi Tactic id.
Elpi Accumulate lp:{{
solve (goal Ctx Ev Ty _ _) _ :-
coq.say "goal" Ev "is\n" Ctx "\n-------\n" Ty.
}}.
Lemma l0 x y z (H : x < y) : y < z -> x < z.
Proof.
elpi id.
Abort.
(* Things are wired up in such a way that assigning a
"wrong" value to Ev fails *)
Elpi Tactic silly.
Elpi Accumulate lp:{{
solve (goal _ Ev _ _ _) _ :- Ev = {{true}}.
solve (goal _ Ev _ _ _) _ :- Ev = {{3}}.
}}.
Lemma l1 : nat.
Proof.
elpi silly.
Show Proof.
Qed.
(* Now we write "intro" in Curry-Howard style *)
Elpi Tactic intro.
Elpi Accumulate lp:{{
solve (goal _ _ _ _ [str S] as G) GS :-
coq.string->name S N,
refine (fun N Src_ Tgt_) G GS.
}}.
Lemma l2 x y z (H : x < y) : y < z -> x < z.
Proof.
elpi intro H1.
Abort.
(* Now let's write a little automation *)
Elpi Tactic auto.
Elpi Accumulate lp:{{
shorten coq.ltac.{ open , or , repeat }.
pred intro i:name, i:goal, o:list sealed-goal.
intro S G GS :- refine (fun S Src_ Tgt_) G GS.
% Ex falso
pred exf i:goal, o:list sealed-goal.
exf (goal Ctx _ Ty _ _ as G) [] :-
std.exists Ctx (x\ sigma w\ x = decl V w {{False}}),
refine {{ match lp:V in False return lp:Ty with end }} G [].
% Constructor
pred kon i:goal, o:list sealed-goal.
kon (goal _ _ Ty _ _ as G) GS :-
coq.safe-dest-app Ty (global (indt GR)) _,
coq.env.indt GR _ _ _ _ Ks Kt,
std.exists2 Ks Kt (k\ t\
coq.saturate t (global (indc k)) P,
refine P G GS).
% entry point; we assert no goals are left
solve G [] :-
repeat (or [open exf, open kon, open (intro `H`)]) (seal G) [].
}}.
Lemma l3 : forall P : Prop, (False -> P) /\ (False \/ True).
Proof.
elpi auto.
Qed.
|
