Why are sForall and sExists defined the way they are?

Stream: iris-lean

[Markus de Medeiros]

Anyone have any clue why sForall and sExists in BIBase are defined like

  sForall : (PROP → Prop) → PROP
  sExists : (PROP → Prop) → PROP

instead of the way it's done in König's thesis as well as Rocq Iris?

  sForall {A} : (A → PROP) → PROP
  sExists {A} : (A → PROP) → PROP

[Mario Carneiro]

The reason for this is because the type of {A} there is hidden and important

[Mario Carneiro]

it's {A : Type u}, and it causes a universe bump in BIBase and also restricts the usage of forall to that particular type universe

[Mario Carneiro]

this is actually a problem in iris as well, it's just more well hidden there because of the use of template universe polymorphism

[Mario Carneiro]

by using sets instead and defining indexed forall in terms of set forall, it's possible to get the best of both worlds: no universe bump and you can index over types in any universe, even larger than the BIBase itself

[Mario Carneiro]

We have analogous difficulties when defining complete lattices in mathlib

[Markus de Medeiros]

Okay, cool. Am I understanding correctly that the "set" in the "set forall" is analogous to image of the function in the "Rocq forall"?

[Mario Carneiro]

yes

[Markus de Medeiros]

For posterity: Here is a concrete #mwe demonstrating a universe problem present in the indexed representation that is not present in the set-based representation:

namespace Indexed
/- Indexed quantifiers -/

class BI (PROP : Type _) : Type _ where
  iQuantifier {A : Type _} : (A → PROP) → PROP

#check BI             -- Indexed.BI.{u_1, u_2} (PROP : Type u_1) : Type (max u_1 (u_2 + 1))
#check BI.iQuantifier -- Indexed.BI.iQuantifier.{u_1, u_2} {PROP : Type u_1} [self : BI PROP] {A : Type u_2} : (A → PROP) → PROP

variable (PROP : Type 3) [BI PROP]
variable (X : Type 2) (Y : Type 2) (d : X → PROP)

#check BI.iQuantifier (fun y : Y => BI.iQuantifier d)
-- Breaks when the universes for X and Y disagree

end Indexed

namespace Set
/- Set-based quantifiers -/

class BI (PROP : Type _) : Type _ where
  sQuantifier : (PROP → Prop) → PROP

def BI.iQuantifier {PROP : Type _} [BI PROP] {ι : Type _} (I : ι → PROP) : PROP :=
  BI.sQuantifier (fun P => ∃ i : ι, I i = P)

#check BI              -- Set.BI.{u_1} (PROP : Type u_1) : Type u_1
#check BI.sQuantifier  -- Set.BI.sQuantifier.{u_1} {PROP : Type u_1} [self : BI PROP] : (PROP → Prop) → PROP
#check BI.iQuantifier  -- Set.BI.iQuantifier.{u_1, u_2} {PROP : Type u_1} [BI PROP] {ι : Type u_2} (I : ι → PROP) : PROP

variable (PROP : Type 1) [BI PROP]
variable (X : Type 2) (Y : Type 6) (d : X → PROP)

#check BI.iQuantifier (fun y : Y => BI.iQuantifier d)
-- Works no matter the universe levels for X, Y and PROP

end Set

[Alex Bai]

also FYI https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1111