## Stream: new members

### Topic: disjointness of inductive type constructors, heq

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


#### Reid Barton (Jul 16 2020 at 11:38):

I suspect this is not provable.

#### 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?

#### Reid Barton (Jul 16 2020 at 17:35):

I think it is not true in all models

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


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

#### Kevin Buzzard (Jul 23 2020 at 22:54):

You know nat = int is undecidable, right?

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

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

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

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

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

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

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