diff --git a/Iris/Iris/ProofMode/Expr.lean b/Iris/Iris/ProofMode/Expr.lean index 63f556053..8e0293403 100644 --- a/Iris/Iris/ProofMode/Expr.lean +++ b/Iris/Iris/ProofMode/Expr.lean @@ -479,6 +479,24 @@ def Hyps.replace : m (Option ((e' : Q($prop)) × Hyps bi e' × Q($e ⊢ $e'))) : let some ⟨_, hyps', pf⟩ ← hyps.replaceCore bi e ivar repl | return none return some ⟨_, hyps', q(replace_finish $pf)⟩ +def Hyps.evalReplace [Monad m] [MonadLiftT MetaM m] + {u} {prop : Q(Type u)} {bi : Q(BI $prop)} (ivar : IVarId) + (repl : (ty : Q($prop)) → m ((ty' : Q($prop)) × Q($ty ⊢ $ty'))) : + ∀ {e}, Hyps bi e → m (Option ((e' : Q($prop)) × Hyps bi e' × Q($e ⊢ $e'))) + | _, .emp _ => return none + | _, .hyp _ name ivar' p ty _ => + if ivar == ivar' then do + let ⟨ty', h⟩ ← repl ty + return some ⟨_, .mkHyp bi name ivar p ty', + q(intuitionisticallyIf_mono (p := $p) $h)⟩ + else return none + | _, .sep _ _ _ _ lhs rhs => do + if let some ⟨_, lhs', h⟩ ← lhs.evalReplace ivar repl then + return some ⟨_, .mkSep lhs' rhs, q(sep_mono_left $h)⟩ + if let some ⟨_, rhs', h⟩ ← rhs.evalReplace ivar repl then + return some ⟨_, .mkSep lhs rhs', q(sep_mono_right $h)⟩ + return none + end replace section dependency diff --git a/Iris/Iris/ProofMode/Porting.lean b/Iris/Iris/ProofMode/Porting.lean index a62a49fd1..6d1c7dbd7 100644 --- a/Iris/Iris/ProofMode/Porting.lean +++ b/Iris/Iris/ProofMode/Porting.lean @@ -19,9 +19,9 @@ import Iris.Std.RocqPorting #rocq_concept proofmode "Tactics" "iStopProof" ported "istop" #rocq_concept proofmode "Tactics" "iRename" ported "irename" #rocq_concept proofmode "Tactics" "iClear" ported "iclear" -#rocq_concept proofmode "Tactics" "iEval" missing "" -#rocq_concept proofmode "Tactics" "iSimpl" missing "" -#rocq_concept proofmode "Tactics" "iUnfold" missing "" +#rocq_concept proofmode "Tactics" "iEval" ported "ieval" +#rocq_concept proofmode "Tactics" "iSimpl" ported "isimp" +#rocq_concept proofmode "Tactics" "iUnfold" ported "iunfold" #rocq_concept proofmode "Tactics" "iExact" ported "iexact" #rocq_concept proofmode "Tactics" "iAssumption" ported "iassumption" #rocq_concept proofmode "Tactics" "iAssumptionCoq" ignored "weird tactic" diff --git a/Iris/Iris/ProofMode/Tactics.lean b/Iris/Iris/ProofMode/Tactics.lean index 2ce9de956..db5829cc2 100644 --- a/Iris/Iris/ProofMode/Tactics.lean +++ b/Iris/Iris/ProofMode/Tactics.lean @@ -8,6 +8,7 @@ public meta import Iris.ProofMode.Tactics.Basic public meta import Iris.ProofMode.Tactics.Cases public meta import Iris.ProofMode.Tactics.Clear public meta import Iris.ProofMode.Tactics.Combine +public meta import Iris.ProofMode.Tactics.Eval public meta import Iris.ProofMode.Tactics.Exact public meta import Iris.ProofMode.Tactics.ExFalso public meta import Iris.ProofMode.Tactics.Exists diff --git a/Iris/Iris/ProofMode/Tactics/Eval.lean b/Iris/Iris/ProofMode/Tactics/Eval.lean new file mode 100644 index 000000000..0aa377cda --- /dev/null +++ b/Iris/Iris/ProofMode/Tactics/Eval.lean @@ -0,0 +1,133 @@ +/- +Copyright (c) 2026 Alvin Tang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Sammler, Alvin Tang +-/ +module + +public meta import Iris.ProofMode.Patterns.SelPattern +public meta import Iris.ProofMode.ProofModeM + +namespace Iris.ProofMode + +public meta section +open Lean Elab Tactic Meta Qq BI Lean.Parser.Tactic + +/-- For iteratively applying the tactic sequences to selection targets in the context -/ +private structure EvalState {u} {prop : Q(Type u)} {bi : Q(BI $prop)} (e : Q($prop)) where + {newE : Q($prop)} + (newHyps : Hyps bi newE) + (pf : Q($e ⊢ $newE)) + +/-- + Apply the tactic sequence `tac` to transform `ty`, which is strengthened when + it is the goal or weakened when it is a hypothesis in the context. + + When `isGoal` is `true`, the tactic sequence results in the proof goal being *strengthened*. + When `isGoal` is `false`, the tactic sequence results in the hypothesis being *weakened*. + + The function returns the new expression and a proof that the expression + is strengthened/weakened. +-/ +private def iEvalOne {u} {prop : Q(Type u)} (bi : Q(BI $prop)) + (tac : TSyntax `Lean.Parser.Tactic.tacticSeq) (isGoal : Bool) (ty : Q($prop)) : + ProofModeM <| Q($prop) × Expr := do + let m : Q($prop) ← mkFreshExprMVar q($prop) + let pf ← mkFreshExprSyntheticOpaqueMVar <| if isGoal then q($m ⊢ $ty) else q($ty ⊢ $m) + let [g] ← evalTacticAt tac pf.mvarId! + | throwError "ieval: the supplied tactic does not produce exactly one subgoal" + let some #[_, _, lhs, rhs] ← g.getType <&> (·.appM? ``Entails) + | throwError "ieval: the goal is not Iris entailment upon applying the supplied tactic" + let newTy : Q($prop) := if isGoal then rhs else lhs + m.mvarId!.assign newTy + g.assign (q(.rfl) : Q($newTy ⊢ $newTy)) + return ⟨m, pf⟩ + +/-- + Apply the tactic sequence `tac` to either the proof goal (when `selTargets` + is `none`) or the hypotheses in the context specified by the selection targets. +-/ +private def iEvalCore {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e} + (hyps : Hyps bi e) (goal : Q($prop)) (tac : TSyntax `Lean.Parser.Tactic.tacticSeq) + (selTargets : Option <| List SelTarget) : ProofModeM Q($e ⊢ $goal) := do + match selTargets with + -- No selection pattern given, apply the tactics to the proof goal + | none => + let ⟨newGoal, (pf : Q($newGoal ⊢ $goal))⟩ ← iEvalOne (isGoal := true) bi tac goal + let pf' ← addBIGoal hyps newGoal + return q($(pf').trans $pf) + -- Selection patterns given, apply the tactics to the chosen hypotheses + | some selTargets => + let mut evalState : EvalState e := { newHyps := hyps, pf := q(.rfl) } + -- Iteratively apply the supplied tactic sequence to the selection targets + for selTarget in selTargets do + evalState ← match selTarget.kind with + | .pure _ => + throwError "ieval: pure hypotheses in the selection pattern is not supported" + | .ipm ivar => + let some ⟨newE, newHyps, pf⟩ ← evalState.newHyps.evalReplace ivar fun ty => do + let ⟨newTy, pf⟩ ← iEvalOne (isGoal := false) bi tac ty + return ⟨newTy, (pf : Q($ty ⊢ $newTy))⟩ + | throwError m!"ieval: unable to find the hypothesis {ivar.name} in the context" + pure { newE, newHyps, pf := q($(evalState.pf).trans $pf) } + let pf' ← addBIGoal evalState.newHyps goal + return q($(evalState.pf).trans $pf') + +/-- + `ieval (tac)` applies the tactic sequence `tac` to the proof goal. +-/ +elab "ieval " "(" tac:tacticSeq ")" : tactic => do + ProofModeM.runTactic λ mvar { hyps, goal, .. } => do + let pf ← iEvalCore hyps goal tac none + mvar.assign pf + +/-- + `ieval (tac) in spats` applies the tactic sequence `tac` to the Iris + hypotheses chosen by the selection pattern `spats`. Pure hypotheses are not + supported by this tactic. +-/ +elab "ieval " "(" tacs:tacticSeq ")" " in " spats:(colGt ppSpace selPat)+ : tactic => do + let selPats ← liftMacroM <| SelPat.parse spats + + ProofModeM.runTactic λ mvar { hyps, goal, .. } => do + let selTargets ← SelPat.resolve hyps selPats + let pf ← iEvalCore hyps goal tacs selTargets + mvar.assign pf + +/-- + `isimp` applies `simp` to the proof goal. This is shorthand for `ieval (simp)`. + + `isimp in spats` applies `simp` to the Iris hypotheses chosen by the + selection pattern `spats`. Pure hypotheses are not supported by this tactic. + This is shorthand for `ieval (simp) in spats`. + + One can also use `isimp [h₁, h₂, …, hₙ]`, `isimp [*]` and + `isimp only [h₁, h₂, …, hₙ]` for the tactic behaviour corresponding to + `simp [h₁, h₂, …, hₙ]`, `simp [*]` and `simp only [h₁, h₂, …, hₙ]`, + respectively. +-/ +syntax "isimp" optConfig (discharger)? (&" only")? (simpArgs)? + (" in " (colGt ppSpace selPat)+)? : tactic + +private def elabSimp (simp : TSyntax `tactic) + (spats : Option (TSyntaxArray `selPat)) : TacticM Unit := + match spats with + | none => do evalTactic (← `(tactic| ieval ($simp:tactic))) + | some spats => do evalTactic (← `(tactic| ieval ($simp:tactic) in $spats*)) + +elab_rules : tactic + | `(tactic| isimp $cfg* $[$disch]? $[[$args,*]]? $[in $spats*]?) => do + elabSimp (← `(tactic| simp $cfg* $[$disch]? $[[$args,*]]?)) spats + | `(tactic| isimp $cfg* $[$disch]? only $[[$args,*]]? $[in $spats*]?) => do + elabSimp (← `(tactic| simp $cfg* $[$disch]? only $[[$args,*]]?)) spats + +/-- `iunfold hs` applies `unfold hs` to the proof goal. This is shorthand for `ieval (unfold)`. -/ +macro "iunfold " hs:ident,+ : tactic => `(tactic| ieval (unfold $hs*)) + +/-- + `iunfold hs in spats` applies `unfold hs` to the Iris hypotheses chosen by + the selection pattern `spats`. Pure hypotheses are not supported by this tactic. + This is shorthand for `ieval (unfold hs) in spats`. +-/ +macro "iunfold " hs:ident,+ " in " spats:(colGt ppSpace selPat)* : tactic => + `(tactic| ieval (unfold $hs*) in $spats*) diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index f8c234699..654be1fbb 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -2856,6 +2856,95 @@ example {n : Nat} {P T : Nat → PROP} {Q : Nat → Prop} {h1 : Q n} {_ : (Q n) end iloeb +section ieval + +/-- Tests `ieval` and `isimp` to simplify the goal and specific Iris hypotheses. -/ +example [BI PROP] {u v w x y z : Nat} : + ⌜(x + y) + 3 = 4⌝ ∗ ⌜(w + z) + 1 = Nat.succ 2⌝ ∗ ⌜(u + v) = v⌝ + ⊢@{PROP} ⌜Nat.succ (x + y) = 2⌝ ∗ ⌜w + z = 2⌝ ∗ ⌜u = 0⌝ := by + iintro ⟨H1, H2, H3⟩ + -- Simplify `(x + y) + 3 = 4` as `x + y = 1` + isimp in H1 + isplitl [H1] + -- Simplify `(x + y).succ = 2` as `x + y = 1` + · isimp + iexact H1 + -- Simplify the goal `w + z + 1 = Nat.succ 2` as `w + z = 2` and `u + v = v` as `u = 0` + · ieval (simp) in H2 H3 + iframe + +/- Tests `isimp` with a pure hypothesis in the selection pattern -/ +/-- error: ieval: pure hypotheses in the selection pattern is not supported -/ +#guard_msgs in +example [BI PROP] {x y : Nat} : + ⌜(x + y) + 3 = 4⌝ ⊢@{PROP} ⌜Nat.succ (x + y) = 2⌝ := by + iintro #H + isimp in %x H + +/- Tests `isimp` with the simplification failing -/ +/-- error: `simp` made no progress -/ +#guard_msgs in +example [BI PROP] {x y : Nat} : ⌜x = 0⌝ ⊢@{PROP} ⌜x = 0⌝ := by + iintro #H + isimp in H + +/-- Tests `isimp` with variants of `simp` -/ +example [BI PROP] {m n p q : Nat} (h1 : m = n + 1) (h2 : r = t) (h3 : s = t) : + ⌜p + q = q + p⌝ ⊢@{PROP} ⌜m - 1 = n⌝ ∗ ⌜r = s⌝ ∗ ⌜q + p = p + q⌝ := by + iintro H + isplitr + -- Simplification with a hypothesis + · isimp [h1] + itrivial + · isplitr + -- Simplification with all rules annotated with `[simp]` and all hypotheses + · isimp [*] + itrivial + -- Simplification only with specific rules + · isimp only [Nat.add_comm] in H + isimp only [Nat.add_comm] + iexact H + +private def def1 := 10 +private def def2 := def1 + +/-- Tests `iunfold` to unfold definitions in an Iris hypothesis and a proof goal -/ +example [BI PROP] : ⌜def2 = 10⌝ ⊢@{PROP} ⌜10 = 10⌝ ∗ ⌜def2 = 10⌝ := by + iintro #H + -- Unfold definitions in an Iris hypothesis + iunfold def2, def1 in H + iframe H + -- Unfold definitions in the proof goal + iunfold def2, def1 + ipureintro + .rfl + +/- Tests `ieval` where the supplied tactic solves the goal completely -/ +/-- error: ieval: the supplied tactic does not produce exactly one subgoal -/ +#guard_msgs in +example [BI PROP] {x y : Nat} (_ : False) : + ⌜(x + y) + 3 = 4⌝ ⊢@{PROP} ⌜Nat.succ (x + y) = 2⌝ := by + iintro H + ieval (contradiction) in H + +/- Tests `ieval` where the supplied tactic produces more than one subgoal -/ +/-- error: ieval: the supplied tactic does not produce exactly one subgoal -/ +#guard_msgs in +example [BI PROP] {x y : Nat} (h : False) : + ⌜(x + y) + 3 = 4⌝ ⊢@{PROP} ⌜Nat.succ (x + y) = 2⌝ := by + iintro H + ieval (cases x) in H + +/- Tests `ieval` where the given tactic breaks the Iris entailment -/ +/-- error: ieval: the goal is not Iris entailment upon applying the supplied tactic -/ +#guard_msgs in +example [BI PROP] {x y : Nat} : + ⌜(x + y) + 3 = 4⌝ ⊢@{PROP} ⌜Nat.succ (x + y) = 2⌝ := by + iintro H + ieval (exfalso) in H + +end ieval + section iaccu /-- Tests `iaccu` with spatial hypotheses `HQ`, `HR1`, `HR2` and `HT`. -/ diff --git a/Iris/tactics.md b/Iris/tactics.md index e4dc259de..c4d28c419 100644 --- a/Iris/tactics.md +++ b/Iris/tactics.md @@ -59,6 +59,9 @@ The proof mode maintains three contexts: the *pure* (Lean) context, the *intuiti ## Rewriting and Induction - `irewrite [`*rules*`]` (`at` *H* | `at ⊢`)? — Rewrite with internal equalities (`≡`). Each rule is a [*pmTerm*](#proof-mode-terms), optionally prefixed with `←` for right-to-left rewriting. Rewrites in the goal by default or in hypothesis *H*. Supports `(occs := ...)` config. Example: `irewrite [← Heq $$ %b] at H`. +- `ieval (`*tac*`)` (`in` [*selPats*](#selection-patterns))? — applies the tactic *tac* to the Iris hypotheses chosen by the selection pattern, if given, or otherwise to proof goal. The tactic *tac* should be a reduction or rewriting tactic such as `simp`, `dsimp` or `unfold`. Note that this tactic does not support pure hypotheses in the selection pattern, in which case *tac* should be used directly. +- `isimp` (*configItem*)\* (*discharger*)? (`only`)? (`[` *h₁*`,` ...`,` *hₙ* `]` | `[*]`)? (`in` [*selPats*](#selection-patterns))? — applies `simp` to the Iris hypotheses chosen by the selection pattern, if given, or otherwise to proof goal. This is a shorthand for `ieval (simp)`. One can also use `[*]` to include all hypotheses in the pure context for simplification, or explicitly specify the lemmas and hypotheses *h₁*, ..., *hₙ*. The optional keyword `only` stipulates the use of only these lemmas and hypotheses. Similar to the built-in tactic `simp`, one can also specify additional configurations (*configItem*) or include a tactic to discharge the side conditions on conditional rewrite rules (*discharger*). +- `iunfold` *x₁*`,` ...`,` *xₙ* (`in` [*selPats*](#selection-patterns))? — applies `unfold` with the arguments *x₁*, ..., *xₙ* to the Iris hypotheses chosen by the selection pattern, if given, or otherwise to proof goal. This is a shorthand for `ieval (unfold` *x₁*`,` ...`,` *xₙ*`)`. - `iloeb as` *IH* (`generalizing` [*selPats*](#selection-patterns))? — Löb induction: adds the induction hypothesis *IH* (guarded by `▷`) to the intuitionistic context. All spatial hypotheses — plus anything selected by [*selPats*](#selection-patterns), including pure variables via `%x` — are generalized into the induction hypothesis. For every hypothesis *H* in *selPats*, all hypotheses dependent on *H* must also be included in *selPats*. - `iloeb as` *IH* `generalizing!` [*selPats*](#selection-patterns) — same as `iloeb as` *IH* `generalizing` [*selPats*](#selection-patterns), except that for every hypothesis *H* in [*selPats*](#selection-patterns), all hypotheses dependent on *H* are implicitly also generalised. - `iinduction` *e* (`using` *r*)? (`with` (*tac*)? `|` *constr₁* `=>` *tac₁* `|` ... `|` *constrₙ* `=>` *tacₙ*)? — All spatial hypotheses, as well as pure/intuitionistic hypotheses dependent on *e*, are generalised and included as premises in the induction hypotheses. The induction principle is determined by the recursor name *r*, if given, or otherwise the default induction principle is chosen. The `with` clause enables alternative names to be given to variables and induction hypotheses. Each of *constr₁*, ..., *constrₙ* is the constructor name followed by the alternative names. Alternative names can be replaced with holes (`_`) for them to remain inaccessible. Each of *tac₁*, ..., *tacₙ* is either a tactic sequence for the induction subgoal or a hole (`_` or `?_`); the latter defers the induction subgoal. The tactic *tac* is optionally given, which is the first tactic applied to all induction subgoals.