Meta-programming

Authors:

Yannick Forster

Théo Winterhalter

Files:

Display all goals and responses

The subject this time is meta-programming in Rocq. 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 Rocq 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 MetaRocq which allows you to write meta-programs in the same language as Rocq.

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

Set Default Goal Selector "!".

Sequencing and backtracking

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.bool
Proof.bool
  constructor.
  Show Proof.true

It picks true

Qed.

Goal exists (b : bool), b = false.exists b : bool, b = false
Proof.exists b : bool, b = false

unshelve eexists lets us give the witness first

  unshelve eexists.bool
?b = false
  -bool constructor.
  -true = false

We're stuck now

    Fail constructor.The command has indeed failed with message:
Unable to unify "false" with "true".
true = false
Abort.
Goal exists (b : bool), b = false.exists b : bool, b = false
Proof.exists b : bool, b = false
  unshelve eexists ; constructor.
  Show Proof.(ex_intro (fun b : bool => b = false) false eq_refl)

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.

Abort.
Goal exists (b : bool), b = false.exists b : bool, b = false
Proof.exists b : bool, b = false

constructor doesn't work for exists 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.

Exercise: Backtracking

For each of the following scripts, predict without running Rocq whether it succeeds, and which goal remains or which witness is chosen. Then check your answer, using Show Proof to see the witness.

The try are only there so that the file compiles whatever the answer.

Goal exists (b : bool), negb b = true.exists b : bool, negb b = true
Proof.exists b : bool, negb b = true
  try (unshelve eexists ; constructor).
Abort.

Goal exists (n : nat), n = 1.exists n : nat, n = 1
Proof.exists n : nat, n = 1
  try (unshelve eexists ; constructor).
Abort.

Goal True \/ (False -> False).True \/ (False -> False)
Proof.True \/ (False -> False)
  try constructor ; intro x.x: False
False
Abort.

Goal True \/ (False -> False).True \/ (False -> False)
Proof.True \/ (False -> False)
  try constructor.True try intro x.True
Abort.

Goal (False -> False) \/ True.(False -> False) \/ True
Proof.(False -> False) \/ True
  try (constructor ; exact I).
Abort.

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 forall n, mult4 n -> not_mult4 n -> False.forall n : nat, mult4 n -> not_mult4 n -> False
Proof.forall n : nat, mult4 n -> not_mult4 n -> False
  intros n h hn.n: nat
h: mult4 n
hn: not_mult4 n
False induction hn.h: mult4 1
False
h: mult4 2
False
h: mult4 3
False
n: nat
h: mult4 (4 + n)
hn: not_mult4 n
IHhn: mult4 n -> False
False
  -h: mult4 1
False inversion h.
  -h: mult4 2
False inversion h.
  -h: mult4 3
False inversion h.
  -n: nat
h: mult4 (4 + n)
hn: not_mult4 n
IHhn: mult4 n -> False
False inversion h.n: nat
h: mult4 (4 + n)
hn: not_mult4 n
IHhn: mult4 n -> False
n0: nat
H0: mult4 n
H: n0 = n
False subst.n: nat
h: mult4 (4 + n)
hn: not_mult4 n
IHhn: mult4 n -> False
H0: mult4 n
False auto.
Abort.
Goal forall n, mult4 n -> not_mult4 n -> False.forall n : nat, mult4 n -> not_mult4 n -> False
Proof.forall n : nat, mult4 n -> not_mult4 n -> False

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.n: nat
h: mult4 n
hn: not_mult4 n
False
  induction hn ;
    [ inversion h
    | inversion h
    | inversion h
    | inversion h ; subst ; auto ].
Abort.
Goal forall n, mult4 n -> not_mult4 n -> False.forall n : nat, mult4 n -> not_mult4 n -> False
Proof.forall n : nat, mult4 n -> not_mult4 n -> False

In fact we can even factorise the three first cases

  intros n h hn.n: nat
h: mult4 n
hn: not_mult4 n
False
  induction hn ; [ inversion h .. | inversion h ; subst ; auto ].

The elipsis represented by .. can be used at most once, and repeats the preceding tactic.

Abort.
Goal forall n, mult4 n -> not_mult4 n -> False.forall n : nat, mult4 n -> not_mult4 n -> False
Proof.forall n : nat, mult4 n -> not_mult4 n -> False
  intros n h hn.n: nat
