lesson4_part4.v

Authors:

Yannick Forster

Théo Winterhalter

Files:

Display all goals and responses

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 "tm_foo" nat ;;
  tmDefinition "tm_bar" (t + t + 2)
).tm_foo has type-checked, generating 1 obligation
Solving obligations automatically...
1 obligation remaining
Obligation 1 of tm_foo: nat.

Next Obligation.nat

This is how we prove a tmLemma

  exact 12.
Defined.No more obligations remaining

After we prove tm_foo, the program continues and defines tm_bar.

Print tm_bar.tm_bar = tm_foo + tm_foo + 2
     : nat

tm_foo + tm_foo + 2

MetaRocq Run (
  t <- tmLemma "baz" nat ;;
  st <- tmEval all t ;;
  tmDefinition "simpl_baz" st
).baz has type-checked, generating 1 obligation
Solving obligations automatically...
1 obligation remaining
Obligation 1 of baz: nat.

Next Obligation.nat
  exact (10 + 2).
Defined.No more obligations remaining

Print simpl_baz.simpl_baz = 12
     : nat

Exercise: Deriving (hard)

We promised MetaRocq could be used to derive automatically certain things. Let's see how this can be done by automatically deriving update functions for a record.

We assume that there is no dependency between the fields, otherwise it's unclear what an update function should do.

This exercise is hard, so it makes sense to make some assumptions first such as the absence of parameters (like in triple below) or of local definitions (like in trap below). Don't hesitate to ask questions if you are stuck.

We'll start with a few record definitions, together with one example of an update function, don't hesitate to write your own and quote them to understand what you need to write.

Record point3D := {
  px : nat ;
  py : nat ;
  pz : nat
}.

Record Zalt := {
  num : nat ;
  positive : bool
}.

Record triple A B C := {
  p1 : A ;
  p2 : B ;
  p3 : C
}.

Record trap := {
  v1 : nat ;
  v2 := 10 ^ v1 ;
  v3 : nat
}.

We write an update for num by hand.

Definition upd_num (f : nat -> nat) (x : Zalt) :=
  match x with
  | Build_Zalt num positive => Build_Zalt (f num) positive
  end.

Now we can look at how it is quoted.

We use $Quote rather than $quote to unfold the constant upd_num when quoting it. Otherwise we would get some tConst which is not as informative.

Definition q_upd_num := $Quote upd_num.
Print q_upd_num.q_upd_num =
tLam "f"
  (tProd {| binder_name := nAnon; binder_relevance := Relevant |}
     (tInd
        {|
          inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat");
          inductive_ind := 0
        |} [])
     (tInd
        {|
          inductive_mind := (MPfile ["Datatypes"; "Init"; "Corelib"], "nat");
          inductive_ind := 0
        |} []))
  (tLam "x"
     (tInd
        {|
          inductive_mind := (MPfile ["lesson4_part4"], "Zalt");
          inductive_ind := 0
        |} [])
     (tCase
        {|
          ci_ind :=
            {|
              inductive_mind := (MPfile ["lesson4_part4"], "Zalt");
              inductive_ind := 0
            |};
          ci_npar := 0;
          ci_relevance := Relevant
        |}
        {|
          puinst := [];
          pparams := [];
          pcontext :=
            [{| binder_name := nNamed "x"; binder_relevance := Relevant |}];
          preturn :=
            tInd
              {|
                inductive_mind := (MPfile ["lesson4_part4"], "Zalt");
                inductive_ind := 0
              |} []
        |} (tRel 0)
        [{|
           bcontext :=
             [{|
                binder_name := nNamed "positive";
                binder_relevance := Relevant
              |};
              {| binder_name := nNamed "num"; binder_relevance := Relevant |}];
           bbody :=
             tApp
               (tConstruct
                  {|
                    inductive_mind := (MPfile ["lesson4_part4"], "Zalt");
                    inductive_ind := 0
                  |} 0 [])
               [tApp (tRel 3) [tRel 1]; tRel 0]
         |}]))
     : term

Below is a meta-program that gives you the definition of an inductive.

Hint: It may be useful to you later, perhaps no as-is, but with some modification to also get the argument of tInd.

Definition get_inductive {A} (ind : A) :=
  t <- tmQuote ind ;;
  match t with
  | tInd ind _ =>
    let kn := ind.(inductive_mind) in
    tmQuoteInductive kn
  | _ => tmFail "Not an inductive type"
  end.

We use it like this to define Zalt_def to inspect at our leisure.

MetaRocq Run (
  mib <- get_inductive Zalt ;;
  tmDefinition "Zalt_def" mib
).

This now contains the definition of Zalt.

You may compare the information you see in here with what appeared in q_upd_num. It might be useful to copy paste them to better compare.

