Lifting a quotient function

Stream: Is there code for X?

[Robin Arnez]

import Mathlib.Data.Quot

noncomputable def Quotient.liftFun {s : Setoid α} (f : (β → α) → γ) : (∀ f₁ f₂, (∀ x, f₁ x ≈ f₂ x) → f f₁ = f f₂) →
    (β → Quotient s) → γ := fun _ q => f (fun a => (q a).out)

theorem Quotient.liftFun_mk {s : Setoid α} (f : (β → α) → γ) (h : ∀ f₁ f₂, (∀ x, f₁ x ≈ f₂ x) → f f₁ = f f₂) (g : β → α) :
    Quotient.liftFun f h (fun x => Quotient.mk s (g x)) = f g := by
  unfold liftFun
  apply h
  intro x
  exact Quotient.mk_out (g x)

Is there a computable version of this function? I feel like this is a safe operation but I haven't seen any computable versions...

[Aaron Liu]

No, this is equivalent to a version of the axiom of choice. You can still make it computable, though.

import Mathlib.Data.Quot

unsafe def Quotient.liftFunImpl {s : Setoid α} (f : (β → α) → γ) : (∀ f₁ f₂, (∀ x, f₁ x ≈ f₂ x) → f f₁ = f f₂) →
    (β → Quotient s) → γ := fun _ q => f (fun a => (q a).unquot)

@[implemented_by Quotient.liftFunImpl]
def Quotient.liftFun {s : Setoid α} (f : (β → α) → γ) : (∀ f₁ f₂, (∀ x, f₁ x ≈ f₂ x) → f f₁ = f f₂) →
    (β → Quotient s) → γ := fun _ q => f (fun a => (q a).out)

theorem Quotient.liftFun_mk {s : Setoid α} (f : (β → α) → γ) (h : ∀ f₁ f₂, (∀ x, f₁ x ≈ f₂ x) → f f₁ = f f₂) (g : β → α) :
    Quotient.liftFun f h (fun x => Quotient.mk s (g x)) = f g := by
  unfold liftFun
  apply h
  intro x
  exact Quotient.mk_out (g x)

[Robin Arnez]

Ah, okay, kinda thought that already. I feel like something like this should exist somewhere in mathlib or batteries though (I guess with an unsafe implementation).

[Aaron Liu]

Actually, you might be able to bypass choice with some dependent type casting shenanigans. I don't actually have a proof yet.

[Robin Arnez]

Huh, okay... I mean ideally liftFun_mk would be defeq but I don't think we will get that.

[RustyYato]

Since this came up in another thread, I'll post it here. Quotient.liftFunImpl is not a sound function! And it is not sound to @[implemented_by Quotient.liftFunImpl] def Quotient.liftFun. Here's the contradiction (adapted from leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Should.20we.20merge.20.60Quotient.2Eout.60.20and.20.60Quotient.2Eunquot.60.3F/near/390172207):

import Mathlib.Data.Quot

unsafe def Quotient.liftFunImpl {s : Setoid α} (f : (β → α) → γ) : (∀ f₁ f₂, (∀ x, f₁ x ≈ f₂ x) → f f₁ = f f₂) →
    (β → Quotient s) → γ := fun _ q => f (fun a => (q a).unquot)

@[implemented_by Quotient.liftFunImpl]
def Quotient.liftFun {s : Setoid α} (f : (β → α) → γ) : (∀ f₁ f₂, (∀ x, f₁ x ≈ f₂ x) → f f₁ = f f₂) →
    (β → Quotient s) → γ := fun _ q => f (fun a => (q a).out)

theorem Quotient.liftFun_mk {s : Setoid α} (f : (β → α) → γ) (h : ∀ f₁ f₂, (∀ x, f₁ x ≈ f₂ x) → f f₁ = f f₂) (g : β → α) :
    Quotient.liftFun f h (fun x => Quotient.mk s (g x)) = f g := by
  unfold liftFun
  apply h
  intro x
  exact Quotient.mk_out (g x)

def choice {α β} [S: Setoid β] (f: ∀i: α, Quotient S): Quotient (piSetoid (α := fun _: α => β)) := by
  apply Quotient.liftFun (β := α) (α := β) (s := S) (γ := Quotient piSetoid) ?_ ?_
  assumption
  exact Quotient.mk _
  intro a b eq
  apply Quot.sound
  assumption

def exoticInstance : Decidable True := by
  apply @Quot.recOnSubsingleton _ _ (fun _ => Decidable True)
  -- lift the identity function
  exact (@choice (α := Trunc Bool) (β := Bool) (S := trueSetoid) id)
  intro f
  replace f: Trunc Bool -> Bool := f
  -- since Trunc is subsingleton, f can only take on one value
  -- but we lifted the identity function, which takes on two values
  apply decidable_of_iff (f (Trunc.mk false) = f (Trunc.mk true))
  simp
  congr 1
  apply Subsingleton.allEq

example : @decide True exoticInstance = true  := .trans (by congr) (decide_true _)
example : @decide True exoticInstance = false := by native_decide

#eval exoticInstance -- isFalse _

The problem here is that Trunc Bool has two computationally distict terms (Trunc.mk true and Trunc.mk false), and by lifting the identity function to Trunc (Trunc Bool -> Bool) via Quotient.liftFun. But this function has impossible properties! For example, f (Trunc.mk false) != f (Trunc.mk true). So it's not even a function really, which allows us to prove false (via native_decide to utilize the bad implemented_by attribute)