Exfalso HEq

Stream: lean4

[Marcus Rossel]

Say we have the following:

structure Thing (n : Nat) where
  a : Int

example (n₁ n₂ : Nat) (t₁ : Thing n₁) (t₂ : Thing n₂) (h : HEq t₁ t₂) (h' : n₁ ≠ n₂) : False := ...

How would one go about proving this theorem?

Using eq_of_heq didn't work for me.

[Reid Barton]

It's not provable

[Reid Barton]

It only really makes sense to care about h : HEq t₁ t₂ if you also know that n₁ = n₂

[Marcus Rossel]

Huh, why is that? Shouldn't Heq t₁ t₂ allow me to derive n₁ = n₂, which is then a contradiction to n₁ ≠ n₂?

[Reid Barton]

No, you can only deduce Thing n₁ = Thing n₂

[Marcus Rossel]

Do you mean t₁ = t₂? I thought type level equalities like Thing n₁ = Thing n₂ weren't possible?

[Reid Barton]

Nope!

[Reid Barton]

You have equality at any type, including Type

[Reid Barton]

It's just not very productive to think about equalities of types usually

[Kyle Miller]

Terms of Thing don't use n, so it's possible for a concrete implementation to erase it from the representation. In fact, it's possible for Int = Thing 0 = Thing 1 = Thing 2 = .... It's also possible that they're all not equal to each other in a concrete implementation, so that's why you can't prove it either way.

[Marcus Rossel]

Ok, I think I should heed the common advice and avoid HEq then :sweat_smile:

[Kyle Miller]

Sigma types (that includes just putting n into the structure as a field) are sort of a way around this.