disjointness of inductive type constructors, heq

Stream: new members

[Kris Brown]

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

[Reid Barton]

I suspect this is not provable.

[Kris Brown]

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?

[Reid Barton]

I think it is not true in all models

[Kris Brown]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

You know nat = int is undecidable, right?

[Kris Brown]

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.

[Reid Barton]

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.

[Reid Barton]

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.

[Reid Barton]

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.

[Reid Barton]

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.

[Mario Carneiro]

@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

[Mario Carneiro]

The proof is embarrasingly simple:

import logic.function.basic

inductive T : (Type → Prop) → Type

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