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

[Aaron Liu]

having fun

import Mathlib.Logic.Small.Defs
import Mathlib.Data.Setoid.Basic

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

theorem Shrink.eq_of_equiv {α : Type u} {β : Type v} [Small.{w} α] [Small.{w} β]
    (equiv : α ≃ β) : Shrink.{w} α = Shrink.{w} β := by
  unfold Shrink
  have hu (x : Type w) : Nonempty (α ≃ x) = Nonempty (β ≃ x) :=
    propext ⟨Nonempty.map equiv.symm.trans, Nonempty.map equiv.trans⟩
  simp [hu]

def castNat : Shrink.{0} Nat' → Shrink.{0} Nat := cast (Shrink.eq_of_equiv equivNat)

theorem contradiction : False := by
  have : (equivShrink _).symm (castNat (equivShrink _ ⟦0⟧)) ≠
      (equivShrink _).symm (castNat (equivShrink _ ⟦1⟧)) := by native_decide
  simpa

/- 'contradiction' depends on axioms:
[propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler, Quot.sound] -/
#print axioms contradiction

[Aaron Liu]

see the implemented_by which makes this happen,
https://github.com/leanprover-community/mathlib4/blob/5123e3ed3fb8a3d1c4393ebe5ef8fbf543d8aa1a/Mathlib/Logic/Small/Defs.lean#L44-L55

[Weiyi Wang]

What should be my takeaway from the example above? I was previously told that I can't trust native_decide because it can be affected by external plugins, but that left me impression that within the boundary of a controlled set of dependencies (lean core & mathlib) it is fairly correct. But this one implies a different story

[Aaron Liu]

the takeaway is that for equivShrinkImpl to be sound we need to make Shrink opaque

[Cameron Zwarich]

Mario Carneiro said:

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

Would proving type erasure correct actually answer the question of which axioms consistent with Lean's type theory are also consistent with the "model" provided by Lean's compiler?

[Cameron Zwarich]

Aaron Liu said:

see the implemented_by which makes this happen,
https://github.com/leanprover-community/mathlib4/blob/5123e3ed3fb8a3d1c4393ebe5ef8fbf543d8aa1a/Mathlib/Logic/Small/Defs.lean#L44-L55

There is probably some value in having native_decide distinguish between implemented_by/extern/unsafe/etc. decls in Lean's core libraries (maybe even just Init) and those outside of it, then only allowing the use of the former by default without additional options (possibly including an option to print the ones that were actually used).

[Eric Wieser]

Aaron Liu said:

the takeaway is that for equivShrinkImpl to be sound we need to make Shrink opaque

Or rather, a sigma type combining Shrink and the Equiv?

[Aaron Liu]

Eric Wieser said:

Aaron Liu said:

the takeaway is that for equivShrinkImpl to be sound we need to make Shrink opaque

Or rather, a sigma type combining Shrink and the Equiv?

of course, otherwise we wouldn't be able to get the Equiv

[Cameron Zwarich]

Another example showing the compiler's incompatibility with the cardinality model is redefining Nat by copying its definition as an inductive. The compiler's special representation for Nat will not be used for your own type. IIRC Idris will use the builtin Nat representation for any type that looks close enough to Nat (and we could do this too), but this will never solve the incompatibility, since you can e.g. always add a field whose size depends on whether FLT is true.

[Violeta Hernández]

Aaron Liu said:

the takeaway is that for equivShrinkImpl to be sound we need to make Shrink opaque

Is this something we should PR?

[Robin Arnez]

Yeah, probably. Might also be good to make Shrink a structure at the same time, for good measure :-)

[Kim Morrison]

I would be happier about removing this implemented_by from Mathlib.

[Robin Arnez]