h: mult4 n
hn: not_mult4 n
False

We can put it in the middle for instance

  induction hn ;
    [ inversion h
    | idtac .. |
      inversion h ; subst ; auto ].h: mult4 2
False
h: mult4 3
False

Here I used idtac which is the tactic that does nothing so the two middle goals are still unsolved.

Abort.
Goal forall n, mult4 n -> not_mult4 n -> False.forall n : nat, mult4 n -> not_mult4 n -> False
Proof.forall n : nat, mult4 n -> not_mult4 n -> False

In fact idtac can even be left out

  intros n h hn.n: nat
h: mult4 n
hn: not_mult4 n
False
  induction hn ; [ inversion h | .. ].h: mult4 2
False
h: mult4 3
False
n: nat
h: mult4 (4 + n)
hn: not_mult4 n
IHhn: mult4 n -> False
False
Abort.
Goal forall n, mult4 n -> not_mult4 n -> False.forall n : nat, mult4 n -> not_mult4 n -> False
Proof.forall n : nat, mult4 n -> not_mult4 n -> False

We can also use try to perform a tactic only if it succeeds

  intros n h hn.n: nat
h: mult4 n
hn: not_mult4 n
False
  try intros x.n: nat
h: mult4 n
hn: not_mult4 n
False

It does nothing because it failed.

  induction hn.h: mult4 1
False
h: mult4 2
False
h: mult4 3
False
n: nat
h: mult4 (4 + n)
hn: not_mult4 n
IHhn: mult4 n -> False
False

We can combine it with solve to make sure we only use inversion if it solves the goal.

  all: try solve [ inversion h ].n: nat
h: mult4 (4 + n)
hn: not_mult4 n
IHhn: mult4 n -> False
False
Abort.

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.mult4 40
Proof.mult4 40
  apply mult4_plus.mult4 36
  apply mult4_plus.mult4 32
  apply mult4_plus.mult4 28
  apply mult4_plus.mult4 24

No way we're doing this forever

  repeat apply mult4_plus.mult4 0
  apply mult4_0.
Abort.
Goal mult4 40.mult4 40
Proof.mult4 40
  do 8 (apply mult4_plus).mult4 8
  do 2 (apply mult4_plus).mult4 0
Abort.
Goal mult4 40.mult4 40
Proof.mult4 40
  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://rocq-prover.org/doc/V9.0.0/refman/coq-tacindex.html

Exercise: Tacticals

Prove each of the following goals with a single sentence, that is one tactic expression ending with a single . after Proof.. Combine ;, [ ... | ... ], .., try, solve, repeat and do.

Goal mult4 12 /\ not_mult4 7 /\ mult4 0 /\ not_mult4 10.mult4 12 /\ not_mult4 7 /\ mult4 0 /\ not_mult4 10
Proof.mult4 12 /\ not_mult4 7 /\ mult4 0 /\ not_mult4 10
Admitted.

Goal forall n, not_mult4 n -> not_mult4 (8 + n).forall n : nat, not_mult4 n -> not_mult4 (8 + n)
Proof.forall n : nat, not_mult4 n -> not_mult4 (8 + n)
Admitted.

Goal forall n, n < 3 -> not_mult4 (n + 1).forall n : nat, n < 3 -> not_mult4 (n + 1)
Proof.forall n : nat, n < 3 -> not_mult4 (n + 1)
Admitted.

Goal forall n, mult4 n -> mult4 (n + 4).forall n : nat, mult4 n -> mult4 (n + 4)
Proof.forall n : nat, mult4 n -> mult4 (n + 4)
Admitted.

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.nat * bool * unit
Proof.nat * bool * unit
  match goal with
  | |- ?A * ?B => pose (A' := A) ; pose (B' := B)
  end.A':= (nat * bool)%type: Set
B':= unit: Set
nat * bool * unit

Note we use question marks to talk about unification variables. This is slightly different from Rocq'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.A':= (nat * bool)%type: Set
B':= unit: Set
A'':= nat: Set
nat * bool * unit

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.The command has indeed failed with message:
Tactic failure: This is expected this time.
A':= (nat * bool)%type: Set
B':= unit: Set
A'':= nat: Set
nat * bool * unit

I recommend this, unless you really want backtracking!

