max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add Option.of_wp_eq and Except.of_wp_eq (#12161)

Browse source 
This PR adds `Option.of_wp_eq` and `Except.of_wp_eq`, similar to the
existing `Except.of_wp`. `Except.of_wp` is deprecated because applying
it requires prior generalization, at which point it is more convenient
to use `Except.of_wp_eq`.
This commit is contained in:
Sebastian Graf 2026-01-26 13:50:23 +01:00 • committed by GitHub
parent 1bf16f710e
commit 0bcac0d46c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 30 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/Std/Do/WP/Basic.lean
View file

@ -143,12 +143,27 @@ you want to use `mvcgen` to reason about `prog`.
theorem ReaderM.of_wp_run_eq {α} {x : α} {prog : ReaderM ρ α} (h : ReaderT.run prog r = x) (P : α → Prop) :
(⊢ₛ wp⟦prog⟧ (⇓ a _ => ⌜P a⌝) r) → P x := h ▸ (· True.intro)
/--
Adequacy lemma for `Except`.
Useful if you want to prove a property about a complex expression `prog : Except ε α` that you have
generalized to a variable `x` and you want to use `mvcgen` to reason about `prog`.
-/
theorem Except.of_wp_eq {ε α : Type u} {x prog : Except ε α} (h : prog = x) (P : Except ε α → Prop) :
(⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.error e)⌝⟩) → P x := by
subst h
intro hspec
simp only [wp, PredTrans.pushExcept_apply, PredTrans.pure_apply] at hspec
split at hspec
case h_1 a s' heq => rw[← heq] at hspec; exact hspec True.intro
case h_2 e s' heq => rw[← heq] at hspec; exact hspec True.intro
/--
Adequacy lemma for `Except`.
Useful if you want to prove a property about an expression `prog : Except ε α` and you want to use
`mvcgen` to reason about `prog`.
-/
theorem Except.of_wp {α} {prog : Except ε α} (P : Except ε α → Prop) :
@[deprecated Except.of_wp_eq (since := "2026-01-26")]
theorem Except.of_wp {ε α : Type u} {prog : Except ε α} (P : Except ε α → Prop) :
(⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.error e)⌝⟩) → P prog := by
intro hspec
simp only [wp, PredTrans.pushExcept_apply, PredTrans.pure_apply] at hspec
@ -156,6 +171,20 @@ theorem Except.of_wp {α} {prog : Except ε α} (P : Except ε α → Prop) :
case h_1 a s' heq => rw[← heq] at hspec; exact hspec True.intro
case h_2 e s' heq => rw[← heq] at hspec; exact hspec True.intro
/--
Adequacy lemma for `Option`.
Useful if you want to prove a property about a complex expression `prog : Option α` that you have
generalized to a variable `x` and you want to use `mvcgen` to reason about `prog`.
-/
theorem Option.of_wp_eq {α : Type u} {x prog : Option α} (h : prog = x) (P : Option α → Prop) :
(⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (some a)⌝, fun _ => ⌜P none⌝⟩) → P x := by
subst h
intro hspec
simp only [wp, PredTrans.pushOption_apply, PredTrans.pure_apply] at hspec
split at hspec
case h_1 a s' heq => rw[← heq] at hspec; exact hspec True.intro
case h_2 s' heq => rw[← heq] at hspec; exact hspec True.intro
/--
Adequacy lemma for `EStateM.run`.
Useful if you want to prove a property about an expression `x` defined as `EStateM.run prog s` and