Stream: Equations devs & users

Topic: What is the point of NoConfusion ?


view this post on Zulip Thomas Lamiaux (Oct 03 2024 at 13:03):

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

  1. Is it supposed to be used as a sort of injection + discriminate ?
  2. 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

view this post on Zulip Thomas Lamiaux (Oct 03 2024 at 13:04):

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

view this post on Zulip Kenji Maillard (Oct 03 2024 at 13:09):

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.

view this post on Zulip Matthieu Sozeau (Oct 03 2024 at 13:48):

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

view this post on Zulip Matthieu Sozeau (Oct 03 2024 at 13:49):

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

view this post on Zulip Matthieu Sozeau (Oct 03 2024 at 13:49):

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

view this post on Zulip Thomas Lamiaux (Oct 04 2024 at 12:31):

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 ?

view this post on Zulip Matthieu Sozeau (Oct 04 2024 at 15:06):

Exactly

view this post on Zulip Thomas Lamiaux (Oct 04 2024 at 16:41):

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

view this post on Zulip Matthieu Sozeau (Oct 04 2024 at 18:54):

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

view this post on Zulip Matthieu Sozeau (Oct 04 2024 at 18:56):

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)

view this post on Zulip Thomas Lamiaux (Oct 07 2024 at 14:34):

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 ?

view this post on Zulip Thomas Lamiaux (Oct 07 2024 at 14:40):

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.

view this post on Zulip Thomas Lamiaux (Oct 07 2024 at 14:41):

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

view this post on Zulip Matthieu Sozeau (Oct 08 2024 at 12:45):

Yes, there must be non-forced indices I believe

view this post on Zulip Matthieu Sozeau (Oct 08 2024 at 12:47):

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