Should we merge `Quotient.out` and `Quotient.unquot`?

Stream: mathlib4

[Eric Wieser]

We currently have docs#Quot.unquot and docs#Quotient.out.

In Lean3, we needed both because the first was unsound while the second was non-computable; but it seems that the definition of "unsound" (previously meta, now unsafe) has changed in Lean 4, since I can now combine the two as:

import Mathlib.Data.Setoid.Basic
import Mathlib.Data.Multiset.Basic

set_option autoImplicit false

#check Classical.indefiniteDescription

instance {α} {s : Setoid α} (q : Quotient s) : Nonempty ({a : α // ⟦a⟧ = q}) :=
⟨Classical.indefiniteDescription _ (Quotient.exists_rep q)⟩

def Quotient.indefiniteDescription {α} {s : Setoid α} (q : Quotient s) : {a : α // ⟦a⟧ = q} :=
unsafe ⟨q.unquot, lcProof⟩

/-- A combination of `Quotient.out` and `Quotient.unquot` -/
def Quotient.outC {α} {s : Setoid α} (q : Quotient s) : α := q.indefiniteDescription

lemma Quotient.outC_mk {α} {s : Setoid α} (q : Quotient s) : ⟦q.outC⟧ = q := q.indefiniteDescription.2

[Eric Wieser]

Is this equivalent to attribute [implemented_by Quot.unquot] Quotient.out? If so, is this change sensible?

[Mario Carneiro]

no, I think this is unsound

[Mario Carneiro]

unquot was and still is unsafe

[Eric Wieser]

Is unsafe not synonymous with unsound? Because outC above is not unsafe IIUC

[Mario Carneiro]

just because you can wrap an unsafe function in a safe wrapper doesn't mean you have actually discharged the safety condition

[Eric Wieser]

What exactly does unsafe mean here?

[Mario Carneiro]

"unsound" is what happens when you make a safe function which has unsafe preconditions

[Mario Carneiro]

unsafe is a syntactic marker on functions with unsafe preconditions

[Eric Wieser]

The context here is this comment on github, where @Scott Morrison suggested I hide the unsafeness of Quot.unquot

[Mario Carneiro]

you can't

[Mario Carneiro]

at least not with that type signature

[Mario Carneiro]

Quotient.out and Quotient.unquot are different functions, they return different values

[Mario Carneiro]

one of them isn't even really a function, it returns values that are impossible by the logic

[Mario Carneiro]

which is why it is unsafe

[Eric Wieser]

I guess I don't see what the point of contagious unsafe is if you can just hide it again

[Eric Wieser]

Are you only supposed to use it if you pinky promise that the contents are genuinely sound and lean is just confused?

[Mario Carneiro]

unsafe means you need a proof obligation to use the function, only this proof obligation is not expressible in the lean logic

[Mario Carneiro]

so you have to do it on paper / "pinky promise" that you have satisfied it

[Eric Wieser]

In which case I should revert the silencing of unsafe from #6367?

[Mario Carneiro]

yes, the instance needs to be unsafe as it is order dependent even though it has inputs that are not

[Eric Wieser]

Mario Carneiro said:

Quotient.out and Quotient.unquot are different functions, they return different values

My proposal is that we delete the former and redefine it as the latter. I agree they are different functions, but within Lean's logic nothing can tell the difference, right?

[Mario Carneiro]

incorrect

[Kyle Miller]

This doesn't seem good:

abbrev X := Trunc Nat

def a : X := ⟦1⟧
def b : X := ⟦2⟧

#eval a.outC = b.outC
-- false

example : a.out = b.out := by
  rw [Subsingleton.elim a b]

[Eric Wieser]

Yes, I think this amounts to implemented_by being allowed to diverge from whatever the logic says

[Mario Carneiro]

more specifically we are causing divergence between compiler behavior and model behavior

[Mario Carneiro]

and this is not okay

[Mario Carneiro]

because the compiler optimizes assuming that the logic is true, so divergence leads to UB

[Eric Wieser]

Are there example uses of term unsafe that are ok?

[Mario Carneiro]

term unsafe can be used correctly, the idea is that while the general function being called has unsafe preconditions, this particular term combines that function with other things such that the composite satisfies the requisite safety conditions

[Mario Carneiro]

If those safety conditions depend on some property of the caller, then you have to propagate the unsafe

[Eric Wieser]

Eric Wieser said:

but within Lean's logic nothing can tell the difference, right?

What I mean't here I guess is "within the model you can't tell the difference". As Kyle points out, within the runtime you certainly can. I wasn't aware that divergence could cause UB in the compiler though, so I think that resolves my misunderstanding.

[Eric Wieser]

Mario Carneiro said:

yes, the instance needs to be unsafe as it is order dependent even though it has inputs that are not

I've reverted the commit

[Mario Carneiro]

The trick is to use that kind of function to use an unchecked array access function like Array.get

[Jannis Limperg]

A nice example is docs#ptrEq vs docs#withPtrEq. The former allows you to distinguish equal objects, which is bad. The latter makes you prove that you won't do that, so it can be safe.

[Mario Carneiro]

Here's how you can weaponize Kyle's example:

abbrev X := Trunc Nat

def a : X := ⟦1⟧
def b : X := ⟦2⟧

@[noinline] def foo (h : a.outC ≠ b.outC) : Nat := False.elim <| by
  apply h
  rw [Subsingleton.elim a b]

#eval if h : a.outC = b.outC then 1 else foo h

[Mario Carneiro]

if you let foo be inlined, it will return 1 because the if statement is optimized away using the fact that False.elim is unreachable

[Yuyang Zhao]

I made something similar for docs#Quotient.choice 1.5 months ago: code / Gabriel's comment

[Yuyang Zhao]

Is the following code also harmful?

private unsafe def Quotient.choiceImpl {ι : Type*} {α : ι → Type*} [S : ∀ i, Setoid (α i)] :
    (∀ i, Quotient (S i)) → @Quotient (∀ i, α i) (by infer_instance) :=
  unsafeCast

def Quotient.choice'Aux {ι : Type*} {α : ι → Type*} [S : ∀ i, Setoid (α i)]
    (f : ∀ i, Quotient (S i)) :
    ∃ q : @Quotient (∀ i, α i) (by infer_instance), ∀ i, ⟦q.out i⟧ = f i :=
  ⟨Quotient.choice f, fun i ↦ Quotient.induction_on_pi f
    (fun a ↦ by rw [choice_eq, eq]; exact @Quotient.mk_out _ piSetoid _ _)⟩

@[implemented_by choiceImpl]
def Quotient.choice' {ι : Type*} {α : ι → Type*} [S : ∀ i, Setoid (α i)]
    (f : ∀ i, Quotient (S i)) :
    @Quotient (∀ i, α i) (by infer_instance) :=
  (Quotient.choice'Aux f).choose

[Yuyang Zhao]

After nesting a Classical.choose, it should lose its internal structure now.

[Mario Carneiro]

@Yuyang Zhao The exact same counterexample given by Gabriel/Chris above works on the revised version:

def exoticInstance : Decidable True :=
  @Quot.recOnSubsingleton _ _ (fun _ => Decidable True) _
    (@Quotient.choice' (@Quotient Bool trueSetoid) (fun _ => Bool) (fun _ => trueSetoid) id)
    (fun f => decidable_of_iff (f ⟦false⟧ = f ⟦true⟧)
      (iff_true_intro (congr_arg f (Quotient.sound trivial))))

-- VM disagrees with type theory:
example : @decide True exoticInstance = true  := .trans (by congr) decide_True
example : @decide True exoticInstance = false := by native_decide

#eval exoticInstance -- isFalse _

[Mario Carneiro]

The basic issue is that (∀ i, Quotient (S i)) -> Quotient (∀ i, α i), while natural-looking, is not sound because it allows you to lift the identity function Trunc A -> Trunc A to Trunc (Trunc A -> A), and even under a Trunc the contained function Trunc A -> A has "impossible properties"

[Yuyang Zhao]

I got it. A quotient has different VM representations and they are sent to different VM representations by the function. With unsafeCast, the function will go to different values at the same equivalence class.

[Yuyang Zhao]

So in this case it is not possible to write a computable Quotient.choice.