Fix #26

src/Iris/Examples/Proofs.lean

@@ -16,9 +16,9 @@ theorem proof_example_1 [BI PROP] (P Q R : PROP) (Φ : α → PROP) :
   ispecialize HRΦ HR as HΦ
   icases HΦ with ⟨x, _HΦ⟩
   iexists x
-  isplit r
+  isplitr
   · iassumption
-  isplit l [HP]
+  isplitl [HP]
   · iexact HP
   · iexact HQ
 

src/Iris/ProofMode/Tactics/Split.lean

@@ -89,23 +89,20 @@ theorem sep_split [BI PROP] {P P1 P2 Q Q1 Q2 : PROP} [inst : FromSep Q Q1 Q2]
     (h : P ⊣⊢ P1 ∗ P2) (h1 : P1 ⊢ Q1) (h2 : P2 ⊢ Q2) : P ⊢ Q :=
   h.1.trans <| (sep_mono h1 h2).trans inst.1
 
-declare_syntax_cat splitSide
-syntax "l" : splitSide
-syntax "r" : splitSide
+inductive splitSide where
+| splitLeft | splitRight
 
-elab "isplit" side:splitSide "[" names:ident,* "]" : tactic => do
-  -- parse syntax
-  let splitRight ← match side with
-    | `(splitSide| l) => pure false
-    | `(splitSide| r) => pure true
-    | _  => throwUnsupportedSyntax
+def isplitCore (side : splitSide) (names : Array (TSyntax `ident)) : TacticM Unit := do
+  let splitRight := match side with
+    | .splitLeft => false
+    | .splitRight => true
 
   -- extract environment
   let (mvar, { u, prop, bi, hyps, goal, .. }) ← istart (← getMainGoal)
   mvar.withContext do
 
   let mut uniqs : NameSet := {}
-  for name in names.getElems do
+  for name in names do
     uniqs := uniqs.insert (← hyps.findWithInfo name)
 
   let Q1 ← mkFreshExprMVarQ prop
@@ -122,5 +119,11 @@ elab "isplit" side:splitSide "[" names:ident,* "]" : tactic => do
   mvar.assign q(sep_split (Q := $goal) $pf $m1 $m2)
   replaceMainGoal [m1.mvarId!, m2.mvarId!]
 
-macro "isplit" &"l" : tactic => `(tactic| isplit r [])
-macro "isplit" &"r" : tactic => `(tactic| isplit l [])
+elab "isplitl" "[" names:(colGt ident)* "]": tactic => do
+  isplitCore .splitLeft names
+
+elab "isplitr" "[" names:(colGt ident)* "]": tactic => do
+  isplitCore .splitRight names
+
+macro "isplitl" : tactic => `(tactic| isplitr [])
+macro "isplitr" : tactic => `(tactic| isplitl [])

src/Iris/Tests/Tactics.lean

@@ -414,31 +414,31 @@ theorem sep_left [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ P -∗ Q -∗ R -∗
   iintro HP
   iintro HQ
   iintro _HR
-  isplit l [HP]
+  isplitl [HP _HR]
   · iexact HP
   · iexact HQ
 
 theorem sep_right [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ P -∗ Q -∗ R -∗ P ∗ Q := by
   iintro HP
   iintro HQ
   iintro _HR
-  isplit r [HQ]
+  isplitr [HQ]
   · iexact HP
   · iexact HQ
 
 theorem sep_left_all [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ P -∗ □ Q -∗ R -∗ P ∗ Q := by
   iintro HP
   iintro □HQ
   iintro _HR
-  isplit l
+  isplitl
   · iexact HP
   · iexact HQ
 
 theorem sep_right_all [BI PROP] [BIAffine PROP] (Q : PROP) : ⊢ □ P -∗ Q -∗ R -∗ P ∗ Q := by
   iintro □HP
   iintro HQ
   iintro _HR
-  isplit r
+  isplitr
   · iexact HP
   · iexact HQ
 
@@ -459,7 +459,7 @@ theorem right [BI PROP] (Q : PROP) : Q ⊢ P ∨ Q := by
 
 theorem complex [BI PROP] (P Q : PROP) : ⊢ P -∗ Q -∗ P ∗ (R ∨ Q ∨ R) := by
   iintro HP HQ
-  isplit l [HP]
+  isplitl [HP]
   · iassumption
   iright
   ileft

tactics.md

@@ -18,8 +18,8 @@
 | `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. |
+| `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`<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*.                                                                                                                                         |