From b1a98c29890e7908ea5c75273321705ba89e19da Mon Sep 17 00:00:00 2001 From: Oliver Soeser Date: Fri, 4 Jul 2025 15:00:11 +0200 Subject: [PATCH 1/7] feat: irevert tactic --- src/Iris/ProofMode/Tactics.lean | 1 + src/Iris/ProofMode/Tactics/Revert.lean | 68 ++++++++++++++++++++++++++ tactics.md | 45 ++++++++--------- 3 files changed, 92 insertions(+), 22 deletions(-) create mode 100644 src/Iris/ProofMode/Tactics/Revert.lean diff --git a/src/Iris/ProofMode/Tactics.lean b/src/Iris/ProofMode/Tactics.lean index 7758fa71..62b7cd1e 100644 --- a/src/Iris/ProofMode/Tactics.lean +++ b/src/Iris/ProofMode/Tactics.lean @@ -11,6 +11,7 @@ import Iris.ProofMode.Tactics.LeftRight import Iris.ProofMode.Tactics.Move import Iris.ProofMode.Tactics.Pure import Iris.ProofMode.Tactics.Remove +import Iris.ProofMode.Tactics.Revert import Iris.ProofMode.Tactics.Rename import Iris.ProofMode.Tactics.Specialize import Iris.ProofMode.Tactics.Split diff --git a/src/Iris/ProofMode/Tactics/Revert.lean b/src/Iris/ProofMode/Tactics/Revert.lean new file mode 100644 index 00000000..b6ba9843 --- /dev/null +++ b/src/Iris/ProofMode/Tactics/Revert.lean @@ -0,0 +1,68 @@ +/- +Copyright (c) 2025 Oliver Soeser. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Oliver Soeser +-/ +import Iris.ProofMode.Tactics.Cases + +namespace Iris.ProofMode +open Lean Elab Tactic Meta Qq BI Std + +theorem wand_revert [BI PROP] {P Q A1 A2 : PROP} + (h1 : P ⊣⊢ A1 ∗ A2) (h2 : A1 ⊢ A2 -∗ Q) : P ⊢ Q := + h1.mp.trans (wand_elim h2) + +theorem forall_revert [BI PROP] {P : PROP} {Ψ : α → PROP} + (h : P ⊢ ∀ x, Ψ x) : ∀ x, P ⊢ Ψ x := + λ x => h.trans (forall_elim x) + +theorem pure_revert [BI PROP] {P Q : PROP} {φ : Prop} + (h : P ⊢ ⌜φ⌝ -∗ Q) : φ → P ⊢ Q := + λ hp => (sep_emp.mpr.trans (sep_mono .rfl (pure_intro hp))).trans (wand_elim h) + +elab "irevert" colGt hyp:ident : tactic => do + let (mvar, { u, prop, bi, e, hyps, goal, .. }) ← istart (← getMainGoal) + + mvar.withContext do + let uniq? ← try? do pure (← hyps.findWithInfo hyp) + if let (some uniq) := uniq? then + let ⟨e', hyps', out, _, _, _, h⟩ := hyps.remove true uniq + let m : Q($e' ⊢ $out -∗ $goal) ← mkFreshExprSyntheticOpaqueMVar <| + IrisGoal.toExpr { hyps := hyps', goal := q(wand $out $goal), .. } + + let pf : Q($e ⊢ $goal) := q(wand_revert $h $m) + + mvar.assign pf + replaceMainGoal [m.mvarId!] + else + let f ← getFVarId hyp + let (some ldecl) := ((← getLCtx).find? f) | throwError "unknown identifier" + + let bibase := mkAppN (mkConst ``BI.toBIBase [u]) #[prop, bi] + + let φ := ldecl.type + let (_, mvarId) ← mvar.revert #[f] + mvarId.withContext do + if ← Meta.isProp φ then + let p := mkAppN (mkConst ``BI.pure [u]) #[prop, bibase, φ] + + let m ← mkFreshExprSyntheticOpaqueMVar <| + IrisGoal.toExpr { u, prop, bi, hyps, goal := mkAppN (mkConst ``wand [u]) #[prop, bibase, p, goal], .. } + + let pf := mkAppN (mkConst ``pure_revert [u]) #[prop, bi, e, goal, φ, m] + + mvarId.assign pf + replaceMainGoal [m.mvarId!] + else + let v ← Meta.getLevel φ + let Φ ← mapForallTelescope' (λ t _ => do + let (some ig) := parseIrisGoal? t | throwError "not in proof mode" + return ig.goal + ) (Expr.mvar mvarId) + let m ← mkFreshExprSyntheticOpaqueMVar <| + IrisGoal.toExpr { u, prop, bi, hyps, goal := mkAppN (mkConst ``BI.forall [u, v]) #[prop, bibase, φ, Φ], ..} + + let pf := mkAppN (mkConst ``forall_revert [u, v]) #[prop, φ, bi, e, Φ, m] + + mvarId.assign pf + replaceMainGoal [m.mvarId!] diff --git a/tactics.md b/tactics.md index 4b0d7b56..0e1e64d8 100644 --- a/tactics.md +++ b/tactics.md @@ -1,28 +1,29 @@ # Tactics -| Syntax | Description | -|----------------------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| -| `istart` | Start the proof mode. | -| `istop` | Stop the proof mode. | -| `irename` *nameFrom* `into` *nameTo* | Rename the hypothesis *nameFrom* to *nameTo*. | -| `iclear` *hyp* | Discard the hypothesis *hyp*. | -| `iexists` *x* | Resolve an existential quantifier in the goal by introducing the variable *x*. | -| `iexact` *hyp* | Solve the goal with the hypothesis *hyp*. | -| `iassumption_lean` | Solve the goal with a hypothesis of the type `⊢ Q` from the Lean context. | -| `iassumption` | Solve the goal with a hypothesis from any context (pure, intuitionistic or spatial). | -| `iex_falso` | Change the goal to `False`. | -| `ipure` *hyp* | Move the hypothesis *hyp* to the pure context. | -| `iintuitionistic` *hyp* | Move the hypothesis *hyp* to the intuitionistic context. | -| `ispatial` *hyp* | Move the hypothesis *hyp* to the spatial context. | -| `iemp_intro` | Solve the goal if it is `emp` and discard all hypotheses. | -| `ipure_intro` | Turn a goal of the form `⌜φ⌝` into a Lean goal `φ`. | -| `ispecialize` *hyp* *args* `as` *name* | Specialize the wand or universal quantifier *hyp* with the hypotheses and variables *args* and assign the name *name* to the resulting hypothesis. | -| `isplit` | Split a conjunction (e.g. `∧`) into two goals, using the entire spatial context for both of them. | -| `isplit` {`l`\|`r`} | Split a separating conjunction (e.g. `∗`) into two goals, using the entire spatial context for the left (`l`) or right (`r`) side. | +| Syntax | Description | +| -------------------------------------- | ------------------------------------------------------------ | +| `istart` | Start the proof mode. | +| `istop` | Stop the proof mode. | +| `irename` *nameFrom* `into` *nameTo* | Rename the hypothesis *nameFrom* to *nameTo*. | +| `iclear` *hyp* | Discard the hypothesis *hyp*. | +| `iexists` *x* | Resolve an existential quantifier in the goal by introducing the variable *x*. | +| `iexact` *hyp* | Solve the goal with the hypothesis *hyp*. | +| `iassumption_lean` | Solve the goal with a hypothesis of the type `⊢ Q` from the Lean context. | +| `iassumption` | Solve the goal with a hypothesis from any context (pure, intuitionistic or spatial). | +| `iex_falso` | Change the goal to `False`. | +| `ipure` *hyp* | Move the hypothesis *hyp* to the pure context. | +| `iintuitionistic` *hyp* | Move the hypothesis *hyp* to the intuitionistic context. | +| `ispatial` *hyp* | Move the hypothesis *hyp* to the spatial context. | +| `iemp_intro` | Solve the goal if it is `emp` and discard all hypotheses. | +| `ipure_intro` | Turn a goal of the form `⌜φ⌝` into a Lean goal `φ`. | +| `ispecialize` *hyp* *args* `as` *name* | Specialize the wand or universal quantifier *hyp* with the hypotheses and variables *args* and assign the name *name* to the resulting hypothesis. | +| `isplit` | Split a conjunction (e.g. `∧`) into two goals, using the entire spatial context for both of them. | +| `isplit` {`l`\|`r`} | Split a separating conjunction (e.g. `∗`) into two goals, using the entire spatial context for the left (`l`) or right (`r`) side. | | `isplit` {`l`\|`r`} `[`*hyps*`]` | Split a separating conjunction (e.g. `∗`) into two goals, using the hypotheses *hyps* as the spatial context for the left (`l`) or right (`r`) side. The remaining hypotheses in the spatial context are used for the opposite side. | -| `ileft`
`iright` | Choose to prove the left (`ileft`) or right (`iright`) side of a disjunction in the goal. | -| `icases` *hyp* `with` *cases-pat* | Destruct the hypothesis *hyp* using the cases pattern *cases-pat*. | -| `iintro` *cases-pats* | Introduce up to multiple hypotheses and destruct them using the cases patterns *cases-pats*. | +| `ileft`
`iright` | Choose to prove the left (`ileft`) or right (`iright`) side of a disjunction in the goal. | +| `icases` *hyp* `with` *cases-pat* | Destruct the hypothesis *hyp* using the cases pattern *cases-pat*. | +| `iintro` *cases-pats* | Introduce up to multiple hypotheses and destruct them using the cases patterns *cases-pats*. | +| `irevert` *hyp* | Revert the hypothesis *hyp*. | ## Cases Patterns From 2c3277980aa4d76f67ddb9c6fa6908345dd4ffbd Mon Sep 17 00:00:00 2001 From: Oliver Soeser Date: Sat, 5 Jul 2025 13:02:30 +0200 Subject: [PATCH 2/7] use Qq for irevert --- src/Iris/ProofMode/Tactics/Revert.lean | 26 ++++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) diff --git a/src/Iris/ProofMode/Tactics/Revert.lean b/src/Iris/ProofMode/Tactics/Revert.lean index b6ba9843..6fabed76 100644 --- a/src/Iris/ProofMode/Tactics/Revert.lean +++ b/src/Iris/ProofMode/Tactics/Revert.lean @@ -38,31 +38,33 @@ elab "irevert" colGt hyp:ident : tactic => do let f ← getFVarId hyp let (some ldecl) := ((← getLCtx).find? f) | throwError "unknown identifier" - let bibase := mkAppN (mkConst ``BI.toBIBase [u]) #[prop, bi] + let bibase : Q(BIBase $prop) := q(@BI.toBIBase $prop $bi) + + let v : Level ← Meta.getLevel ldecl.type + have α : Q(Sort v) := ldecl.type - let φ := ldecl.type let (_, mvarId) ← mvar.revert #[f] mvarId.withContext do - if ← Meta.isProp φ then - let p := mkAppN (mkConst ``BI.pure [u]) #[prop, bibase, φ] + if ← Meta.isProp α then + have φ : Q(Prop) := α + let p : Q($prop) := q(@BI.pure $prop $bibase $φ) - let m ← mkFreshExprSyntheticOpaqueMVar <| - IrisGoal.toExpr { u, prop, bi, hyps, goal := mkAppN (mkConst ``wand [u]) #[prop, bibase, p, goal], .. } + let m : Q($e ⊢ $p -∗ $goal) ← mkFreshExprSyntheticOpaqueMVar <| + IrisGoal.toExpr { u, prop, bi, hyps, goal := q(wand $p $goal), .. } - let pf := mkAppN (mkConst ``pure_revert [u]) #[prop, bi, e, goal, φ, m] + let pf : Q($φ → ($e ⊢ $goal)) := q(pure_revert $m) mvarId.assign pf replaceMainGoal [m.mvarId!] else - let v ← Meta.getLevel φ - let Φ ← mapForallTelescope' (λ t _ => do + let Φ : Q($α → $prop) ← mapForallTelescope' (λ t _ => do let (some ig) := parseIrisGoal? t | throwError "not in proof mode" return ig.goal ) (Expr.mvar mvarId) - let m ← mkFreshExprSyntheticOpaqueMVar <| - IrisGoal.toExpr { u, prop, bi, hyps, goal := mkAppN (mkConst ``BI.forall [u, v]) #[prop, bibase, φ, Φ], ..} + let m : Q($e ⊢ ∀ x, $Φ x) ← mkFreshExprSyntheticOpaqueMVar <| + IrisGoal.toExpr { u, prop, bi, hyps, goal := q(BI.forall $Φ), ..} - let pf := mkAppN (mkConst ``forall_revert [u, v]) #[prop, φ, bi, e, Φ, m] + let pf : Q(∀ (x : $α), $e ⊢ $Φ x) := q(forall_revert $m) mvarId.assign pf replaceMainGoal [m.mvarId!] From 8e38f9780c118b753ac97038e59fe21145fea125 Mon Sep 17 00:00:00 2001 From: Oliver Soeser Date: Mon, 7 Jul 2025 10:51:50 +0200 Subject: [PATCH 3/7] irevert tests --- src/Iris/Tests/Tactics.lean | 39 ++++++++++++++++++++++++++++++++++++- 1 file changed, 38 insertions(+), 1 deletion(-) diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean index 48c610a4..64efc456 100644 --- a/src/Iris/Tests/Tactics.lean +++ b/src/Iris/Tests/Tactics.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2022 Lars König. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Lars König +Authors: Lars König, Oliver Soeser -/ import Iris.BI import Iris.ProofMode @@ -115,6 +115,43 @@ theorem multiple_patterns [BI PROP] (Q : PROP) : ⊢ □ (P1 ∧ P2) -∗ Q ∨ end intro +-- revert +namespace revert + +theorem spatial [BI PROP] (P : PROP) (H : ⊢ P -∗ P) : P ⊢ P := by + iintro HP + irevert HP + exact H + +theorem intuitionistic [BI PROP] (P : PROP) (H : ⊢ □ P -∗ P) : □ P ⊢ P := by + iintro □HP + irevert HP + exact H + +theorem pure [BI PROP] (P : PROP) (Hφ : φ) : ⊢ (⌜φ⌝ -∗ P) -∗ P := by + iintro H + irevert Hφ + iexact H + +theorem «forall» [BI PROP] (Φ : α → PROP) : ⊢ (∀ x, Φ x) → Φ x := by + iintro H + irevert x + iexact H + +theorem multiple_spatial [BI PROP] (P Q : PROP) : + ⊢ (P -∗ P) -∗ P -∗ Q -∗ P := by + iintro H HP HQ + irevert HP + iexact H + +theorem multiple_intuitionistic [BI PROP] (P Q : PROP) : + ⊢ (□ P -∗ P) -∗ □ P -∗ Q -∗ P := by + iintro H □HP HQ + irevert HP + iexact H + +end revert + -- exists namespace «exists» From abee8fd290bee64ff0d4a930d1e73d7953c27707 Mon Sep 17 00:00:00 2001 From: Oliver Soeser Date: Thu, 31 Jul 2025 13:20:09 +0200 Subject: [PATCH 4/7] explicitly bind x --- src/Iris/Tests/Tactics.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean index 64efc456..87805624 100644 --- a/src/Iris/Tests/Tactics.lean +++ b/src/Iris/Tests/Tactics.lean @@ -133,7 +133,7 @@ theorem pure [BI PROP] (P : PROP) (Hφ : φ) : ⊢ (⌜φ⌝ -∗ P) -∗ P := b irevert Hφ iexact H -theorem «forall» [BI PROP] (Φ : α → PROP) : ⊢ (∀ x, Φ x) → Φ x := by +theorem «forall» [BI PROP] (x : α) (Φ : α → PROP) : ⊢ (∀ x, Φ x) → Φ x := by iintro H irevert x iexact H From 8c014f757fbb412520de92f864abd3e0bd0eaddf Mon Sep 17 00:00:00 2001 From: Oliver Soeser Date: Thu, 31 Jul 2025 13:26:13 +0200 Subject: [PATCH 5/7] fix whitespace anomaly --- tactics.md | 46 +++++++++++++++++++++++----------------------- 1 file changed, 23 insertions(+), 23 deletions(-) diff --git a/tactics.md b/tactics.md index 0e1e64d8..b769ec7d 100644 --- a/tactics.md +++ b/tactics.md @@ -1,29 +1,29 @@ # Tactics -| Syntax | Description | -| -------------------------------------- | ------------------------------------------------------------ | -| `istart` | Start the proof mode. | -| `istop` | Stop the proof mode. | -| `irename` *nameFrom* `into` *nameTo* | Rename the hypothesis *nameFrom* to *nameTo*. | -| `iclear` *hyp* | Discard the hypothesis *hyp*. | -| `iexists` *x* | Resolve an existential quantifier in the goal by introducing the variable *x*. | -| `iexact` *hyp* | Solve the goal with the hypothesis *hyp*. | -| `iassumption_lean` | Solve the goal with a hypothesis of the type `⊢ Q` from the Lean context. | -| `iassumption` | Solve the goal with a hypothesis from any context (pure, intuitionistic or spatial). | -| `iex_falso` | Change the goal to `False`. | -| `ipure` *hyp* | Move the hypothesis *hyp* to the pure context. | -| `iintuitionistic` *hyp* | Move the hypothesis *hyp* to the intuitionistic context. | -| `ispatial` *hyp* | Move the hypothesis *hyp* to the spatial context. | -| `iemp_intro` | Solve the goal if it is `emp` and discard all hypotheses. | -| `ipure_intro` | Turn a goal of the form `⌜φ⌝` into a Lean goal `φ`. | -| `ispecialize` *hyp* *args* `as` *name* | Specialize the wand or universal quantifier *hyp* with the hypotheses and variables *args* and assign the name *name* to the resulting hypothesis. | -| `isplit` | Split a conjunction (e.g. `∧`) into two goals, using the entire spatial context for both of them. | -| `isplit` {`l`\|`r`} | Split a separating conjunction (e.g. `∗`) into two goals, using the entire spatial context for the left (`l`) or right (`r`) side. | +| Syntax | Description | +|----------------------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| +| `istart` | Start the proof mode. | +| `istop` | Stop the proof mode. | +| `irename` *nameFrom* `into` *nameTo* | Rename the hypothesis *nameFrom* to *nameTo*. | +| `iclear` *hyp* | Discard the hypothesis *hyp*. | +| `iexists` *x* | Resolve an existential quantifier in the goal by introducing the variable *x*. | +| `iexact` *hyp* | Solve the goal with the hypothesis *hyp*. | +| `iassumption_lean` | Solve the goal with a hypothesis of the type `⊢ Q` from the Lean context. | +| `iassumption` | Solve the goal with a hypothesis from any context (pure, intuitionistic or spatial). | +| `iex_falso` | Change the goal to `False`. | +| `ipure` *hyp* | Move the hypothesis *hyp* to the pure context. | +| `iintuitionistic` *hyp* | Move the hypothesis *hyp* to the intuitionistic context. | +| `ispatial` *hyp* | Move the hypothesis *hyp* to the spatial context. | +| `iemp_intro` | Solve the goal if it is `emp` and discard all hypotheses. | +| `ipure_intro` | Turn a goal of the form `⌜φ⌝` into a Lean goal `φ`. | +| `ispecialize` *hyp* *args* `as` *name* | Specialize the wand or universal quantifier *hyp* with the hypotheses and variables *args* and assign the name *name* to the resulting hypothesis. | +| `isplit` | Split a conjunction (e.g. `∧`) into two goals, using the entire spatial context for both of them. | +| `isplit` {`l`\|`r`} | Split a separating conjunction (e.g. `∗`) into two goals, using the entire spatial context for the left (`l`) or right (`r`) side. | | `isplit` {`l`\|`r`} `[`*hyps*`]` | Split a separating conjunction (e.g. `∗`) into two goals, using the hypotheses *hyps* as the spatial context for the left (`l`) or right (`r`) side. The remaining hypotheses in the spatial context are used for the opposite side. | -| `ileft`
`iright` | Choose to prove the left (`ileft`) or right (`iright`) side of a disjunction in the goal. | -| `icases` *hyp* `with` *cases-pat* | Destruct the hypothesis *hyp* using the cases pattern *cases-pat*. | -| `iintro` *cases-pats* | Introduce up to multiple hypotheses and destruct them using the cases patterns *cases-pats*. | -| `irevert` *hyp* | Revert the hypothesis *hyp*. | +| `ileft`
`iright` | Choose to prove the left (`ileft`) or right (`iright`) side of a disjunction in the goal. | +| `icases` *hyp* `with` *cases-pat* | Destruct the hypothesis *hyp* using the cases pattern *cases-pat*. | +| `iintro` *cases-pats* | Introduce up to multiple hypotheses and destruct them using the cases patterns *cases-pats*. | +| `irevert` *hyp* | Revert the hypothesis *hyp*. | ## Cases Patterns From ce592db3ec01b0c8387f882826ca33daa82aaa24 Mon Sep 17 00:00:00 2001 From: Oliver Soeser Date: Thu, 31 Jul 2025 14:48:43 +0200 Subject: [PATCH 6/7] descriptive error message --- src/Iris/ProofMode/Tactics/Revert.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Iris/ProofMode/Tactics/Revert.lean b/src/Iris/ProofMode/Tactics/Revert.lean index 6fabed76..35e80943 100644 --- a/src/Iris/ProofMode/Tactics/Revert.lean +++ b/src/Iris/ProofMode/Tactics/Revert.lean @@ -25,7 +25,7 @@ elab "irevert" colGt hyp:ident : tactic => do mvar.withContext do let uniq? ← try? do pure (← hyps.findWithInfo hyp) - if let (some uniq) := uniq? then + if let some uniq := uniq? then let ⟨e', hyps', out, _, _, _, h⟩ := hyps.remove true uniq let m : Q($e' ⊢ $out -∗ $goal) ← mkFreshExprSyntheticOpaqueMVar <| IrisGoal.toExpr { hyps := hyps', goal := q(wand $out $goal), .. } @@ -36,7 +36,7 @@ elab "irevert" colGt hyp:ident : tactic => do replaceMainGoal [m.mvarId!] else let f ← getFVarId hyp - let (some ldecl) := ((← getLCtx).find? f) | throwError "unknown identifier" + let some ldecl := (← getLCtx).find? f | throwError "irevert: {hyp.getId} not in scope" let bibase : Q(BIBase $prop) := q(@BI.toBIBase $prop $bi) @@ -58,7 +58,7 @@ elab "irevert" colGt hyp:ident : tactic => do replaceMainGoal [m.mvarId!] else let Φ : Q($α → $prop) ← mapForallTelescope' (λ t _ => do - let (some ig) := parseIrisGoal? t | throwError "not in proof mode" + let (some ig) := parseIrisGoal? t | throwError "irevert: not in proof mode" return ig.goal ) (Expr.mvar mvarId) let m : Q($e ⊢ ∀ x, $Φ x) ← mkFreshExprSyntheticOpaqueMVar <| From 2ad360f8fb79b5906369cd43987f82fe883d5a03 Mon Sep 17 00:00:00 2001 From: Oliver Soeser Date: Mon, 25 Aug 2025 11:59:01 +0200 Subject: [PATCH 7/7] simplify --- src/Iris/ProofMode/Tactics/Revert.lean | 4 +--- src/Iris/Tests/Tactics.lean | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Iris/ProofMode/Tactics/Revert.lean b/src/Iris/ProofMode/Tactics/Revert.lean index 35e80943..8c5c9442 100644 --- a/src/Iris/ProofMode/Tactics/Revert.lean +++ b/src/Iris/ProofMode/Tactics/Revert.lean @@ -30,9 +30,7 @@ elab "irevert" colGt hyp:ident : tactic => do let m : Q($e' ⊢ $out -∗ $goal) ← mkFreshExprSyntheticOpaqueMVar <| IrisGoal.toExpr { hyps := hyps', goal := q(wand $out $goal), .. } - let pf : Q($e ⊢ $goal) := q(wand_revert $h $m) - - mvar.assign pf + mvar.assign q(wand_revert $h $m) replaceMainGoal [m.mvarId!] else let f ← getFVarId hyp diff --git a/src/Iris/Tests/Tactics.lean b/src/Iris/Tests/Tactics.lean index 87805624..30b9ff3a 100644 --- a/src/Iris/Tests/Tactics.lean +++ b/src/Iris/Tests/Tactics.lean @@ -118,7 +118,7 @@ end intro -- revert namespace revert -theorem spatial [BI PROP] (P : PROP) (H : ⊢ P -∗ P) : P ⊢ P := by +theorem spatial [BI PROP] (P Q : PROP) (H : ⊢ P -∗ Q) : P ⊢ Q := by iintro HP irevert HP exact H