Print Zalt_def.Zalt_def =
{|
  ind_finite := BiFinite;
  ind_npars := 0;
  ind_params := [];
  ind_bodies :=
    [{|
       ind_name := "Zalt";
       ind_indices := [];
       ind_sort := sType (Universe.make' Level.lzero);
       ind_type := tSort (sType (Universe.make' Level.lzero));
       ind_kelim := IntoAny;
       ind_ctors :=
         [{|
            cstr_name := "Build_Zalt";
            cstr_args :=
              [{|
                 decl_name :=
                   {|
                     binder_name := nNamed "positive";
                     binder_relevance := Relevant
                   |};
                 decl_body := None;
                 decl_type :=
                   tInd
                     {|
                       inductive_mind :=
                         (MPfile ["Datatypes"; "Init"; "Corelib"], "bool");
                       inductive_ind := 0
                     |} []
               |};
               {|
                 decl_name :=
                   {|
                     binder_name := nNamed "num";
                     binder_relevance := Relevant
                   |};
                 decl_body := None;
                 decl_type :=
                   tInd
                     {|
                       inductive_mind :=
                         (MPfile ["Datatypes"; "Init"; "Corelib"], "nat");
                       inductive_ind := 0
                     |} []
               |}];
            cstr_indices := [];
            cstr_type :=
              tPro "num"
                (tInd
                   {|
                     inductive_mind :=
                       (MPfile ["Datatypes"; "Init"; "Corelib"], "nat");
                     inductive_ind := 0
                   |} [])
                (tPro "positive"
                   (tInd
                      {|
                        inductive_mind :=
                          (MPfile ["Datatypes"; "Init"; "Corelib"], "bool");
                        inductive_ind := 0
                      |} [])
                   (tRel 2));
            cstr_arity := 2
          |}];
       ind_projs := [];
       ind_relevance := Relevant
     |}];
  ind_universes := Monomorphic_ctx;
  ind_variance := None
|}
     : mutual_inductive_body

To help you build the derive_updates meta-program, we'll give you some useful tools.

Also check out the following useful constructs:

tmMkDefinition takes a string and a term and produces a definition using that name (if fresh, otherwise it fails) and unquoting the given term.
tmFreshName takes a string and will return a new string that is fresh in the current environment, based on the given one (typically by adding a number at the end).

If you plan to handle parameters:

it_mkLambda_or_LetIn takes c : context and t : term and produces a new λ-abstraction with body t and quantifying over c. Basically it does the right thing by inserting as many tLam as necessary.
subst l 0 t will substitute the variables of t using the terms provided in l. For this exercise, you can provide garbage (just some random tRel k will suffice), what matters is the number of terms you provide. Providing 3 will reduce tRel 5 to tRel 2.

Handy concatenation notation.

Notation "a # b" := (String.append a b).Notation "_ # _" was already used. [notation-overridden,parsing,default]

To debug we recommend you use the following in place of tmMkDefinition

Definition tmDebugDefinition na (t : term) :=
  t <- tmEval all t ;;
  tmDefinition na t.

mkr 3 2 will produce [ tRel 4 ; tRel 3 ; tRel 2 ]

Fixpoint mkr i off :=
  match i with
  | 0 => []
  | S i => tRel (off + i) :: mkr i off
  end.

Extract the name from aname or use d as default.

Definition get_name (a : aname) d :=
  match a.(binder_name) with
  | nNamed na => na
  | nAnon => d
  end.

Definition derive_updates {A} (ind : A) : TemplateMonad unit :=
  REPLACE_ME.

Tip

Use the same as derive_updates with tmDebugDefinition instead of tmMkDefinition. It will help debug because I don't expect the error messages to be very useful.

Definition debug_derive_updates {A} (ind : A) : TemplateMonad unit :=
  REPLACE_ME.

Below, one of them should always fail.

Fail MetaRocq Run (derive_updates nat).The command has indeed failed with message:
Invalid argument or not yet implemented. The argument must be a TemplateProgram: @REPLACE_ME

Test that it works. If you manage to execute those lines, it's very likely that it does, but better safe than sorry.

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.envb: nat -> bool
env: nat -> Prop
s: form
(forall n : nat, env n <-> envb n = true) ->
reflect env s <-> decider envb s = true
Proof.envb: nat -> bool
env: nat -> Prop
s: form
(forall n : nat, env n <-> envb n = true) ->
reflect env s <-> decider envb s = true
  intros Henv.envb: nat -> bool
env: nat -> Prop
s: form
Henv: forall n : nat, env n <-> envb n = true
reflect env s <-> decider envb s = true
  induction s; cbn.envb: nat -> bool
env: nat -> Prop
x: nat
Henv: forall n : nat, env n <-> envb n = true
env x <-> envb x = true
envb: nat -> bool
env: nat -> Prop
Henv: forall n : nat, env n <-> envb n = true
True <-> true = true
envb: nat -> bool
env: nat -> Prop
Henv: forall n : nat, env n <-> envb n = true
False <-> false = true
envb: nat -> bool
env: nat -> Prop
s1, s2: form
Henv: forall n : nat, env n <-> envb n = true
IHs1: reflect env s1 <-> decider envb s1 = true
IHs2: reflect env s2 <-> decider envb s2 = true
(reflect env s1 -> reflect env s2) <->
(if decider envb s1 then decider envb s2 else true) = true
envb: nat -> bool
env: nat -> Prop
s1, s2: form
Henv: forall n : nat, env n <-> envb n = true
IHs1: reflect env s1 <-> decider envb s1 = true
IHs2: reflect env s2 <-> decider envb s2 = true
reflect env s1 /\ reflect env s2 <->
decider envb s1 && decider envb s2 = true
envb: nat -> bool
env: nat -> Prop
s1, s2: form
Henv: forall n : nat, env n <-> envb n = true
IHs1: reflect env s1 <-> decider envb s1 = true
IHs2: reflect env s2 <-> decider envb s2 = true
reflect env s1 \/ reflect env s2 <->
decider envb s1 || decider envb s2 = true
  all: try now firstorder congruence.envb: nat -> bool
env: nat -> Prop
s1, s2: form
Henv: forall n : nat, env n <-> envb n = true
IHs1: reflect env s1 <-> decider envb s1 = true
IHs2: reflect env s2 <-> decider envb s2 = true
(reflect env s1 -> reflect env s2) <->
(if decider envb s1 then decider envb s2 else true) = true
envb: nat -> bool
env: nat -> Prop
s1, s2: form
Henv: forall n : nat, env n <-> envb n = true
IHs1: reflect env s1 <-> decider envb s1 = true
IHs2: reflect env s2 <-> decider envb s2 = true
reflect env s1 /\ reflect env s2 <->
decider envb s1 && decider envb s2 = true
envb: nat -> bool
env: nat -> Prop
s1, s2: form
Henv: forall n : nat, env n <-> envb n = true
IHs1: reflect env s1 <-> decider envb s1 = true
IHs2: reflect env s2 <-> decider envb s2 = true
reflect env s1 \/ reflect env s2 <->
decider envb s1 || decider envb s2 = true
  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.Notation "_ == _" was already used. [notation-overridden,parsing,default]

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
        (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
        (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
        (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.env: nat -> Prop
s: form
decider (fun n : nat => if dec (env n) then true else false) s ->
reflect env s
Proof.env: nat -> Prop
s: form
decider (fun n : nat => if dec (env n) then true else false) s ->
reflect env s
  intros H.env: nat -> Prop
s: form
H: decider (fun n : nat => if dec (env n) then true else false) s
reflect env s
  eapply decider_iff.env: nat -> Prop
s: form
H: decider (fun n : nat => if dec (env n) then true else false) s
forall n : nat, env n <-> ?envb n = true
env: nat -> Prop
s: form
H: decider (fun n : nat => if dec (env n) then true else false) s
decider ?envb s = true
  2: eassumption.env: nat -> Prop
s: form
H: decider (fun n : nat => if dec (env n) then true else false) s
forall n : nat,
env n <-> (fun n0 : nat => if dec (env n0) then true else false) n = true
  cbn.env: nat -> Prop
s: form
H: decider (fun n : nat => if dec (env n) then true else false) s
forall n : nat, env n <-> (if dec (env n) then true else false) = true intros n.env: nat -> Prop
s: form
H: decider (fun n : nat => if dec (env n) then true else false) s
n: nat
env n <-> (if dec (env n) then true else false) = true 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.forall A B : Prop, A -> B -> A
Proof.forall A B : Prop, A -> B -> A
  cauto.
Qed.

Goal forall A B C : Prop, ~ A \/ ~ B \/ (C /\ True) <-> ~ (A /\ B /\ ~ C).forall A B C : Prop, ~ A \/ ~ B \/ C /\ True <-> ~ (A /\ B /\ ~ C)
Proof.forall A B C : Prop, ~ A \/ ~ B \/ C /\ True <-> ~ (A /\ B /\ ~ C)
  cauto.
Qed.

Note that the tactic nicely generates counterexamples if it does not work:

Goal forall A B : Prop, A -> B.forall A B : Prop, A -> B
Proof.forall A B : Prop, A -> B
  cauto.A, B: Prop
a: A
n: ~ B
false
Abort.