I have been thinking about it for a while but I can't seem to understand, what is the point of NoConfusion and NoConfusionHom ?

- Is it supposed to be used as a sort of injection + discriminate ?
- Is it for elaborating the pattern matching ? Because I tried but I can't figure out an example where it is actually needed. For instance, I thought of writing a dec eq but it works without

```
From Equations Require Import Equations.
Inductive vec A : nat -> Type :=
| vnil : vec A 0
| vcons : A -> forall (n : nat), vec A n -> vec A (S n).
Arguments vnil {_}.
Arguments vcons {_} _ {_} _.
Equations EqDec_Vec {A} (eqA : A -> A -> bool) {n m} (v1 : vec A n) (v2 : vec A m) : bool :=
EqDec_Vec eqA (n:=0) (m:=0) vnil vnil := true ;
EqDec_Vec eqA (n := S _) (m := S _) (vcons a1 v1') (vcons a2 v2') := eqA a1 a2 && EqDec_Vec eqA v1' v2' ;
EqDec_Vec eqA _ _ := false.
Equations EqDecHom_Vec {A} (eqA : A -> A -> bool) {n} (v1 v2 : vec A n) : bool :=
EqDecHom_Vec eqA vnil vnil := true ;
EqDecHom_Vec eqA (vcons a1 v1') (vcons a2 v2') := eqA a1 a2 && EqDecHom_Vec eqA v1' v2' .
```

so I just don't get, and how I should explain it in the tutorials

btw if I can't manage to get it, it probably means it is worth an explanation

Did you have a look at section 4.3 of equations reloaded ? I think it contains a precise explanation of why the homogeneous version exists.

They are both used to elaborate pattern matching, and indeed they do both injection and discriminate. In your example you're using NoConfusion on nat not vectors

The tactic `noconf H`

applies either repeated injection or discrimination to H, you can use it anywhere injection or discriminate would be used

And it's using the derived NoConfusion instances you have in your context

So if I understand correctly NoCounsion and no NoConfusionHom are needed, but simply not for vec because the constructors are orthogonal on the indices which are all forced ?

Exactly

I am reading the paper from top to bottom to be sure to get it. Sth I don't get is this paragraph

This result should settle these issues once and for all by providing a solid theoretical background to the axiomatic dependent pattern-matching implemented in Agda. However, note that this solution involves constructing during unification a substitution that should come from a chain of computationally-relevant type equivalences which are not actually built by the unifier. They are proven to exist and enjoy a strong definitional property in the metatheoretical proofs only. While we were able to reproduce this result [Sozeau and Mangin 2019a, file theories/telescopes.v], any change to the core calculus implies a requirement of trust towards its implementation, whose burden we avoid in the case of Eqations by providing a definitional translation.

I have some trouble understanding what the downside is

The pattern-matching compilation in Cockx's thesis, which involves proof-relevant manipulations of equalities is not implemented in Agda, it is only used to justify the unifications that are done at type-checking time. With equations, we get these concrete proof terms in the definitions, so we are sure it does not extend the type theory. There were a few cases where K splipped in in Agda's implementation, unnoticed, because it doesn't keep evidence like Equations does

There is a downside in Equations case, which is that the guard checker can be thrown of by these proof terms (i.e. not see that something is a subterm because it was type-cast/transported)

I have read the whole paper in detail but I am still not quite sure when UIP is needed. From what I understand, it is for non-forced arguments ?

I have only found this paragraph about NoConfusionHom

Note that this derivation will fail if equality of constructors in the inductive family cannot be reduced to equalities of their non-forced arguments. Typically, this is the case of equality: implementing homogeneous no-confusion on equality would be equivalent to UIP as it would be showing that equality of equalities is equivalent to True!

[...]

The fact that NoConfusionHom is derivable on an inductive family actually ensures that one will never need UIP in pattern-matching problems involving it

[...]

To summarize, we have now two notions of no-confusion: one that applies to heterogeneous goals and another for homogeneous ones. We will favor the homogeneous one during simplification, but the heterogeneous version is still useful if we want to use UIP.

Following the resolution procedure, it says

In case the previous rule failed (NoConf), we need to turn the equality into an equality of packed inductives. This step requires UIP on the type of the indices of the inductive type, or it will fail.

[...]

There are two simplification steps which can make use of UIP on a given type: dependent Deletion, as expected, and Pack which requires it on the indices of the inductive type.

which from what I understand only happens if there are non forced indices

Yes, there must be non-forced indices I believe

The most trivial way it appears is when simplifying heterogeneous equalities/equalities in sigma-types: `(n, v) = (n, w) : { n : nat & I n } `

requires to turn n = n into eq_refl to proceed (i.e. dependent deletion).

Last updated: Oct 13 2024 at 01:02 UTC