# Smart Matches

**URL:** <https://discourse.rocq-prover.org/t/smart-matches/1106>\
**Category:** Using Rocq\
**Created:** [November 7, 2020, 11:31am UTC](https://discourse.rocq-prover.org/t/smart-matches/1106 "2020-11-07T11:31:49Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![gert-smolka](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/gert-smolka/32/20_2.png) [@gert-smolka](https://discourse.rocq-prover.org/u/gert-smolka)\
**Post date:** [November 7, 2020, 11:31am UTC](https://discourse.rocq-prover.org/t/smart-matches/1106/1 "2020-11-07T11:31:49Z")

</div>

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?

```auto
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.

```

---

<div class="post-metadata">

**Author:** ![JasonGross](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jasongross/32/32_2.png) [@JasonGross](https://discourse.rocq-prover.org/u/JasonGross)\
**Post date:** [November 8, 2020, 8:02pm UTC](https://discourse.rocq-prover.org/t/smart-matches/1106/2 "2020-11-08T20:02:23Z")

</div>

I’m not sure when it first appeared, but the publication on this is called “Proof Trick: Small Inversions” and is available [here](https://hal.inria.fr/inria-00489412/en/). I’ve just opened [a new issue to document this feature](https://github.com/coq/coq/issues/13323), btw.

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [November 12, 2020, 6:40pm UTC](https://discourse.rocq-prover.org/t/smart-matches/1106/3 "2020-11-12T18:40:35Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![gert-smolka](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/gert-smolka/32/20_2.png) [@gert-smolka](https://discourse.rocq-prover.org/u/gert-smolka)\
**Post date:** [November 12, 2020, 7:12pm UTC](https://discourse.rocq-prover.org/t/smart-matches/1106/4 "2020-11-12T19:12:06Z")

</div>

I can confirm that the mentioned [paper by Monien](https://hal.inria.fr/inria-00489412/en/) discusses the technique that is used by Coq to compile away smart matches.