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

[Edwin Fernando]

I am having some trouble trying to instantiate BIBase in a way I believe is because of iris-lean's sForall type (PROP → Prop) → PROP. I would like to keep the syntax and semantics of PROP (propositions in separation logic), separate. So an excerpt of my instantiation looks like

instance : BIBase (Assertion) where
  Entails P Q    := ∀ s : Store, ∀ : h Heap, P.denote s h → Q.denote s h
  and         := Assertion.and

where denote is a inductively defined on Assertion, defining the satsifiability relation giving semantics to the syntax of Assertions in separation logic. To be clear I define PROP := Assertion. I run into problems defining Assertion though for the sForall and sExists because of positivity.

inductive Assertion : Type
  ...
  | sForall : (Ψ : Assertion → Prop) → Assertion

I want to note that the distinction between the syntax and semantics in Assertion seems standard in separation logic papers. But the classical separation logic example just directly provides the semantics in the BIBase instantiation. I might be able to do this as well which would avoid definition of (syntax) Assertion and the positivity violation entirely. But I don't think this is ideal, the code becomes difficult to write correctly and read, and the split between syntax and semantics aids in understanding of complicated separation logics.

And since sForall is more general than iForall, I'm unable to just define iForall in the syntax instead. I wanted to ask if there's some trivial workaround, whether you think this may be a disadvantage of sForall as (PROP → Prop) → PROP. Happy to provide more info on something in particular and I might just be making a silly mistake

[Michael Sammler]

Indeed, the BI interface assumes that you have impredicative quantification in your logic, which prevents syntactic assertions as far as I can tell. The standard in Iris is to use semantic assertions as shown by the classical separation logic example. I would recommend that you try the semantic approach. It has worked very well for complicated separation logics as shown by Iris / iProp.

[Markus de Medeiros]

@Remy Seassau did some work in this direction, maybe he could chime in?

[Remy Seassau]

Ah yes, we also ran into this issue

[Remy Seassau]

We ended up using a semantic definition of sForall to tie it to our syntactic definition of forall

[Edwin Fernando]

Thank you very much for the answers, and sorry for the late response.

Michael Sammler said:

Indeed, the BI interface assumes that you have impredicative quantification in your logic, which prevents syntactic assertions as far as I can tell. The standard in Iris is to use semantic assertions as shown by the classical separation logic example. I would recommend that you try the semantic approach. It has worked very well for complicated separation logics as shown by Iris / iProp.

Okay I didn't know the direct semantic way (henceforth I'll refer to as deep embedding) is standard and the syntax + semantics way (shallow embedding) is not generally possible. But I still want to try to figure it out to thoroughly understand the technical details. Also I want to note that I only want to use MoSeL, and not the whole of Iris, as that probably makes a difference.

I think there's a way around this impredicativity, by including in the syntax an sForall (lean) or iForall (rocq) constructor. This constructor takes as arguments semantics of other assertions. I think this is exactly what the below approach is

Remy Seassau said:

We ended up using a semantic definition of sForall to tie it to our syntactic definition of forall

I tried something like this already. And the problem I run into is violation of positivity (of inductive definitions).

(original definition)

inductive Assertion : List TyDet → List TyRand → Type
  | iForall : ∀ {α}, (α → Assertion ds rs) → Assertion ds rs

(iris-lean's Set predicate definition)

inductive Assertion : List TyDet → List TyRand → Type
  | sForall : (Assertion ds rs → Prop) → Assertion ds rs

The former compiles and the latter does not: arg #5 of 'Assertion.sForall' has a non positive occurrence of the datatypes being declared. So could you let me know what you had done @Remy Seassau , or just share me a link on GitHub perhaps so I could study an example?