Curry-Howard tactics
How to create simple tactics by using (proof) terms and the elaborator of
Rocq. 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.
- From elpi Require Import elpi.
- [Loading ML file ppx_deriving.runtime (implicit dependency) ... done] [Loading ML file re (implicit dependency) ... done] [Loading ML file re.str (implicit dependency) ... done] [Loading ML file elpi.util (implicit dependency) ... done] [Loading ML file elpi.lexer_config (implicit dependency) ... done] [Loading ML file menhirLib (implicit dependency) ... done] [Loading ML file stdlib-shims (implicit dependency) ... done] [Loading ML file elpi.parser (implicit dependency) ... done] [Loading ML file camlp-streams (implicit dependency) ... done] [Loading ML file easy-format (implicit dependency) ... done] [Loading ML file biniou (implicit dependency) ... done] [Loading ML file yojson (implicit dependency) ... done] [Loading ML file atdgen-runtime (implicit dependency) ... done] [Loading ML file elpi.trace.atd (implicit dependency) ... done] [Loading ML file elpi.trace.runtime (implicit dependency) ... done] [Loading ML file elpi.runtime (implicit dependency) ... done] [Loading ML file elpi.compiler (implicit dependency) ... done] [Loading ML file elpi (implicit dependency) ... done] [Loading ML file rocq-elpi.elpi ... done]
- 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.
- 1 goal x, y, z : nat H : x < y ============================ y < z -> x < z
- Proof.
- elpi id.
- goal X0 c0 c1 c2 c3 is [decl c3 `H:r` (app [global (const «lt»), c0, c1]), decl c2 `z:r` (global (indt «nat»)), decl c1 `y:r` (global (indt «nat»)), decl c0 `x:r` (global (indt «nat»))] ------- prod `_:r` (app [global (const «lt»), c1, c2]) c4 \ app [global (const «lt»), c0, c2]
- Abort.
Things are wired up in such a way that assigning a "wrong" value to the goal's evar fails:
- Elpi Tactic silly.
- Elpi Accumulate lp:{{ solve (goal _ Ev _ _ _) _ :- Ev = {{true}}. solve (goal _ Ev _ _ _) _ :- Ev = {{3}}. }}.
- Lemma l1 : nat.
- 1 goal ============================ nat
- Proof.
- elpi silly.
- No more goals.
- Show Proof.
- 3
- 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.
- 1 goal x, y, z : nat H : x < y ============================ y < z -> x < z
- Proof.
- elpi intro H1.
- 1 goal x, y, z : nat H : x < y H1 : y < z ============================ x < z
- Abort.
And now let's write a little automation:
- Elpi Tactic auto.
- Elpi Accumulate lp:{{ shorten coq.ltac.{ open , or , repeat }. pred intro name, goal -> list sealed-goal. intro S G GS :- refine (fun S Src_ Tgt_) G GS. % Ex falso pred exf goal -> 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 goal -> 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).
- 1 goal ============================ forall P : Prop, (False -> P) /\ (False \/ True)
- Proof.
- elpi auto.
- No more goals.
- Qed.