Hmm you're right, this is the only occurrence of implemented_by in mathlib that's not on an opaque. The way I see it, we only need implemented_by here because of a missing feature (notably lean4#9508), so the implemented_by will go away eventually. In the meantime we can probably use opaque to fix the problem or leave it to anyone needing it to implement it themselves.

[Cameron Zwarich]

Kim Morrison said:

I would be happier about removing this implemented_by from Mathlib.

I would be happier if Mathlib had no uses of implemented_by. Between adding missing csimps, improved compiler performance, and new features, how realistic is this future?

[Weiyi Wang]

I only see 4 implemented_by by code search, so I guess... not far away?

[Cameron Zwarich]

To me it looks like this:

• equivShrink in Mathlib/Logic/Small/Defs.lean. This will be solved by #9508, which should happen next quarter (because it's needed to make a good Iterator API).
• memoFix in Mathlib/Util/MemoFix.lean. The real problem here is the use of very unsafe unsafe code (which also uses unsafeBaseIO), although its usage is restricted to tactics. It's only used by Mathlib/Lean/Expr/ReplaceRec.lean, but I don't see a way to do this with safe code without slightly changing the interface.
• Float.valUnsafe and Float.mkUnsafe in Mathlib/Util/CompileInductive.lean. The compiler will support recursors for arbitrary inductives soonish, so this file will just be deleted.

[Kim Morrison]

chore: Revert "feat: computable shrink (#28112)" #29419

reverts the change introducing this most recent invalid implemented_by.

[Eric Wieser]

(lean4#9508 is the right link for Cameron's message)

[Dexin Zhang]

May I ask why Shrink can still be computable, while its definition uses Classical.choose?

[Robin Arnez]

Well, the definition couldn't be computable in its current state (as figured out in this thread) but if Shrink would be opaque then it is fine to assert certain things about its runtime behavior, in particular you can assume it that Shrink alpha has the same runtime representation as alpha

[Robin Arnez]

And after lean4#9508, you could use Classical.choose but you wouldn't use the constructor / projection but instead an autogenerated function to convert between Shrink alpha and alpha like

def_type_with_rep Shrink.{v} (α : Type u) [h : Small.{v} α] where
  absType := h.equiv_small.choose
  repType := α
  toRep := h.equiv_small.choose_spec.some.invFun
  fromRep := h.equiv_small.choose_spec.some.toFun
  fromRep_toRep := by simp
  toRep_fromRep := by simp

#check Shrink.ofRep -- α -> Small.{v} α
#check Shrink.rep -- Small.{v} α -> α

[Dexin Zhang]

But Shrink as a function returns Type is indeed computable even after #29419... Do you mean we can write Shrink computably, but can never computably construct an element of it?

[Robin Arnez]

Computability of Shrink itself is not a concern; types are irrelevant in Lean; the question is whether you'd be able to create a value Shrink α from a value of α. This is possible with an @[implemented_by] and should be possible without after some variant of lean4#9508 has been implemented.

[Dexin Zhang]

I see. So functions returning Types (like Shrink) are actually erased in runtime?

[William Sørensen]

Hi sorry for introducing this instance of False through native decide :man_facepalming:. I was wondering though how would the new proposal override_repr solve this? I tried just skimming the gh thread but I couldn’t find an example. Could someone link me this? It would just be really nice to see because it would be super useful for coinductives through QPF

[William Sørensen]

Wait lol i am completely blind. Ok I see now how it would be implemented. Do we know if / when this is planned to be added to lean?

[James E Hanson]

Mario Carneiro said:

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

Is there a reference that talks about this failure of injectivity for inductive types?

[Aaron Liu]

Kyle Miller said:

Here's an example:

import Mathlib

inductive IsntInj (f : Type → Prop) : Type

example : ¬ Function.Injective IsntInj :=
  Function.cantor_injective IsntInj

Here's an example

[Kevin Buzzard]

Huh! Lean is Ok with that inductive being in Type rather than Type 1?

[Violeta Hernández]

Kevin Buzzard said:

Huh! Lean is Ok with that inductive being in Type rather than Type 1?

None of the constructors (of which there are none) make use of f, which is why I think this is allowed.

[Kevin Buzzard]

Huh,

inductive Thing (f : Type 7 → Type 2) : Type 4

is also fine (I would have used Type 37 but apparently such silly ideas are now banned).

[Aaron Liu]

not banned, just needs a bit of work

inductive Thing (f : Type (25 + 12) → Type 2) : Type 4

or, if you actually want 37 we can do

set_option maxUniverseOffset 255 in
inductive Thing (f : Type 37 → Type 2) : Type 4

[Aaron Liu]

I tried adding some constructors and it still works?

[Robin Arnez]

Well, for something like

inductive Thing (f : Type 30 → Type 2) : Type 4 where
  | hello (x : f PUnit)

you could've also done

inductive OtherThing (α : Type 2) : Type 4 where
  | hello (x : α)

def Thing (f : Type 30 → Type 2) : Type 4 := OtherThing (f PUnit)

The parameters of the inductive simply aren't put into the universe restrictions because you can model them indirectly.

[Violeta Hernández]

Wait, why is the universe number capped now?

[Floris van Doorn]

Violeta Hernández said:

Wait, why is the universe number capped now?

It's not, see the set_option maxUniverseOffset 255 above.
It's just that universe levels are stored in unary, so something like Type 1000000 creates a universe expression with a million Level.succ's, so they are capped by default.

[Trebor Huang]

Kevin Buzzard said:

Huh! Lean is Ok with that inductive being in Type rather than Type 1?

Even if we are to take the universe level into account, it should be Type too. Notice that List (A : Type) : Type is valid, and Type is at the same universe level as Type -> Prop. If we raise the universe level here we're basically in an ultra-predicative logic where most inductive constructions give you proper classes instead of sets.