add OFEs, later modality

src/Iris/Algebra/OFE.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2023 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Std.Logic
+
+namespace Iris
+
+/-- Ordered family of equivalences -/
+class OFE (α : Type) where
+  Equiv : α → α → Prop
+  Dist : Nat → α → α → Prop
+  equiv_eqv : Equivalence Equiv
+  dist_eqv : Equivalence (Dist n)
+  equiv_dist : Equiv x y ↔ ∀ n, Dist n x y
+  dist_lt : Dist n x y → m < n → Dist m x y
+
+open OFE
+
+scoped infix:25 " ≡ " => OFE.Equiv
+scoped notation x " ≡{" n "}≡ " y:26 => OFE.Dist n x y
+
+namespace OFE
+
+def NonExpansive [OFE α] (f : α → α) :=
+  ∀ n x₁ x₂, x₁ ≡{n}≡ x₂ → f x₁ ≡{n}≡ f x₂
+
+def NonExpansive₂ [OFE α] (f : α → α → α) :=
+  ∀ n x₁ x₂, x₁ ≡{n}≡ x₂ → ∀ y₁ y₂, y₁ ≡{n}≡ y₂ → f x₁ y₁ ≡{n}≡ f x₂ y₂
+
+structure Chain (α : Type) [OFE α] where
+  chain : Nat → α
+  cauchy : n ≤ i → chain i ≡{n}≡ chain n
+
+instance [OFE α] : CoeFun (Chain α) (fun _ => Nat → α) := ⟨Chain.chain⟩
+
+def ofDiscrete (Equiv : α → α → Prop) (equiv_eqv : Equivalence Equiv) : OFE α where
+  Equiv := Equiv
+  Dist _ := Equiv
+  equiv_eqv := equiv_eqv
+  dist_eqv := equiv_eqv
+  equiv_dist := (forall_const _).symm
+  dist_lt h _ := h
+
+end OFE
+
+/-- Complete ordered family of equivalences -/
+class COFE (α : Type) extends OFE α where
+  compl : Chain α → α
+  conv_compl {c : Chain α} : compl c ≡{n}≡ c n
+
+namespace COFE
+
+def ofDiscrete (Equiv : α → α → Prop) (equiv_eqv : Equivalence Equiv) : COFE α :=
+  let _ := OFE.ofDiscrete Equiv equiv_eqv
+  { compl := fun c => c 0
+    conv_compl := fun {_ c} => equiv_eqv.2 (c.cauchy (Nat.zero_le _)) }

src/Iris/BI/BI.lean

@@ -3,15 +3,29 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro
 -/
+import Iris.Algebra.OFE
 import Iris.BI.BIBase
 
 namespace Iris
-open Iris.Std
+open Iris.Std OFE
 open Lean
 
 /-- Require that a separation logic with carrier type `PROP` fulfills all necessary axioms. -/
-class BI (PROP : Type) extends BI.BIBase PROP where
+class BI (PROP : Type) extends COFE PROP, BI.BIBase PROP where
+  Equiv P Q := P ⊣⊢ Q
+
   entails_preorder : Preorder Entails
+  equiv_iff {P Q : PROP} : (P ≡ Q) ↔ P ⊣⊢ Q := by simp
+
+  and_ne : OFE.NonExpansive₂ and
+  or_ne : OFE.NonExpansive₂ or
+  imp_ne : OFE.NonExpansive₂ imp
+  forall_ne {P₁ P₂ : α → PROP} : (∀ x, P₁ x ≡{n}≡ P₂ x) → iprop(∀ x, P₁ x) ≡{n}≡ iprop(∀ x, P₂ x)
+  exists_ne {P₁ P₂ : α → PROP} : (∀ x, P₁ x ≡{n}≡ P₂ x) → iprop(∃ x, P₁ x) ≡{n}≡ iprop(∃ x, P₂ x)
+  sep_ne : OFE.NonExpansive₂ sep
+  wand_ne : OFE.NonExpansive₂ wand
+  persistently_ne : OFE.NonExpansive persistently
+  later_ne : OFE.NonExpansive later
 
   pure_intro {φ : Prop} {P : PROP} : φ → P ⊢ ⌜φ⌝
   pure_elim' {φ : Prop} {P : PROP} : (φ → True ⊢ P) → ⌜φ⌝ ⊢ P
