diff --git a/Iris/Iris/ProofMode/Expr.lean b/Iris/Iris/ProofMode/Expr.lean index 4655aa822..63f556053 100644 --- a/Iris/Iris/ProofMode/Expr.lean +++ b/Iris/Iris/ProofMode/Expr.lean @@ -205,6 +205,35 @@ partial def Hyps.intuitionisticIVarIds {u prop bi} : | _, .hyp _ _ ivar p _ _ => if isTrue p then [ivar] else [] | _, .sep _ _ _ _ lhs rhs => lhs.intuitionisticIVarIds ++ rhs.intuitionisticIVarIds +/-- + Given any hypotheses `hyps` representing `e`, filter in all spatial hypotheses + and prove that `e` implies the set of spatial hypotheses. +-/ +def Hyps.buildAccuProof {prop : Q(Type u)} {bi : Q(BI $prop)} {e} + (hyps : Hyps bi e) : (spatialProps : Q($prop)) × Q($e ⊢ $spatialProps) := + let ⟨spatialProps, pf⟩ := buildAccuProofAux hyps (e' := q(iprop(emp))) q(iprop(emp)) q(.rfl) + let pf : Q($e ⊢ $spatialProps) := q(sep_emp.mpr.trans $pf) + ⟨spatialProps, pf⟩ + where + buildAccuProofAux {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e e' : Q($prop)} + (hyps : Hyps bi e) (spatialProps : Q($prop)) (pf : Q($e' ⊢ $spatialProps)) : + (newSpatialProps : Q($prop)) × Q($e ∗ $e' ⊢ $newSpatialProps) := + match hyps with + | .emp _ => ⟨spatialProps, q(emp_sep.mp.trans $pf)⟩ + | .hyp _ _ _ p ty _ => + match matchBool p with + | .inl _ => + ⟨spatialProps, q((sep_mono_left intuitionistically_elim_emp).trans (emp_sep.mp.trans $pf))⟩ + | .inr _ => + if spatialProps == q(iprop(emp)) then + let pf : Q($e' ⊢ iprop(emp)) := pf + ⟨ty, q((sep_mono_right $pf).trans sep_emp.mp)⟩ + else ⟨q(iprop($ty ∗ $spatialProps)), q(sep_mono_right $pf)⟩ + | .sep _ _ _ _ lhs rhs => + let ⟨spatialPropsR, pfR⟩ := buildAccuProofAux rhs spatialProps pf + let ⟨spatialPropsLR, pfLR⟩ := buildAccuProofAux lhs spatialPropsR pfR + ⟨q($spatialPropsLR), q(sep_assoc.mp.trans $pfLR)⟩ + variable (oldIVar : IVarId) (new : Name) {prop : Q(Type u)} {bi : Q(BI $prop)} in def Hyps.rename : ∀ {e}, Hyps bi e → Option (Hyps bi e) | _, .emp _ => none diff --git a/Iris/Iris/ProofMode/Porting.lean b/Iris/Iris/ProofMode/Porting.lean index f239a4f0a..a62a49fd1 100644 --- a/Iris/Iris/ProofMode/Porting.lean +++ b/Iris/Iris/ProofMode/Porting.lean @@ -56,7 +56,7 @@ import Iris.Std.RocqPorting #rocq_concept proofmode "Tactics" "iAssert" ported "ihave _ : _" #rocq_concept proofmode "Tactics" "iRewrite" ported "irewrite" #rocq_concept proofmode "Tactics" "iInv" missing "" -#rocq_concept proofmode "Tactics" "iAccu" missing "" +#rocq_concept proofmode "Tactics" "iAccu" ported "iaccu" #rocq_concept proofmode "Tactics" "rules for trivial" ported "itrivial" #rocq_concept proofmode "Intro Patterns" missing "" diff --git a/Iris/Iris/ProofMode/Tactics.lean b/Iris/Iris/ProofMode/Tactics.lean index f74191c1c..2ce9de956 100644 --- a/Iris/Iris/ProofMode/Tactics.lean +++ b/Iris/Iris/ProofMode/Tactics.lean @@ -1,6 +1,7 @@ /- A description of the tactics can be found in `tactics.md`. -/ module +public meta import Iris.ProofMode.Tactics.Accu public meta import Iris.ProofMode.Tactics.Apply public meta import Iris.ProofMode.Tactics.Assumption public meta import Iris.ProofMode.Tactics.Basic diff --git a/Iris/Iris/ProofMode/Tactics/Accu.lean b/Iris/Iris/ProofMode/Tactics/Accu.lean new file mode 100644 index 000000000..76c3d6dc1 --- /dev/null +++ b/Iris/Iris/ProofMode/Tactics/Accu.lean @@ -0,0 +1,32 @@ +/- +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.ProofModeM + +namespace Iris.ProofMode + +public meta section +open Lean Elab Tactic Meta Qq + +/-- + Given that the proof goal is a metavariable, `iaccu` combines all hypotheses + in the spatial context with the separating conjunction and solves the proof + goal by unifying the metavariable with the combined proposition. +-/ +elab "iaccu" : tactic => do + ProofModeM.runTactic λ mvar { hyps, goal, .. } => do + if !goal.isMVar then + throwError m!"iaccu: {goal} is not a metavariable" + + let ⟨spatial, pf⟩ := hyps.buildAccuProof + + -- Assign and unify the metavariable + let defEq ← isDefEq goal spatial + if !defEq then + throwError "iaccu: could not assign goal metavariable to {spatial}" + + mvar.assign pf diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index 49c042c62..f8c234699 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -2856,6 +2856,36 @@ example {n : Nat} {P T : Nat → PROP} {Q : Nat → Prop} {h1 : Q n} {_ : (Q n) end iloeb +section iaccu + +/-- Tests `iaccu` with spatial hypotheses `HQ`, `HR1`, `HR2` and `HT`. -/ +example [BI PROP] (P Q R1 R2 S T : PROP) : + (□ P -∗ Q -∗ (R1 ∗ R2) -∗ □ S -∗ T -∗ ∃ U, U ∧ ⌜U = iprop(Q ∗ R1 ∗ R2 ∗ T)⌝) := by + iintro #HP HQ ⟨HR1, HR2⟩ #HS HT + iexists ?_ + isplit + · iaccu + · ipureintro <;> rfl + +/-- Tests `iaccu` where there is no spatial hypothesis in the context. -/ +example [BI PROP] (P Q R : PROP) : + (□ P -∗ □ Q -∗ □ R -∗ ∃ S, S ∧ ⌜S = iprop(emp)⌝) := by + iintro #HP #HQ #HR + iexists ?_ + isplit + · iaccu + · ipureintro <;> rfl + +/- Tests `iaccu` where the proof goal is not a metavariable -/ +/-- error: iaccu: R is not a metavariable -/ +#guard_msgs in +example [BI PROP] (P Q R : PROP) : + □ P -∗ Q -∗ R := by + iintro #HP HQ + iaccu + +end iaccu + section iinduction /-- Inductively defined binary tree data structure -/ diff --git a/Iris/tactics.md b/Iris/tactics.md index 6b4f2cc97..e4dc259de 100644 --- a/Iris/tactics.md +++ b/Iris/tactics.md @@ -46,6 +46,7 @@ The proof mode maintains three contexts: the *pure* (Lean) context, the *intuiti - `ispecialize` [*pmTerm*](#proof-mode-terms) — Specialize a hypothesis according to [*pmTerm*](#proof-mode-terms). - `iexact` *H* — Solve the goal with the hypothesis *H*. - `iassumption` — Solve the goal with a matching hypothesis from the intuitionistic or spatial context. +- `iaccu` — Given the goal is a metavariable, solve the goal by combining all hypotheses in the spatial context with the separating conjunction and unifying the metavariable with the combined proposition. ## Modalities