feat: irevert tactic #74

MackieLoeffel · 2025-07-21T13:02:56Z

This should use the MakeAffinely ⌜ φ ⌝ P to add the <affine> modality in front of ⌜ φ ⌝ for logics that require it. Otherwise, irevert can make the goal unprovable. See
https://gitlab.mpi-sws.org/iris/iris/-/blob/306d8d024f9d6522c0e733fd7eb27b0af676d4ca/iris/proofmode/coq_tactics.v

MackieLoeffel · 2025-07-21T13:18:03Z

It would also be good to have tests for the failing cases:

What happens when the name is not used?

What happens when a pure hypothesis is used in another hypothesis?

For the second point: When I try the following test,

theorem fail [BI PROP] (Φ : Bool → PROP) : ⊢ ∀ x, <affine> ⌜x = true⌝ -∗ Φ x -∗ Φ x := by iintro x %_ H irevert x

something very weird happens:

Goals (1) PROP : Type u_1 inst : BI PROP Φ : Bool → PROP ⊢ ∗H : Φ _fvar.2200 ⊢ «forall» fun x x_1 => Φ x

-Original file line number
+Diff line change
@@ Expand Up / @@ -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

-Original file line number
+Diff line change
@@ -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), .. }
+          mvar.assign q(wand_revert $h $m)
+          replaceMainGoal [m.mvarId!]
+        else
+          let f ← getFVarId hyp
+          let some ldecl := (← getLCtx).find? f | throwError "irevert: {hyp.getId} not in scope"
+          let bibase : Q(BIBase $prop) := q(@BI.toBIBase $prop $bi)
+          let v : Level ← Meta.getLevel ldecl.type
+          have α : Q(Sort v) := ldecl.type
+          let (_, mvarId) ← mvar.revert #[f]
+          mvarId.withContext do
+            if ← Meta.isProp α then
+              have φ : Q(Prop) := α
+              let p : Q($prop) := q(@BI.pure $prop $bibase $φ)
+              let m : Q($e ⊢ $p -∗ $goal) ← mkFreshExprSyntheticOpaqueMVar <|
+                IrisGoal.toExpr { u, prop, bi, hyps, goal := q(wand $p $goal), .. }
+              let pf : Q($φ → ($e ⊢ $goal)) := q(pure_revert $m)
+              mvarId.assign pf
+              replaceMainGoal [m.mvarId!]
+            else
+              let Φ : Q($α → $prop) ← mapForallTelescope' (λ t _ => do
+                let (some ig) := parseIrisGoal? t | throwError "irevert: not in proof mode"
+                return ig.goal
+              ) (Expr.mvar mvarId)
+              let m : Q($e ⊢ ∀ x, $Φ x) ← mkFreshExprSyntheticOpaqueMVar <|
+                IrisGoal.toExpr { u, prop, bi, hyps, goal := q(BI.forall $Φ), ..}
+              let pf : Q(∀ (x : $α), $e ⊢ $Φ x) := q(forall_revert $m)
+              mvarId.assign pf
+              replaceMainGoal [m.mvarId!]

-Original file line number
+Diff line change
@@ -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
@@ Expand Down Expand Up @@
     end intro
+    -- revert
+    namespace revert
+    theorem spatial [BI PROP] (P Q : PROP) (H : ⊢ P -∗ Q) : P ⊢ Q := 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] (x : α) (Φ : α → PROP) : ⊢ (∀ x, Φ x) → Φ x := by
+      iintro H
+      irevert x
+      iexact H
+    theorem multiple_spatial [BI PROP] (P Q : PROP) :
+        ⊢ (P -∗ P) -∗ P -∗ <affine> Q -∗ P := by
+      iintro H HP HQ
+      irevert HP
+      iexact H
+    theorem multiple_intuitionistic [BI PROP] (P Q : PROP) :
+        ⊢ (□ P -∗ P) -∗ □ P -∗ <affine> Q -∗ P := by
+      iintro H □HP HQ
+      irevert HP
+      iexact H
+    end revert
     -- exists
     namespace «exists»
@@ Expand Down @@

-Original file line number
+Diff line change
@@ Expand Up / @@ -23,6 +23,7 @@ @@
     | `ileft`<br>`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
@@ Expand Down @@

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: irevert tactic #74

Uh oh!

Diff view

Diff view

There are no files selected for viewing

MackieLoeffel Jul 21, 2025

Uh oh!

MackieLoeffel Jul 21, 2025

Uh oh!

feat: irevert tactic #74

Are you sure you want to change the base?

Uh oh!

feat: irevert tactic #74

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

MackieLoeffel Jul 21, 2025

Choose a reason for hiding this comment

Uh oh!

MackieLoeffel Jul 21, 2025

Choose a reason for hiding this comment

Uh oh!