feat: add weakest precondition

Iris/Iris/Algebra/OFE.lean

@@ -275,6 +275,13 @@ infixr:25 " -c> " => ContractiveHom
 instance [OFE α] [OFE β] : CoeFun (α -c> β) (fun _ => α → β) := ⟨fun x => x.toHom.f⟩
 instance [OFE α] [OFE β] (f : α -c> β) : Contractive f := f.contractive
 
+def _root_.Function.toContractiveHom (f : α → β) [OFE α] [OFE β] [ι : OFE.Contractive f] : α -c> β where
+  f := f
+  contractive := ι
+
+@[simp] theorem _root_.Function.toContractiveHom_apply {f : α → β} [OFE α] [OFE β] [ι : OFE.Contractive f] {x} :
+  f.toContractiveHom x = f x := by rfl
+
 theorem InvImage.equivalence {α : Sort u} {β : Sort v}
     {r : β → β → Prop} {f : α → β} (H : Equivalence r) : Equivalence (InvImage r f) where
   refl _ := H.refl _
@@ -1770,4 +1777,3 @@ theorem OFE.cast_dist [Iα : OFE α] [Iβ : OFE β] {x y : α}
     (Ht : α = β) (HIt : Iα = Ht ▸ Iβ)  (H : x ≡{n}≡ y) :
     (Ht ▸ x) ≡{n}≡ (Ht ▸ y) := by
   subst Ht; subst HIt; exact H
-

Iris/Iris/BI/Updates.lean

@@ -105,7 +105,7 @@ class BIUpdate (PROP : Type _) [BI PROP] extends BUpd PROP where
   frame_r {P R : PROP} : (|==> P) ∗ R ⊢ |==> (P ∗ R)
 
 class BIFUpdate (PROP : Type _) [BI PROP] extends FUpd PROP where
-  [ne {E1 E2 : CoPset} : OFE.NonExpansive (FUpd.fupd E1 E2 (PROP := PROP))]
+  [ne {E1 E2 : CoPset} : OFE.NonExpansive (iprop(|={E1,E2}=> · : PROP))]
   subset {E1 E2 : CoPset} : E2 ⊆ E1 → ⊢ |={E1,E2}=> |={E2,E1}=> (emp : PROP)
   except0 {E1 E2 : CoPset} {P : PROP} : (◇ |={E1,E2}=> P) ⊢ |={E1,E2}=> P
   mono {E1 E2 : CoPset} {P Q : PROP} : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q
@@ -200,25 +200,32 @@ variable [BI PROP] [BIFUpdate PROP]
 
 open BIFUpdate LawfulSet
 
-theorem fupd_mask_intro_subseteq {E1 E2 : CoPset} {P : PROP} : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P :=
-  λ h => (emp_sep.2.trans <| sep_mono_l <| subset h).trans <|
+theorem fupd_mask_intro_subseteq {E1 E2 : CoPset} {P : PROP} (h : E2 ⊆ E1) :
+    P ⊢ |={E1,E2}=> |={E2,E1}=> P :=
+  (emp_sep.2.trans <| sep_mono_l <| subset h).trans <|
     frame_r.trans <| mono <| frame_r.trans <| mono emp_sep.1
 
+@[rocq_alias fupd_mask_subseteq]
+theorem fupd_mask_subseteq {E1 E2 : CoPset} (h : E2 ⊆ E1) : ⊢@{PROP} |={E1,E2}=> |={E2,E1}=> emp :=
+  fupd_mask_intro_subseteq h
+
 theorem fupd_intro {E : CoPset} {P : PROP} : P ⊢ |={E}=> P :=
   (fupd_mask_intro_subseteq λ _ => id).trans trans
 
 -- Introduction lemma for a mask-chaging fupd
-theorem fupd_mask_intro {E1 E2 : CoPset} {P : PROP} :
-    E2 ⊆ E1 → ((|={E2,E1}=> emp) -∗ P) ⊢ |={E1,E2}=> P :=
-  λ h => (wand_mono_r fupd_intro).trans <|
+theorem fupd_mask_intro {E1 E2 : CoPset} {P : PROP} (h : E2 ⊆ E1) :
+  ((|={E2,E1}=> emp) -∗ P) ⊢ |={E1,E2}=> P :=
+  (wand_mono_r fupd_intro).trans <|
     (emp_sep.2.trans <| sep_mono_l <| subset h).trans <|
     frame_r.trans <| (mono wand_elim_r).trans trans
 
