PRFA.live_coding6

Live coding session for the sixth lecture of MPRI PRFA (2-7-2)

The subject this time is meta-programming in Coq. Meta-programming is the activity of writing programs that manipulate and produce programs.

You have actually been using meta-programming all this time, because tactics are a form of meta-program if you see proof terms as programs.

In Coq itself, there are many options to meta-program. The most basic is called Ltac and it's the tactic language you have been writing your proofs in. We will also see MetaCoq which allows you to write meta-programs in the same language as Coq.

Other options include Ltac2, Mtac, and Coq-ELPI.

Set Default Goal Selector "!".

Ltac

Semicolon ; is a bit more complicated than just sequential composition.

First, t1 ; t2 applies t2 to all subgoals generated by t1. So split ; constructor will solve the goal nat × nat.

QUESTION: Do you know what it will produce as a witness of nat × nat?

Second, Ltac bakes in backtracking: each tactic can have several successes. For instance the constructor tactic has a success for each constructor that matches the goal.

Goal bool.
Proof.
  constructor.
  Show Proof. (* It picks true *)
Qed.

Goal ∃ (b : bool ), b = false.
Proof.
  (* unshelve eexists lets us give the witness first *)
  unshelve eexists.
  - constructor.
  - (* We're stuck now *)
    Fail constructor.
Restart.
  unshelve eexists ; constructor.
  Show Proof.
  (* This time it picked false! *)
  (* Actually, it first picked true, but then constructor failed to
    prove true = false. So it went back and picked another success for
    the goal bool, namely false.
  *)
  (* This might also be a surprise but constructor can be used to prove
    x = x, just like reflexivity. We'll see more about that next week.
  *)
Restart.
  (* constructor doesn't work for ∃ because it can't guess the
    witness, but we can use econstructor instead to generate an existential
    variable to be filled later. When doing this, we can prove the goal with
    just a succession of econstructor.

    As before I use unshelve to make sure it asks us to also give the witness.
  *)
  unshelve econstructor ; econstructor.
Qed.

Tacticals

We will now give you a list of useufl *taticals*, that is tactics that take tactics as arguments.

Applying different tactics to different subgoals

Inductive mult4 : nat → Prop :=
| mult4_0 : mult4 0
| mult4_plus n : mult4 n → mult4 (4 + n).

Inductive not_mult4 : nat → Prop :=
| not_mult4_1 : not_mult4 1
| not_mult4_2 : not_mult4 2
| not_mult4_3 : not_mult4 3
| not_mult4_plus n : not_mult4 n → not_mult4 (4 + n).

Goal ∀ n , mult4 n → not_mult4 n → False.
Proof.
  intros n h hn. induction hn.
  - inversion h.
  - inversion h.
  - inversion h.
  - inversion h. subst. auto.
Restart.
  (* We are not doing the same in all branches so we can't just use ; *)
  (* But we can do the following. *)
  intros n h hn.
  induction hn ; [ inversion h | inversion h | inversion h | inversion h ; subst ; auto ].
Restart.
  (* In fact we can even factorise the three first cases *)
  intros n h hn.
  induction hn ; [ inversion h .. | inversion h ; subst ; auto ].
  (* The elipsis represented by .. can be used at most once, and repeats
    the preceding tactic.
  *)
Restart.
  intros n h hn.
  (* We can put it in the middle for instance *)
  induction hn ; [ inversion h | idtac .. | inversion h ; subst ; auto ].
  (* Here I used idtac which is the tactic that does nothing so the two
    middle goals are still unsolved. *)
Restart.
  (* In fact idtac can even be left out *)
  intros n h hn.
  induction hn ; [ inversion h | .. ].
Restart.
  (* We can also use try to perform a tactic only if it succeeds *)
  intros n h hn.
  try intros x. (* It does nothing because it failed. *)
  induction hn.
  (* We can combine it with solve to make sure we only use inversion
    if it solves the goal.
  *)
  all: try solve [ inversion h ].
Abort.

Repeating

You can also repeat a certain tactic a number of times using do or repeat. Note that repeat may repeat the tactic 0 times without failing. So if t fails, repeat t will still succeed.

Goal mult4 40.
Proof.
  apply mult4_plus.
  apply mult4_plus.
  apply mult4_plus.
  apply mult4_plus.
  (* No way we're doing this forever *)
  repeat apply mult4_plus.
  apply mult4_0.
Restart.
  do 8 (apply mult4_plus).
  do 2 (apply mult4_plus).
Restart.
  repeat constructor.
Qed.

There is more of course, but we'll let you discover them on your own. Typically when you will need them. For this you can of course ask questions, but you can also look at the tactic index: https://coq.inria.fr/doc/V8.18.0/refman/coq-tacindex.html

Case analysis on the goal

In Ltac you also have access to the goal and you can examine its shape or that of the hypotheses, which can be very useful to build your own custom tactics.

Goal nat × bool × unit.
Proof.
  match goal with
  | |- ?A × ?B ⇒ pose (A' := A) ; pose (B' := B)
  end.
  (* Note we use question marks to talk about unification variables.
    This is slightly different from Coq's usual pattern matching.
    Also remark that we are matching on a type here! *)

  (* match goal backtracks when the tactic inside fails *)
  match goal with
  | |- ?A × ?B ⇒ fail (* The ideal tactic to fail *)
  | |- ?A × ?B × ?C ⇒ pose (A'' := A)
  end.

  (* lazymatch goal doesn't backtrack in the branches *)
  Fail lazymatch goal with
  | |- ?A × ?B ⇒ fail "This is expected this time" (* We give a custom error *)
  | |- ?A × ?B × ?C ⇒ pose (B'' := B)
  end.

  (* I recommend this, unless you really want backtracking! *)

  (* It also fails when none of the branches match *)
  Fail lazymatch goal with
  | |- nat ⇒ idtac
  end.

  (* We can use this to fill automatically the goal *)

  repeat lazymatch goal with
  | |- ?A × ?B ⇒ split
  | |- nat ⇒ exact 13
  | |- bool ⇒ exact false
  | |- unit ⇒ exact tt
  end.
  Show Proof.
Qed.

The repeat match basically implements some variant of auto.

We can also define tactics at top level so we can use them many times.

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.

Lemma test : ∀ (A B : Prop), (A → B ) → A ∧ B.
Proof.
  intros. (* No need to specify the names we won't be using them. *)
  split_or_apply.
  - Fail split_or_apply.
    admit.
  - split_or_apply.
Restart.
  intros.
  change (id (A ∧ B)). repeat split_or_apply.
  (* It only works syntactically! *)
  unfold id. change B with (id B).
  repeat split_or_apply. (* Except when it tries to unify things. *)
Abort.

MetaCoq

MetaCoq can do things which are unattainable in Ltac, for instance you can use it to write your own Derive mechanics.

MetaCoq is also an exciting project in which the meta-theory of Coq is studied including verification of a type checker for Coq written in Coq, and verified extraction. Ask us if you want to know more!

We'll go step by step.

First you need to use make to build MetaCoqPrelude and make sure you open VSCoq with the _CoqProject at its root.

From PRFA Require Import MetaCoqPrelude.

MetaCoq has an representation of Coq terms as an inductive types:

Print term.

No need to understand it all, but you can see how the syntax of Coq is encoded. It is actually almost in one-to-one correspondance with the OCaml implementation.

Quoting

The power of MetaCoq is it allows you to go back and forth between this term representation and actual Coq terms.

We talk about quoting for the action going from actual Coq definitions to their MetaCoq 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
  ).

Some explanation is perhaps necessary.

transform takes a function that will tell what to do to 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 MetaCoq

Finally, MetaCoq also contains a representation of Coq vernacular commands like Definition, Print, Locate, which can be useful to write more complex meta-programs.

MetaCoq 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 *)

MetaCoq Run (
  t <- tmLemma "baz" nat ;;
  st <- tmEval all t ;;
  tmDefinition "simpl_baz" st
).
Next Obligation.
  exact (10 + 2).
Defined.

Print simpl_baz.