In my context, I have hypotheses of the form:

```
Inductive bar =
| Bar : forall x z y (Hx : foo x y) (Hy : foo y z), bar.
H1 : foo x y
H2 : foo y z
H3 : foo x y'
H4 : foo y' z
H5 : Bar x z y H1 H2 = Bar x z y' H3 H4
```

I'd like to use `inversion`

(or similar) to deduce that `y = y'`

, `H1 = H3`

, and `H2 = H4`

. However, `inversion H5`

no-ops, which I'm assuming is because `y`

and `y'`

have different types (and same with `H1 = H3`

and `H2 = H4`

).

This is admittedly a super-weird case, but am I just plain out of luck?

What's the definition of `Bar`

?

oops—example updated with the definition of `Bar`

.

What type does `x z y`

have? I don't think you can get what you want unless you have UIP on that type (but you can consistently assume this as an axiom).

Their type is a simple inductive data type (nothing fancy). Regarding UIP, is there some sort of "inverse `rew`

" that could work?

To be clear, I don't see why inversion should no op, it should produce `y = y'`

and then equalities between sigma types for the remaining members. You can try `injection`

instead.

If `x z y`

have decidable equality you get UIP definitionally and otherwise you can assume UIP. In that case you can use the `noconf`

tactic from Equations to simplify this goal.

```
From Equations Require Import Equations.
Require Import Equations.Prop.Classes.
Axiom T : Type.
Axiom foo : T -> T -> Type.
Inductive bar :=
| Bar : forall x z y (Hx : foo x y) (Hy : foo y z), bar.
Derive NoConfusionHom for bar.
Set Equations With UIP.
Instance uip_t : UIP T.
Proof. Admitted.
Goal forall x y y' z
(H1 : foo x y)
(H2 : foo y z)
(H3 : foo x y')
(H4 : foo y' z)
(H5 : Bar x z y H1 H2 = Bar x z y' H3 H4),
existT (fun y => foo y z) y H2 = existT _ y' H4.
Proof.
intros.
noconf H5.
reflexivity.
Qed.
```

A ha, trying to derive `NoConfusionHom`

made me realize my minimal example was actually (totally) incorrect!

What's I'm really trying to do is:

```
Inductive foo :=
| ...
| Foo_Trans : forall x z y (Hx : foo x y) (Hy : foo y z), foo x z.
(* Context: *)
H1 : foo x y
H2 : foo y z
H3 : foo x y'
H4 : foo y' z
H5 : Foo_Trans x z y H1 H2 = Foo_Trans x z y' H3 H4
```

I assume the recursion in `foo`

is what's causing the issue. Sorry for giving the wrong example.

Because now, trying to derive `NoConfusionHom`

gives me "Error: Incorrect elimination of "y" in the inductive type "is_subtype_of3": ill-formed elimination predicate."

Now that I'm looking at my problem from a 30,000 foot view, I'm wondering if I've been way overcomplicating the whole thing (specifically, I'm trying to prove that the `Foo_Trans`

constructor is subsumed by all the other constructors of `foo`

, so I could just define a new version of `foo`

without that constructor and prove this new relation to be transitive).

You can try to derive just `NoConfusion`

That gives "Error: Incorrect elimination of "pr2 y" in the inductive type "is_subtype_of3": ill-formed elimination predicate." :grimacing:

Hmm, that probably warrants a bug report to Equations, not sure why that would happen.

You can import `Program`

from Coq and then use the `depelim`

tactic from there, but it will insert some axioms. If you want to be free of those then you will need to do some manual reasoning using UIP since Equations is not working

What's foo's signature? The example seems type-incorrect

And is it in Type or Prop?

`foo : type -> type -> Prop`

, I think

where `type`

is a recursive `Inductive`

type in `Type`

.

I think that `Prop`

is your problem.

if `p1, p2 : P : Prop`

, inversion cannot learn anything from `H : p1 = p2`

.

Because `H`

could hold simply by postulated proof irrelevance.

Correction: that _might_ work if your goal is in Prop, but details confuse me right now.

my usual example is that, given `Inductive foo : Prop := | f1 | f2.`

you can’t prove `f1 <> f2`

.

anyway, an equality of proofs is weird, so either move the type to `Type`

or, from the 30,000 foot view, reconsider how you’re stating things.

I agree that you can remove the constructor and prove the relation transitive.

and I don’t understand how your context would come up in the task, or what your strategy is.

Moving `foo`

into `Type`

and using `Derive NoConfusionHom`

with `noconf`

actually worked! (although fortunately, I was able to restate what I was trying to prove in a "normal" way)

Last updated: Jun 15 2024 at 08:01 UTC