From 3e55b4021852d07e49e142d4e99072e86cd00cbe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Klaus=20Kra=C3=9Fnitzer?= Date: Tue, 14 Jul 2026 17:17:24 +0200 Subject: [PATCH] feat: port HeapLang pure step tactics Port the wp_pure wrapper tactic family from iris_heap_lang/proofmode.v: wp_lam, wp_let, wp_seq, wp_closure, wp_if, wp_if_true, wp_if_false, wp_proj, wp_inj, wp_pair, wp_unop, wp_binop, wp_op, wp_case, and wp_match. The Lean implementation follows the Rocq implementation with these tactics being thin wrappers around wp_pure. Raise the precedence of wp_pure's focus argument to hl_exp:10 mirroring wp_bind. At default precedence, e.g. `wp_pure ; wp_lam` misparses the focus pattern instead of sequencing. Import PrimitiveLaws from HeapLang/ProofMode, since the wp_rec macro expands to an application of the wp_rec lemma defined there. Add a test section per tactic covering at least one successful and one failing case --- Iris/Iris/HeapLang/ProofMode.lean | 22 +- Iris/Iris/Tests/HeapLang/WeakestPre.lean | 567 ++++++++++++++++++++++- 2 files changed, 585 insertions(+), 4 deletions(-) diff --git a/Iris/Iris/HeapLang/ProofMode.lean b/Iris/Iris/HeapLang/ProofMode.lean index f71882eb7..9492c94b2 100644 --- a/Iris/Iris/HeapLang/ProofMode.lean +++ b/Iris/Iris/HeapLang/ProofMode.lean @@ -1,12 +1,14 @@ /- -Copyright (c) 2026 Fernando Leal. All rights reserved. +Copyright (c) 2026 Fernando Leal, Klaus Kraßnitzer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fernando Leal, Klaus Kraßnitzer -/ module public import Iris.ProofMode public import Iris.HeapLang.Tactic public import Iris.HeapLang.Instances +public import Iris.HeapLang.PrimitiveLaws public import Iris.ProgramLogic.WeakestPre public import Iris.ProgramLogic.Language public import Iris.ProgramLogic.EctxLanguage @@ -343,7 +345,7 @@ public theorem tac_wp_pure [ι : IrisGS_gen hlc Exp GF] {Δ Δ'} {s : Stuckness} refine .trans (BI.laterN_mono _ H) ?_ iintro $ !> -; itrivial -elab "wp_pure " colGt ppSpace focus:hl_exp : tactic => +elab "wp_pure " colGt ppSpace focus:hl_exp:10 : tactic => ProofModeM.runTacticWp fun mvar {hyps, ι, s, E, e, Φ, ..} => do let focus ← elabTermEnsuringTypeQ (← `(hl($focus))) q(HeapLang.Exp) trace[wp_pure] m!"Focusing with {focus}" @@ -375,5 +377,21 @@ macro "wp_pures" : tactic => `(tactic| repeat wp_pure) macro "wp_rec" : tactic => `(tactic | (wp_bind _ _; iapply $(mkIdent `wp_rec):ident; rfl; imodintro; wp_finish)) +macro "wp_if" : tactic => `(tactic | wp_pure (if _ then _ else _)) +macro "wp_if_true" : tactic => `(tactic | wp_pure (if #true then _ else _)) +macro "wp_if_false" : tactic => `(tactic | wp_pure (if #false then _ else _)) +macro "wp_unop" : tactic => `(tactic | wp_pure (&(Exp.unop _ _))) +macro "wp_binop" : tactic => `(tactic | wp_pure (&(Exp.binop _ _ _))) +macro "wp_op" : tactic => `(tactic | first | wp_unop | wp_binop) +macro "wp_lam" : tactic => `(tactic | wp_rec) +macro "wp_let" : tactic => `(tactic | (wp_pure (rec _ &(.named _) := _); wp_lam)) +macro "wp_seq" : tactic => `(tactic | (wp_pure (rec _ _ := _); wp_lam)) +macro "wp_proj" : tactic => `(tactic | first | wp_pure (fst(_)) | wp_pure (snd(_))) +macro "wp_case" : tactic => `(tactic | wp_pure (&(Exp.case _ _ _))) +macro "wp_inj" : tactic => `(tactic | first | wp_pure (injl(_)) | wp_pure (injr(_))) +macro "wp_pair" : tactic => `(tactic | wp_pure ((_, _))) +macro "wp_closure" : tactic => `(tactic | wp_pure (rec &_ &_ := _)) +macro "wp_match" : tactic => `(tactic | (wp_case; wp_closure; wp_lam)) + initialize registerTraceClass `wp_bind initialize registerTraceClass `wp_pure diff --git a/Iris/Iris/Tests/HeapLang/WeakestPre.lean b/Iris/Iris/Tests/HeapLang/WeakestPre.lean index ffd2e2ef0..62477bfb5 100644 --- a/Iris/Iris/Tests/HeapLang/WeakestPre.lean +++ b/Iris/Iris/Tests/HeapLang/WeakestPre.lean @@ -1,6 +1,7 @@ /- -Copyright (c) 2026 Fernando Leal. All rights reserved. +Copyright (c) 2026 Fernando Leal, Klaus Kraßnitzer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fernando Leal, Klaus Kraßnitzer -/ module @@ -224,6 +225,568 @@ n : Int example (n : Int) : ⊢@{IProp GF} WP hl((#1 * #2 <<< #3 ≤ #n + (#1 &&& #2 ^^^ #3)) = #true) {{ v, ⌜v = hl_val(#true)⌝ }} := by wp_pures +end wp_pure +section pure_tactics -end wp_pure +variable {GF : BundledGFunctors} [HeapLangGS hlc GF] + +section wp_lam + +def addOne : Val := hl_val% λ x, x + #1 + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl((#1 + #1)) {{ v, ⌜v = hl_val(#2)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(v(λ x, x + #1) #1) {{ v, ⌜v = hl_val(#2)⌝ }} := by + wp_lam + +/-- +error: iapply: cannot apply WP hl(v(&?_) v(&?_)) @ ?_ ; ?_ {{ ?_ }} to WP hl(let x := #1; (x + #1)) {{ v, ⌜v = hl_val(#2)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl((λ x, x + #1) #1) {{ v, ⌜v = hl_val(#2)⌝ }} := by + wp_lam + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl((#1 + #1)) {{ v, ⌜v = hl_val(#2)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(&addOne #1) {{ v, ⌜v = hl_val(#2)⌝ }} := by + wp_lam + +/-- +error: iapply: cannot apply WP hl(v(&?_) v(&?_)) @ ?_ ; ?_ {{ ?_ }} to WP hl(v(&addOne) (#1 + #1)) {{ v, ⌜v = hl_val(#3)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(&addOne (#1 + #1)) {{ v, ⌜v = hl_val(#3)⌝ }} := by + wp_lam + +end wp_lam + +section wp_let + +/-- +error: Tactic `wp_pure` failed: Cannot find expression to evaluate + +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl(#1; #2) {{ v, ⌜v = hl_val(#2)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(#1; #2) {{ v, ⌜v = hl_val(#2)⌝ }} := by + wp_let + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl((#1 + #1)) {{ v, ⌜v = hl_val(#2)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(let x := #1; x + #1) {{ v, ⌜v = hl_val(#2)⌝ }} := by + wp_let + +end wp_let + +section wp_seq + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ |={⊤}=> ⌜hl_val(#2) = hl_val(#2)⌝ +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(#1; #2) {{ v, ⌜v = hl_val(#2)⌝ }} := by + wp_seq + +/-- +error: Tactic `wp_pure` failed: Cannot find expression to evaluate + +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl(let x := #1; x) {{ v, ⌜v = hl_val(#1)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(let x := #1; x) {{ v, ⌜v = hl_val(#1)⌝ }} := by + wp_seq + +end wp_seq + +section wp_closure + +/-- +error: Tactic `wp_pure` failed: Cannot find expression to evaluate + +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl((#1 + #1)) {{ v, ⌜v = hl_val(#2)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(#1 + #1) {{ v, ⌜v = hl_val(#2)⌝ }} := by + wp_closure + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl((v(λ x, (x + #1))) #1) {{ v, ⌜v = hl_val(#2)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl((λ x, x + #1) #1) {{ v, ⌜v = hl_val(#2)⌝ }} := by + wp_closure + +end wp_closure + +section wp_if + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ |={⊤}=> ⌜hl_val(#1) = hl_val(#1)⌝ +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(if #true then #1 else #2) {{ v, ⌜v = hl_val(#1)⌝ }} := by + wp_if + +/-- +error: Tactic `wp_pure` failed: Cannot find expression to evaluate + +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl((#1 + #2)) {{ v, ⌜v = hl_val(#3)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(#1 + #2) {{ v, ⌜v = hl_val(#3)⌝ }} := by + wp_if + +end wp_if + +section wp_if_true + +/-- +error: Tactic `wp_pure` failed: Cannot find expression to evaluate + +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl(if #false then #1 else #2) {{ v, ⌜v = hl_val(#2)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(if #false then #1 else #2) {{ v, ⌜v = hl_val(#2)⌝ }} := by + wp_if_true + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ |={⊤}=> ⌜hl_val(#1) = hl_val(#1)⌝ +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(if #true then #1 else #2) {{ v, ⌜v = hl_val(#1)⌝ }} := by + wp_if_true + +end wp_if_true + +section wp_if_false + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ |={⊤}=> ⌜hl_val(#2) = hl_val(#2)⌝ +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(if #false then #1 else #2) {{ v, ⌜v = hl_val(#2)⌝ }} := by + wp_if_false + +/-- +error: Tactic `wp_pure` failed: Cannot find expression to evaluate + +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl(if #true then #1 else #2) {{ v, ⌜v = hl_val(#1)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(if #true then #1 else #2) {{ v, ⌜v = hl_val(#1)⌝ }} := by + wp_if_false + +end wp_if_false + +section wp_proj + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ |={⊤}=> ⌜hl_val(#1) = hl_val(#1)⌝ +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(fst(v((#1, #2)))) {{ v, ⌜v = hl_val(#1)⌝ }} := by + wp_proj + +/-- +error: Tactic `wp_pure` failed: Cannot find expression to evaluate + +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl((#1, #2)) {{ v, ⌜v = hl_val((#1, #2))⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl((#1, #2)) {{ v, ⌜v = hl_val((#1, #2))⌝ }} := by + wp_proj + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ |={⊤}=> ⌜hl_val(#2) = hl_val(#2)⌝ +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(snd(v((#1, #2)))) {{ v, ⌜v = hl_val(#2)⌝ }} := by + wp_proj + +end wp_proj + +section wp_inj + +/-- +error: Tactic `wp_pure` failed: Cannot find expression to evaluate + +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl(injr((#1 + #1))) {{ v, ⌜v = hl_val(injr(#2))⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(injr(#1 + #1)) {{ v, ⌜v = hl_val(injr(#2))⌝ }} := by + wp_inj + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ |={⊤}=> ⌜hl_val(injr(#1)) = hl_val(injr(#1))⌝ +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(injr(#1)) {{ v, ⌜v = hl_val(injr(#1))⌝ }} := by + wp_inj + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ |={⊤}=> ⌜hl_val(injl(#1)) = hl_val(injl(#1))⌝ +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(injl(#1)) {{ v, ⌜v = hl_val(injl(#1))⌝ }} := by + wp_inj + +end wp_inj + +section wp_pair + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ |={⊤}=> ⌜hl_val((#1, #2)) = hl_val((#1, #2))⌝ +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl((#1, #2)) {{ v, ⌜v = hl_val((#1, #2))⌝ }} := by + wp_pair + +/-- +error: Tactic `wp_pure` failed: Cannot find expression to evaluate + +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl(((#1 + #1), #2)) {{ v, ⌜v = hl_val((#2, #2))⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl((#1 + #1, #2)) {{ v, ⌜v = hl_val((#2, #2))⌝ }} := by + wp_pair + +end wp_pair + +section wp_unop + +/-- +error: Tactic `wp_pure` failed: Cannot find expression to evaluate + +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl((#1 + #2)) {{ v, ⌜v = hl_val(#3)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(#1 + #2) {{ v, ⌜v = hl_val(#3)⌝ }} := by + wp_unop + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ |={⊤}=> ⌜hl_val(#!true) = hl_val(#false)⌝ +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(~#true) {{ v, ⌜v = hl_val(#false)⌝ }} := by + wp_unop + +end wp_unop + +section wp_binop + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ |={⊤}=> ⌜hl_val(#(1 + 2)) = hl_val(#3)⌝ +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(#1 + #2) {{ v, ⌜v = hl_val(#3)⌝ }} := by + wp_binop + +/-- +error: Tactic `wp_pure` failed: Cannot find expression to evaluate + +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl((~#true)) {{ v, ⌜v = hl_val(#false)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(~#true) {{ v, ⌜v = hl_val(#false)⌝ }} := by + wp_binop + +end wp_binop + +section wp_op + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ |={⊤}=> ⌜hl_val(#!true) = hl_val(#false)⌝ +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(~#true) {{ v, ⌜v = hl_val(#false)⌝ }} := by + wp_op + +/-- +error: Tactic `wp_pure` failed: Cannot find expression to evaluate + +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl(if #true then #1 else #2) {{ v, ⌜v = hl_val(#1)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(if #true then #1 else #2) {{ v, ⌜v = hl_val(#1)⌝ }} := by + wp_op + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ |={⊤}=> ⌜hl_val(#(1 + 2)) = hl_val(#3)⌝ +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(#1 + #2) {{ v, ⌜v = hl_val(#3)⌝ }} := by + wp_op + +end wp_op + +section wp_case + +/-- +error: Tactic `wp_pure` failed: Cannot find expression to evaluate + +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl(match injl(#1) with | injl(x) => (x + #1) | injr(y) => y) {{ v, ⌜v = hl_val(#2)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} + WP hl(match injl(#1) with | injl(x) => x + #1 | injr(y) => y) + {{ v, ⌜v = hl_val(#2)⌝ }} := by + wp_case + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl(let x := #1; (x + #1)) {{ v, ⌜v = hl_val(#2)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} + WP hl(match v(injl(#1)) with | injl(x) => x + #1 | injr(y) => y) + {{ v, ⌜v = hl_val(#2)⌝ }} := by + wp_case + +end wp_case + +section wp_match + +/-- +error: unsolved goals +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl((#1 + #1)) {{ v, ⌜v = hl_val(#2)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} + WP hl(match v(injl(#1)) with | injl(x) => x + #1 | injr(y) => y) + {{ v, ⌜v = hl_val(#2)⌝ }} := by + wp_match + +/-- +error: Tactic `wp_pure` failed: Cannot find expression to evaluate + +hlc : HasLC +GF✝ : BundledGFunctors +ι : IrisGS_gen hlc Exp GF✝ +GF : BundledGFunctors +inst✝ : HeapLangGS hlc GF +⊢ ⏎ + ⊢ WP hl(if #true then #1 else #2) {{ v, ⌜v = hl_val(#1)⌝ }} +-/ +#guard_msgs in +example : ⊢@{IProp GF} WP hl(if #true then #1 else #2) {{ v, ⌜v = hl_val(#1)⌝ }} := by + wp_match + +end wp_match + +end pure_tactics