## Stream: Coq users

### Topic: Beginner question: dependent pattern matching

#### k32 (Jun 15 2020 at 19:58):

Hello. I am struggling with dependent pattern matching in this situation (synthetic example):

``````  Record foo := mkFoo
{ foo1 : nat;
foo2 : (fun x => match x with
| 0 => nat
| _ => bool
end) foo1
}.

Goal forall a b c d, mkFoo a b = mkFoo c d -> False.
intros.
inversion H.
subst.
assert (b = d).
``````

Is there a tactic to prove (b = d)?

#### Théo Winterhalter (Jun 15 2020 at 20:13):

This is probably going to be a complicated proof (`b = d`). You probably will have to rely on UIP (or its proof in your particular case), though it may be the case that I'm missing something. In any case, your whole lemma is wrong but I assume that is just for the sake of the example.

#### Jakob Botsch Nielsen (Jun 15 2020 at 20:15):

With Equations and some dependent eliminations it is provable without axioms:

``````Derive NoConfusionHom for foo.
Goal forall a b c d, mkFoo a b = mkFoo c d -> False.
intros.
inversion H.
subst.
assert (b = d).
{ destruct c.
- now depelim H2.
- depelim H2.
cbn.
now destruct H0. }
``````

There is probably a more straightforward way :smile:

#### k32 (Jun 15 2020 at 20:17):

Yes, please don't mind the top goal (`False`). It was a bit cumbersome to write down type of `b = d` before `subst`.

#### Théo Winterhalter (Jun 15 2020 at 20:31):

Yes, I did not mean with the UIP axiom but its proof. And here, the complicated proof is done by `Derive NoConfusion`.

#### k32 (Jun 15 2020 at 21:46):

Ok, that did work for the synthetic example, but not in a general case :

``````Record foo {f : nat -> Type} :=
mkFoo
{ foo1 : nat;
foo2 : f foo1
}.
``````

#### Théo Winterhalter (Jun 15 2020 at 21:47):

This time I fear it is more complicated, and maybe not provable without UIP?

#### Gaëtan Gilbert (Jun 15 2020 at 21:47):

Jakob Botsch Nielsen said:

With Equations and some dependent eliminations it is provable without axioms:

``````Derive NoConfusionHom for foo.
Goal forall a b c d, mkFoo a b = mkFoo c d -> False.
intros.
inversion H.
subst.
assert (b = d).
{ destruct c.
- now depelim H2.
- depelim H2.
cbn.
now destruct H0. }
``````

There is probably a more straightforward way :smile:

Why do you need to `destruct c`?

#### k32 (Jun 15 2020 at 21:50):

...in the worst case I can make a tactic to solve this for any particular `f`, I guess...

#### Kenji Maillard (Jun 15 2020 at 22:26):

Using UIP (some version can be found in `Coq.Logic.Eqdep_dec`) you can sort it out at least:

``````From Equations Require Import Equations.
From Coq Require Import Logic.Eqdep_dec.

Record foo {f : nat -> Type} :=
mkFoo
{ foo1 : nat;
foo2 : f foo1
}.
Derive NoConfusionHom for foo.

Goal forall f a (b : f a) c (d : f c), mkFoo f a b = mkFoo f c d -> True.
intros.
inversion H.
subst.
assert (b = d).
{  destruct c.
- now depelim H2.
- depelim H2.
now rewrite (UIP_refl_nat (S c) _). } (* changes the proof of S c = S c in the goal by eq_refl  ultimately using the decidability of equality on nat *)
``````

#### Kenji Maillard (Jun 15 2020 at 22:47):

Even though tbh I think the following is more useful in general

``````From Equations Require Import Equations.

Record foo {f : nat -> Type} :=
mkFoo
{ foo1 : nat;
foo2 : f foo1
}.
Derive NoConfusionHom for foo.

Definition transp {A} {B : A-> Type} {x y : A} (e : x = y) : B x -> B y :=
fun bx => eq_rect x B bx y e.

Definition ap {A B} (f : A -> B) {x y : A} : x = y -> f x = f y.
Proof. now intros ->. Defined.

Goal forall f a (b : f a) c (d : f c)
(H : mkFoo f a b = mkFoo f c d),
transp (ap foo1 H) b = d.
Proof.
intros. depelim H. reflexivity.
Defined.
``````

#### k32 (Jun 15 2020 at 22:50):

Thanks everyone for the input!

#### Cyril Cohen (Jun 16 2020 at 00:06):

Note that what creates the need for UIP is the start of your script @k32 indeed, in

`````` intros.
inversion H.
``````

