potential finChoice optimization

Stream: lean4

[RustyYato]

This is kind of a follow up to:
#mathlib4 > Should we merge `Quotient.out` and `Quotient.unquot`? @ 💬

I'm defining a version of Fintype which instead works on bijections on Fin n (this should be theoretically equivalent to Mathlib's Fintype, but would have a much smaller memory footprint), and I want to implement finChoice but without needing to collect all the quotients into a list, since that would defeat the purpose of by change (the memory footprint would be large for large types).
So, what I've done is write a function like this:

def finChoice'
  {α: Fin n -> Type _}
  {S: ∀i, Setoid (α i)}
  (f: (∀i, α i) -> β) (resp: ∀a b: ∀i, α i, (∀i, a i ≈ b i) -> f a = f b)
  (q: ∀i, Quotient (S i)) : β

and an unsafe version

unsafe def unsafeFinChoice
  {α: Fin n -> Type*}
  {S: ∀i, Setoid (α i)}
  (f: (∀i, α i) -> β) (_resp: ∀a b: ∀i, α i, (∀i, a i ≈ b i) -> f a = f b)
  (q: ∀i, Quotient (S i)) : β := f (fun i => (q i).lift id lcProof)

now I want to know if it is safe to add @[implemented_by unsafeFinChoice] def finChoice' ....

From the previous thread, it looks like the issue was that Trunc Bool has two non-defeq terms, that compare equal
and this means that (f: ∀i: Trunc Bool, α i) could take on two values depending on which term was actually
being represented. But that shouldn't be possible for (f: ∀i, Fin n, α i), so I think this should be safe.

[RustyYato]

I was able to use this to generate an optimized version of finChoice for my bijection based Fintype.
Then I tried to break this impl using exoticInstance: Decable True from the previous thread, but the instance works correctly (native_decide proves that @decide True exoticInstance = true).

[Mario Carneiro]

yes, it's provable.

import Mathlib.Data.Quot
import Mathlib.Tactic.GeneralizeProofs

unsafe def unsafeFinChoice {n β}
  {α: Fin n → Type u}
  {S: ∀i, Setoid (α i)}
  (f: (∀i, α i) → β) (_resp: ∀a b, a ≈ b → f a = f b)
  (q: ∀i, Quotient (S i)) : β := f (fun i => (q i).lift id lcProof)

@[implemented_by unsafeFinChoice]
def finChoice' {n β}
    {α: Fin n → Type u}
    {S: ∀i, Setoid (α i)}
    (f: (∀i, α i) → β) (resp: ∀a b, a ≈ b → f a = f b)
    (q: ∀i, Quotient (S i)) : β :=
  (go n (Nat.le_refl _)).lift (fun g => f fun i => g i i.2) fun a b h => by
    exact resp _ _ fun i => h i i.2
where
  go (a) (h : a ≤ n) : @Quotient (∀i, i.1 < a → α i) inferInstance :=
    match a with
    | 0 => ⟦nofun⟧
    | a + 1 => by
      refine (go a (Nat.le_of_lt h)).lift₂ (q₂ := q ⟨a, h⟩) ?_ ?_
      · refine fun g b => ⟦fun i hi => ?_⟧
        if h' : i.1 < a then exact g _ h'
        else
          have : i = ⟨a, h⟩ := Fin.ext <| (Nat.lt_succ_iff_lt_or_eq.1 hi).resolve_left h'
          exact this ▸ b
      · intro b1 f1 b2 f2 eqb eqf
        refine Quotient.sound fun i hi => ?_
        split
        · apply eqb
        · dsimp; generalize_proofs p; subst p; exact eqf

[RustyYato]

Yes, I know that is provable. My question is whether the implemented_by is actually safe, since unsafeFinChoice basically just unwraps the quotient without any checks. I think it should be safe, but I wasn't sure.

[Edward van de Meent]

If you think these are equal, just prove finChoice' = unsafeFinChoice, check no unsafe axioms were used, and mark the lemma with csimp

[Edward van de Meent]

That, in theory, should make sure that evaluation/compilation uses the unsafe version for evaluation in a sound way

[Robin Arnez]

This is very similar to this: #Is there code for X? > Lifting a quotient function @ 💬 which is as far as I know, sound

[Mario Carneiro]

Edward van de Meent said:

If you think these are equal, just prove finChoice' = unsafeFinChoice, check no unsafe axioms were used, and mark the lemma with csimp

You can't prove finChoice' = unsafeFinChoice directly because unsafeFinChoice is unsafe - it doesn't make much sense to reason about the expression without breaking the logic

[Mario Carneiro]

however you can characterize it uniquely: it's Quotient.lift applied to a quotient value which is the pointwise lift of q

[RustyYato]

Robin Arnez said:

This is very similar to this: #Is there code for X? > Lifting a quotient function @ 💬 which is as far as I know, sound

No, that function (with the implemented_by) is not sound. We can see that by adapting @Mario Carneiro 's exoticInstance from the thread linked in my OP

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 _

[RustyYato]

In fact it's because of problems like this that I'm asking this question. I think this should be safe if you are lifting Fin n -> Quotient _ (and probably even Nat -> Quotient _) since Fin n and Nat are canonical representations, but something like Trunc α -> Quotient _ for nontrivial α is not safe since you have two computationally distinct terms for Trunc α, which causes issues. (it needs to be normalized in some way).