feat: remaining introduction patterns and case destruction patterns

Iris/Iris/ProofMode/Expr.lean

@@ -140,12 +140,13 @@ def Hyps.mkHyp {prop : Q(Type u)} (bi : Q(BI $prop))
     (name : Name) (ivar : IVarId) (p : Q(Bool)) (ty : Q($prop)) (e := q(iprop(□?$p $ty))) : Hyps bi e :=
   .hyp (mkIntuitionisticIf bi p (mkNameAnnotation name ivar ty)) name ivar p ty ⟨⟩
 
--- TODO: should this ensure that adding a hypothesis to emp creates a
--- hyp node instead of a sep node?
 def Hyps.add {prop : Q(Type u)} (bi : Q(BI $prop))
     (name : Name) (ivar : IVarId) (p : Q(Bool)) (ty : Q($prop)) {e} (h : Hyps bi e)
-    : Hyps bi q(iprop($e ∗ □?$p $ty)) :=
-  Hyps.mkSep h (.mkHyp bi name ivar p ty)
+    : (e' : Q($prop)) × Hyps bi e' × Q(iprop($e ∗ □?$p $ty ⊣⊢ $e')) :=
+  match h with
+  -- Adding a hypothesis to `emp` creates a `.hyp` node instead of a `.sep` node
+  | .emp _ => ⟨_, .mkHyp bi name ivar p ty, q(emp_sep)⟩
+  | _ => ⟨_, .mkSep h (.mkHyp bi name ivar p ty), q(.rfl)⟩
 
 partial def parseHyps? {prop : Q(Type u)} (bi : Q(BI $prop)) (expr : Expr) :
     Option ((s : Q($prop)) × Hyps bi s) := do
@@ -533,9 +534,9 @@ def Hyps.findWithInfo {u prop bi} (hyps : @Hyps u prop bi s) (name : Ident) : Me
 /-- Hyps.addWithInfo should be used by tactics that introduce a hypothesis based on the name given by the user. -/
 def Hyps.addWithInfo {prop : Q(Type u)} (bi : Q(BI $prop))
     (name : TSyntax ``binderIdent) (p : Q(Bool)) (ty : Q($prop)) {e} (h : Hyps bi e)
-    : MetaM (IVarId × Hyps bi q(iprop($e ∗ □?$p $ty))) := do
+    : MetaM (IVarId × (e' : Q($prop)) × Hyps bi e' × Q(iprop($e ∗ □?$p $ty ⊣⊢ $e'))) := do
   let ivar' ← mkFreshIVarId (isTrue p)
   let (nameTo, nameRef) ← getFreshName name
   addHypInfo nameRef nameTo ivar' prop ty (isBinder := true)
-  let hyps := Hyps.add bi nameTo ivar' p ty h
-  return ⟨ivar', hyps⟩
+  let ⟨e', hyps, pf⟩ := Hyps.add bi nameTo ivar' p ty h
+  return ⟨ivar', e', hyps, pf⟩

Iris/Iris/ProofMode/Patterns/CasesPattern.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, Alvin Tang
 -/
 module
 
@@ -15,50 +15,74 @@ open Lean
 declare_syntax_cat icasesPat
 syntax icasesPatAlts := sepBy1(icasesPat, " | ")
 syntax binderIdent : icasesPat
+/-- Drop the hypothesis. -/
 syntax "-" : icasesPat
+/-- Frame the hypothesis and cancel it against the goal. -/
 syntax "$" : icasesPat
+/--
+  Destruct a (separating) conjunction or existential; an existential variable is
+  bound with `%x` where `x` is the name for it.
+-/
 syntax "⟨" icasesPatAlts,* "⟩" : icasesPat
+/-- Destruct a disjunction, one goal per disjunct. -/
 syntax "(" icasesPatAlts ")" : icasesPat
-syntax "%" binderIdent : icasesPat
+/-- Move the hypothesis to the pure Lean context and give it a name. -/
+syntax "%" rcasesPat : icasesPat
+/-- Move the hypothesis to the intuitionistic context and destruct the proposition. -/
 syntax "#" icasesPat : icasesPat
+/-- Move the hypothesis to the spatial context and destruct the proposition. -/
 syntax "∗" icasesPat : icasesPat
+/-- Eliminate the modality at the top of the hypothesis and destruct the remaining proposition. -/
 syntax ">" icasesPat : icasesPat
+/-- Introduce a pure equality and use it for rewriting in the backward direction. -/
+syntax "←" : icasesPat
+/-- Introduce a pure equality and use it for rewriting in the forward direction. -/
+syntax "→" : icasesPat
 
--- TODO: attach syntax to iCasesPat such that one can use withRef to
--- associate the errors with the right part of the syntax
 inductive iCasesPat
-  | one (name : TSyntax ``binderIdent)
-  | clear
-  | frame
-  | conjunction (args : List iCasesPat)
-  | disjunction (args : List iCasesPat)
-  | pure           (pat : TSyntax ``binderIdent)
-  | intuitionistic (pat : iCasesPat)
-  | spatial        (pat : iCasesPat)
-  | mod            (pat : iCasesPat)
+  | one (ref : Syntax) (name : TSyntax ``binderIdent)
+  | clear (ref : Syntax)
+  | frame (ref : Syntax)
+  | conjunction (ref : Syntax) (args : List iCasesPat)
+  | disjunction (ref : Syntax) (args : List iCasesPat)
+  | pure (ref : Syntax) (pat : TSyntax `rcasesPat)
+  | intuitionistic (ref : Syntax) (pat : iCasesPat)
+  | spatial (ref : Syntax) (pat : iCasesPat)
+  | mod (ref : Syntax) (pat : iCasesPat)
+  | rewrite (ref : Syntax) (forward : Bool)
   deriving Repr, Inhabited
 
+def iCasesPat.ref : iCasesPat → Syntax
+  | .one r _ | .clear r | .frame r | .conjunction r _ | .disjunction r _
+  | .pure r _ | .intuitionistic r _ | .spatial r _ | .mod r _ | .rewrite r _ => r
+
 partial def iCasesPat.parse (pat : TSyntax `icasesPat) : MacroM iCasesPat := do
   match go ⟨← expandMacros pat⟩ with
   | none => Macro.throwUnsupported
   | some pat => return pat
 where
-  go : TSyntax `icasesPat → Option iCasesPat
-  | `(icasesPat| $name:binderIdent) => some <| .one name
-  | `(icasesPat| -) => some <| .clear
-  | `(icasesPat| $) => some <| .frame
-  | `(icasesPat| ⟨$[$args],*⟩) => args.mapM goAlts |>.map (.conjunction ·.toList)
-  | `(icasesPat| %$pat:binderIdent) => some <| .pure pat
-  | `(icasesPat| #$pat) => go pat |>.map .intuitionistic
-  | `(icasesPat| ∗$pat) => go pat |>.map .spatial
-  | `(icasesPat| >$pat) => go pat |>.map .mod
-  | `(icasesPat| ($pat)) => goAlts pat
-  | _ => none
-  goAlts : TSyntax ``icasesPatAlts → Option iCasesPat
-  | `(icasesPatAlts| $args|*) =>
-    match args.getElems with
-    | #[arg] => go arg
-    | args   => args.mapM go |>.map (.disjunction ·.toList)
-  | _ => none
+  go (stx : TSyntax `icasesPat) : Option iCasesPat :=
+    let ref := stx.raw
+    match ref with
+    | `(icasesPat| $name:binderIdent) => some <| .one ref name
+    | `(icasesPat| -) => some <| .clear ref
+    | `(icasesPat| $) => some <| .frame ref
+    | `(icasesPat| ⟨$[$args],*⟩) => args.mapM goAlts |>.map (.conjunction ref ·.toList)
+    | `(icasesPat| %$pat:rcasesPat) => some <| .pure ref pat
+    | `(icasesPat| #$pat) => go pat |>.map <| .intuitionistic ref
+    | `(icasesPat| ∗$pat) => go pat |>.map <| .spatial ref
+    | `(icasesPat| >$pat) => go pat |>.map <| .mod ref
+    | `(icasesPat| ($pat)) => goAlts pat
+    | `(icasesPat| ←) => some <| .rewrite ref false
+    | `(icasesPat| →) => some <| .rewrite ref true
+    | _ => none
+  goAlts (stx : TSyntax ``icasesPatAlts) : Option iCasesPat :=
+    let ref := stx.raw
+    match stx with
+    | `(icasesPatAlts| $args|*) =>
+      match args.getElems with
+      | #[arg] => go arg
+      | args   => args.mapM go |>.map (.disjunction ref ·.toList)
+    | _ => none
 
 end Iris.ProofMode

Iris/Iris/ProofMode/Patterns/IntroPattern.lean

@@ -1,37 +1,73 @@
 /-
 Copyright (c) 2025 Michael Sammler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michael Sammler
+Authors: Michael Sammler, Alvin Tang
 -/
 module
 
 public import Iris.ProofMode.Patterns.CasesPattern
+public import Iris.ProofMode.Patterns.SelPattern
 meta import Iris.Std.RocqPorting
 
 @[expose] public section
 
 namespace Iris.ProofMode
 open Lean
 
+declare_syntax_cat selPatFrame
+syntax ("!" noWs)? selPat : selPatFrame
+
 declare_syntax_cat introPat
 
 syntax icasesPat : introPat
+/-- Introduce a modality, analogous to applying `imodintro`. -/
 syntax "!>" : introPat
+/-- Try to solve the goal using `itrivial`. -/
 syntax "//" : introPat
+/-- Apply simplification. -/
+syntax "/=" : introPat
+/-- Apply simplifcation (`/=`) and try solving the goal (`//`). -/
+syntax "//=" : introPat
+/-- Introduce all universal quantifiers. -/
+syntax "*" : introPat
+/-- Introduce all universal quantifiers, pure arrows and wands. -/
+syntax "**" : introPat
+/-- Introduces a pure proof goal, analogous to applying `ipureintro`. -/
+syntax "!%" : introPat
+/--
+  Given selection patterns `spats`, the introduction pattern `{ spats }`
+  *clears* the hypotheses chosen by `spats`. Prefix an element in the selection
+  patterns with `!` to *frame* the hypotheses instead.
+-/
+syntax "{" (colGt ppSpace selPatFrame)* ppSpace "}" : introPat
 
 @[rocq_alias intro_pat]
 inductive IntroPat
   | intro (case : iCasesPat)
   | trivial
   | modintro
+  | simp
+  | simptrivial
+  | all
+  | allwand
+  | pureintro
+  | clear (selPats : List <| Bool × SelPat)
   deriving Repr, Inhabited
 
 partial def IntroPat.parse (term : Syntax) : MacroM (Syntax × IntroPat) := do
   match ← expandMacros term with
   | `(introPat| $case:icasesPat) => return (term, .intro (← iCasesPat.parse case))
   | `(introPat| //) => return (term, .trivial)
   | `(introPat| !>) => return (term, .modintro)
+  | `(introPat| /=) => return (term, .simp)
+  | `(introPat| //=) => return (term, .simptrivial)
+  | `(introPat| *) => return (term, .all)
+  | `(introPat| **) => return (term, .allwand)
+  | `(introPat| !%) => return (term, .pureintro)
+  | `(introPat| { $spats:selPatFrame* }) => return (term, .clear (← spats.toList.mapM parseSelPats))
   | _ => Macro.throwUnsupported
+  where parseSelPats (spat : TSyntax `selPatFrame) : MacroM <| Bool × SelPat := do
+    return ⟨!spat.raw[0].getArgs.isEmpty, ← SelPat.parseOne ⟨spat.raw[1]⟩⟩
 
 #rocq_ignore gallina_ident "Not necessary in Lean"
 #rocq_ignore intro_pat.big_conj "Not necessary in Lean"

Iris/Iris/ProofMode/Patterns/ProofModeTerm.lean

@@ -16,7 +16,7 @@ open Lean
 declare_syntax_cat pmTerm
 
 syntax term : pmTerm
-syntax term colGt " $$ " (colGt specPat)+ : pmTerm
+syntax term colGt " $$ " (colGt ppSpace specPat)+ : pmTerm
 
 @[rocq_alias iTrm]
 structure PMTerm where

Iris/Iris/ProofMode/Patterns/SelPattern.lean

@@ -15,9 +15,13 @@ open Lean Meta Std
 declare_syntax_cat selPat
 
 syntax ident : selPat
+/-- Choose all hypothesis from the pure context. -/
 syntax "%" : selPat
+/-- Choose a specific hypothesis from the pure context. -/
 syntax "%" noWs ident : selPat
+/-- Choose all hypotheses in the intuitionistic context. -/
 syntax "#" : selPat
+/-- Choose all hypotheses in the spatial context. -/
 syntax "∗" : selPat
 
 @[rocq_alias sel_pat]
@@ -69,6 +73,7 @@ def SelPat.resolveOne (hyps : Hyps bi e) : SelPat → ProofModeM (List SelTarget
       return [⟨.ipm ivar, true⟩]
   | .leanIdent name => do
       let ldecl ← getLocalDeclFromUserName name.getId
+      addLocalVarInfo name (← getLCtx) ldecl.toExpr ldecl.type
       return [⟨.pure ldecl.fvarId, true⟩]
   | .intuitionistic =>
       return hyps.intuitionisticIVarIds.map (⟨.ipm ·, false⟩)

Iris/Iris/ProofMode/Porting.lean

@@ -27,7 +27,7 @@ import Iris.Std.RocqPorting
 #rocq_concept proofmode "Tactics" "iAssumptionCoq" ignored "weird tactic"
 #rocq_concept proofmode "Tactics" "iExFalso" ported "iexfalso"
 #rocq_concept proofmode "Tactics" "iPure (basic)" ported "ipure"
-#rocq_concept proofmode "Tactics" "iPure (pure destructuring patterns)" missing "(also for other tactics using ipure)"
+#rocq_concept proofmode "Tactics" "iPure (pure destructuring patterns)" ported "ipure ... as ..."
 #rocq_concept proofmode "Tactics" "iEmpIntro" ported "iempintro"
 #rocq_concept proofmode "Tactics" "iPureIntro" ported "ipureintro"
 #rocq_concept proofmode "Tactics" "iFrame (basic)" ported "iframe"
@@ -59,7 +59,7 @@ import Iris.Std.RocqPorting
 #rocq_concept proofmode "Tactics" "iAccu" missing ""
 #rocq_concept proofmode "Tactics" "rules for trivial" ported "itrivial"
 
-#rocq_concept proofmode "Intro Patterns" missing ""
+#rocq_concept proofmode "Intro Patterns" ported ""
 #rocq_concept proofmode "Intro Patterns" "IIdent (pattern: H)" ported "pattern: H"
 #rocq_concept proofmode "Intro Patterns" "IFresh (pattern: ?)" ported "pattern: _"
 #rocq_concept proofmode "Intro Patterns" "IDrop (pattern: _)" ported "pattern: -"
@@ -70,15 +70,15 @@ import Iris.Std.RocqPorting
 #rocq_concept proofmode "Intro Patterns" "IIntuitionistic (pattern: #H)" ported "pattern: #H"
 #rocq_concept proofmode "Intro Patterns" "ISpatial (pattern: -#H)" ported "pattern: ∗H"
 #rocq_concept proofmode "Intro Patterns" "IModalElim (pattern: >H)" ported "pattern: >H"
-#rocq_concept proofmode "Intro Patterns" "IRewrite (pattern: ->/<-)" missing ""
-#rocq_concept proofmode "Intro Patterns" "IPureIntro (pattern: !%)" missing ""
+#rocq_concept proofmode "Intro Patterns" "IRewrite (pattern: ->/<-)" ported "pattern: →/←"
+#rocq_concept proofmode "Intro Patterns" "IPureIntro (pattern: !%)" ported "pattern: !%"
 #rocq_concept proofmode "Intro Patterns" "IModalIntro (pattern: !>)" ported "pattern: !>"
-#rocq_concept proofmode "Intro Patterns" "ISimpl (pattern: /=)" missing ""
+#rocq_concept proofmode "Intro Patterns" "ISimpl (pattern: /=)" ported "pattern: /="
 #rocq_concept proofmode "Intro Patterns" "IDone (pattern: //)" ported "pattern: //"
-#rocq_concept proofmode "Intro Patterns" "IForall (pattern: *)" missing ""
-#rocq_concept proofmode "Intro Patterns" "IAll (pattern: **)" missing ""
-#rocq_concept proofmode "Intro Patterns" "IClear (pattern: {selpat})" missing ""
-#rocq_concept proofmode "Intro Patterns" "IClearFrame (pattern: {$selpat})" missing ""
+#rocq_concept proofmode "Intro Patterns" "IForall (pattern: *)" ported "pattern: *"
+#rocq_concept proofmode "Intro Patterns" "IAll (pattern: **)" ported "pattern: **"
+#rocq_concept proofmode "Intro Patterns" "IClear (pattern: {selpat})" ported "pattern: { H, ... }"
+#rocq_concept proofmode "Intro Patterns" "IClearFrame (pattern: {$selpat})" ported "pattern: { !H, ... }"
 
 #rocq_concept proofmode "Specialization Patterns" missing ""
 #rocq_concept proofmode "Specialization Patterns" "SIdent (pattern: H)" ported "pattern: H"