-theorem fupd_mask_intro_discard {E1 E2 : CoPset} {P : PROP} [Absorbing P] : E2 ⊆ E1 → P ⊢ |={E1,E2}=> P :=
-  λ h => (wand_intro' sep_elim_r).trans <| fupd_mask_intro h
+theorem fupd_mask_intro_discard {E1 E2 : CoPset} {P : PROP} [Absorbing P] (h : E2 ⊆ E1) :
+    P ⊢ |={E1,E2}=> P :=
+  (wand_intro' sep_elim_r).trans <| fupd_mask_intro h
 
-theorem fupd_elim {E1 E2 E3 : CoPset} {P Q : PROP} : (Q ⊢ |={E2,E3}=> P) → (|={E1,E2}=> Q) ⊢ |={E1,E3}=> P :=
-  λ h => (mono h).trans trans
+theorem fupd_elim {E1 E2 E3 : CoPset} {P Q : PROP} (h : Q ⊢ |={E2,E3}=> P) :
+    (|={E1,E2}=> Q) ⊢ |={E1,E3}=> P :=
+  (mono h).trans trans
 
 theorem fupd_frame_l {E1 E2 : CoPset} {P Q : PROP} : P ∗ (|={E1,E2}=> Q) ⊢ |={E1,E2}=> P ∗ Q :=
   sep_symm.trans <| frame_r.trans <| mono sep_symm
@@ -311,6 +318,78 @@ variable [BI PROP] [BIFUpdate PROP]
 
 open BIFUpdate LawfulSet
 
+theorem step_fupdN_contractive {E1 E2 : CoPset} {n : Nat} [ι : BILaterContractive PROP] :
+    OFE.Contractive (iprop(|={E1}[E2]▷=>^[n + 1] · : PROP)) where
+  distLater_dist {i x y} xy_i := by
+    induction n with
+    | zero => exact ne.ne (ι.distLater_dist (ne.ne <| xy_i · ·))
+    | succ n IH => exact ne.ne (later_ne.ne (ne.ne IH))
+
+theorem step_fupdN_ne {E1 E2 : CoPset} {n : Nat} :
+    OFE.NonExpansive (iprop(|={E1}[E2]▷=>^[n] · : PROP)) where
+  ne {i x y} xy_i := by
+    induction n with
+    | zero => simp [Nat.repeat, xy_i]
+    | succ n IH => exact ne.ne (later_ne.ne (ne.ne IH))
+
+@[rocq_alias step_fupdN_wand]
+theorem step_fupdN_wand {Eo Ei : CoPset} {n : Nat} {P Q : PROP} :
+    (|={Eo}[Ei]▷=>^[n] P) ⊢ (P -∗ Q) -∗ (|={Eo}[Ei]▷=>^[n] Q) := by
+  refine wand_intro' ?_
+  induction n with
+  | zero =>
+    exact wand_elim_l
+  | succ n IH =>
+    calc iprop((P -∗ Q) ∗ |={Eo,Ei}=> ▷ |={Ei,Eo}=> _)
+      _ ⊢ |={Eo,Ei}=> (P -∗ Q) ∗ ▷ |={Ei,Eo}=> _  := (fupd_frame_l ..)
+      _ ⊢ |={Eo,Ei}=> (▷ (P -∗ Q)) ∗ ▷ |={Ei,Eo}=> _  := mono (sep_mono (later_intro) .rfl)
+      _ ⊢ |={Eo,Ei}=> ▷ ((P -∗ Q) ∗ |={Ei,Eo}=> _) := mono (later_sep.2)
+      _ ⊢ |={Eo,Ei}=> ▷ |={Ei,Eo}=> ((P -∗ Q) ∗ _) := mono (later_mono (fupd_frame_l ..))
+      _ ⊢ |={Eo,Ei}=> ▷ |={Ei,Eo}=> _ := mono (later_mono (mono IH))
+
+@[rocq_alias step_fupd_wand]
+theorem step_fupd_wand {Eo Ei : CoPset} {P Q : PROP} :
+    (|={Eo}[Ei]▷=> P) ⊢ (P -∗ Q) -∗ (|={Eo}[Ei]▷=> Q) :=
+  step_fupdN_wand (n := 1)
+
+@[rocq_alias step_fupd_mask_mono]
+theorem step_fupd_mask_mono {Eo₁ Eo₂ Ei₁ Ei₂ : CoPset} {P : PROP}
+    (Ei₂_Ei₁ : Ei₂ ⊆ Ei₁) (Eo₁_Eo₂ : Eo₁ ⊆ Eo₂) :
+    (|={Eo₁}[Ei₁]▷=> P) ⊢ |={Eo₂}[Ei₂]▷=> P := by
+  refine emp_sep.2.trans ?_
+  refine (sep_mono (fupd_mask_intro_subseteq Eo₁_Eo₂) .rfl).trans ?_
+  refine fupd_frame_r.trans ?_
+  refine BI.Entails.trans (mono ?_) (trans (E2 := Eo₁))
+  refine fupd_frame_l.trans ?_
+  refine BI.Entails.trans (mono ?_) (trans (E2 := Ei₁))
+  refine (sep_mono (fupd_mask_intro_subseteq Ei₂_Ei₁) .rfl).trans ?_
+  refine fupd_frame_r.trans ?_
+  refine mono ?_
+  refine (sep_mono later_intro .rfl).trans ?_
+  refine later_sep.2.trans ?_
+  refine later_mono ?_
+  refine  fupd_frame_r.trans ?_
+  refine BI.Entails.trans (mono ?_) (trans (E2 := Ei₁))
+  refine fupd_frame_l.trans ?_
+  refine BI.Entails.trans (mono ?_) (trans (E2 := Eo₁))
+  refine fupd_frame_r.trans ?_
+  exact mono emp_sep.1
+
+@[rocq_alias step_fupd_intro]
+theorem step_fupd_intro {Ei Eo : CoPset} {P : PROP} (Ei_Eo : Ei ⊆ Eo) :
+    ▷ P ⊢ |={Eo}[Ei]▷=> P := by
+  calc iprop(▷ P)
+    _ ⊢ |={Ei}=> ▷ P := fupd_intro
+    _ ⊢ |={Ei}[Ei]▷=> P := mono <| later_mono fupd_intro
+    _ ⊢ |={Eo}[Ei]▷=> P := step_fupd_mask_mono (subset_refl) Ei_Eo
+
+@[rocq_alias step_fupdN_le]
+theorem step_fupdN_le {n m : Nat} {Eo Ei : CoPset} {P : PROP} :
+    n ≤ m → Ei ⊆ Eo → (|={Eo}[Ei]▷=>^[n] P) ⊢ |={Eo}[Ei]▷=>^[m] P
+  | .refl, _ => .rfl
+  | .step (m := m) n_m, Ei_Eo =>
+    step_fupdN_le n_m Ei_Eo |>.trans (later_intro.trans (step_fupd_intro Ei_Eo))
+
 @[rocq_alias step_fupd_fupd]
 theorem step_fupd_fupd {Eo Ei : CoPset} {P : PROP} : (|={Eo}[Ei]▷=> P) ⊣⊢ (|={Eo}[Ei]▷=> |={Eo}=> P) :=
   ⟨mono <| later_mono <| mono fupd_intro, mono <| later_mono BIFUpdate.trans⟩

Iris/Iris/BI/WeakestPre.lean

@@ -0,0 +1,146 @@
+module
+
+public import Iris.Std.CoPset
+public import Iris.BI
+public meta import Iris.BI
+public import Iris.BI.BIBase
+public meta import Iris.Std.Rewrite
+public import Std
+meta import Lean
+public import Lean
+
+public import Iris.BI.BI
+public import Iris.BI.Classes
+public import Iris.BI.DerivedLaws
+public import Iris.BI.DerivedLawsLater
+public import Iris.BI.Extensions
+public import Iris.BI.SIProp
+public meta import Iris.Std.RocqPorting
+
+public section
+
+namespace Iris
+
+open Lean
+
+inductive Stuckness where
+| NotStuck
+| MaybeStuck
+
+namespace Stuckness
+
+@[simp]
+instance instLE: LE Stuckness where
+  le x y := ¬ (x = .MaybeStuck ∧ y = .NotStuck)
+
+instance : Std.IsPreorder Stuckness where
+  le_refl  := by grind only [Stuckness, LE.le, instLE]
+  le_trans := by grind only [Stuckness, LE.le, instLE]
+
+@[simp] theorem le_MaybeStuck {s : Stuckness} : s ≤ MaybeStuck := by
+  cases s <;> grind only [Stuckness, LE.le, instLE]
+
+@[simp] theorem NotSuck_le {s : Stuckness} : NotStuck ≤ s := by
+  cases s <;> grind only [Stuckness, LE.le, instLE]
+
+end Stuckness
+
+class Wp (PROP Expr : Type _) (Val : outParam (Type _)) (A : Type _) where
+  wp : A → CoPset → Expr → (Val → PROP) → PROP
+
+class TotalWP (PROP Expr) (Val : outParam (Type _)) (A : Type _) where
+  totalWp : A → CoPset → Expr → (Val → PROP) → PROP
+
+syntax wpExpr :=
+  term:max (" @ " term:max (" ; " term:max) <|> ((" ? ")? )) <|> (" ? ")?
+
+declare_syntax_cat wpPostcondInner
+syntax ident ", " term : wpPostcondInner
+syntax term : wpPostcondInner
+
+declare_syntax_cat wpPostcond
+-- Avoids conflicts with
+-- example {a : PUnit.{i}} : PUnit.{i} := a
+--                      ^^
+-- see: https://github.com/leanprover-community/iris-lean/pull/393
+syntax " {" "{ " wpPostcondInner " }" "} " : wpPostcond
+syntax " [" "{ " wpPostcondInner " }" "] " : wpPostcond
+syntax " ⦃ " wpPostcondInner " ⦄ " : wpPostcond
+syntax " 〖 " wpPostcondInner " 〗 "  : wpPostcond
+
+syntax (name := wp) "WP " wpExpr wpPostcond : term
+
+open Lean in
+meta def parseWpExpr : Lean.TSyntax ``wpExpr → Lean.MacroM (TSyntax `term × TSyntax `term × TSyntax `term) := fun
+  | `(wpExpr| $e @ $s ; $E) =>
+    return (e, s, E)
+  | `(wpExpr| $e @ $E) =>
+    return (e, ←`(Stuckness.NotStuck), E)
+  | `(wpExpr| $e @ $E ?) =>
+    return (e, ←`(Stuckness.MaybeStuck), E)
+  | `(wpExpr| $e:term) =>
+    return (e, ←`(Stuckness.NotStuck), ←`(⊤))
+  | `(wpExpr| $e:term ?) =>
+    return (e, ←`(Stuckness.MaybeStuck), ←`(⊤))
+  | _ => Lean.Macro.throwUnsupported
+
+open Lean in
+meta def parseWpPostcondInner (stx : TSyntax `wpPostcondInner) : MacroM (TSyntax `term) := do
+  match stx with
+  | `(wpPostcondInner| $v:ident, $Φ:term) => `(fun $v => iprop($Φ))
+  | `(wpPostcondInner| $Φ:term) => return iprop(Φ)
+  | _ => Macro.throwUnsupported
+
+open Lean in
+meta def parseWpPostcond (stx : TSyntax `wpPostcond) : MacroM (TSyntax `term × Bool) := do
+  match stx with
+  | `(wpPostcond| {{ $inner:wpPostcondInner }})
+  | `(wpPostcond| ⦃ $inner:wpPostcondInner ⦄) =>
+    return (←parseWpPostcondInner inner, false)
+  | `(wpPostcond| [{ $inner:wpPostcondInner }])
+  | `(wpPostcond| 〖 $inner:wpPostcondInner 〗) =>
+    return (←parseWpPostcondInner inner, true)
+  | _ => Macro.throwUnsupported (α := TSyntax `term × Bool)
+
+@[macro wp]
+meta def wpMacro : Lean.Macro := fun stx => do
+  match stx with
+  | `(WP $expr $postcond) =>
+    let (e, s, E) ← parseWpExpr expr
+    let (Φ, useTotal?) ← parseWpPostcond postcond
+    if useTotal? then
+      `(TotalWP.totalWp $s $E $e $Φ)
+    else
+      `(Wp.wp $s $E $e $Φ)
+  | _ => Lean.Macro.throwUnsupported
+
+meta def unexpandWpPostcondInner : TSyntax `term → PrettyPrinter.UnexpandM (TSyntax `wpPostcondInner)
+  | `(fun $v:ident => iprop($Φ:term)) => `(wpPostcondInner|$v:ident, $Φ:term)
+  | `(iprop($Φ:term)) => `(wpPostcondInner| $Φ:term)
+  | `(fun $v:ident => $Φ:term) => `(wpPostcondInner|$v:ident, $Φ:term)
+  | `($Φ:term) => `(wpPostcondInner| $Φ:term)
+
+open Lean in
+meta def makeWpExpr (s E e : TSyntax `term) : PrettyPrinter.UnexpandM (TSyntax ``wpExpr) := do
+  match s, E with
+  | `(Stuckness.NotStuck), `(⊤) => `(wpExpr| $e:term)
+  | `(Stuckness.NotStuck), E => `(wpExpr| $e:term @ $E:term)
+  | `(Stuckness.MaybeStuck), `(⊤) => `(wpExpr| $e:term ?)
+  | `(Stuckness.MaybeStuck), E => `(wpExpr| $e:term @ $E:term ?)
+  | s, E => `(wpExpr| $e:term @ $s:term ; $E:term)
+
+@[app_unexpander Wp.wp]
+meta def unexpanderWp : PrettyPrinter.Unexpander
+  | `($_wp $s $E $e $Φ) => do
+    let wpExpr ← makeWpExpr s E e
+    let wpPostcondInner ← unexpandWpPostcondInner Φ
+    `(WP $wpExpr {{ $wpPostcondInner }})
+  | _ => throw ()
+
+@[app_unexpander TotalWP.totalWp]
+meta def unexpanderTotalWp : PrettyPrinter.Unexpander
+  | `($_wp $s $E $e $Φ) => do
+    let wpExpr ← makeWpExpr s E e
+    let wpPostcondInner ← unexpandWpPostcondInner Φ
+    `(WP $wpExpr [{ $wpPostcondInner }])
+  | _ => throw ()

Iris/Iris/HeapLang/Notation.lean

@@ -6,6 +6,7 @@ Authors: Michael Sammler
 module
 
 public import Iris.HeapLang.Syntax
+public meta import Lean.PrettyPrinter.Parenthesizer
 
 public meta section
 namespace Iris.HeapLang
@@ -149,6 +150,12 @@ syntax:100 "fork(" hl_exp  ")" : hl_exp
 /-- assert -/
 syntax:100 "assert(" hl_exp  ")" : hl_exp
 
+open Lean.PrettyPrinter.Parenthesizer in
+@[category_parenthesizer hl_exp]
+def hl_exp.parenthesizer : CategoryParenthesizer := fun prec => do
+  maybeParenthesize `hl_exp false (fun stx => Unhygienic.run `(hl_exp|($(⟨stx⟩)))) prec <|
+    parenthesizeCategoryCore `hl_exp prec
+
 partial def unpackHLExp [Monad m] [MonadRef m] [MonadQuotation m] : Term → m (TSyntax `hl_exp)
   | `(hl($e)) => `(hl_exp|$e)
   | `($t) => `(hl_exp|{$t})

Iris/Iris/Instances/IProp/Instance.lean

@@ -16,6 +16,9 @@ namespace Iris
 
 open COFE
 
+@[ext]
+theorem IProp.ext {P Q : IProp GF} : P ⊣⊢ Q → P = Q := OFE.Leibniz.eq_of_eqv ∘ BI.equiv_iff.mpr
+
 /-- Apply an OFunctor at a fixed type -/
 abbrev COFE.OFunctorPre.ap (F : OFunctorPre) (T : Type _) [OFE T] :=
   F T T

Iris/Iris/Instances/Lib/LaterCredits.lean

@@ -64,10 +64,9 @@ section Operations
 
 variable {GF : BundledGFunctors} [LC : LcGS GF]
 
-theorem lc_split {n m} : £ (n + m) ⊣⊢@{IProp GF} £ n ∗ £ m := by
+theorem lc_split {n m} : £ (n + m) ⊣⊢@{IProp GF} £ n ∗ £ m :=
   -- FIXME: Timeout on iOwn_op. Why?
-  refine .trans ?_ iOwn_op
-  exact .rfl
+  iOwn_op (E := LC.lc_elem) (a1 := ◯ n) (a2 := ◯ m)
 
 @[rocq_alias lc_zero]
 theorem lc_zero : ⊢@{IProp GF} |==> £ 0 := iOwn_unit (ε := UCMRA.unit)