Iprop logic

src/Iris/Algebra/CMRA.lean

@@ -680,8 +680,8 @@ instance empty_cancelable : Cancelable (unit : α) where
     _ ≡{n}≡ unit • t := e
     _ ≡{n}≡ t := unit_left_id.dist
 
-theorem dst_incN {n} {x y : α} (H : y ≡{n}≡ x) : x ≼{n} y :=
-  ⟨unit, H.trans (equiv_dist.mp unit_right_id n).symm⟩
+theorem _root_.Iris.OFE.Dist.to_incN {n} {x y : α} (H : x ≡{n}≡ y) : x ≼{n} y :=
+  ⟨unit, ((equiv_dist.mp unit_right_id n).trans H).symm⟩
 
 end ucmra
 

src/Iris/Algebra/IProp.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2025 Markus de Medeiros. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+
+import Iris.Algebra.CMRA
+import Iris.Algebra.OFE
+import Iris.Algebra.UPred
+import Iris.Algebra.COFESolver
+import Init.Data.Vector
+
+namespace Iris
+
+def GFunctors := Array COFE.OFunctorPre
+
+def GId (FF : GFunctors) : Type _ := Fin FF.size
+
+instance (FF : GFunctors) : GetElem GFunctors (GId FF) COFE.OFunctorPre (fun _ _ => True) where
+  getElem _ x _ := (show Array _ from FF)[x.1]
+
+abbrev IsGFunctors (G : GFunctors) := ∀ (i : GId G), RFunctorContractive G[i]
+
+def SubG (FF₁ FF₂ : GFunctors) : Prop :=
+  ∀ i : GId FF₁, ∃ j : GId FF₂, FF₁[i] = FF₂[j]
+
+def GName := LeibnizO Nat
+
+abbrev IResF (FF : GFunctors) : COFE.OFunctorPre :=
+  DiscreteFunOF (fun i : GId FF => GenMapOF GName FF[i])
+
+section IProp
+open COFE
+
+variable (FF : GFunctors) [IG : IsGFunctors FF]
+
+def iPrePropO : Type _ := OFunctor.Fix (UPredOF (IResF FF))
+
+instance : COFE (iPrePropO FF) := inferInstanceAs (COFE (OFunctor.Fix _))
+
+def IResUR : Type := (i : GId FF) → GName → Option (FF[i] (iPrePropO FF) (iPrePropO FF))
+
+instance : UCMRA (IResUR FF) :=
+  ucmraDiscreteFunO (β := fun (i : GId FF) => GName → Option (FF[i] (iPrePropO FF) (iPrePropO FF)))
+
+abbrev IProp := UPred (IResUR FF)
+
+end IProp
+end Iris

src/Iris/Algebra/UPred.lean

