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

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 13 2024 at 01:02 UTC