(*|
:Authors: Yannick Forster, Théo Winterhalter
:Files:
- `Source <../files/lesson4_part3.v>`_
- `Exercise sheet <../files/tp4.v>`_
- `MetaRocq prelude <../files/MetaRocqPrelude.v>`_
.. role:: coq(code)
:language: coq
:class: highlight
.. default-role:: coq
|*)
(*| .. coq:: none |*)
Axiom REPLACE_ME : forall {A : Type}, A.
From Stdlib Require Import Lia List ZArith.
Import ListNotations.
Create HintDb indb.
Axiom DNE : forall P : Prop, ~~ P -> P.
From Stdlib Require Import Classical.
#[export] Hint Extern 3 (@eq nat _ _) => lia : indb.
#[export] Hint Extern 3 (@eq Z _ _) => lia : indb.
From Stdlib Require Import Setoid.
Set Default Goal Selector "!".
Ltac split_or_apply :=
match goal with
| |- ?A /\ ?B => split
| h : ?B -> ?A |- ?A => apply h (* Here we match on any hypothesis *)
(* The name [h] is of our choosing, it's going to apply to hypothesis
[H : nat -> bool] for instance. *)
end.
Ltac my_assumption :=
match goal with
| H : ?A |- ?A => apply H
end.
Ltac splits :=
lazymatch goal with
| |- ?A * ?B => split ; splits
| _ => idtac
end.
Ltac handle_hyp h :=
lazymatch type of h with
| (?A * ?B)%type => destruct h
| nat => induction h
| _ => idtac
end.
Ltac fwd h :=
match type of h with
| ?P -> _ =>
let h' := fresh in
assert (h' : P) ; [| specialize (h h') ; clear h' ]
end.
Ltac forward_gen h tac :=
match type of h with
| ?P -> _ =>
let h' := fresh in
assert (h' : P) ; [ tac | specialize (h h') ; clear h' ]
end.
Tactic Notation "forward" constr(H) := forward_gen H ltac:(idtac).
Tactic Notation "forward" constr(H) "by" tactic(tac) := forward_gen H tac.
Ltac my_tauto :=
lazymatch goal with
| h : ?P |- ?P => exact h
| |- True => constructor
| |- _ /\ _ => split ; my_tauto
| |- _ -> _ => intro ; my_tauto
| h : False |- _ => destruct h
| h : _ /\ _ |- _ => destruct h ; my_tauto
| h : _ \/ _ |- _ => destruct h ; my_tauto
| h1 : ?P -> ?Q, h2 : ?P |- _ => specialize (h1 h2) ; my_tauto
| |- _ \/ _ => (left ; my_tauto) || (right ; my_tauto)
end.
(*| |*)
(*|
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Meta-programming using MetaRocq
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
MetaRocq is a meta-programming framework that reuses the programming language underlying Rocq
as meta-programming language.
To follow along, download the `MetaRocq prelude <../files/MetaRocqPrelude.v>`_
next to this file and compile it with `rocq compile MetaRocqPrelude.v`.
|*)
Require Import MetaRocqPrelude.
(*| 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.
(*|
~~~~~~~~~~~~~~~~~
Print Assumptions
~~~~~~~~~~~~~~~~~
In Rocq, you have a very useful command which can tell you on which axiom a
given lemma depends.
See how it works below.
|*)
Axiom LEM : forall (P : Prop), P \/ ~ P.
Axiom funext : forall A B (f g : A -> B), (forall x, f x = g x) -> f = g.
Lemma foo_ax :
(fun n => n + 0) = (fun n => n).
Proof.
apply funext. intro. rewrite <- plus_n_O. reflexivity.
Qed.
Print Assumptions foo_ax. (*| Only `funext` is listed. |*)
(*| We will now try to implement our own `Print Assumptions` using MetaRocq.
For this, we need to be able to manipulate not only the term but also its
environment to be able to check its dependencies.
For instance, if we inspect `foo_ax` above, we need to know that `funext` is
indeed referring to an axiom, and this information is not contained within
`foo_ax` itself.
We can use `$quote_rec` to get both the term and its dependencies as follows:
|*)
Definition q_foo := $quote_rec foo_ax.
Check q_foo. (*| `global_env × term` |*)
(*|
We can for instance querry the environment to see whether it contains
some constant such as `plus_n_O` or `funext`.
|*)
Definition foo_env :=
let (env, _) := q_foo in env.
Compute lookup_constant foo_env (MPfile ["Peano"; "Init"; "Corelib"], "plus_n_O").
(*|
We get `Some` and then a big record with a `cst_type` and `cst_body` which
is also of the form `Some _`.
The presence of this `cst_body` means that this is a `Definition` and not an
`Axiom`.
Indeed check out what it returns for `funext`.
Warning: You have to change `tp4` into the name of your file, here this
assumes you didn't rename it and it is `tp4.v`.
|*)
Compute lookup_constant foo_env (MPfile ["tp4"], "funext").
(*| This time, `cst_body := None`. It's an axiom. |*)
(*|
To give you inspiration for the rest here is the (deep) identity function on
`term`.
|*)
Fixpoint identity (t : term) :=
match t with
| tRel n => tRel n
| tVar id => tVar id
| tEvar ev args => tEvar ev (map identity args)
| tSort s => tSort s
| tCast t kind v => tCast (identity t) kind (identity v)
| tProd na ty body => tProd na (identity ty) (identity body)
| tLambda na ty body => tLambda na (identity ty) (identity body)
| tLetIn na def def_ty body => tLetIn na (identity def) (identity def_ty) (identity body)
| tApp f args => tApp (identity f) (map identity args)
| tConst c u => tConst c u
| tInd ind u => tInd ind u
| tConstruct ind idx u => tConstruct ind idx u
| tCase ind p discr brs =>
let p' := map_predicate id identity identity p in
let brs' := map_branches identity brs in
tCase ind p' (identity discr) brs'
| tProj proj t => tProj proj (identity t)
| tFix mfix idx => tFix (map (map_def identity identity) mfix) idx
| tCoFix mfix idx => tCoFix (map (map_def identity identity) mfix) idx
| tInt i => tInt i
| tFloat f => tFloat f
| tString s => tString s
| tArray u arr def ty => tArray u (map identity arr) (identity def) (identity ty)
end.
(*|
.. raw:: html
Exercise: Print Assumptions
..
|*)
(*|
Define a Rocq function `assumptions : global_env × term -> list kername`
such that `Compute assumptions ($quote_rec f)` returns the list of
assumptions (axioms) that `f` depends on, including recursively.
Note: You cannot convince Rocq that it is terminating, so we'll deactivate
termination checking. That's ok when meta-programming.
Hint: You may use the `flat_map` and `lookup_constant` functions too.
|*)
Unset Guard Checking.
Fixpoint assms (env : global_env) (t : term) {struct t} : list kername :=
REPLACE_ME.
Set Guard Checking.
Definition assumptions p :=
assms p.1 p.2.
Compute assumptions ($quote_rec 0).
Compute assumptions ($quote_rec foo_ax).
Definition bar_ax : nat :=
let x := foo_ax in
139.
Compute assumptions ($quote_rec bar_ax).
Module test.
Lemma DNE P : ~~ P -> P.
Proof.
tauto.
Qed.
End test.
Compute assumptions ($quote_rec test.DNE).
(*|
.. raw:: html
Exercise: Folding multiply-add
..
|*)
(*|
Define a function which replaces any subterm of the form `a * b + c` with
`muladd a b c` defined below.
Hint: You can use `u == v` to check whether `u` and `v` are equal terms
(it returns a boolean).
|*)
Definition muladd a b c :=
a * b + c.
#[bypass_check(guard)] Fixpoint fold_muladd (t : term) : term :=
REPLACE_ME.
(*| Test it with the following. |*)
(*|
.. raw:: html
Exercise: Folding multiply-add with transform
..
|*)
(*|
Now that you suffered through the definition of `fold_muladd`, define it again
using `transform`.
`transform` takes `h : tm_handler` and transforms `t : term` into another
`term`.
The handler is typically of the form `fun t k => ...` where `t` is the subterm
to inspect/transform and `k` is a continuation. Calling `k` on a subterm
(or on `t`) itself, gives control back to `transform` which will decompose
the subterm once, and then call the handler again on the subsequent subterms.
|*)
Definition muladd_handler : tm_handler :=
REPLACE_ME.
Definition fold_muladd_alt :=
transform muladd_handler.
(*|
If you want, you can also do the same for `assumptions` by using
`tm_fold` which is similar but implements a fold instead.
|*)
Definition assum_fold (env : global_env) : fold_handler (list kername) :=
REPLACE_ME.
Definition assumptions_alt p : list kername :=
tm_fold (assum_fold p.1) [] p.2.
Compute assumptions_alt ($quote_rec 0).
Compute assumptions_alt ($quote_rec foo_ax).
Compute assumptions_alt ($quote_rec bar_ax).
Compute assumptions_alt ($quote_rec test.DNE).
(*|
.. raw:: html
Exercise: Reification
..
|*)
(*|
Write a command `reify` that turns a Rocq expression of type `nat` into an
expression of the following datatype.
Expressions that do not start with `+` or `*` are reified as constants.
|*)
Inductive arith :=
| aPlus : arith -> arith -> arith
| aTimes : arith -> arith -> arith
| aConst : nat -> arith.
#[bypass_check(guard)] Fixpoint reify (t : term) : term :=
REPLACE_ME.
Goal 4 * (9 + 12) + (3 + 1 * 7) = 2.
Proof.
Admitted.
(*|
.. raw:: html
Exercise: Instantiating axioms (advanced)
..
|*)
(*|
Write a meta-program that takes a definition potentially using an axioms and
a proof of said axiom to produce a new definition, equal to the original one
expcet that uses of the axioms are replaced by the proof.
The axiom to be replaced is going to be given as a `kername`, like those
collected by `assumptions`.
You don't actually have to verify that the constant is indeed an axiom.
Hint: You will need `eq_constant`.
|*)
Definition instantiate_axiom (ax : kername) (prf : term) : term -> term :=
REPLACE_ME.
Axiom mystery : nat.
Definition what :=
mystery * 3.
(*|
.. raw:: html
Exercise: Removing axioms (advanced)
..
|*)
(*|
A slightly harder version would be to turn a definition using axioms to one
assuming these axioms with an implication.
For instance, for the `foo_ax` defined above which uses `funext`, we would
expect something of the following type:
`(forall A B (f g : A -> B), (forall x, f x = g x) -> f = g) -> (fun n => n + 0) = (fun n => n)`
Hint: You can use `assumptions` and `lookup_constant` to get the type of a
constant, and `lift0 1 t` to weaken `t` by adding one new variable in the
context.
You can also use a variant of `transform` called `transform_nb` which also
tracks the number of introduced variables (to know how much to lift by).
|*)
Definition unaxiom (p : global_env * term) : term :=
REPLACE_ME.
Axiom unkown : bool.
Axiom random : nat -> nat.
Definition test f :=
if unkown then what else random (f 9).
(*|
.. raw:: html