MPRI PRFA — Proof Assistants

Meta-programming

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 "!".

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

It picks true

Qed.Unnamed_thm is defined

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.Unnamed_thm0 is defined

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).mult4 is defined
mult4_ind is defined
mult4_sind is defined

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).not_mult4 is defined
not_mult4_ind is defined
not_mult4_sind is defined

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.Unnamed_thm1 is defined

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

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.Unnamed_thm2 is defined

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.split_or_apply is defined

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.