Zulip Chat Archive

Stream: new members

Topic: disjointness of inductive type constructors, heq


view this post on Zulip Kris Brown (Jul 16 2020 at 09:44):

I'm trying to prove something very simple based on the disjointness of inductive type constructors. The strategy I'd use that works for normal equality doesn't seem to work when I have terms with heterogeneous equality. Is there a way to do this?

inductive X :   Type
 | x1 (n:): X n
 | x2 (n:): X n

 lemma xx :  m n, ¬ (X.x1 m == X.x2 n) := by begin
 intros h,
 contradiction -- this would work for ∀ m, ¬ (X.x1 m  = X.x2 m)
 end

view this post on Zulip Reid Barton (Jul 16 2020 at 11:38):

I suspect this is not provable.

view this post on Zulip Kris Brown (Jul 16 2020 at 17:25):

Is this because you suspect it's not true? Or is it just a matter of engineering a variation of meta def contradiction : tactic unit := ... in the core library that works with heq too?

view this post on Zulip Reid Barton (Jul 16 2020 at 17:35):

I think it is not true in all models

view this post on Zulip Kris Brown (Jul 23 2020 at 22:31):

I'm still confused about how this is not true if inductive type constructors are disjoint. If not true in all models, maybe at least true in domain I'm working with? Are there additional hypotheses I can add to allow me to prove, e.g., the bottom example?

inductive X: bool  Type
 | nil (b: bool): X b
 | mk  (b: bool): X b

example: ¬ X.nil tt == X.mk tt := by simp only [not_false_iff, heq_iff_eq]
example: ¬ X.nil tt == X.mk ff := by sorry

view this post on Zulip Kevin Buzzard (Jul 23 2020 at 22:54):

Equality of types is a really poorly behaved thing. Are you sure you want to do what you're doing? If I ever see a goal with == in then I stop what I'm doing and go back to before it appeared.

view this post on Zulip Kevin Buzzard (Jul 23 2020 at 22:54):

You know nat = int is undecidable, right?

view this post on Zulip Kris Brown (Jul 23 2020 at 23:07):

Yes, that makes sense, though this felt like a much more restricted setting than type equality in general. I'll first attempt to redesign things to not use this pattern, though.

view this post on Zulip Reid Barton (Jul 24 2020 at 00:08):

A proof of X.x1 m == X.x2 n is basically a proof h that X m = X n and a proof that if you rewrite one side of the original == across h then they are equal.

view this post on Zulip Reid Barton (Jul 24 2020 at 00:10):

And I'm pretty sure there is no reason that different X m and X n couldn't be identified in a way that makes an X.x1 equal to an X.x2.

view this post on Zulip Reid Barton (Jul 24 2020 at 00:11):

I mean we can just imagine that X n = bool for all n, but we identify x1 and x2 with ff and tt differently depending on the parity of n. That seems consistent to me.

view this post on Zulip Reid Barton (Jul 24 2020 at 00:17):

In relation to your other question, the point is that a hypothesis X m = X n is basically worthless; but if you actually know that m = n, you're in good shape.

view this post on Zulip Mario Carneiro (Jul 24 2020 at 04:00):

@Kris Brown I remember it was somewhat big news when it was discovered (in Agda, I think) that injectivity of inductive type families is inconsistent. There is a lean example of this floating around somewhere

view this post on Zulip Mario Carneiro (Jul 24 2020 at 04:02):

The proof is embarrasingly simple:

import logic.function.basic

inductive T : (Type  Prop)  Type

example : ¬ function.injective T := function.cantor_injective _

Last updated: May 13 2021 at 23:16 UTC