It also fails when none of the branches match

  Fail lazymatch goal with
  | |- nat => idtac
  end.The command has indeed failed with message:
No matching clauses for match.
A':= (nat * bool)%type: Set
B':= unit: Set
A'':= nat: Set
nat * bool * unit

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.(let A' := (nat * bool)%type in
 let B' := unit in let A'' := nat in (13, false, tt))
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 : forall (A B : Prop), (A -> B) -> A /\ B.forall A B : Prop, (A -> B) -> A /\ B
Proof.forall A B : Prop, (A -> B) -> A /\ B
  intros.A, B: Prop
H: A -> B
A /\ B

No need to specify the names we won't be using them.

  split_or_apply.A, B: Prop
H: A -> B
A
A, B: Prop
H: A -> B
B
  -A, B: Prop
H: A -> B
A Fail split_or_apply.The command has indeed failed with message:
No matching clauses for match.
A, B: Prop
H: A -> B
A
    admit.
  -A, B: Prop
H: A -> B
B split_or_apply.A, B: Prop
H: A -> B
A
Abort.
Lemma test : forall (A B : Prop), (A -> B) -> A /\ B.forall A B : Prop, (A -> B) -> A /\ B
Proof.forall A B : Prop, (A -> B) -> A /\ B
  intros.A, B: Prop
H: A -> B
A /\ B
  change (id (A /\ B)).A, B: Prop
H: A -> B
id (A /\ B) repeat split_or_apply.A, B: Prop
H: A -> B
id (A /\ B)

It only works syntactically!

  unfold id.A, B: Prop
H: A -> B
A /\ B change B with (id B).A, B: Prop
H: A -> B
A /\ id B
  repeat split_or_apply.A, B: Prop
H: A -> B
A
A, B: Prop
H: A -> B
A

Except when it tries to unify things.

Abort.

As a reminder, here is a tactic defined with match goal.

Ltac my_assumption :=
  match goal with
  | H : ?A |- ?A => apply H
  end.

Goal forall P Q R, P -> Q -> R -> P.forall P Q R : Type, P -> Q -> R -> P
Proof.forall P Q R : Type, P -> Q -> R -> P
  intros.P, Q, R: Type
X: P
X0: Q
X1: R
P
  my_assumption.
Qed.

Exercise: Repeated split

Define a tactic splits to perform split repeatedly on goals of the shape A * B but not on any other kinds of goals (for instance it should not solve True).

For instance, on (nat * bool) * (unit * bool) it should yield 4 subgoals.

Hint: You will need split and match goal or lazymatch goal and idtac.

Try it on these goals.

Goal nat * bool.nat * bool
Proof.nat * bool
Admitted.

Goal nat * (bool * unit) * (unit * nat * bool) * unit.nat * (bool * unit) * (unit * nat * bool) * unit
Proof.nat * (bool * unit) * (unit * nat * bool) * unit
Admitted.

The `clear` tactic

It is possible to forget about hypotheses using the clear tactic as follows.

It is sometimes useful before applying the induction tactic to get rid of something in the generated induction hypothesis.

Goal forall P Q R, P -> Q -> R -> P.forall P Q R : Type, P -> Q -> R -> P
Proof.forall P Q R : Type, P -> Q -> R -> P
  intros P Q R p q r.P, Q, R: Type
p: P
q: Q
r: R
P
  clear Q p q.P, R: Type
r: R
P
  Fail clear P. (* Cannot get rid of something used elsewhere. *)The command has indeed failed with message:
P is used in conclusion.
P, R: Type
r: R
P
  clear. (* Without arguments it clears everything it can *)P: Type
P
  exfalso.P: Type
False
  clear.False
Abort.

Exercise: Clearing before induction

Prove the following by induction on n. In particular, don't use lia, we want you to use the induction hypothesis.

Goal forall n, n mod 14 = 7 -> n - n = 0.forall n : nat, n mod 14 = 7 -> n - n = 0
Proof.forall n : nat, n mod 14 = 7 -> n - n = 0
Admitted.

Matching on the type of an expression

The same way we can match on the goal, we can match the type of an expression using the type of construct.

Ltac handle_hyp h :=
  lazymatch type of h with
  | (?A * ?B)%type => destruct h
  | nat => induction h
  | _ => idtac
  end.

Goal forall (n : nat * nat), fst n = snd n.forall n : nat * nat, fst n = snd n
Proof.forall n : nat * nat, fst n = snd n
  intro n.n: nat * nat
fst n = snd n
  handle_hyp n.n, n0: nat
fst (n, n0) = snd (n, n0)
  handle_hyp n.n0: nat
fst (0, n0) = snd (0, n0)
n, n0: nat
IHn: fst (n, n0) = snd (n, n0)
fst (S n, n0) = snd (S n, n0)
Abort.

The `fresh` tactic

Not all tactics operate on goals, some are used to produce values, or even names (as in variable names).

This is the case of the fresh tactic which you can use to get a fresh name (as in not used in the currrent context) to give to a newly introduced variable.

Goal forall n m k, n + m - k = m + n - k.forall n m k : nat, n + m - k = m + n - k
Proof.forall n m k : nat, n + m - k = m + n - k
  let N := fresh in
  intro N. (* Here it chooses [H], not very cool, we can guide naming a bit *)H: nat
forall m k : nat, H + m - k = m + H - k
  let N := fresh "n" in
  intro N. (* We suggested [n] and it stick with it. *)H, n: nat
forall k : nat, H + n - k = n + H - k
  let N := fresh "n" in
  intro N. (* This time, [n] was already taken, so it chose [n0] instead *)H, n, n0: nat
H + n - n0 = n + H - n0
  let na := fresh H in
  destruct H as [| na]. (* This time we suggested to use the name of [H] *)n, n0: nat
0 + n - n0 = n + 0 - n0
H0, n, n0: nat
S H0 + n - n0 = n + S H0 - n0
  (* It picked [H0] *)
Abort.

Exercise: Forward reasoning

A very useful tactic that should be part of the standard library, but is not, is the fwd tactic. Given H : P -> Q, fwd H will yield two goals:

one where P must be proven
and one where H has been replaced by H : Q

Note that there shouldn't be anything else appearing in the goal.

Try on the following goal. Do not use apply, only intros, fwd and assumption.

Goal forall P Q R, (P -> Q -> R) -> (P -> Q) -> P -> R.forall P Q R : Type, (P -> Q -> R) -> (P -> Q) -> P -> R
Proof.forall P Q R : Type, (P -> Q -> R) -> (P -> Q) -> P -> R
Admitted.

Exercise: Forward reasoning with a tactic (harder)

Try to generalise the code for fwd so that you can also provide a tactic. If H : P -> Q then forward_gen H tac will also apply tac to try and solve the goal P first.

Once forward_gen is defined, we define handy notations: Tactic Notation "forward" constr(H) := forward_gen H ltac:(idtac). and Tactic Notation "forward" constr(H) "by" tactic(tac) := forward_gen H tac.

Goal forall P Q R, (P -> Q -> R) -> (P -> Q) -> P -> R.forall P Q R : Type, (P -> Q -> R) -> (P -> Q) -> P -> R
Proof.forall P Q R : Type, (P -> Q -> R) -> (P -> Q) -> P -> R
Admitted.

Exercise: A tauto tactic

Write a tactic my_tauto that solves the following goals. You can start from the following, and expand it: Ltac my_tauto := lazymatch goal with | |- True => constructor end.

Section Tauto.

  Variables (P Q R : Prop).

  Goal P -> True /\ True.P, Q, R: Prop
P -> True /\ True
  Proof.P, Q, R: Prop
P -> True /\ True
  Admitted.

  Goal P -> P.P, Q, R: Prop
P -> P
  Proof.P, Q, R: Prop
P -> P
  Admitted.

  Goal P -> (P -> R) -> R.P, Q, R: Prop
P -> (P -> R) -> R
  Proof.P, Q, R: Prop
P -> (P -> R) -> R
  Admitted.

  Goal False \/ True.P, Q, R: Prop
False \/ True
  Proof.P, Q, R: Prop
False \/ True
  Admitted.

  Goal (P \/ Q \/ False) /\ (P -> Q) -> True /\ (R \/ Q).P, Q, R: Prop
(P \/ Q \/ False) /\ (P -> Q) -> True /\ (R \/ Q)
  Proof.P, Q, R: Prop
(P \/ Q \/ False) /\ (P -> Q) -> True /\ (R \/ Q)
  Admitted.

End Tauto.