Hi, I am trying to finish the tuto on dependent matching https://github.com/coq/platform-docs/pull/9 and I am some trouble understanding the difference between NoConfusion and NoConfusionHom.

From what I understand, NoConfusion is basically checking that the head constructors are the same. For vec, it basically can be written as:

```
Definition NoConfusion_vec'
(A : Type)
(x : sigma (fun index : nat => vec A index))
(y : sigma (fun index : nat => vec A index)) : Prop :=
match pr2 x, pr2 y with
| vnil, vnil => True
| @vcons _ a n v, @vcons _ a' n' v' =>
let x : sigma (fun a : A => (sigma (fun index : nat => vec A index))) :=
{| pr1 := a; pr2 := {| pr1 := n; pr2 := v |} |} in
let y := {| pr1 := a'; pr2 := {| pr1 := n'; pr2 := v' |} |} in
x = y
| _, _ => False
end.
```

wheras NoConfusionHom seems to additionaly check as precondition that the indices are the same. I have some trouble writting sth that works but basically the printed term lloks like that

```
NoConfusionHom : ∀ (A : Type) (n : nat), vec A n → vec A n → Prop :=
fun A n v v' =>
match v in (vec _ n0) return (vec A n0 -> Prop) with
| vnil =>
fun y : vec A 0 =>
match y in (vec _ n0) return (n0 = 0 -> Prop) with
| vnil => apply_noConfusion 0 0 (fun _ : True => True)
| @vcons _ _ n0 _ => apply_noConfusion (S n0) 0 (False_rect Prop)
end eq_refl
| @vcons _ a n v =>
fun y : vec A (S n0) =>
match y in (vec _ n1) return (n1 = S n0 -> Prop) with
| vnil => apply_noConfusion 0 (S n0) (False_rect Prop)
| @vcons _ y2 n1 v0 =>
apply_noConfusion (S n1) (S n0) (fun H : n1 = n0 =>
DepElim.solution_left n0 (fun [...] => [...] = [...]) n1 H v0)
end eq_refl
end v'.
```

So basically, **while** matching for the head constructors, NoConfusion seems to additionally check whether the indices are the same or not

I have some trouble understanding what is the added value of that as its type is

```
∀ (A : Type) (n : nat), vec A n → vec A n → Prop
```

so it requires both vectors to be of the same length anyway

(deleted)

Does it uses axiomK somehow to simplify the vcons , voncs case to unify the indices and return sth simpler ?

NoConfusion works on vectors of different lengths (but of course it’s False outside the diagonal), while NoConfusionHom also uses NoConfusion on the indices. NoConfusionHom is only derivable if the indices have UIP indeed. But not necessarily through an axiom, for example nat has UIP provably.

Actually you need UIP only if you need to discriminate indices, some inductive definitions might not need it (e.g only variables in index positions in all constructors)

I understand, but I don't get what it brings more the table ?

Do you have an example where it is actually needed ?

Last updated: Oct 13 2024 at 01:02 UTC