Cardinality model incompatible with Lean compiler

Stream: general

[Violeta Hernández]

Something funny I figured out, the axiom α ≃ β → α = β is incompatible with native_decide:

import Mathlib.Data.Setoid.Basic

axiom equiv_of_eq {α β : Type} (f : α ≃ β) : α = β

def Nat' := Quotient (Setoid.ker fun x : Nat ↦ x - 1)
@[simp] theorem mk_zero : (⟦0⟧ : Nat') = ⟦1⟧ := Quotient.sound rfl

def equivNat : Nat' ≃ Nat where
  toFun x := x.lift _ fun _ _ ↦ id
  invFun x := ⟦x + 1⟧
  left_inv x := x.inductionOn fun x ↦ x.recOn (by simp) (by simp)
  right_inv x := by simp

def castNat : Nat' → Nat := cast (equiv_of_eq equivNat)

theorem contradiction : False := by
  have : castNat ⟦0⟧ ≠ castNat ⟦1⟧ := by native_decide
  simpa

-- 'contradiction' depends on axioms: [equiv_of_eq, propext, Lean.ofReduceBool, Quot.sound]
#print axioms contradiction

This is pretty inconsequential all things considered; there's easier ways to prove False using native_decide (e.g. bad implemented_by tags). But I guess this one more pitfall with compiled Lean to be aware of.

[Violeta Hernández]

Relating to this: are we absolutely sure cast can't be used for evil in "core" Lean? Even if that's just crashing the VM through a bad #eval. Do we always know that equal types must have the exact same VM representation?

[Mario Carneiro]

we get that property from the other extremal model, where you tag all types so that different inductives are distinct

[Mario Carneiro]

in that model, equality of types implies that they have the same construction, although there are some fun exceptions to this rule involving the inductive types which are not injective by cantor's theorem

[Mario Carneiro]

But a full answer to this question involves proving the correctness of type erasure, a la this paper