@@ -34,8 +48,7 @@ class BI (PROP : Type) extends BI.BIBase PROP where
   exists_elim {Φ : α → PROP} {Q : PROP} : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q
 
   sep_mono {P P' Q Q' : PROP} : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'
-  emp_sep_1 {P : PROP} : emp ∗ P ⊢ P
-  emp_sep_2 {P : PROP} : P ⊢ emp ∗ P
+  emp_sep {P : PROP} : emp ∗ P ⊣⊢ P
   sep_symm {P Q : PROP} : P ∗ Q ⊢ Q ∗ P
   sep_assoc_l {P Q R : PROP} : (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R)
 
@@ -50,6 +63,15 @@ class BI (PROP : Type) extends BI.BIBase PROP where
   persistently_absorb_l {P Q : PROP} : <pers> P ∗ Q ⊢ <pers> P
   persistently_and_l {P Q : PROP} : <pers> P ∧ Q ⊢ P ∗ Q
 
+  later_mono {P Q : PROP} : (P ⊢ Q) → ▷ P ⊢ ▷ Q
+  later_intro {P : PROP} : P ⊢ ▷ P
+
+  later_forall_2 {Φ : α → PROP} : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a
+  later_exists_false {Φ : α → PROP} : (▷ ∃ a, Φ a) ⊢ ▷ False ∨ ∃ a, ▷ Φ a
+  later_sep {P Q : PROP} : ▷ (P ∗ Q) ⊣⊢ ▷ P ∗ ▷ Q
+  later_persistently {P Q : PROP} : ▷ <pers> P ⊣⊢ <pers> ▷ P
+  later_false_em {P : PROP} : ▷ P ⊢ ▷ False ∨ (▷ False → P)
+
 namespace BI
 
 attribute [instance] BI.entails_preorder

src/Iris/BI/BIBase.lean

@@ -28,6 +28,7 @@ class BIBase (PROP : Type) where
   sep : PROP → PROP → PROP
   wand : PROP → PROP → PROP
   persistently : PROP → PROP
+  later : PROP → PROP
 
 namespace BIBase
 
@@ -45,6 +46,8 @@ syntax:35 term:36 " ∗ " term:35 : term
 syntax:25 term:26 " -∗ " term:25 : term
 /-- Persistency modality. `persistently` is a primitive of BI. -/
 syntax:max "<pers> " term:40 : term
+/-- Later modality. `later` is a primitive of BI. -/
+syntax:max "▷ " term:40 : term
 
 /-- Bidirectional implication on separation logic propositions. -/
 syntax:27 term:28 " ↔ " term:28 : term
@@ -66,6 +69,7 @@ macro_rules
   | `(iprop($P ∗ $Q))   => ``(BIBase.sep iprop($P) iprop($Q))
   | `(iprop($P -∗ $Q))  => ``(BIBase.wand iprop($P) iprop($Q))
   | `(iprop(<pers> $P)) => ``(BIBase.persistently iprop($P))
+  | `(iprop(▷ $P))      => ``(BIBase.later iprop($P))
 
 delab_rule BIBase.emp
   | `($_) => ``(iprop($(mkIdent `emp)))

src/Iris/BI/DerivedLaws.lean

