## Stream: Coq users

### Topic: Inversion with different types? (kinda cursed)

#### Joshua Grosso (Oct 29 2020 at 18:05):

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?

#### Li-yao (Oct 29 2020 at 18:15):

What's the definition of `Bar`?

#### Joshua Grosso (Oct 29 2020 at 18:20):

oops—example updated with the definition of `Bar`.

#### Jakob Botsch Nielsen (Oct 29 2020 at 18:40):

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

#### Joshua Grosso (Oct 29 2020 at 18:44):

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

#### Jakob Botsch Nielsen (Oct 29 2020 at 18:50):

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.

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

#### Joshua Grosso (Oct 29 2020 at 19:01):

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.

#### Joshua Grosso (Oct 29 2020 at 19:02):

Because now, trying to derive `NoConfusionHom` gives me "Error: Incorrect elimination of "y" in the inductive type "is_subtype_of3": ill-formed elimination predicate."

#### Joshua Grosso (Oct 29 2020 at 19:04):

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

#### Jakob Botsch Nielsen (Oct 29 2020 at 19:05):

You can try to derive just `NoConfusion`

#### Joshua Grosso (Oct 29 2020 at 19:07):

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

#### Jakob Botsch Nielsen (Oct 29 2020 at 19:29):

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

#### Paolo Giarrusso (Oct 30 2020 at 01:19):

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

#### Paolo Giarrusso (Oct 30 2020 at 01:21):

And is it in Type or Prop?

#### Joshua Grosso (Oct 30 2020 at 01:24):

`foo : type -> type -> Prop`, I think

#### Joshua Grosso (Oct 30 2020 at 01:25):

where `type` is a recursive `Inductive` type in `Type`.

#### Paolo Giarrusso (Oct 30 2020 at 01:33):

I think that `Prop` is your problem.

#### Paolo Giarrusso (Oct 30 2020 at 01:34):

if `p1, p2 : P : Prop`, inversion cannot learn anything from `H : p1 = p2`.

#### Paolo Giarrusso (Oct 30 2020 at 01:34):

Because `H` could hold simply by postulated proof irrelevance.

#### Paolo Giarrusso (Oct 30 2020 at 01:35):

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

#### Paolo Giarrusso (Oct 30 2020 at 01:36):

my usual example is that, given `Inductive foo : Prop := | f1 | f2.` you can’t prove `f1 <> f2`.

#### Paolo Giarrusso (Oct 30 2020 at 01:38):

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.

#### Paolo Giarrusso (Oct 30 2020 at 01:39):

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

#### Paolo Giarrusso (Oct 30 2020 at 01:40):

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

#### Joshua Grosso (Oct 30 2020 at 02:37):

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: Oct 04 2023 at 23:01 UTC