diff --git a/Iris/Iris/Algebra/OFE.lean b/Iris/Iris/Algebra/OFE.lean index d6224f101..d1c5bbd2b 100644 --- a/Iris/Iris/Algebra/OFE.lean +++ b/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 - diff --git a/Iris/Iris/BI/Updates.lean b/Iris/Iris/BI/Updates.lean index 07618cf34..2187c2bcd 100644 --- a/Iris/Iris/BI/Updates.lean +++ b/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⟩ diff --git a/Iris/Iris/BI/WeakestPre.lean b/Iris/Iris/BI/WeakestPre.lean new file mode 100644 index 000000000..1b7a1fd60 --- /dev/null +++ b/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 () diff --git a/Iris/Iris/HeapLang/Notation.lean b/Iris/Iris/HeapLang/Notation.lean index 09625dd27..3eb35d996 100644 --- a/Iris/Iris/HeapLang/Notation.lean +++ b/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}) diff --git a/Iris/Iris/Instances/IProp/Instance.lean b/Iris/Iris/Instances/IProp/Instance.lean index 6d1d24cfd..7337a2197 100644 --- a/Iris/Iris/Instances/IProp/Instance.lean +++ b/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 diff --git a/Iris/Iris/Instances/Lib/LaterCredits.lean b/Iris/Iris/Instances/Lib/LaterCredits.lean index 1c1be4397..ac0ead815 100644 --- a/Iris/Iris/Instances/Lib/LaterCredits.lean +++ b/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) diff --git a/Iris/Iris/ProgramLogic/Language.lean b/Iris/Iris/ProgramLogic/Language.lean index 9102bdc33..0d3ff4276 100644 --- a/Iris/Iris/ProgramLogic/Language.lean +++ b/Iris/Iris/ProgramLogic/Language.lean @@ -5,11 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. module meta import Iris.Std.RocqPorting -public import Iris.Std.FromMathlib public import Iris.Std.Relation -public import Iris.Std.List -public meta import Lean.PrettyPrinter.Delaborator -public import Batteries.Data.List.Basic +public import Iris.BI.WeakestPre #rocq_ignore LanguageMixin "This feature was implemented differently using typeclasses" #rocq_ignore language "This feature was implemented differently using typeclasses" @@ -26,7 +23,7 @@ class ToVal (Expr : Type _) (Val : outParam (Type _)) where toVal : Expr → Option Val ofVal : Val → Expr /-- If `toVal` is defined for an expression, `coe` is its inverse -/ - coe_of_toVal_eq_some (e : Expr) (v : Val) : toVal e = some v → ofVal v = e + coe_of_toVal_eq_some {e : Expr} {v : Val} : toVal e = some v → ofVal v = e /-- `toVal` is defined `coe`, and works as its inverse -/ toVal_coe (v : Val) : toVal (ofVal v) = some v export ToVal (toVal coe_of_toVal_eq_some toVal_coe) @@ -46,7 +43,7 @@ instance : Coe Val Expr where coe := ofVal @[grind! ., rocq_alias of_to_val_flip] theorem toVal_eq_iff_coe (e : Expr) (v : Val) : v = e ↔ toVal e = some v := - ⟨(· ▸ toVal_coe v), coe_of_toVal_eq_some e v⟩ + ⟨(· ▸ toVal_coe v), coe_of_toVal_eq_some⟩ @[rocq_alias of_val_inj] instance : ι.ofVal.Injective := by @@ -210,22 +207,29 @@ theorem toVal_none_of_reducible : Reducible (e, σ) → toVal e = none := by grind only [Reducible, val_stuck] @[rocq_alias val_irreducible] -theorem val_irreducible : (toVal e).isSome → Irreducible (e, σ) := by +theorem val_irreducible : (toVal e).isSome → ∀ σ, Irreducible (e, σ) := by grind only [Irreducible, val_stuck, = Option.isSome_none] end ReducibilityLemmas @[rocq_alias atomicity] inductive Atomicity where -| WeaklyAtomic -| StronglyAtomic + | WeaklyAtomic + | StronglyAtomic + +@[rocq_alias stuckness_to_atomicity, coe] +abbrev Atomicity.ofStuckness : Stuckness → Atomicity + | .MaybeStuck => .StronglyAtomic + | .NotStuck => .WeaklyAtomic + +instance : Coe Stuckness Atomicity where coe := Atomicity.ofStuckness @[rocq_alias Atomic] class Atomic (a : Atomicity) (e : Expr) : Prop where - atomic (σ : State) obs e' σ' eₜ : + atomic {σ : State} {obs e' σ' eₜ} : (e, σ) --> (e', σ', eₜ) → match a with - | .WeaklyAtomic => ¬ Reducible (e', σ') + | .WeaklyAtomic => Irreducible (e', σ') | .StronglyAtomic => (toVal e').isSome @[rocq_alias strongly_atomic_atomic] @@ -481,75 +485,3 @@ theorem erasedStep_pureSteps {t₁ t₂ t₃ : List Expr} {σ₁ σ₂ : State} exact Std.List.Forall₂.append ps_ps₃ <| .cons lastSteps ss_ss₃ end Language - -section test -open Language - -section notations - -/-- -info: (e, σ) --> (e, σ, []) : Prop --/ -#guard_msgs in -variable (e : Expr) (σ : State) (obs : Obs) [PrimStep Expr State Obs] in -#check (PrimStep.primStep (e, σ) obs (e,σ,[])) - -/-- -info: (t, σ) -->ₜₚ (t, σ) : Prop --/ -#guard_msgs in -variable (t : List Expr) (σ : State) (obs : List Obs) [Language Expr State Obs Val] in -#check (Language.Step (t, σ) obs (t,σ)) - -/-- -info: (t, σ) -->ₜₚ^[0] (t, σ) : Prop --/ -#guard_msgs in -variable (t : List Expr) (σ : State) (obs : List Obs) [Language Expr State Obs Val] in -#check (Language.NSteps 0 (t, σ) obs (t,σ)) - -/-- -info: (t, σ) -·->ₜₚ (t, σ) : Prop --/ -#guard_msgs in -variable (t : List Expr) (σ : State) [Language Expr State Obs Val] in -#check (ErasedStep (t, σ) (t,σ)) - -/-- -info: e -ᵖ-> e : Prop --/ -#guard_msgs in -variable (e : Expr) [Language Expr State Obs Val] in -#check (PurePrimStep e e) - -/-- -info: e -ᵖ->^[0] e : Prop --/ -#guard_msgs in -variable (e : Expr) [Language Expr State Obs Val] in -#check (Relation.Iterate PurePrimStep 0 e e) - -/-- -info: e -ᵖ->* e : Prop --/ -#guard_msgs in -variable (e : Expr) [Language Expr State Obs Val] in -#check (Relation.ReflTransGen PurePrimStep e e) - -/-- -info: e -ᵖ->* e : Prop --/ -#guard_msgs in -variable (e : Expr) [Language Expr State Obs Val] in -#check (Relation.ReflTransGen PurePrimStep e e) - -/-- -info: t -ᵖ->ₜₚ* t : Prop --/ -#guard_msgs in -variable (t : List Expr) [Language Expr State Obs Val] in -#check (PureSteps t t) - -end notations - -end test diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean new file mode 100644 index 000000000..8cbd4df47 --- /dev/null +++ b/Iris/Iris/ProgramLogic/WeakestPre.lean @@ -0,0 +1,684 @@ +/- +Copyright (c) 2026 Fernando Leal. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Iris.Algebra +public import Iris.Instances.Lib.FUpd +public import Iris.BI +public import Iris.BI.WeakestPre +public import Iris.ProofMode +public import Iris.ProgramLogic.Language +public import Iris.Std.CoPset + +namespace Iris + +open ProgramLogic Language.Notation Std + +@[expose] public section + +/-! +TODO: AddModal, ElimAcc instances +-/ + +/-- Carrier typeclass for the `stateInterp` operation. + +This operation cannot be placed directly inside of `IrisGS_gen` +because Lean then wouldn't be able to derive from its arguments +the values of `Expr` and `Val`, and so they're asked explicitly. +This was not a problem in Iris Rocq becuse of canonical structures. +In Iris Lean, we instead fix our choice of `State` from the choice +of `Expr`, so `Expr` cannot be inferred from `State` instead. +-/ +class StateInterp (State : Type _) (Obs : outParam $ Type _) (GF : BundledGFunctors) + where + /-- Interpretation of a state in a language model. Takes a state, + number of steps, list of observations prior to the state, and number of + threads previously spawned. -/ + stateInterp : State → Nat → List Obs → Nat → IProp GF + +export StateInterp (stateInterp) + +@[rocq_alias irisGS_gen] +class IrisGS_gen (hlc : outParam Bool) (Expr : Type _) {Val : Type _} {State : Type _} + {Obs : Type _} [Λ : Language Expr State Obs Val] (GF : BundledGFunctors) extends + StateInterp State Obs GF, InvGS_gen hlc GF where + /-- Number of later credits obtained from taking one step in the + operational semantics of our language. -/ + numLatersPerStep : Nat → Nat + -- TODO: Even when referenced with the typeclass instance, the + -- display of `numLatersPerStep` is still kinda awful. + /-- Postcondition of forked threads -/ + forkPost : Val → IProp GF + /-- The number of steps in the state interpretation should only be + considered a lower bound. -/ + stateInterp_mono σ ns obs nt : + iprop(stateInterp σ ns obs nt ⊢ |={∅}=> stateInterp σ (ns + 1) obs nt) + +variable {hlc : outParam Bool} {Expr State Obs Val} +variable [Λ : Language Expr State Obs Val] +variable {GF : BundledGFunctors} [ι : IrisGS_gen hlc Expr GF] + +/-- Reducibility condition depending on stuckness. -/ +abbrev Stuckness.MaybeReducible : Stuckness → Expr × State → Prop +| .NotStuck, (e₁, σ₁) => PrimStep.Reducible (e₁, σ₁) +| _, _ => True + +@[rocq_alias wp_pre] +def wp.pre (s : Stuckness) (wp : CoPset -> Expr -> (Val -> IProp GF) -> IProp GF) (E : CoPset) + (e₁ : Expr) (Φ : Val -> IProp GF) : IProp GF := + match toVal e₁ with + | some v => iprop(|={E}=> Φ v) + | none => iprop(∀ (σ₁ : State) (ns : Nat) (obs obs' : List Obs) (nt : Nat), + stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ + ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂, σ₂, eₜ)⌝ -∗ + £ (ι.numLatersPerStep ns + 1) ={∅}▷=∗^[ι.numLatersPerStep ns + 1] |={∅,E}=> + stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ + wp E e₂ Φ ∗ [∗list] e' ∈ eₜ, wp ⊤ e' ι.forkPost) + +@[rocq_alias wp_pre_contractive] +instance wp.pre.contractive s : OFE.Contractive (wp.pre s (ι := ι)) where + distLater_dist := by + intros n wp wp' Hwp E e₁ Φ + unfold pre + cases toVal e₁ + case some _ => + exact .rfl + case none => + refine BI.forall_ne (fun σ₁ => ?_) + refine BI.forall_ne (fun ns => ?_) + refine BI.forall_ne (fun obs => ?_) + refine BI.forall_ne (fun obs' => ?_) + refine BI.forall_ne (fun nt => ?_) + refine BI.wand_ne.ne .rfl ?_ + refine BIFUpdate.ne.ne ?_ + refine BI.sep_ne.ne .rfl ?_ + refine BI.forall_ne (fun e₂ => ?_) + refine BI.forall_ne (fun σ₂ => ?_) + refine BI.forall_ne (fun eₜ => ?_) + refine BI.wand_ne.ne .rfl ?_ + refine BI.wand_ne.ne .rfl ?_ + refine BIFUpdate.ne.ne ?_ + refine OFE.Contractive.distLater_dist fun m m_n => ?_ + refine BIFUpdate.ne.ne ?_ + refine step_fupdN_ne.ne ?_ + refine BIFUpdate.ne.ne ?_ + refine BI.sep_ne.ne .rfl ?_ + refine BI.sep_ne.ne ?_ ?_ + · exact Hwp m m_n _ _ _ + · exact BI.BigSepL.bigSepL_dist <| fun _ => Hwp m m_n _ _ _ + +@[rocq_alias wp_def] +instance wp.def : Wp (IProp GF) (Expr) (Val) Stuckness where + wp s := fixpoint (wp.pre s) + +#rocq_ignore wp_aux "We do not use Iris' custom seal/unseal visibility control" +#rocq_ignore wp' "We do not use Iris' custom seal/unseal visibility control" +#rocq_ignore wp_unseal "We do not use Iris' custom seal/unseal visibility control" + +section Wp + +@[rocq_alias wp_unfold] +theorem wp_unfold {s E} {e : Expr} {Φ : Val → IProp GF} : + WP e @ s ; E {{ Φ }} ⊣⊢ wp.pre s (Wp.wp (PROP := IProp GF) s) E e Φ := + BI.equiv_iff.1 <| fixpoint_unfold (f := (wp.pre s).toContractiveHom) E e Φ + +@[rocq_alias wp_ne] +instance wp_ne {s : Stuckness} {E} {e : Expr} : + OFE.NonExpansive (Wp.wp (PROP := IProp GF) s E e) where + ne {n Φ₁ Φ₂} HΦ := by + induction n using Nat.strongRecOn generalizing e E Φ₁ Φ₂ with | ind n IH => + simp only [IProp.ext wp_unfold] + dsimp only [wp.pre] + cases toVal e + case some v => + exact BIFUpdate.ne.ne <| HΦ v + case none => + refine BI.forall_ne fun σ₁ => ?_ + refine BI.forall_ne fun ns => ?_ + refine BI.forall_ne fun obs => ?_ + refine BI.forall_ne fun obs' => ?_ + refine BI.forall_ne fun nt => ?_ + refine BI.wand_ne.ne .rfl ?_ + refine BIFUpdate.ne.ne ?_ + refine BI.sep_ne.ne .rfl ?_ + refine BI.forall_ne fun e₂ => ?_ + refine BI.forall_ne fun σ₂ => ?_ + refine BI.forall_ne fun eₜ => ?_ + refine BI.wand_ne.ne .rfl ?_ + refine BI.wand_ne.ne .rfl ?_ + refine step_fupdN_contractive.distLater_dist fun m n_m => ?_ + refine BIFUpdate.ne.ne ?_ + refine BI.sep_ne.ne .rfl ?_ + refine BI.sep_ne.ne ?_ .rfl + exact IH m n_m <| OFE.dist_lt HΦ n_m + +#rocq_ignore wp_proper "Derivable using NonExpansive.eqv" + +@[rocq_alias wp_contractive] +instance wp_contractive (s : Stuckness) E (e : Expr) (h : toVal e = none) : + OFE.Contractive (Wp.wp (PROP := IProp GF) s E e) where + distLater_dist {n Φ₁ Φ₂} HΦ := by + simp only [IProp.ext wp_unfold] + simp only [wp.pre, h] + refine BI.forall_ne fun σ₁ => ?_ + refine BI.forall_ne fun ns => ?_ + refine BI.forall_ne fun obs => ?_ + refine BI.forall_ne fun obs' => ?_ + refine BI.forall_ne fun nt => ?_ + refine BI.wand_ne.ne .rfl ?_ + refine BIFUpdate.ne.ne ?_ + refine BI.sep_ne.ne .rfl ?_ + refine BI.forall_ne fun e₂ => ?_ + refine BI.forall_ne fun σ₂ => ?_ + refine BI.forall_ne fun eₜ => ?_ + refine BI.wand_ne.ne .rfl ?_ + refine BI.wand_ne.ne .rfl ?_ + refine step_fupdN_contractive.distLater_dist fun m n_m => ?_ + refine BIFUpdate.ne.ne ?_ + refine BI.sep_ne.ne .rfl ?_ + refine BI.sep_ne.ne ?_ .rfl + refine wp_ne.ne ?_ + exact HΦ m n_m + +@[rocq_alias wp_value_fupd'] +theorem wp_value_fupd' {s : Stuckness} {E} {Φ : Val → IProp GF} {v : Val} : + WP (v : Expr) @ s ; E {{ Φ }} ⊣⊢ |={E}=> Φ v := by + simp [IProp.ext wp_unfold, toVal_coe, BI.BIBase.BiEntails.rfl, wp.pre] + +@[rocq_alias wp_strong_mono] +theorem wp_strong_mono {s₁ s₂ : Stuckness} {E₁ E₂} {e : Expr} {Φ Ψ : Val → IProp GF} + (hs : s₁ ≤ s₂) (hE : E₁ ⊆ E₂) : + ⊢ WP e @ s₁ ; E₁ {{ Φ }} -∗ (∀ v, Φ v ={E₂}=∗ Ψ v) -∗ WP e @ s₂ ; E₂ {{ Ψ }} := by + iloeb as IH generalizing %e %Φ %Ψ %E₁ %E₂ %hE + rw [IProp.ext wp_unfold, IProp.ext wp_unfold] + iintro H HΦ + dsimp only [wp.pre] + match toVal e with + | none => + dsimp only + iintro %σ₁ %ns %obs %obs' %nt Hσ + imod fupd_mask_subseteq hE with Hclose + icases H $$ Hσ with >⟨%h, H⟩ + imodintro + isplit + · simp only [LE.le] at hs + ipure_intro + grind [cases Stuckness] + · iintro %e₂ %σ₂ %eₜ #hstep hc + dsimp only [Nat.repeat] + imod H $$ hstep hc with H + iintro !> !>; imod H; iintro !> + iapply step_fupdN_wand $$ H + iintro >⟨aux, H, Hefs⟩ + imod Hclose + imodintro + iframe aux + isplitr [Hefs] + · iapply IH $$ %e₂ %Φ %Ψ %E₁ %E₂ %hE H HΦ + · iapply BI.BigSepL.bigSepL_impl $$ Hefs + iintro !> %k %e' %_ H + iapply IH $$ %e' %_ %_ %⊤ %_ %LawfulSet.subset_refl H + iintro %v H + imodintro + iassumption + | some v => + dsimp only + imod fupd_mask_mono hE $$ H with h + iapply HΦ $$ h + +@[rocq_alias fupd_wp] +theorem fupd_wp {s : Stuckness}{E}{e : Expr} {Φ : Val → IProp GF} : + (|={E}=> WP e @ s ; E {{ Φ }}) ⊢ WP e @ s ; E {{ Φ }} := by + simp only [IProp.ext wp_unfold] + iintro H + match h: toVal e with + | some v => + simp only [wp.pre, h] + imod H + iassumption + | none => + simp only [wp.pre, h] + iintro %σ₁ %ns %obs %obs' %nt + imod H with H + iassumption + +theorem fupd_wp_iff {s : Stuckness}{E}{e : Expr} {Φ : Val → IProp GF} : + WP e @ s ; E {{ Φ }} ⊣⊢ (|={E}=> WP e @ s ; E {{ Φ }}) := + ⟨fupd_mask_intro_discard LawfulSet.subset_refl, fupd_wp⟩ + +@[rocq_alias wp_fupd] +theorem wp_fupd (s : Stuckness) E (e : Expr) (Φ : Val → IProp GF) : + WP e @ s ; E {{v, |={E}=> Φ v }} ⊢ WP e @ s ; E {{ Φ }} := by + iintro h + iapply wp_strong_mono (Std.IsPreorder.le_refl _) LawfulSet.subset_refl $$ h + iintro %v h + iassumption + +@[rocq_alias wp_atomic] +theorem wp_atomic {s : Stuckness} {E1 E2 : CoPset} {e : Expr} {Φ : Val → IProp GF} + [ι : Language.Atomic ↑s e] : + (|={E1,E2}=> WP e @ s ; E2 {{v, |={E2,E1}=> Φ v }}) ⊢ (WP e @ s ; E1 {{ Φ }}) := by + simp only [IProp.ext wp_unfold] + iintro H + match He : toVal e with + | some v => + simp only [wp.pre, He] + iapply BIFUpdate.trans (E2 := E2) + imod H + iassumption + | none => + simp only [wp.pre, He] + iintro %σ₁ %ns %obs %obs' %nt Hσ + imod H + imod H $$ Hσ with ⟨$, H⟩ + imodintro + iintro %e2 %σ2 %efs %Hstep Hcred + ihave aux := H $$ %e2 %σ2 %efs %Hstep Hcred + iapply step_fupdN_wand $$ aux + iintro >(⟨Hσ,H,Hefs⟩) + irevert %ι + match s with + | .NotStuck => + simp only [IProp.ext wp_unfold] + dsimp only [wp.pre] + match h₂ : toVal e2 with + | some v2 => + iintro %ι + icases H with > > $ + iframe + | none => + iintro %ι + icases H $$ %σ2 %(ns +1) %([]) %_ %(nt + efs.length) [Hσ] with >⟨%h, _⟩ + · exact .rfl + exact ((Language.not_reducible_iff_irreducible.mpr (ι.atomic Hstep)) h).elim + | .MaybeStuck => + iintro %ι + have ⟨v, h⟩ := Option.isSome_iff_exists.mp (ι.atomic Hstep) + obtain ⟨rfl⟩ := (ToVal.coe_of_toVal_eq_some h) + simp only [IProp.ext wp_value_fupd'] + imod H with > H + iframe + +@[rocq_alias wp_credit_access] +theorem wp_credit_access {s : Stuckness} {E : CoPset} {e : Expr} {Φ} {P: IProp GF} (h : toVal e = none) + (Htri : ∀ m k, ι.numLatersPerStep m + ι.numLatersPerStep k ≤ ι.numLatersPerStep (m + k)) : + (∀ (σ₁ : State) ns obs nt, + stateInterp σ₁ ns obs nt ={E}=∗ + ∃ k m, stateInterp σ₁ m obs nt ∗ ⌜ns = m + k⌝ ∗ ( + ∀ nt (σ₂: State) obs, £ (ι.numLatersPerStep k) -∗ stateInterp σ₂ (m+1) obs nt ={E}=∗ + stateInterp σ₂ (ns+1) obs nt ∗ P)) ⊢ + WP e @ s ; E {{ v, P ={E}=∗ Φ v }} -∗ + WP e @ s ; E {{ Φ }} := by + simp only [IProp.ext wp_unfold] + iintro Hupd Hwp + simp only [wp.pre, h] + iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + imod Hupd $$ Hσ₁ with ⟨%k, %m, Hσ₁, %h, Hpost⟩; subst h + imod Hwp $$ Hσ₁ with ⟨$,Hwp⟩ + imodintro + iintro %e₂ %σ₂ %efs %Hstep Hc + simp only [IProp.ext lc_split] + icases Hc with ⟨Hc,Hone⟩ + ihave Hc := lc_weaken _ (Htri m k) $$ Hc + icases lc_split $$ Hc with ⟨Hm, Hk⟩ + icombine Hm Hone as Hm + dsimp only [Nat.repeat] + ihave Hwp := Hwp $$ [] [Hm] + · ipure_intro; assumption + · simp [OFE.eq_of_eqv (BI.equiv_iff.mpr lc_split)] + iapply step_fupd_wand $$ Hwp; iintro Hwp + iapply step_fupdN_le (n := ι.numLatersPerStep m) (by grind only) LawfulSet.subset_refl + iapply step_fupdN_wand $$ Hwp; iintro >⟨SI, Hwp, $⟩ + icases Hpost $$ Hk SI with >⟨$, HP⟩ + imodintro + iapply wp_strong_mono (Std.IsPreorder.le_refl s) (LawfulSet.subset_refl) $$ Hwp + iintro %v HΦ + iapply HΦ $$ HP + +@[rocq_alias wp_step_fupdN_strong] +theorem wp_step_fupdN_strong {s : Stuckness} {E1 E2 : CoPset} {e : Expr} {P : IProp GF} {Φ} {n} + (toVal_e : toVal e = none) (E2_E1 : E2 ⊆ E1) : + (∀ (σ : State) ns obs nt, stateInterp σ ns obs nt ={E1, ∅}=∗ ⌜n ≤ ι.numLatersPerStep ns + 1⌝) + ∧ ((|={E1,E2}=> |={∅}▷=>^[n] |={E2,E1}=> P) + ∗ WP e @ s ; E2 {{ v, P ={E1}=∗ Φ v}}) ⊢ + WP e @ s ; E1 {{ Φ }} := by + match n with + | 0 => + iintro ⟨-, ⟨Hp, Hwp⟩⟩ + iapply wp_strong_mono (Std.IsPreorder.le_refl s) E2_E1 $$ Hwp + iintro %v H + dsimp only [Nat.repeat] + imod Hp + imod Hp + iapply H $$ Hp + | n+1 => + simp only [IProp.ext wp_unfold] + simp only [wp.pre, toVal_e] + iintro H %σ₁ %ns %obs %obs' %nt Hσ₁ + by_cases Hn : n ≤ ι.numLatersPerStep ns + · icases H with ⟨-, ⟨Hp, Hwp⟩⟩ + imod Hp + dsimp only [Nat.repeat] + imod Hwp $$ Hσ₁ with ⟨$, H⟩ + iintro !> %e₂ %σ₂ %efs %Hstep Hcred + icases H $$ %_ %_ %_ %Hstep Hcred with H + dsimp only [Nat.repeat] + imod H; imod Hp + iintro !> !> + imod H; imod Hp + imodintro + generalize ι.numLatersPerStep ns = n0 at * + induction n generalizing n0 with + | zero => + iapply step_fupdN_wand $$ H + iintro >⟨$, Hwp, $⟩ + dsimp only [Nat.repeat] + imod Hp + imodintro + iapply wp_strong_mono (Std.IsPreorder.le_refl s) E2_E1 $$ Hwp + iintro %v HΦ + iapply HΦ $$ Hp + | succ n IH => + obtain ⟨n0, rfl⟩ : ∃ n0', n0 = n0' + 1 := by cases n0 <;> grind + dsimp only [Nat.repeat] + imod Hp; imod H; imodintro; imodintro; imod Hp; imod H; imodintro + iapply IH n0 (Nat.le_of_succ_le_succ Hn) $$ [$]; + · icases H with ⟨interp, -⟩ + imod interp $$ Hσ₁ with %h + grind only + +@[rocq_alias wp_bind] +theorem wp_bind (K : Expr → Expr) [κ : Language.Context K] {s : Stuckness} {E : CoPset} {e : Expr} + {Φ : Val → IProp GF} : + -- TODO: Have `WP` use the correct `Val` type from the `Wp` instance (it should anyways, it's an outParam, no?) + WP e @ s ; E {{v, WP (K (↑v : Val)) @ s ; E {{ Φ }} }} ⊢ WP (K e) @ s ; E {{ Φ }} := by + iintro H + iloeb as IH generalizing %E %e %Φ + rewrite (occs := [2]) [IProp.ext wp_unfold] + simp only [wp.pre] + match h : toVal e with + | some v => + simp only [ToVal.coe_of_toVal_eq_some h] + iapply fupd_wp $$ H + | none => + rw [IProp.ext wp_unfold] + simp only [wp.pre, κ.toVal_eq_none_fill h, Nat.repeat] + iintro %σ₁ %step %obs %obs' %n Hσ + imod H $$ [$] with ⟨%_, H⟩ + imodintro + isplit + · ipure_intro; grind only [cases Stuckness, Language.Context.reducible_fill] + · iintro %e₂ %σ₂ %efs %HKstep Hcred + obtain ⟨e₂', rfl, Hstep⟩ := κ.primStep_fill_inv h HKstep + icases H $$ %e₂' %σ₂ %efs %Hstep Hcred with >H; imodintro; imodintro + imod H; imodintro; iapply step_fupdN_wand $$ H; iintro H + imod H with ⟨$, H, $⟩; imodintro; iapply IH $$ H + +@[rocq_alias wp_bind_inv] +theorem wp_bind_inv (K : Expr → Expr) [κ : Language.Context K] {s : Stuckness} {E : CoPset} {e : Expr} + {Φ : Val → IProp GF} : + WP (K e) @ s ; E {{ Φ }} ⊢ WP e @ s ; E {{v, WP (K (↑v : Val)) @ s ; E {{ Φ }} }} := by + iintro H + iloeb as IH generalizing %E %e %Φ + rewrite (occs := [3]) [IProp.ext wp_unfold] + simp only [wp.pre] + match h : toVal e with + | some v => + simp only [ToVal.coe_of_toVal_eq_some h] + iapply fupd_wp $$ H + | none => + rewrite (occs := [2]) [IProp.ext wp_unfold] + simp only [wp.pre, κ.toVal_eq_none_fill h, Nat.repeat] + iintro %σ₁ %step %obs %obs' %n Hσ + imod H $$ [$] with ⟨%_, H⟩ + imodintro + isplit + · ipure_intro; grind only [cases Stuckness, Language.Context.reducible_fill_inv] + · iintro %e₂ %σ₂ %efs %Hstep Hcred + icases H $$ %(K e₂) %σ₂ %efs %(κ.primStep_fill Hstep) Hcred with >H; imodintro; imodintro + imod H; imodintro; iapply step_fupdN_wand $$ H; iintro H + imod H with ⟨$, H, $⟩; imodintro; iapply IH $$ H + +/-! ## Derived rules -/ + +@[rocq_alias wp_mono] +theorem wp_mono {s : Stuckness} {E : CoPset} {e : Expr} {Φ Ψ : Val → IProp GF} : + (∀ v, Φ v ⊢ Ψ v) → WP e @ s ; E {{ Φ }} ⊢ WP e @ s ; E {{ Ψ }} := by + iintro %HΦ H + iapply wp_strong_mono (Std.IsPreorder.le_refl s) (LawfulSet.subset_refl) $$ H + iintro %v HΨ !> + iapply HΦ $$ HΨ + +@[rocq_alias wp_stuck_mono] +theorem wp_stuck_mono {s₁ s₂ : Stuckness} {E : CoPset} {e : Expr} {Φ : Val → IProp GF} : + s₁ ≤ s₂ → WP e @ s₁; E {{ Φ }} ⊢ WP e @ s₂ ; E {{ Φ }} := by + iintro %s₁s₂ Hwp + iapply wp_strong_mono s₁s₂ (LawfulSet.subset_refl) $$ Hwp + iintro %v HΦ + iframe HΦ + +@[rocq_alias wp_stuck_weaken] +theorem wp_stuck_weaken {s : Stuckness} {E : CoPset} {e : Expr} {Φ : Val → IProp GF} : + WP e @ s; E {{ Φ }} ⊢ WP e @ E ?{{ Φ }} := + wp_stuck_mono (Stuckness.le_MaybeStuck) + +@[rocq_alias wp_mask_mono] +theorem wp_mask_mono {s : Stuckness} {E₁ E₂ : CoPset} {e : Expr} {Φ : Val → IProp GF} + (E₁_E₂ : E₁ ⊆ E₂) : WP e @ s; E₁ {{ Φ }} ⊢ WP e @ s; E₂ {{ Φ }} := by + iintro Hwp + iapply wp_strong_mono (Std.IsPreorder.le_refl s) E₁_E₂ $$ Hwp + iintro %v HΦ + iframe HΦ + +#rocq_ignore wp_mono' "No `Proper` typeclass in Lean" +#rocq_ignore wp_flip_mono' "No `Proper` typeclass in Lean" + +@[rocq_alias wp_value_fupd] +theorem wp_value_fupd {s : Stuckness} {E : CoPset} {e : Expr} {v : Val} {Φ : Val → IProp GF} : + Language.IntoVal e v → WP e @ s; E {{ Φ }} ⊣⊢ |={E}=> Φ v + | ⟨h⟩ => h ▸ wp_value_fupd' + +@[rocq_alias wp_value'] +theorem wp_value' {s : Stuckness} {E : CoPset} {v : Val} {Φ : Val → IProp GF} : + Φ v ⊢ WP (v : Expr) @ s; E {{ Φ }} := + fupd_intro.trans wp_value_fupd'.2 + +@[rocq_alias wp_value] +theorem wp_value {s : Stuckness} {E : CoPset} {e : Expr} {v : Val} {Φ : Val → IProp GF} : + Language.IntoVal e v → Φ v ⊢ WP e @ s; E {{ Φ }} + | ⟨h⟩ => h ▸ wp_value' + +@[rocq_alias wp_frame_l] +theorem wp_frame_l {s : Stuckness} {E : CoPset} {e : Expr} {Φ : Val → IProp GF} {R : IProp GF} : + R ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, R ∗ Φ v }} := by + iintro ⟨_, H⟩ + iapply wp_strong_mono (Std.IsPreorder.le_refl s) (LawfulSet.subset_refl) $$ H + iframe + iintro %x + iapply fupd_intro + +@[rocq_alias wp_frame_r] +theorem wp_frame_r {s : Stuckness} {E : CoPset} {e : Expr} {Φ : Val → IProp GF} {R : IProp GF} : + WP e @ s; E {{ Φ }} ∗ R ⊢ WP e @ s; E {{ v, R ∗ Φ v }} := + BI.sep_comm.1.trans wp_frame_l + +@[rocq_alias wp_step_fupdN] +theorem wp_step_fupdN {s : Stuckness} {E₁ E₂ : CoPset} {e : Expr} {P : IProp GF} {Φ : Val → IProp GF} {n : Nat} + (toVal_e : toVal e = none) (E₂E₁ : E₂ ⊆ E₁) : + (∀ (σ : State) ns obs nt, stateInterp σ ns obs nt ={E₁,∅}=∗ ⌜n ≤ (ι.numLatersPerStep ns)+1⌝) ∧ + (((|={E₁\E₂,∅}=> |={∅}▷=>^[n] |={∅,E₁\E₂}=> P) ∗ + WP e @ s; E₂ {{ v, P ={E₁}=∗ Φ v }})) -∗ + WP e @ s; E₁ {{ Φ }} := by + iintro H + iapply wp_step_fupdN_strong (s := s) (P := P) (n := n) toVal_e E₂E₁ $$ [H] + iapply BI.and_mono_r $$ H + iintro ⟨HP, $⟩ + imod fupd_mask_subseteq_emptyset_difference (show E₁\ E₂ ⊆ E₁ from LawfulSet.diff_subset_left) with G + imod HP + imod G with - + rw [show E₁ \ (E₁ \ E₂) = E₂ from LawfulSet.diff_self_diff_of_subset E₂E₁] + imodintro + iapply step_fupdN_wand $$ HP; iintro H + iapply fupd_mask_frame LawfulSet.empty_subset + imod H + imodintro + simp [LawfulSet.diff_empty, ←LawfulSet.diff_subset_decomp E₂E₁, fupd_intro] + +@[rocq_alias wp_step_fupd] +theorem wp_step_fupd {s : Stuckness} {E₁ E₂ : CoPset} {e : Expr} {P : IProp GF} {Φ : Val → IProp GF} + (toVal_e : toVal e = none) (E₂E₁ : E₂ ⊆ E₁) : + (|={E₁}[E₂]▷=> P) -∗ WP e @ s; E₂ {{ v, P ={E₁}=∗ Φ v }} -∗ WP e @ s; E₁ {{ Φ }} := by + iintro HR H + iapply wp_step_fupdN_strong (n := 1) (P := P) toVal_e E₂E₁ $$ [-] + iframe H + isplit + · iintro %σ %ns %obj %nt interp + iapply fupd_mask_intro_discard LawfulSet.empty_subset $$ [HR] + simp [BI.true_intro] + · imod HR + dsimp only [Nat.repeat] + iframe + +@[rocq_alias wp_frame_step_l] +theorem wp_frame_step_l {s : Stuckness} {E₁ E₂ : CoPset} {e : Expr} {Φ : Val → IProp GF} {R : IProp GF} + (toVal_e : toVal e = none) (E₂E₁ : E₂ ⊆ E₁) : + (|={E₁}[E₂]▷=> R) ∗ WP e @ s; E₂ {{ Φ }} ⊢ WP e @ s; E₁ {{ v, R ∗ Φ v }} := by + iintro ⟨Hu, Hwp⟩ + iapply wp_step_fupd toVal_e E₂E₁ $$ Hu + iapply wp_mono $$ Hwp + iintro %x $ $ + +@[rocq_alias wp_frame_step_r] +theorem wp_frame_step_r {s : Stuckness} {E₁ E₂ : CoPset} {e : Expr} {Φ : Val → IProp GF} {R : IProp GF} + (h1 : toVal e = none) (h2 : E₂ ⊆ E₁) : + WP e @ s; E₂ {{ Φ }} ∗ (|={E₁}[E₂]▷=> R) ⊢ WP e @ s; E₁ {{ v, Φ v ∗ R }} := + (BI.sep_comm.1.trans <| wp_frame_step_l h1 h2 |>.trans <| wp_mono (fun _ => BI.sep_comm.1)) + +@[rocq_alias wp_frame_step_l'] +theorem wp_frame_step_l' {s : Stuckness} {E₁ E₂ : CoPset} {e : Expr}{Φ : Val → IProp GF} {R : IProp GF} + (toVal_e : toVal e = none) (E₂E₁ : E₂ ⊆ E₁) : + (▷ R) ∗ WP e @ s; E₂ {{ Φ }} ⊢ WP e @ s; E₁ {{ v, R ∗ Φ v }} := by + iintro ⟨Hu, Hwp⟩ + iapply wp_frame_step_l toVal_e E₂E₁ + iframe + iapply fupd_mask_intro E₂E₁ + iintro H + imodintro + imod H + imodintro + iapply BI.true_intro $$ H + +@[rocq_alias wp_frame_step_r'] +theorem wp_frame_step_r' {s : Stuckness} {E₁ E₂ : CoPset} {e : Expr} {Φ : Val → IProp GF} {R : IProp GF} + (h1 : toVal e = none) (h2 : E₂ ⊆ E₁) : WP e @ s; E₂ {{ Φ }} ∗ (▷ R) ⊢ WP e @ s; E₁ {{ v, Φ v ∗ R }} := + (BI.sep_comm.1.trans <| wp_frame_step_l' h1 h2 |>.trans <| wp_mono (fun _ => BI.sep_comm.1)) + +@[rocq_alias wp_wand] +theorem wp_wand {s : Stuckness} {E : CoPset} {e : Expr} {Φ Ψ : Val → IProp GF} : + WP e @ s ; E {{ Φ }} ⊢ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s ; E {{ Ψ }} := by + iintro Hwp H + iapply wp_strong_mono (Std.IsPreorder.le_refl s) LawfulSet.subset_refl $$ Hwp + iintro %v HΦ + icases H $$ HΦ with H + imodintro; iframe + +@[rocq_alias wp_wand_l] +theorem wp_wand_l {s : Stuckness} {E : CoPset} {e : Expr} {Φ : Val → IProp GF} : + (∀ v, Φ v -∗ Ψ v) ∗ WP e @ s ; E {{ Φ }} ⊢ WP e @ s ; E {{ Ψ }} := + BI.wand_elim' wp_wand + +@[rocq_alias wp_wand_r] +theorem wp_wand_r {s : Stuckness} {E : CoPset} {e : Expr} {Φ : Val → IProp GF} : + WP e @ s ; E {{ Φ }} ∗ (∀ v, Φ v -∗ Ψ v) ⊢ WP e @ s ; E {{ Ψ }} := + BI.wand_elim wp_wand + +@[rocq_alias wp_frame_wand] +theorem wp_frame_wand {s : Stuckness} {E : CoPset} {e : Expr} {Φ :Val → IProp GF} {R : IProp GF} : + R ⊢ WP e @ s; E {{ v, R -∗ Φ v }} -∗ WP e @ s; E {{ Φ }} := by + iintro R Hwp + iapply wp_wand $$ Hwp + iintro %v H + iapply H $$ R + +end Wp + +section ProofModeClasses + +open ProofMode + +variable {hlc : outParam Bool} +variable {Expr State Obs Val : Type _} +variable [Λ : Language Expr State Obs Val] +variable {GF : BundledGFunctors} +variable [ι : IrisGS_gen hlc Expr GF] + +variable {s : Stuckness} {E : CoPset} {e : Expr} {v : Val} {Φ Ψ : Val → IProp GF} {P Q R : IProp GF} + +@[rocq_alias frame_wp] +instance frameWp {p : Bool} [H : ∀ v, Frame p R (Φ v) (Ψ v)] : + -- TODO: move FrameInstantiateExistDisabled over the `FrameInstantiateExistDisabled` constant + -- Blocked by #390 + -- see: https://github.com/leanprover-community/iris-lean/pull/393 + Frame p R (WP e @ s ; E {{ Φ }}) (WP e @ s ; E {{ Ψ }}) where + frame := by + refine wp_frame_l.trans ?_ + apply wp_mono + exact fun v => frame + +@[rocq_alias is_except_0_wp] +instance isExcept0Wp : IsExcept0 (WP e @ s ; E {{ Φ }}) where + is_except0 := + calc iprop(◇ _) + _ ⊢ ◇ |={E}=> _ := BI.except0_mono fupd_intro + _ ⊢ |={E}=> _ := BIFUpdate.except0 + _ ⊢ WP e @ s ; E {{ Φ }} := fupd_wp + +@[rocq_alias elim_modal_fupd_wp] +instance elimModalFupdWp p : + ElimModal True p false iprop(|={E}=> P) P (WP e @ s ; E {{ Φ }}) (WP e @ s ; E {{ Φ }}) where + elim_modal := by + iintro %_ ⟨H, G⟩ + icases BI.intuitionisticallyIf_elim $$ H with H + iapply fupd_wp + imod H; imodintro + iapply G $$ H + +@[rocq_alias elim_modal_bupd_wp] +instance elimModalBupdWp p : + ElimModal True p false iprop(|==> P) P (WP e @ s ; E {{ Φ }}) (WP e @ s ; E {{ Φ }}) where + elim_modal := by + rintro ⟨⟩ + refine BI.sep_mono (BI.intuitionisticallyIf_mono (BIUpdateFUpdate.fupd_of_bupd (E := E))) .rfl |>.trans ?_ + apply elimModalFupdWp _ |>.elim_modal ⟨⟩ + +/-- Error message instance for non-mask-changing view shifts. Also uses a slightly +different error: we cannot apply `fupd_mask_subseteq` if `e` is not atomic, so +we tell the user to first add a leading `fupd` and then change the mask of that. -/ +@[rocq_alias elim_modal_fupd_wp_wrong_mask] +instance elimModalFupdWp_wrongMask : + ElimModal (PMError "Goal and eliminated modality must have the same mask. + Use `iapply fupd_wp; imod (fupd_mask_subseteq E₂)` to adjust the mask of your goal to `E₂`") + p false iprop(|={E₂}=> P) iprop(False) (WP e @ s ; E₁ {{ Φ }}) iprop(False) where + elim_modal := nofun + +@[rocq_alias elim_modal_fupd_wp_atomic] +instance elimModalFupdWpAtomic : + ElimModal (Language.Atomic ↑s e) p false iprop(|={E₁,E₂}=> P) P (WP e @ s ; E₁ {{ Φ }}) (WP e @ s ; E₂ {{ v, |={E₂,E₁}=> Φ v}}) where + elim_modal := by + rintro atomic; iintro ⟨H, G⟩ + icases BI.intuitionisticallyIf_elim $$ H with H + iapply wp_atomic + imod H; imodintro + iapply G $$ H + +@[rocq_alias elim_modal_fupd_wp_atomic_wrong_mask] +instance elimModalFupdWpAtomic_wrongMask : + ElimModal (PMError "Goal and eliminated modality must have the same mask. + Use `iapply fupd_wp; imod (fupd_mask_subseteq E₂)` to adjust the mask of your goal to `E₂`") + p false iprop(|={E₁,E₂}=> P) iprop(False) (WP e @ s ; E₁ {{ Φ }}) iprop(False) where + elim_modal := nofun + +end ProofModeClasses diff --git a/Iris/Iris/ProofMode/Tactics/Revert.lean b/Iris/Iris/ProofMode/Tactics/Revert.lean index cb9e4b987..8027b4ba2 100644 --- a/Iris/Iris/ProofMode/Tactics/Revert.lean +++ b/Iris/Iris/ProofMode/Tactics/Revert.lean @@ -69,7 +69,12 @@ private def RevertState.revertLeanForallHyp ProofModeM (@RevertState u prop bi origE origGoal) := do let { e, hyps, goal, reverted, pf } := st let x : Q($α) := mkFVar f - have Φ : Q($α → $prop) := ← mkLambdaFVars #[x] goal + -- abstract over x in the goal + let Φ ← mkLambdaFVars #[x] goal + -- make sure that the binder info is set to default, otherwise the + -- printing of BI.forall breaks + have Φ : Q($α → $prop) := + match Φ with | .lam n t b _ => .lam n t b .default | e => e let goal' : Q($prop) := q(BI.forall $Φ) have pf' : Q(($e ⊢ $goal') → ($origE ⊢ $origGoal)) := ← withLocalDeclDQ `h q($e ⊢ BI.forall $Φ) fun h => do diff --git a/Iris/Iris/Std/GenSets.lean b/Iris/Iris/Std/GenSets.lean index 68027f797..3c40aa10b 100644 --- a/Iris/Iris/Std/GenSets.lean +++ b/Iris/Iris/Std/GenSets.lean @@ -119,6 +119,9 @@ theorem eq_subset {X Y : S} : X ⊆ Y → Y ⊆ X → X = Y := by ext x exact ⟨H1 x, H2 x⟩ +instance : Std.Antisymm (fun x y : S => x ⊆ y) where + antisymm _ _ := eq_subset + /-- Proper subset is equivalent to subset plus inequality. -/ theorem ssubset_subset {X Y : S} : (X ⊂ Y) ↔ (X ⊆ Y ∧ X ≠ Y) := by simp [SSubset, Subset]; grind only @@ -353,10 +356,17 @@ theorem insert_subset_subset {s₁ s₂ : S} {x : A} (H : s₁ ⊆ s₂) : inser theorem subset_refl {s : S} : s ⊆ s := by intro x _; assumption +instance : Std.Refl (fun x y : S => x ⊆ y) where + refl _ := subset_refl + /-- Subset relation is transitive. -/ theorem subset_trans {s₁ s₂ s₃ : S} : s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃ := by intro h1 h2 x hx; exact h2 _ (h1 _ hx) +-- ↓ It looks like a face 🥹 +instance : Trans (fun x y : S => x ⊆ y) (·⊆ ·) (·⊆ ·) where + trans := subset_trans + /-! ### Disjointness -/ /-- Disjoint sets have empty intersection and vice versa. -/ @@ -442,6 +452,12 @@ theorem diff_subset_left {s₁ s₂ : S} : s₁ \ s₂ ⊆ s₁ := by intro y G; rw [mem_diff] at G exact G.left +theorem diff_self_diff_of_subset {s u : S} : s ⊆ u → u \ (u \ s) = s := by + intro su + apply eq_subset + · intro x; grind [mem_diff] + · intro x xs; simp [mem_diff, su x xs, xs] + /-- A set is disjoint from the part removed by taking a difference. -/ theorem disjoint_diff_right {s₁ s₂ : S} : s₁ ## (s₂ \ s₁) := by intro x ⟨hx1, hx2⟩ diff --git a/Iris/Iris/Tests.lean b/Iris/Iris/Tests.lean index ccd8f5cd1..5ff15ac5c 100644 --- a/Iris/Iris/Tests.lean +++ b/Iris/Iris/Tests.lean @@ -5,3 +5,5 @@ public import Iris.Tests.InstancesImport public import Iris.Tests.Notation public import Iris.Tests.Tactics public import Iris.Tests.HeapLang +public import Iris.Tests.Language +public import Iris.Tests.WP diff --git a/Iris/Iris/Tests/Language.lean b/Iris/Iris/Tests/Language.lean new file mode 100644 index 000000000..28afb5ec5 --- /dev/null +++ b/Iris/Iris/Tests/Language.lean @@ -0,0 +1,80 @@ +/- +Copyright (c) 2026 Fernando Leal. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Iris.ProgramLogic.Language + +@[expose] public section + +namespace Iris.Tests +open Iris ProgramLogic Language Notation + +/-! This section provides tests for notation used for the Language interface. -/ +section Notation + +/-- +info: (e, σ) --> (e, σ, []) : Prop +-/ +#guard_msgs in +variable (e : Expr) (σ : State) (obs : Obs) [PrimStep Expr State Obs] in +#check (PrimStep.primStep (e, σ) obs (e,σ,[])) + +/-- +info: (t, σ) -->ₜₚ (t, σ) : Prop +-/ +#guard_msgs in +variable (t : List Expr) (σ : State) (obs : List Obs) [Language Expr State Obs Val] in +#check (Language.Step (t, σ) obs (t,σ)) + +/-- +info: (t, σ) -->ₜₚ^[0] (t, σ) : Prop +-/ +#guard_msgs in +variable (t : List Expr) (σ : State) (obs : List Obs) [Language Expr State Obs Val] in +#check (Language.NSteps 0 (t, σ) obs (t,σ)) + +/-- +info: (t, σ) -·->ₜₚ (t, σ) : Prop +-/ +#guard_msgs in +variable (t : List Expr) (σ : State) [Language Expr State Obs Val] in +#check (ErasedStep (t, σ) (t,σ)) + +/-- +info: e -ᵖ-> e : Prop +-/ +#guard_msgs in +variable (e : Expr) [Language Expr State Obs Val] in +#check (PurePrimStep e e) + +/-- +info: e -ᵖ->^[0] e : Prop +-/ +#guard_msgs in +variable (e : Expr) [Language Expr State Obs Val] in +#check (Relation.Iterate PurePrimStep 0 e e) + +/-- +info: e -ᵖ->* e : Prop +-/ +#guard_msgs in +variable (e : Expr) [Language Expr State Obs Val] in +#check (FromMathlib.Relation.ReflTransGen PurePrimStep e e) + +/-- +info: e -ᵖ->* e : Prop +-/ +#guard_msgs in +variable (e : Expr) [Language Expr State Obs Val] in +#check (FromMathlib.Relation.ReflTransGen PurePrimStep e e) + +/-- +info: t -ᵖ->ₜₚ* t : Prop +-/ +#guard_msgs in +variable (t : List Expr) [Language Expr State Obs Val] in +#check (PureSteps t t) + +end Notation diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 71bbf0fff..edfb8d86c 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -362,6 +362,19 @@ example [BI PROP] (Φ : Bool → PROP) : ⊢ ∀ x, ⌜x = true⌝ -∗ iintro %x %hp H iexact H +/- Tests that `irevert` clears binder info (see https://github.com/leanprover-community/iris-lean/pull/393#issuecomment-4506443579) -/ +/-- +error: unsolved goals +PROP : Type u_1 +inst✝ : BI PROP +P : PROP +⊢ ⏎ + ⊢ ∀ x, P +-/ +#guard_msgs in +example [BI PROP] (P : PROP) {x : Nat} : ⊢ P := by + irevert %x + /- Tests `irevert` failing with dependency -/ /-- error: irevert: proofmode hypothesis H depends on x -/ #guard_msgs in diff --git a/Iris/Iris/Tests/WP.lean b/Iris/Iris/Tests/WP.lean new file mode 100644 index 000000000..5b09f796e --- /dev/null +++ b/Iris/Iris/Tests/WP.lean @@ -0,0 +1,206 @@ +/- +Copyright (c) 2026 Fernando Leal. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Iris.ProgramLogic.WeakestPre +public import Iris.HeapLang + +@[expose] public section + +namespace Iris.Tests +open Iris + +/- This section checks whether the syntax is recognized correctly for all combinations -/ +section TestWP +set_option linter.unusedVariables false + +variable (PROP Expr : Type _) (Val : outParam (Type _)) (A : Type _) +variable [Wp PROP Expr Val A] +variable [Wp PROP Expr Val Stuckness] +variable [TotalWP PROP Expr Val A] +variable [TotalWP PROP Expr Val Stuckness] + +variable (e : Expr) (s : A) (E : CoPset) + +-- Base no-binder cases +variable (Φ : Val → PROP) + +/-- info: WP e @ s ; E {{ Φ }} : PROP -/ +#guard_msgs in #check WP e @ s ; E {{ Φ }} +/-- info: WP e @ E {{ Φ }} : PROP -/ +#guard_msgs in #check WP e @ E {{ Φ }} +/-- info: WP e @ E ? {{ Φ }} : PROP -/ +#guard_msgs in #check WP e @ E ? {{ Φ }} +/-- info: WP e {{ Φ }} : PROP -/ +#guard_msgs in #check WP e {{ Φ }} +/-- info: WP e ? {{ Φ }} : PROP -/ +#guard_msgs in #check WP e ? {{ Φ }} + +/-- info: WP e @ s ; E [{ Φ }] : PROP -/ +#guard_msgs in #check WP e @ s ; E [{ Φ }] +/-- info: WP e @ E [{ Φ }] : PROP -/ +#guard_msgs in #check WP e @ E [{ Φ }] +/-- info: WP e @ E ? [{ Φ }] : PROP -/ +#guard_msgs in #check WP e @ E ? [{ Φ }] +/-- info: WP e [{ Φ }] : PROP -/ +#guard_msgs in #check WP e [{ Φ }] +/-- info: WP e ? [{ Φ }] : PROP -/ +#guard_msgs in #check WP e ? [{ Φ }] + +/-- info: WP e @ s ; E {{ Φ }} : PROP -/ +#guard_msgs in #check WP e @ s ; E ⦃ Φ ⦄ +/-- info: WP e @ E {{ Φ }} : PROP -/ +#guard_msgs in #check WP e @ E ⦃ Φ ⦄ +/-- info: WP e @ E ? {{ Φ }} : PROP -/ +#guard_msgs in #check WP e @ E ? ⦃ Φ ⦄ +/-- info: WP e {{ Φ }} : PROP -/ +#guard_msgs in #check WP e ⦃ Φ ⦄ +/-- info: WP e ? {{ Φ }} : PROP -/ +#guard_msgs in #check WP e ? ⦃ Φ ⦄ + +/-- info: WP e @ s ; E [{ Φ }] : PROP -/ +#guard_msgs in #check WP e @ s ; E 〖 Φ 〗 +/-- info: WP e @ E [{ Φ }] : PROP -/ +#guard_msgs in #check WP e @ E 〖 Φ 〗 +/-- info: WP e @ E ? [{ Φ }] : PROP -/ +#guard_msgs in #check WP e @ E ? 〖 Φ 〗 +/-- info: WP e [{ Φ }] : PROP -/ +#guard_msgs in #check WP e 〖 Φ 〗 +/-- info: WP e ? [{ Φ }] : PROP -/ +#guard_msgs in #check WP e ? 〖 Φ 〗 + +-- Base binder cases +variable (Φ : PROP) + +/-- info: WP e @ s ; E {{ v, Φ }} : PROP -/ +#guard_msgs in #check WP e @ s ; E {{v, Φ }} +/-- info: WP e @ E {{ v, Φ }} : PROP -/ +#guard_msgs in #check WP e @ E {{ v, Φ}} +/-- info: WP e @ E ? {{ v, Φ }} : PROP -/ +#guard_msgs in #check WP e @ E ? {{ v, Φ}} +/-- info: WP e {{ v, Φ }} : PROP -/ +#guard_msgs in #check WP e {{v, Φ }} +/-- info: WP e ? {{ v, Φ }} : PROP -/ +#guard_msgs in #check WP e ? {{v, Φ }} + +/-- info: WP e @ s ; E [{ v, Φ }] : PROP -/ +#guard_msgs in #check WP e @ s ; E [{v, Φ }] +/-- info: WP e @ E [{ v, Φ }] : PROP -/ +#guard_msgs in #check WP e @ E [{ v, Φ }] +/-- info: WP e @ E ? [{ v, Φ }] : PROP -/ +#guard_msgs in #check WP e @ E ? [{ v, Φ }] +/-- info: WP e [{ v, Φ }] : PROP -/ +#guard_msgs in #check WP e [{v, Φ }] +/-- info: WP e ? [{ v, Φ }] : PROP -/ +#guard_msgs in #check WP e ? [{v, Φ }] + +/-- info: WP e @ s ; E {{ v, Φ }} : PROP -/ +#guard_msgs in #check WP e @ s ; E ⦃v, Φ⦄ +/-- info: WP e @ E {{ v, Φ }} : PROP -/ +#guard_msgs in #check WP e @ E ⦃v, Φ⦄ +/-- info: WP e @ E ? {{ v, Φ }} : PROP -/ +#guard_msgs in #check WP e @ E ? ⦃v, Φ⦄ +/-- info: WP e {{ v, Φ }} : PROP -/ +#guard_msgs in #check WP e ⦃v, Φ⦄ +/-- info: WP e ? {{ v, Φ }} : PROP -/ +#guard_msgs in #check WP e ? ⦃v, Φ⦄ + +/-- info: WP e @ s ; E [{ v, Φ }] : PROP -/ +#guard_msgs in #check WP e @ s ; E 〖v, Φ〗 +/-- info: WP e @ E [{ v, Φ }] : PROP -/ +#guard_msgs in #check WP e @ E 〖v, Φ〗 +/-- info: WP e @ E ? [{ v, Φ }] : PROP -/ +#guard_msgs in #check WP e @ E ? 〖v, Φ〗 +/-- info: WP e [{ v, Φ }] : PROP -/ +#guard_msgs in #check WP e 〖v, Φ〗 +/-- info: WP e ? [{ v, Φ }] : PROP -/ +#guard_msgs in #check WP e ? 〖v, Φ〗 + +-- BI binder cases +variable [BI PROP] + +/-- info: WP e ? {{ v, Φ ∗ Φ }} : PROP -/ +#guard_msgs in #check WP e ? {{v, Φ ∗ Φ}} +/-- info: WP e ? {{ v, Φ ∧ Φ }} : PROP -/ +#guard_msgs in #check WP e ? {{v, Φ ∧ Φ}} +/-- info: WP e ? {{ v, Φ ∨ Φ }} : PROP -/ +#guard_msgs in #check WP e ? {{v, Φ ∨ Φ}} +/-- info: WP e ? {{ v, Φ -∗ Φ }} : PROP -/ +#guard_msgs in #check WP e ? {{v, Φ -∗ Φ}} + +/-- info: WP e ? [{ v, Φ ∗ Φ }] : PROP -/ +#guard_msgs in #check WP e ? [{v, Φ ∗ Φ}] +/-- info: WP e ? [{ v, Φ -∗ Φ }] : PROP -/ +#guard_msgs in #check WP e ? [{v, Φ -∗ Φ}] + +/-- info: WP e ? {{ v, Φ ∗ Φ }} : PROP -/ +#guard_msgs in #check WP e ? ⦃v, Φ ∗ Φ⦄ +/-- info: WP e ? [{ v, Φ ∗ Φ }] : PROP -/ +#guard_msgs in #check WP e ? 〖v, Φ ∗ Φ〗 + +/-- info: WP e @ E {{ v, Φ ∗ Φ }} : PROP -/ +#guard_msgs in #check WP e @ E {{v, Φ ∗ Φ}} +/-- info: WP e {{ v, Φ -∗ Φ }} : PROP -/ +#guard_msgs in #check WP e {{v, Φ -∗ Φ}} + +-- BI no-binder cases +variable (Φ : Val → PROP) + +/-- info: WP e ? {{ v, Φ v ∗ Φ v }} : PROP -/ +#guard_msgs in #check WP e ? {{v, Φ v ∗ Φ v}} +/-- info: WP e ? {{ v, Φ v ∧ Φ v }} : PROP -/ +#guard_msgs in #check WP e ? {{v, Φ v ∧ Φ v}} +/-- info: WP e ? {{ v, Φ v ∨ Φ v }} : PROP -/ +#guard_msgs in #check WP e ? {{v, Φ v ∨ Φ v}} +/-- info: WP e ? {{ v, Φ v -∗ Φ v }} : PROP -/ +#guard_msgs in #check WP e ? {{v, Φ v -∗ Φ v}} +/-- info: WP e ? [{ v, Φ v ∗ Φ v }] : PROP -/ +#guard_msgs in #check WP e ? [{v, Φ v ∗ Φ v}] +/-- info: WP e ? [{ v, Φ v -∗ Φ v }] : PROP -/ +#guard_msgs in #check WP e ? [{v, Φ v -∗ Φ v}] +/-- info: WP e ? {{ v, Φ v ∗ Φ v }} : PROP -/ +#guard_msgs in #check WP e ? ⦃v, Φ v ∗ Φ v⦄ +/-- info: WP e ? [{ v, Φ v ∗ Φ v }] : PROP -/ +#guard_msgs in #check WP e ? 〖v, Φ v ∗ Φ v〗 +/-- info: WP e @ E {{ v, Φ v ∗ Φ v }} : PROP -/ +#guard_msgs in #check WP e @ E {{v, Φ v ∗ Φ v}} +/-- info: WP e {{ v, Φ v -∗ Φ v }} : PROP -/ +#guard_msgs in #check WP e {{v, Φ v -∗ Φ v}} + +end TestWP + +section HeapLangTestWP +set_option linter.unusedVariables false + +open Iris.HeapLang + +variable (PROP : Type _) [BI PROP] +variable [Wp PROP Exp Val Stuckness] +variable (E : CoPset) (Φ : Val → PROP) (P : PROP) + +/-- info: WP hl(#1) {{ Φ }} : PROP -/ +#guard_msgs in #check WP hl(#1) {{ Φ }} +/-- info: WP hl((#1 + #2)) {{ Φ }} : PROP -/ +#guard_msgs in #check WP hl(#1 + #2) {{ Φ }} +/-- info: WP hl((#1 < #2)) {{ Φ }} : PROP -/ +#guard_msgs in #check WP hl(#1 < #2) {{ Φ }} +/-- info: WP hl(if (#0 < #1) then #1 else #2) {{ Φ }} : PROP -/ +#guard_msgs in #check WP hl(if #0 < #1 then #1 else #2) {{ Φ }} +/-- info: WP hl((λ x, x)) {{ Φ }} : PROP -/ +#guard_msgs in #check WP hl(λ x, x) {{ Φ }} +/-- info: WP hl((rec f x := f x)) {{ Φ }} : PROP -/ +#guard_msgs in #check WP hl(rec f x := f x) {{ Φ }} +/-- info: WP hl(#1; #2) {{ Φ }} : PROP -/ +#guard_msgs in #check WP hl(#1; #2) {{ Φ }} +/-- info: WP hl((#1, #2)) {{ Φ }} : PROP -/ +#guard_msgs in #check WP hl((#1, #2)) {{ Φ }} +/-- info: WP hl(ref(#0)) {{ Φ }} : PROP -/ +#guard_msgs in #check WP hl(ref(#0)) {{ Φ }} +/-- info: WP hl(if (#1 < #2) then (#1 + #1) else #0) {{ Φ }} : PROP -/ +#guard_msgs in #check WP hl(if #1 < #2 then #1 + #1 else #0) {{ Φ }} +/-- info: WP hl(#1) {{ v, ⌜v = hl_val(#1)⌝ }} : PROP -/ +#guard_msgs in #check (WP hl(#1) {{ v, ⌜v = hl_val(#1)⌝ }} : PROP) + +end HeapLangTestWP diff --git a/Iris/PORTING.md b/Iris/PORTING.md index d3c20031d..deb1b7be8 100644 --- a/Iris/PORTING.md +++ b/Iris/PORTING.md @@ -87,14 +87,14 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p - [x] Unit - [x] Emtpy - [x] Product - - [ ] Sum + - [x] Sum - [x] Discrete - [x] Leibniz - [x] Option - [x] Later - [x] Discrete functions - [x] Isomorphisms - - [ ] Sigma + - [x] Sigma - [ ] `proofmode_classes.v` - [ ] IsOp - [ ] `reservation_map.v` @@ -259,7 +259,7 @@ Some porting tasks will require other tasks as dependencies, the GitHub issues p - [ ] Fupd mask change laws - [ ] Fupd step derived rules - [ ] Fupd plainly general laws -- [ ] `weakestpre.v` +- [x] `weakestpre.v` - [ ] `lib/atomic.v` - [ ] `lib/core.v` - [ ] `lib/counterexamples.v` @@ -289,3 +289,4 @@ See proofmode at https://leanprover-community.github.io/iris-lean/ - [x] `language.v` - [x] `ectx_language.v` - [x] `ectxi_language.v` + - [x] `weakestpre.v`