How to prove theorems that use `cast`

Stream: lean4

[Casavaca]

Hi, everyone.

Does anyone know how to prove this simple theorem?

theorem fin_cast (n : Nat) (h : Fin m = Fin n) (a : Fin m) : (cast h a).val = a.val := by
  have heq : HEq (cast h a) a := by simp [cast_heq]
  -- ???
/-
Goals (1)
m n : Nat
h : Fin m = Fin n
a : Fin m
heq : HEq (cast h a) a
⊢ (cast h a).val = a.val
-/

[Simon Hudon]

You can prove it by generalizing the types Fin m and Fin n and use type variables. Then you can do subst h; constructor.

In general, you may have an easier time working with m = n instead of Fin m = Fin n and writing a function Fin.cast : m = n -> Fin n -> Fin m. Then you can write lemmas about Fin.cast and reason about Nat equality rather than equality between types. Theorems about type equality are notoriously weak. From Fin n = Fin m, you might expect that you could prove n = m but the logic wont take you there. You won't be about to prove more straightforward equations like Nat /= Fin n either btw.

[Kyle Miller]

Simon Hudon said:

You can prove it by generalizing the types Fin m and Fin n and use type variables. Then you can do subst h; constructor.

How does this work? The goal involves .val, which depends on these being Fin's, and I don't see how to generalize it.

[Kyle Miller]

This theorem should be provable due to cardinality:

theorem fin_injective (h : Fin m = Fin n) : m = n := sorry

With it, you can then prove the theorem with

theorem fin_cast (h : Fin m = Fin n) (a : Fin m) : (cast h a).val = a.val := by
  cases fin_injective h
  rfl

[Kyle Miller]

You also should be able to prove Nat /= Fin n since Nat is an infinite type.

[Kyle Miller]

Using Lean 3:

import tactic

theorem fin_cast (m n : ℕ) (h : fin m = fin n) (a : fin m) : (cast h a).val = a.val :=
begin
  cases fin_injective h,
  refl,
end

theorem nat_ne_fin (m : ℕ) : ℕ ≠ fin m :=
begin
  intro h,
  have : infinite ℕ := infer_instance,
  rw h at this,
  apply this.not_fintype,
  apply_instance,
end

[Simon Hudon]

Good points, I spoke too quickly.

[Simon Hudon]

My point was that the axioms don't allow you to reason directly about type equality. For types of different cardinalities or when you can prove a proposition about one type and not about another, indeed, you can conclude that types are different.

[Casavaca]

Interesting. I wonder why we cannot prove Fin n = Fin m -> n = m?

In my imagination, if we apply injection on a equation of a type family, we should get that all indices are equal. E.g.

Fin m = Fin n → m = n
vector α n = vector β m → α = β ∧ n = m

[Mario Carneiro]

We can prove Fin n = Fin m -> n = m, but not for the reason you stated. The only provable equalities of types are for when the types have different cardinalities. This works out for Fin because Fintype.card (Fin n) = n, but in the majority of cases this method is not available, including Vector.

You could axiomatize that all type families are injective, but that is a short trip to inconsistency, because of this type family:

inductive Foo : (Type u → Prop) → Type u

The assertion Foo x = Foo y -> x = y is a direct contradiction to Cantor's theorem.

[Casavaca]

Could you tell me a little more / point to me something to read? I'm guessing something something have different cardinalities so it cannot be injective, but I don't understand this.

[Mario Carneiro]

Which part? That we can prove injectivity for Fin or that we can prove non-injectivity for Foo?

[Mario Carneiro]

The second part is Cantor's theorem: for any $X$ you cannot have an injective function from $\mathcal{P}(X)$ to $X$ because $\mathcal{P}(X)$ is "too big"

[Eric Wieser]

Kyle Miller said:

This theorem should be provable due to cardinality:

theorem fin_injective (h : Fin m = Fin n) : m = n := sorry

Note that Lean 3 has this, docs#fin_injective

[Mario Carneiro]

It's not entirely trivial to prove, you need the pigeonhole principle to show that the cardinalities of finite sets are different

[Casavaca]

I can see now why inductive Foo : (Type u → Prop) → Type u in not injective. Thanks very much.

But injective type family is so intuitive. I wonder if there is a simple way to make it work, e.g., by add some limitations. Is there some work related to this?

[Leonardo de Moura]

@Casavaca The following thread should be relevant. https://github.com/leanprover/lean/issues/654
BTW, this feature is a recurrent source of unsoundness in other systems. Examples:

• Idris: https://github.com/idris-lang/Idris-dev/issues/3687
• Agda: https://lists.chalmers.se/pipermail/agda/2010/001526.html
• F*