Stream: Coq users

Topic: Inversion with different types? (kinda cursed)


view this post on Zulip 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?

view this post on Zulip Li-yao (Oct 29 2020 at 18:15):

What's the definition of Bar?

view this post on Zulip Joshua Grosso (Oct 29 2020 at 18:20):

oops—example updated with the definition of Bar.

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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."

view this post on Zulip 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).

view this post on Zulip Jakob Botsch Nielsen (Oct 29 2020 at 19:05):

You can try to derive just NoConfusion

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 01:19):

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

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 01:21):

And is it in Type or Prop?

view this post on Zulip Joshua Grosso (Oct 30 2020 at 01:24):

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

view this post on Zulip Joshua Grosso (Oct 30 2020 at 01:25):

where type is a recursive Inductive type in Type.

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 01:33):

I think that Prop is your problem.

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 01:34):

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

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 01:34):

Because H could hold simply by postulated proof irrelevance.

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 01:35):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 30 2020 at 01:39):

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

view this post on Zulip 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.

view this post on Zulip 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: Mar 28 2024 at 23:01 UTC