Smart Matches

Using Coq
1

I’m a big fan of smart matches, they provide an elegant transparent abstraction layer for index-dependent plain matches. A nice example appears below.

In practice the dependent elimination tactic coming with the Equations package is convenient, but from the proof terms it generates the translation to index-dependent plain matches is not obvious.

I would guess smart matches appeared around 2013 with the new match compiler. What was the first Coq release they appeared in?

Inductive even: nat -> Type :=
| E1: even 0
| E2: forall n, even n -> even (S (S n)).

Lemma even_unique :
  forall n (a b : even n), a = b.
Proof.
  induction a; intros b.
  - refine (match b with E1 => _ end).
    reflexivity.
  - enough { b' | b = E2 n b' } as [b' ->].
    { f_equal. apply IHa. }
    refine (match b with E2 n' b' => _ end).
    exists b'. reflexivity.
Qed.
2

I’m not sure when it first appeared, but the publication on this is called “Proof Trick: Small Inversions” and is available here. I’ve just opened a new issue to document this feature, btw.

3

Isn’t that paper about a different way to implement inversion? The word “inference” does not appear there?

4

I can confirm that the mentioned paper by Monien discusses the technique that is used by Coq to compile away smart matches.