Stream: Equations devs & users

Topic: Derive NoConfusion failing

Ali Caglayan (Nov 25 2021 at 09:43):

Hi, I am failing to derive NoConfusion for an inductive type. Here is a reduced example:

From Coq.Sets Require Import Ensembles.
From Equations Require Import Equations.

Axiom Formula : Set.

Inductive Foo : Ensemble Formula -> Formula -> Prop :=
| bar {Γ φ} : In _ Γ φ -> Foo Γ φ
.

Derive NoConfusion for Foo.

Any idea what might be going wrong? cc @Matthieu Sozeau

I get:

Incorrect elimination of "pr2 y" in the inductive type "Foo":
ill-formed elimination predicate.

Which is a bit mysterious.
I am using the current master version for equations.

Matthieu Sozeau (Nov 25 2021 at 10:12):

There is no NoConfusion principle for inductives in Prop, as it would contradict proof-irrelevance to be able to distinguish proofs :)

Matthieu Sozeau (Nov 25 2021 at 10:12):

That precondition should be checked though

Ali Caglayan (Nov 25 2021 at 19:15):

Is this really something that cannot be done however? I don't use proof-irrelevance. Would anything go wrong if it were allowed? AFAIK Prop doesn't have it, only SProp right?

Paolo Giarrusso (Nov 25 2021 at 20:19):

coq is designed so that postulating proof irrelevance on Prop is consistent. Hence, a proof of NoConfusion wouldn't be sound.

Paolo Giarrusso (Nov 25 2021 at 20:20):

Maybe you can postulate the negation for a specific type (I don't see how to state it in general), but moving the given type to Type seems easier.

Ali Caglayan (Nov 25 2021 at 21:07):

The problem with moving the above type into Type for example is that I can no longer do case analysis on Ensembles. I have used ensembles quite a lot, so I am not really sure if I can replace all uses with a Type version or even if that makes any sense anymore. I like to define various ensembles as an inductive type, but not being able to eliminate into Type isn't great.

Matthieu Sozeau (Nov 26 2021 at 09:52):

Maybe the question is more: why would you need NoConfusion on that type? It's probably never used as an index.

Ali Caglayan (Nov 26 2021 at 10:24):

That type is really a type of proofs, and I was hoping to do some sort of depth measurement on those proofs for use as a measure in recursion.

Ali Caglayan (Nov 26 2021 at 10:24):

It looks unlikely that I can write a depth function keeping it in prop then.

Ali Caglayan (Nov 26 2021 at 10:25):

But originally I was trying to derive the subterm for the type instead of using depth.

Matthieu Sozeau (Nov 26 2021 at 10:27):

Likewise, subterm is not available on derivations in Prop, for the same reason: there cannot be a non-trivial well-founded relation on Prop's as it would mean you could distinguish two proofs of the same statement (one being "smaller" than another)

Matthieu Sozeau (Nov 26 2021 at 10:27):

What you can do is index the Prop by a nat and induct on that.

Paolo Giarrusso (Nov 26 2021 at 10:30):

Makes sense... And outside the Equations error messages, this question probably isn't Equations-specific any more I guess?

Ali Caglayan (Nov 26 2021 at 10:31):

No this just seems to be me failing to come to terms with Prop 0:-)

Paolo Giarrusso (Nov 26 2021 at 10:33):

But the error messages are worth an issue anyway, I could also mistake that error message for some bug.

Paolo Giarrusso (Nov 26 2021 at 10:34):

(The underlying Coq error message could be improved as well)

Ali Caglayan (Nov 27 2021 at 12:52):

Indexing the Prop by nat worked exactly how I wanted. It is a good idea!

Jason Gross (Jan 30 2022 at 23:32):

Very belatedly, shouldn't there be a NoConfusion / inversion principle for all Props with a single constructor, all of whose arguments are either in Prop or else variables which are used as indices of the type family?

Paolo Giarrusso (Jan 31 2022 at 01:17):

Silly Q: Do you havs a proven example? I'm wondering if you could have a model with proof irrelevance for some propositions, where your example constructors wouldn't be injective...

Jason Gross (Jan 31 2022 at 02:44):

If you have proof-irrelevance for any proposition with two or more constructors (such as or), where you cannot derive which constructor was used from the indices and parameters of the inductive family, then the constructors are not injective. If you have proof-irrelevance for any proposition whose constructor has a non-prop argument whose value cannot be uniquely derived from the indices & parameters of the inductive family, then the constructor is not injective. All other props have injective constructors. If any proposition constructively fails to satisfy proof irrelevance (that is, has an injection from bool to the prop), then you can smuggle any discrete information you'd like out of any proposition, via this proposition. This constrains the models you're looking for quite severely @Paolo Giarrusso , if they exist at all

Jason Gross (Jan 31 2022 at 02:46):

I guess that proof-irrelevance for or doesn't give you proof-irrelevance for inhabited Type....

Matthieu Sozeau (Feb 02 2022 at 15:56):

I think those are pretty much True, False and conjunction no? It is indeed provable that (p = q : A /\ B) <-> (proj1 p = proj1 q /\ proj2 p = proj2 q).

Last updated: Dec 07 2023 at 09:01 UTC