feat: add total weakest preconditions

Iris/Iris.lean

@@ -10,5 +10,7 @@ public import Iris.HeapLang.Lib
 public import Iris.Instances
 public import Iris.Instances.Lib
 public import Iris.ProofMode
+public import Iris.ProgramLogic.TotalAdequacy
+public import Iris.ProgramLogic.TotalEctxLifting
 public import Iris.Std
 public import Iris.Tests

Iris/Iris/Algebra/COFESolver.lean

@@ -28,7 +28,7 @@ def A' : Nat → Σ α : Type u, COFE α
   | n+1 => let ⟨A, _⟩ := A' n; ⟨F A A, inferInstance⟩
 
 variable (F) in
-def A (n : Nat) : Type u := (A' F n).1
+abbrev A (n : Nat) : Type u := (A' F n).1
 
 instance instA' (n) : COFE (A' F n).1 := (A' F n).2
 instance instA (n) : COFE (A F n) := (A' F n).2

Iris/Iris/Algebra/IProp.lean

@@ -85,12 +85,12 @@ def IProp.fold : IPre GF -n> IProp GF :=
   OFE.Iso.inv <| OFunctor.Fix.iso (F := (UPredOF (IResF GF)))
 
 @[rocq_alias iProp_solution.iProp_fold_unfold]
-theorem IProp.fold_unfold (P : IProp GF) : IProp.fold GF (IProp.unfold GF P) = P := by
-  simp only [IProp.fold, IProp.unfold, OFE.Iso.inv_hom]
+theorem IProp.fold_unfold (P : IProp GF) : IProp.fold GF (IProp.unfold GF P) = P :=
+  OFunctor.Fix.iso (F := UPredOF (IResF GF)) |>.inv_hom
 
 @[rocq_alias iProp_solution.iProp_unfold_fold]
-theorem IProp.unfold_fold (P : IPre GF) : IProp.unfold GF (IProp.fold GF P) = P := by
-  simp only [IProp.unfold, IProp.fold, OFE.Iso.hom_inv]
+theorem IProp.unfold_fold (P : IPre GF) : IProp.unfold GF (IProp.fold GF P) = P :=
+  OFunctor.Fix.iso (F := UPredOF (IResF GF)) |>.hom_inv
 
 end IProp
 

Iris/Iris/BI/WeakestPre.lean

@@ -55,13 +55,22 @@ syntax " [" noWs "{ " wpPostcondInner " }" noWs "] " : wpPostcond
 syntax (name := wp) "WP " wpExpr wpPostcond : term
 
 syntax texanPostcondInner := ((ppSpace (binderIdent <|> bracketedBinder))+ ", ")? " RET " term:min "; " term:min
+
 declare_syntax_cat texanPostcond
 syntax " {" noWs "{ " texanPostcondInner " }" noWs "} " : texanPostcond
 declare_syntax_cat texanPrecond
 syntax " {" noWs "{ " term:min " }" noWs "} " : texanPrecond
 
 syntax (name := texanTriple) texanPrecond wpExpr texanPostcond : term
 
+
+declare_syntax_cat totalTexanPostcond
+syntax " [" noWs "{ " texanPostcondInner " }" noWs "] " : totalTexanPostcond
+declare_syntax_cat totalTexanPrecond
+syntax " [" noWs "{ " term:min " }" noWs "] " : totalTexanPrecond
+
+syntax (name := totalTexanTriple) totalTexanPrecond wpExpr totalTexanPostcond : term
+
 open Lean in
 meta def parseWpExpr : Lean.TSyntax ``wpExpr → Lean.MacroM (TSyntax `term × TSyntax `term × TSyntax `term) := fun
   | `(wpExpr| $e @ $s ; $E) =>
@@ -92,6 +101,16 @@ meta def parseWpPostcond (stx : TSyntax `wpPostcond) : MacroM (TSyntax `term ×
     return (←parseWpPostcondInner inner, true)
   | _ => Macro.throwUnsupported (α := TSyntax `term × Bool)
 
+open Lean in
+private meta def transformTexanBinders
+    (xs : Array (TSyntax [`Lean.binderIdent, `Lean.Parser.Term.bracketedBinder])) :
+    MacroM <| TSyntaxArray [`ident, `Lean.Parser.Term.hole,
+      `Lean.Parser.Term.bracketedBinder] :=
+  xs.mapM fun
+    | `(binderIdent|_) => `(hole|_)
+    | `(binderIdent|$i:ident) => `(ident|$i)
+    | `(bracketedBinder|$x) => `(bracketedBinder|$x)
+
 @[macro wp]
 meta def wpMacro : Lean.Macro := fun stx => do
   match stx with
@@ -106,26 +125,27 @@ meta def wpMacro : Lean.Macro := fun stx => do
 
 meta def parseTexanTriple : Syntax → MacroM Term
   | `({{ $P:term }} $wpExpr {{ $[$[$xs]* ,]? RET $pat ; $Q:term }}) => do
-    let transform (xs : Array (TSyntax [`Lean.binderIdent, `Lean.Parser.Term.bracketedBinder])) : MacroM <| TSyntaxArray [`ident, `Lean.Parser.Term.hole, `Lean.Parser.Term.bracketedBinder] :=
-      xs.mapM fun
-        | `(binderIdent|_) => `(hole|_)
-        | `(binderIdent|$i:ident) => `(ident|$i)
-        | `(bracketedBinder|$x) => `(bracketedBinder|$x)
-
     let k ← match xs with
             | some xs =>
-              let xs ← transform xs -- TSyntax cast
+              let xs ← transformTexanBinders xs
               `(iprop(∀ $xs*, $Q:term -∗ Φ $pat))
             | none => `($Q:term -∗ Φ $pat)
     `(∀ Φ, $P -∗ ▷ $k -∗ (WP $wpExpr {{ Φ }}))
+  | `([{ $P:term }] $wpExpr [{ $[$[$xs]* ,]? RET $pat ; $Q:term }]) => do
+    let k ← match xs with
+            | some xs =>
+              let xs ← transformTexanBinders xs
+              `(iprop(∀ $xs*, $Q:term -∗ Φ $pat))
+            | none => `($Q:term -∗ Φ $pat)
+    `(∀ Φ, $P -∗ $k -∗ (WP $wpExpr [{ Φ }]))
   | _ => Lean.Macro.throwUnsupported
 
 @[macro Iris.BI.iprop]
 meta def wpTexanTriple : Lean.Macro
   | `(iprop($P)) => do `(iprop(□ $(← parseTexanTriple P)))
   | _ => Lean.Macro.throwUnsupported
 
-@[macro texanTriple]
+@[macro texanTriple, macro totalTexanTriple]
 meta def wpTexanTripleTerm : Lean.Macro
   | P => do `(⊢ $(← parseTexanTriple P))
 

Iris/Iris/Instances/IProp/Instance.lean

@@ -170,25 +170,19 @@ def IProp.foldi : FF.api τ (IPre FF) -n> FF.api τ (IProp FF) :=
 
 @[rocq_alias inG_unfold_fold]
 theorem IProp.unfoldi_foldi (x : FF.api τ (IPre FF)) : unfoldi (foldi x) = x := by
-  refine OFE.eq_dist.mpr fun n => ?_
-  refine .trans (OFunctor.map_comp (F := FF τ |>.fst) ..).symm.dist ?_
-  refine .trans ?_ (OFunctor.map_id (F := FF τ |>.fst) x).dist
-  apply OFunctor.map_ne.ne <;> intro _ <;> simp [IProp.unfold, IProp.fold]
+  have h : (IProp.unfold FF).comp (IProp.fold FF) = OFE.Hom.id := OFE.Hom.ext <| funext (IProp.unfold_fold FF)
+  rw [unfoldi, foldi, ← OFunctor.map_comp, h, OFunctor.map_id]
 
 @[rocq_alias inG_fold_unfold]
 theorem IProp.foldi_unfoldi (x : FF.api τ (IProp FF)) : foldi (unfoldi x) = x := by
-  refine OFE.eq_dist.mpr fun n => ?_
-  refine .trans (OFunctor.map_comp (F := FF τ |>.fst) ..).symm.dist ?_
-  refine .trans ?_ (OFunctor.map_id (F := FF τ |>.fst) x).dist
-  apply OFunctor.map_ne.ne <;> intro _ <;> simp [IProp.unfold, IProp.fold]
+  have h : (IProp.fold FF).comp (IProp.unfold FF) = OFE.Hom.id := OFE.Hom.ext <| funext (IProp.fold_unfold FF)
+  rw [unfoldi, foldi, ← OFunctor.map_comp, h, OFunctor.map_id]
 
 @[rocq_alias iProp_unfold_equivI]
 theorem IProp.unfold_equivI (P Q : IProp FF) :
     (IProp.unfold FF P ≡ IProp.unfold FF Q) ⊢@{IProp FF} P ≡ Q := by
-  have h := BI.internalEq.of_internalEquiv_ne (PROP := IProp FF) (IProp.fold FF)
+  simpa only [IProp.fold_unfold] using BI.internalEq.of_internalEquiv_ne (PROP := IProp FF) (IProp.fold FF)
     (x := IProp.unfold FF P) (y := IProp.unfold FF Q)
-  rw [IProp.fold_unfold, IProp.fold_unfold] at h
-  exact h
 
 theorem IProp.unfoldi_discreteE {v : FF.api τ (IProp FF)} (hv : OFE.DiscreteE v) :
     OFE.DiscreteE (unfoldi.f v) where