@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2025 Markus de Medeiros. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+
+import Iris.Algebra.CMRA
+import Iris.Algebra.OFE
+
+namespace Iris
+open CMRA
+
+/-- The data of a UPred object is an indexed proposition over M (Bundled version) -/
+@[ext]
+structure UPred (M : Type _) [UCMRA M] where
+  holds : Nat → M → Prop
+  mono {n1 n2 x1 x2} : holds n1 x1 → x1 ≼{n2} x2 → n2 ≤ n1 → holds n2 x2
+
+instance [UCMRA M] : Inhabited (UPred M) :=
+  ⟨fun _ _ => True, fun _ _ _ => ⟨⟩⟩
+
+instance [UCMRA M] : CoeFun (UPred M) (fun _ => Nat → M → Prop) where
+  coe x := x.holds
+
+section UPred
+
+variable {M : Type} [UCMRA M]
+
+open UPred
+
+instance : OFE (UPred M) where
+  Equiv P Q := ∀ n x, ✓{n} x → (P n x ↔ Q n x)
+  Dist n P Q := ∀ n' x, n' ≤ n → ✓{n'} x → (P n' x ↔ Q n' x)
+  dist_eqv := {
+    refl _ _ _ _ _ := .rfl
+    symm H _ _ A B := (H _ _ A B).symm
+    trans H1 H2 _ _ A B := (H1 _ _ A B).trans (H2 _ _ A B) }
+  equiv_dist := ⟨
+    fun Heqv _ _ _ _ Hvalid => Heqv _ _ Hvalid,
+    fun Hdist _ _ Hvalid => Hdist _ _ _ (Nat.le_refl _) Hvalid⟩
+  dist_lt Hdist Hlt _ _ Hle Hvalid :=
+    Hdist _ _ (Nat.le_trans Hle (Nat.le_of_succ_le Hlt)) Hvalid
+
+theorem uPred_ne {P : UPred M} {n} {m₁ m₂} (H : m₁ ≡{n}≡ m₂) : P n m₁ ↔ P n m₂ :=
+  ⟨fun H' => P.mono H' H.to_incN (Nat.le_refl _),
+   fun H' => P.mono H' H.symm.to_incN (Nat.le_refl _)⟩
+
+theorem uPred_proper {P : UPred M} {n} {m₁ m₂} (H : m₁ ≡ m₂) : P n m₁ ↔ P n m₂ :=
+  uPred_ne H.dist
+
+theorem uPred_holds_ne {P Q : UPred M} {n₁ n₂ x}
+    (HPQ : P ≡{n₂}≡ Q) (Hn : n₂ ≤ n₁) (Hx : ✓{n₂} x) (HQ : Q n₁ x) : P n₂ x :=
+  (HPQ _ _ (Nat.le_refl _) Hx).mpr (Q.mono HQ .rfl Hn)
+
+instance : IsCOFE (UPred M) where
+  compl c := {
+    holds n x := ∀ n', n' ≤ n → ✓{n'} x → (c n') n' x
+    mono {n1 n2 x1 x2 HP Hx12 Hn12 n3 Hn23 Hv} := by
+      refine mono _ ?_ (Hx12.le Hn23) (Nat.le_refl _)
+      exact HP _ (Nat.le_trans Hn23 Hn12) ((Hx12.le Hn23).validN Hv) }
+  conv_compl {n c i x} Hin Hv := by
+    refine .trans ?_ (c.cauchy Hin _ _ (Nat.le_refl _) Hv).symm
+    refine ⟨fun H => H _ (Nat.le_refl _) Hv, fun H n' Hn' Hv' => ?_⟩
+    exact (c.cauchy Hn' _ _ (Nat.le_refl _) Hv').mp (mono _ H .rfl Hn')
+
+abbrev UPredOF (F : COFE.OFunctorPre) [URFunctor F] : COFE.OFunctorPre :=
+  fun A B _ _ => UPred (F B A)
+
+def uPred_map [UCMRA α] [UCMRA β] (f : β -C> α) : UPred α -n> UPred β := by
+  refine ⟨fun P => ⟨fun n x => P n (f x), ?_⟩, ⟨?_⟩⟩
+  · intro n1 n2 x1 x2 HP Hm Hn
+    exact P.mono HP (f.monoN _ Hm) Hn
+  · intro n x1 x2 Hx1x2 n' y Hn' Hv
+    exact Hx1x2 _ _ Hn' (f.validN Hv)
+
+instance [URFunctor F] : COFE.OFunctor (UPredOF F) where
+  cofe := inferInstance
+  map f g := uPred_map (URFunctor.map (F := F) g f)
+  map_ne.ne _ _ _ Hx _ _ Hy _ _ z2 Hn _ :=
+    uPred_ne <| URFunctor.map_ne.ne (Hy.le Hn) (Hx.le Hn) z2
+  map_id _ _ z _ := uPred_proper <| URFunctor.map_id z
+  map_comp f g f' g' _ _ H _ := uPred_proper <| URFunctor.map_comp g' f' g f H
+
+instance [URFunctorContractive F] : COFE.OFunctorContractive (UPredOF F) where
+  map_contractive.1 {_ x y} HKL _ _ _ Hn _ := by
+    refine uPred_ne <| (URFunctorContractive.map_contractive.1
+      (x := (x.snd, x.fst)) (y := (y.snd, y.fst)) ?_ _).le Hn
+    exact fun m Hm => ⟨(HKL m Hm).2, (HKL m Hm).1⟩
+
+end UPred

src/Iris/Examples/Resources.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2025 Markus de Medeiros. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+import Iris.BI
+import Iris.ProofMode
+import Iris.Algebra.IProp
+import Iris.Instances.UPred.Instance
+import Iris.Algebra.Agree
+
+namespace Iris.Examples
+open Iris.BI
+
+section no_resources
+
+abbrev FF0 : GFunctors := #[]
+
+local instance : IsGFunctors FF0 := nofun
+
+-- A proof with no resources
+example (P Q : IProp FF0) : P ∗ Q ⊢ ⌜True⌝ := by
+  iintro ⟨HP, HQ⟩
+  ipure_intro
+  trivial
+
+example (P Q : IProp FF0) : P ∗ Q ⊢ P := by
+  iintro ⟨HP, HQ⟩
+  iexact HP
+
+end no_resources
+
+section const_agree
+
+abbrev FF1 : GFunctors := #[COFE.constOF (Agree (LeibnizO String))]
+abbrev γ : GId FF1 := ⟨0, Nat.zero_lt_succ _⟩
+theorem HγE  (i : GId FF1) : i = γ := by unfold γ; cases i; congr; apply Nat.lt_one_iff.mp; trivial
+theorem HγLookup : FF1[γ] = COFE.constOF (Agree (LeibnizO String)) := rfl
+local instance : IsGFunctors FF1 := fun i => by rw [HγE i, HγLookup]; infer_instance
+
+@[simp]
+def MyAg (S : String) : Agree (LeibnizO String) := ⟨[⟨S⟩], by simp⟩
+
+@[simp]
+def MyR (S : String) : IResUR FF1 := fun i _ => some (HγE i ▸ MyAg S)
+
+theorem MyR_always_invalid (S₁ S₂ : String) (Hne : S₁ ≠ S₂) (n : Nat) : ¬✓{n} MyR S₁ • MyR S₂ := by
+  simp [CMRA.op, CMRA.ValidN]
+  exists γ, ⟨0⟩
+  rw [← HγE ⟨Nat.zero, Nat.le.refl⟩]
+  simp [instIsGFunctorsFF1, CMRA.ValidN, CMRA.op, Agree.op, Agree.validN,
+        instCOFELeibnizO, COFE.ofDiscrete, OFE.ofDiscrete, optionOp, optionValidN]
+  exact fun a => id (Ne.symm Hne)
+
+def AgreeString (S : String) : IProp FF1 := UPred.ownM (MyR S)
+
+example : AgreeString "I <3 iris-lean!" ⊢ (AgreeString "I don't :<" -∗ False) := by
+  iintro H H2
+  istop
+  apply (UPred.ownM_op _ _).2.trans    -- Combine ghost state
+  apply (UPred.ownM_valid _).trans     -- Reduce to invalidity
+  apply UPred.ownM_always_invalid_elim -- The resource is invalid
+  apply MyR_always_invalid; simp       -- Simplify
+
+end const_agree
+end Iris.Examples

src/Iris/Instances/UPred.lean

@@ -0,0 +1 @@
+import Iris.Instances.UPred.Instance