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)?

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.

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:

Yes, please don't mind the top goal (`False`

). It was a bit cumbersome to write down type of `b = d`

before `subst`

.

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

.

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

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

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`

?

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

, I guess...

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 *)
```

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

Thanks everyone for the input!

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).

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

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

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.

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

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: Jun 15 2024 at 05:01 UTC