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.

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

That precondition should be checked though

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?

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

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.

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.

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

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.

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

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

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)

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

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

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

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

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

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

Very belatedly, shouldn't there be a NoConfusion / inversion principle for all `Prop`

s with a single constructor, all of whose arguments are either in `Prop`

or else variables which are used as indices of the type family?

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

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

I guess that proof-irrelevance for `or`

doesn't give you proof-irrelevance for `inhabited Type`

....

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: May 28 2023 at 18:29 UTC