Quot lifting `(_ -> T) -> T` to `(_ -> Q) -> Q`

Stream: general

[Max Nowak 🐉]

Take the following MWE. How do you implement Q.ctor? I haven't played around with Quotients before.

inductive T
| ctor : (Nat -> T) -> T
| ...

inductive Rel : T -> T -> Prop | ...
def Q := Quot Rel
def Q.ctor : (Nat -> Q) -> Q := ?

[Edward van de Meent]

this depends a lot on the Rel you defined.

[Max Nowak 🐉]

I can prove that it is an equivalence relation. Other than that, it's a little complex unfortunately.

[Edward van de Meent]

can you prove that, for example, (\forall n, Rel (f n) (g n)) -> Rel (ctor f) (ctor g)? because if that's not true, there is no clear "natural" implementation.

[Edward van de Meent]

also, if you can prove that the relation is an equivalence relation, better use Quotient for that better API

[Max Nowak 🐉]

Yes I can prove that.

[Max Nowak 🐉]

And yeah I am using Quotient in my own code.

[Edward van de Meent]

by the way, such a function cannot generally be computable, since it requires a choice for every Nat.

[Max Nowak 🐉]

That is fine, this is supposed to be a ctor anyway.

[Edward van de Meent]

here you go:

import Mathlib.Data.Quot

inductive T
| ctor : (Nat -> T) -> T
| nil

noncomputable def Q.ctor (r : Setoid T)
    (hr:∀ (f g : Nat → T), (∀ n, f n ≈ g n) → r (T.ctor f) (T.ctor g)):
    (Nat -> Quotient r) -> Quotient r := fun g =>
  Quotient.lift
    (⟦T.ctor ·⟧ : (Nat → T) → Quotient r)
    (by simp_rw [Quotient.eq]; exact hr)
    (Quotient.choice g)

[Max Nowak 🐉]

I also managed to get the following working:

noncomputable def Q.ctor (r : Setoid T)
  (hr: ∀ (f g : Nat → T), f ≈ g → T.ctor f ≈ T.ctor g)
  (g : Nat -> Quotient r)
  : Quotient r
  := Quotient.lift (fun k => ⟦.ctor k⟧) (fun f g p => Quot.sound (hr f g p)) (Quotient.choice g)

Thanks a ton! :D

[Max Nowak 🐉]

Slightly off-topic, but: Since this is supposed to be a ctor anyway, I don't care about it being noncomputable. I don't want to have to mark any code that uses this ctor as noncomputable however. How do I deal with that?

Right now I'm doing opaque impl := sorry, and then @[implemented_by], but this feels very dirty.

[Edward van de Meent]

Afaik, that's the only way to do this...

[Kim Morrison]

You can write noncomputable theory at the top of every file!

[Eric Wieser]

Edward van de Meent said:

by the way, such a function cannot generally be computable, (since it requires a choice for every Nat)

I know that finite choice can be done computably; can countable choice not also be?

[Johan Commelin]

That's Nat.find

[Yaël Dillies]

No, Johan. Computable choice is (∀ n, Inhabited (α n)) → Inhabited (∀ n, α n). This cannot be done computably

[Johan Commelin]

Ooh, right, I got something mixed up

[Johan Commelin]

And just to clarify. When you write Inhabited, you mean it in the sense it is typically used in type theory lingo. I.e., what we call Trunc in Lean:

import Mathlib

variable (α : Nat → Type)

def countableChoice₁ [∀ n, Inhabited (α n)] : Inhabited (∀ n, α n) :=
  ⟨fun _ ↦ default⟩

def countableChoice₂ [∀ n, Nonempty (α n)] : Nonempty (∀ n, α n) :=
  ⟨fun _ ↦ Classical.choice inferInstance⟩

noncomputable
def countableChoice₃ (h : ∀ n, Trunc (α n)) : Trunc (∀ n, α n) :=
  Trunc.mk fun n ↦ Trunc.out (h n)

#print axioms countableChoice₁ -- 'countableChoice₁' does not depend on any axioms

#print axioms countableChoice₂ -- 'countableChoice₃' depends on axioms: [Classical.choice]

#print axioms countableChoice₃ -- 'countableChoice₃' depends on axioms: [Classical.choice]