@@ -221,7 +221,6 @@ theorem sep_right_comm [BI PROP] {P Q R : PROP} : (P ∗ Q) ∗ R ⊣⊢ (P ∗
 theorem sep_sep_sep_comm [BI PROP] {P Q R S : PROP} : (P ∗ Q) ∗ (R ∗ S) ⊣⊢ (P ∗ R) ∗ (Q ∗ S) :=
   sep_assoc.trans <| (sep_congr_r sep_left_comm).trans sep_assoc.symm
 
-theorem emp_sep [BI PROP] {P : PROP} : emp ∗ P ⊣⊢ P := ⟨emp_sep_1, emp_sep_2⟩
 instance [BI PROP] : LeftId (α := PROP) BiEntails emp sep := ⟨emp_sep⟩
 
 theorem sep_emp [BI PROP] {P : PROP} : P ∗ emp ⊣⊢ P := sep_comm.trans emp_sep
@@ -236,7 +235,7 @@ instance [BI PROP] : LawfulBigOp sep (emp : PROP) BiEntails where
   left_id := emp_sep
   congr_l := sep_congr_l
 
-theorem true_sep_2 [BI PROP] {P : PROP} : P ⊢ True ∗ P := emp_sep_2.trans (sep_mono_l true_intro)
+theorem true_sep_2 [BI PROP] {P : PROP} : P ⊢ True ∗ P := emp_sep.2.trans (sep_mono_l true_intro)
 
 theorem wand_intro' [BI PROP] {P Q R : PROP} (h : Q ∗ P ⊢ R) : P ⊢ Q -∗ R :=
   wand_intro <| sep_symm.trans h
@@ -263,7 +262,7 @@ theorem sep_exists_l [BI PROP] {P : PROP} {Ψ : α → PROP} : P ∗ (∃ a, Ψ
 theorem sep_exists_r [BI PROP] {Φ : α → PROP} {Q : PROP} : (∃ a, Φ a) ∗ Q ⊣⊢ ∃ a, Φ a ∗ Q :=
   sep_comm.trans <| sep_exists_l.trans <| exists_congr fun _ => sep_comm
 
-theorem wand_rfl [BI PROP] {P : PROP} : ⊢ P -∗ P := wand_intro emp_sep_1
+theorem wand_rfl [BI PROP] {P : PROP} : ⊢ P -∗ P := wand_intro emp_sep.1
 
 @[rw_mono_rule]
 theorem wandIff_congr [BI PROP] {P P' Q Q' : PROP} (h1 : P ⊣⊢ Q) (h2 : P' ⊣⊢ Q') :
@@ -278,10 +277,10 @@ theorem wandIff_congr_r [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : (P ∗-∗
 theorem wandIff_refl [BI PROP] {P : PROP} : ⊢ P ∗-∗ P := and_intro wand_rfl wand_rfl
 
 theorem wand_entails [BI PROP] {P Q : PROP} (h : ⊢ P -∗ Q) : P ⊢ Q :=
-  emp_sep_2.trans (wand_elim h)
+  emp_sep.2.trans (wand_elim h)
 
 theorem entails_wand [BI PROP] {P Q : PROP} (h : P ⊢ Q) : ⊢ P -∗ Q :=
-  wand_intro (emp_sep_1.trans h)
+  wand_intro (emp_sep.1.trans h)
 
 theorem equiv_wandIff [BI PROP] {P Q : PROP} (h : P ⊣⊢ Q) : ⊢ P ∗-∗ Q :=
   wandIff_refl.trans (wandIff_congr_l h).2

src/Iris/Instances/Classical/Instance.lean

@@ -3,11 +3,13 @@ Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König
 -/
+import Std.Tactic.RCases
 import Iris.BI
 import Iris.Instances.Data
+import Iris.Std.Equivalence
 
 namespace Iris.Instances.Classical
-open Iris.BI Iris.Instances.Data
+open Iris.BI Iris.Instances.Data Std
 
 /- Instance of `BIBase` and `BI` for classical (non-affine) separation logic. -/
 
@@ -25,28 +27,41 @@ instance : BIBase (HeapProp Val) where
   sep P Q        σ := ∃ σ1 σ2, σ = σ1 ∪ σ2 ∧ σ1 || σ2 ∧ P σ1 ∧ Q σ2
   wand P Q       σ := ∀ σ', σ || σ' → P σ' → Q (σ ∪ σ')
   persistently P _ := P ∅
+  later P        σ := P σ
 
-instance : BI (HeapProp Val) where
-  entails_preorder.refl := by
-      simp only [BI.Entails]
-      intro _ _ h
-      exact h
-  entails_preorder.trans := by
-      simp only [BI.Entails]
-      intro _ _ _ h_xy h_yz σ h_x
-      apply h_yz σ
-      apply h_xy σ
-      exact h_x
-
-  pure_intro := by
-    simp only [BI.Entails, BI.pure]
-    intro _ _ h _ _
+instance : Std.Preorder (Entails (PROP := HeapProp Val)) where
+  refl := by
+    simp only [BI.Entails]
+    intro _ _ h
     exact h
-  pure_elim' := by
-    simp only [BI.Entails, BI.pure]
-    intro _ _ h_φP σ h_φ
-    apply h_φP h_φ σ
-    simp
+  trans := by
+    simp only [BI.Entails]
+    intro _ _ _ h_xy h_yz σ h_x
+    apply h_yz σ
+    apply h_xy σ
+    exact h_x
+
+instance : BI (HeapProp Val) where
+  toCOFE := COFE.ofDiscrete Eq equivalence_eq
+
+  entails_preorder := by infer_instance
+  equiv_iff {P Q} := ⟨
+    fun h : P = Q => h ▸ ⟨refl, refl⟩,
+    fun ⟨h₁, h₂⟩ => funext fun σ => propext ⟨h₁ σ, h₂ σ⟩
+  ⟩
+
+  and_ne          := by rintro _ _ _ rfl _ _ rfl; rfl
+  or_ne           := by rintro _ _ _ rfl _ _ rfl; rfl
+  imp_ne          := by rintro _ _ _ rfl _ _ rfl; rfl
+  sep_ne          := by rintro _ _ _ rfl _ _ rfl; rfl
+  wand_ne         := by rintro _ _ _ rfl _ _ rfl; rfl
+  persistently_ne := by rintro _ _ _ rfl; rfl
+  later_ne        := by rintro _ _ _ rfl; rfl
+  forall_ne {_ _ P Q} h := (funext h : P = Q) ▸ rfl
+  exists_ne {_ _ P Q} h := (funext h : P = Q) ▸ rfl
+
+  pure_intro h _ _ := h
+  pure_elim' h_φP σ h_φ := h_φP h_φ σ ⟨⟩
 
   and_elim_l := by
     intros
@@ -123,16 +138,16 @@ instance : BI (HeapProp Val) where
     constructor
     · exact h_PQ σ₁ h_P
     · exact h_P'Q' σ₂ h_P'
-  emp_sep_1 := by
+  emp_sep.mp := by
     simp only [BI.Entails, BI.sep, BI.emp]
-    intro _ _ ⟨σ₁, σ₂, h_union, _, h_emp, h_P⟩
+    intro _ ⟨σ₁, σ₂, h_union, _, h_emp, h_P⟩
     rw [h_emp] at h_union
     rw [← empty_union] at h_union
     rw [h_union]
     exact h_P
-  emp_sep_2 := by
+  emp_sep.mpr := by
     simp only [BI.Entails, BI.sep, BI.emp]
-    intro _ σ h_P
+    intro σ h_P
     apply Exists.intro ∅
     apply Exists.intro σ
     constructor
@@ -240,4 +255,10 @@ instance : BI (HeapProp Val) where
     · exact h_P
     · exact h_Q
 
-end Iris.Instances.Classical
+  later_mono := id
+  later_intro _ := id
+  later_forall_2 _ := id
+  later_exists_false _ h := .inr h
+  later_sep := ⟨fun _ => id, fun _ => id⟩
+  later_persistently := ⟨fun _ => id, fun _ => id⟩
+  later_false_em _ h := .inr fun _ => h

src/Iris/Std/Equivalence.lean

@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2023 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+
+theorem equivalence_eq : Equivalence (@Eq α) := ⟨.refl, .symm, .trans⟩