Meta-programming using MetaRocq
MetaRocq is a meta-programming framework that reuses the programming language underlying Rocq as meta-programming language.
For this, MetaRocq has an representation of Rocq terms as an inductive types:
Print term.- No need to understand it all, but you can see how the syntax of Rocq is
encoded. It is actually almost in one-to-one correspondance with the OCaml implementation.
Quoting
The power of MetaRocq is it allows you to go back and forth between this term representation and actual Rocq terms.
We talk about quoting for the action going from actual Rocq definitions to their MetaRocq representation.
Below you see how one can quote the identity function on natural numbers. It starts with a tLam and takes as argument a name for the variable, here "x". Then comes the type of the argument which is a complicated reference to the inductive type nat. Finally the body of the function is tRel 0. This means the 0th variable, in other words the last one to have been introduced, which is x here. This is what we call de Bruijn indices. In fact the "x" annotation is just to help printing, but carries no meaning.
Check $quote (fun (x : nat) => x).We can then use $unquote to perform the opposite action.
Check $unquote (tLam "y" ($quote bool) ($quote (fun (x : nat) => x))).As we said, you have to use de Bruin indices to deal with variables:
Definition tNat :=
$quote nat.
Definition idNat :=
$unquote (tLam "x" tNat (tRel 0)).
Print idNat.Power function
The usual example of meta-programming is the power function. The idea is that mpow 5 x will reduce to (let p := x * x in p * p) * x.
Note: When performing meta-programming, it's safe to deactivate the guard checker locally.
#[bypass_check(guard)] Fixpoint mpow' (n : nat) : term :=
match n with
| 0 => $quote 1
| 1 => tRel 0
| 2 => tApp ($quote mult) [ tRel 0 ; tRel 0 ]
| S n' as n =>
if n mod 2 =? 0
then tLet "p" ($quote nat) (mpow' (div n 2)) (tApp ($quote mult) [ tRel 0 ; tRel 0 ])
else tApp ($quote mult) [ mpow' n' ; tRel 0 ]
end.
Print mpow'. See how quoting got expanded at definition time
Definition mpow n :=
tLam "x" ($quote nat) (mpow' n).
Definition pow3 :=
$unquote (mpow 3).
Print pow3.
Definition pow5 :=
$unquote (mpow 5).
Print pow5.
Definition pow13 :=
$unquote (mpow 13).
Print pow13.Transforming terms
We can build terms, but of course we can also inspect them to produce new terms. For this we can build functions that match on the syntax and produce new terms (see exercises). We also provide some utility to do it in a shorter way, altough it might feel more technically involved, we'll let you judge what you prefer.
We'll write a transformation that dupplicates all uses of S inside a term.
Definition double_S :=
transform (fun t k =>
match t with
| tApp s [ n ] =>
if s == $quote S then tApp s [ k t ]
else k t
| _ => k t
end
).transform takes a function that will tell what to do t o the term that deviates from applying the identity function. This function takes as argument a term to inspect t, and a continuation k. Here we do a match on t and look at the only case we find interesting: application of S to some n. If it's not of this form, then we call the continuation on the whole term t so that it does it's job of calling our function on the subterms. When it some S n, we dupplicate the S and then we still call the continuation on t. The reason is that the continuation will not call our program on n if we call k n since it will only call our program on its subterms.
Don't worry if this is a bit hard to get your head around it. It is for me as well!
Let's still look at what it does.
Compute $unquote (double_S ($quote 10)).
Compute $unquote (double_S ($quote (2 * 3))).To see clearer, let's not reduce *
Eval cbn - ["*"] in $unquote (double_S ($quote (2 * 3))).We see here, that this operation is really syntactic, and not semantic.
** Manipulating commands with MetaRocq
Finally, MetaRocq also contains a representation of Rocq vernacular commands like Definition, Print, Locate, which can be useful to write more complex meta-programs.
MetaRocq Run (
t <- tmLemma "foo" nat ;;
tmDefinition "bar" (t + t + 2)
).
Next Obligation. This is how we prove a tmLemma
exact 12.
Defined.After we prove foo, the program continues and defines bar.
Print bar. foo + foo + 2
MetaRocq Run (
t <- tmLemma "baz" nat ;;
st <- tmEval all t ;;
tmDefinition "simpl_baz" st
).
Next Obligation.
exact (10 + 2).
Defined.
Print simpl_baz.Proof by reflection
Proof by reflection is a powerful technique to solve difficult proof goals efficiently if they can be transformed into a computational problem.
Instead of constructing a complex proof term for a difficult goal we 1. Define a syntactic representation of the shape of goals we want to solve and an interpretation function from shape to actual goals -- a reflection procedure. 2. Implement a decision procedure for goals that have this syntactic shape 3. Prove the decision procedure correct 4. We implement a "reification" procedure translating a goal into its shape, using meta-programming. 4. When trying to prove a difficult goal, we employ the decision procedure on the shape of the goal.
The process of going from a goal to its shape is called reification.
In this example, we will care about propositional logic of the following shape:
Inductive form: Type :=
| var (x: nat)
| top
| bot
| imp (s t: form)
| and (s t : form)
| or (s t : form).We write a reflection procedure from form to Propositions:
Fixpoint reflect (env : nat -> Prop) (s : form) :=
match s with
| var x => env x
| top => True
| bot => False
| imp s t => reflect env s -> reflect env t
| and s t => (reflect env s) /\ (reflect env t)
| or s t => (reflect env s) \/ (reflect env t)
end.We now write a decision procedure employing boolean logic:
Fixpoint decider (env : nat -> bool) (s : form) :=
match s with
| var x => env x
| top => true
| bot => false
| imp s t => if decider env s then decider env t else true
| and s t => andb (decider env s) (decider env t)
| or s t => orb (decider env s) (decider env t)
end.We prove the decision procedure correct:
Lemma decider_iff envb env s :
(forall n, env n <-> envb n = true) ->
reflect env s <-> decider envb s = true.
Proof.
intros Henv.
induction s; cbn.
all: try now firstorder congruence.
all: destruct (decider envb s1), (decider envb s2); firstorder.
Qed.We now turn to implementing a reification procedure. Crucially, the reification procedure must map parts of the goal that do not fall into the shapes defined as form as var. To ensure that the same goals are mapped to the same variable, we implement the following procedure adding an element to a list if it is not in there, and otherwise returning the index of the element in the list:
Fixpoint index {A} (d : A -> A -> bool) a l :=
match l with
| [] => None
| x :: l =>
if d x a then Some 0 else
match index d a l with
| Some n => Some (S n)
| None => None
end
end.
Definition list_add {A} (d : A -> A -> bool) a l :=
match index d a l with
| Some n => (n, l)
| None => (length l, l ++ [a])
end.We now write the recursive reification procedure using MetaRocq:
From MetaRocq.Utils Require Import ReflectEq.
Fixpoint reify_rec f l : (form * list term) :=
let catchall := fun _ : unit =>
let '(n, s_env) := list_add term_eqb f l in
(var n, s_env) in
match f with
| tInd {| inductive_mind := cst;
inductive_ind := 0 |} [] =>
if cst == (MPfile ["Logic"; "Init"; "Corelib"], "False")
then
(bot, [])
else if cst == (MPfile ["Logic"; "Init"; "Corelib"], "True") then
(top, [])
else catchall tt
| tApp (tConst cst []) [s] =>
if cst == (MPfile ["Logic"; "Init"; "Corelib"], "not")
then
let (s_form, s_env) := reify_rec s l in
ret (imp s_form bot, s_env)
else
catchall tt
| tApp (tInd {| inductive_mind := cst;
inductive_ind := 0 |} []) [s; t]
| tApp (tConst cst []) [s; t] =>
if cst == (MPfile ["Logic"; "Init"; "Corelib"], "and")
then
let (s_form, s_env) := reify_rec s l in
let (t_form, t_env) := reify_rec t s_env in
ret (and s_form t_form, t_env)
else if cst == (MPfile ["Logic"; "Init"; "Corelib"], "or")
then
let (s_form, s_env) := reify_rec s l in
let (t_form, t_env) := reify_rec t s_env in
ret (or s_form t_form, t_env)
else if cst == (MPfile ["Logic"; "Init"; "Corelib"], "iff")
then
let (s_form, s_env) := reify_rec s l in
let (t_form, t_env) := reify_rec t s_env in
(and (imp s_form t_form) (imp t_form s_form), t_env)
else
catchall tt
| tProd na s t =>
let (s_form, s_env) := reify_rec s l in
let (t_form, t_env) := reify_rec t s_env in
(imp s_form t_form, t_env)
| _ => catchall tt
end.We write a reification tactic which takes a proposition as input,
quotes it into MetaRocq syntax,
runs the recursive reification function, and
unquotes all variable denotations in the variable list again into Propositions
Ltac reify f :=
constr:(ltac:(
run_template_program (mlet t <- tmQuote f ;;
let (x, lx) := reify_rec t (@nil term) in
mlet lx' <- monad_map (tmUnquoteTyped Prop) lx ;;
ret (x, lx'))
(fun x => exact x))).We now assume a strong form of classical logic to prove reification correct:
Axiom dec : forall P, {P} + {~P}.
Lemma decider_reflect env s :
decider (fun n => if dec (env n) then true else false) s ->
reflect env s.
Proof.
intros H.
eapply decider_iff.
2: eassumption.
cbn. intros n. destruct (dec (env n)); firstorder congruence.
Qed.Lastly, we write a tactic which reifies a goal, applies the correctness theorem of the decider; and then repeatedly destruct the dec axiom to solve the goal:
Ltac cauto_r :=
lazymatch goal with
| |- ?G =>
lazymatch reify G with
| (?fx, ?lx) =>
change (reflect (fun n => List.nth n lx False) fx);
apply decider_reflect
end
end.
Ltac intro_Prop :=
match goal with
| |- forall P : Prop, _ => intro
end.
Ltac cauto :=
repeat intro_Prop;
cauto_r;
cbn; repeat destruct dec; try reflexivity.
Goal forall A B : Prop, A -> B -> A.
Proof.
cauto.
Qed.
Goal forall A B C : Prop, ~ A \/ ~ B \/ (C /\ True) <-> ~ (A /\ B /\ ~ C).
Proof.
cauto.
Qed.Note that the tactic nicely generates counterexamples if it does not work:
Goal forall A B : Prop, A -> B.
Proof.
cauto.
Abort.