the tactic `inversion` does a reeeealy bad job: it generates an equality `e1 : a = b` on the first components as expected, but since it does not know how to deal with dependent pairs, the second components are repackaged and equated as an equality between generic Coq sigma types, inside which there is a second equality `e2 : a = b`, still on the first components, which is thus the one that must be used to equate the second components via a transport (as noted by @Kenji Maillard ).
However in the absence of UIP, `e2` would have no reason to be the same as `e1`. Luckly, in your example UIP holds on `nat` and you do not need an axiom to show in fact `e1 = e2` and move forward. BTW, @Kenji Maillard script does not start with inversion and thus should not require UIP in any way.

Here, is another axiom-free, UIP-free example using the lower level ssreflect dependent elimination tactic `case: _ /`:

``````Require Import ssreflect ssrfun.

Section example.
Context {X : Type} (* does not need to be nat *) (f : X -> Type).

Record foo := mkFoo { foo1 : X; foo2 : f foo1 }.

Lemma dual_elim (P : forall a, f a -> Prop) a (b : f a) c (d : f c) :
mkFoo a b = mkFoo c d -> P a b -> P c d.
Proof.
by rewrite -[d]/(foo2 (mkFoo c d)) -[c]/(foo1 (mkFoo c d)); case: _ /.
Qed.

End example.
``````

It shows an equality of `foo`s allows for the simultenaous subsitution of its components in a Curryfied predicate, which I believe was the intention of the original post (which used to proceed components by components instead of simultaneously, which was the cause of the problem).

#### Cyril Cohen (Jun 16 2020 at 09:04):

Note also that the transport theorem is a consequence of the dependent elimination `foo_eq_rect`:

``````Require Import ssreflect ssrfun.

Section example.
Context {X : Type} (* does not need to be nat *) (f : X -> Type).

Record foo := mkFoo { foo1 : X; foo2 : f foo1 }.

Lemma foo_eq_rect
(P : forall a (b : f a) c (d : f c), mkFoo a b = mkFoo c d -> Prop)
a (b : f a) c (d : f c) (e : mkFoo a b = mkFoo c d) :
P a b a b erefl -> P a b c d e.
Proof.
pose Q ab cd := match ab, cd with mkFoo a b, mkFoo c d => P a b c d end.
by move=> Prefl; have: Q (mkFoo a b) (mkFoo c d) e by case: _ / e.
Qed.

Lemma cast_foo a (b : f a) c (d : f c) (e : mkFoo a b = mkFoo c d) :
ecast c (f c) (congr1 foo1 e) b = d.
Proof. by elim/foo_eq_rect : e. Qed.

End example.
``````

#### Karl Palmskog (Jun 16 2020 at 09:22):

whoa, really useful stuff here, please consider posting the different solutions in the Discourse (since our Zulip is still completely opaque to general public)

#### Jakob Botsch Nielsen (Jun 16 2020 at 13:07):

Gaëtan Gilbert said:

Jakob Botsch Nielsen said:

With Equations and some dependent eliminations it is provable without axioms:

``````Derive NoConfusionHom for foo.
Goal forall a b c d, mkFoo a b = mkFoo c d -> False.
intros.
inversion H.
subst.
assert (b = d).
{ destruct c.
- now depelim H2.
- depelim H2.
cbn.
now destruct H0. }
``````

There is probably a more straightforward way :smile:

Why do you need to `destruct c`?

Otherwise it seems `depelim` does not manage to simplify anything, it produces just another equality between sigmas.

#### Anton Trunov (Jun 16 2020 at 18:24):

Looks like in this case writing down a proof term explicitly might be a bit more intuitive (YMMV):

``````Section example.
Context {X : Type} (f : X -> Type).

Record foo := mkFoo { foo1 : X; foo2 : f foo1 }.

Definition dual_elim (P : forall a, f a -> Prop) a (b : f a) c (d : f c) :
mkFoo a b = mkFoo c d -> P a b -> P c d
:=
fun (e : mkFoo a b = mkFoo c d) =>
match
e in (_ = mkFoocd)
return match mkFoocd with
| mkFoo u v => P a b -> P u v
end
with
| eq_refl => fun pab => pab
end.

End example.
``````

#### Anton Trunov (Jun 16 2020 at 18:25):

Especially, provided Coq can infer some parts of that pattern-matching above and let us write simply:

``````Section example.
Context {X : Type} (f : X -> Type).

Record foo := mkFoo { foo1 : X; foo2 : f foo1 }.

Definition dual_elim (P : forall a, f a -> Prop) a (b : f a) c (d : f c) :
mkFoo a b = mkFoo c d -> P a b -> P c d
:=
fun (e : mkFoo a b = mkFoo c d) =>
match e in (_ = mkFoo u v) return (P a b -> P u v) with
| eq_refl => fun pab => pab
end.

End example.
``````

Last updated: Jan 28 2023 at 06:30 UTC