refactor: move if-then-else tactic to Init

src/Init.lean

@@ -7,6 +7,7 @@ prelude
 import Init.Prelude
 import Init.Notation
 import Init.Tactics
+import Init.TacticsExtra
 import Init.Core
 import Init.Control
 import Init.Data.Basic

src/Init/Classical.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Mario Carneiro
 -/
 prelude
 import Init.Core
@@ -123,21 +123,15 @@ theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
 theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
   Decidable.byContradiction (dec := propDecidable _) h
 
+end Classical
+
 /--
 `by_cases (h :)? p` splits the main goal into two cases, assuming `h : p` in the first branch, and `h : ¬ p` in the second branch.
 -/
 syntax "by_cases " (atomic(ident " : "))? term : tactic
 
+macro_rules
+  | `(tactic| by_cases $e) => `(tactic| by_cases h : $e)
 macro_rules
   | `(tactic| by_cases $h : $e) =>
-    `(tactic|
-      cases em $e with
-      | inl $h => _
-      | inr $h => _)
-  | `(tactic| by_cases $e) =>
-    `(tactic|
-      cases em $e with
-      | inl h => _
-      | inr h => _)
-
-end Classical
+    `(tactic| open Classical in refine if $h:ident : $e then ?pos else ?neg)

src/Init/Data/AC.lean

@@ -150,18 +150,18 @@ theorem Context.evalList_mergeIdem (ctx : Context α) (h : ContextInformation.is
       rfl
     | cons z zs =>
       by_cases h₂ : x = y
-      case inl =>
+      case pos =>
         rw [h₂, mergeIdem_head, ih]
         simp [evalList, ←ctx.assoc.1, h.1, EvalInformation.evalOp]
-      case inr =>
+      case neg =>
         rw [mergeIdem_head2]
         by_cases h₃ : y = z
-        case inl =>
+        case pos =>
           simp [mergeIdem_head, h₃, evalList]
           cases h₄ : mergeIdem (z :: zs) with
           | nil => apply absurd h₄; apply mergeIdem_nonEmpty; simp
           | cons u us => simp_all [mergeIdem, mergeIdem.loop, evalList]
-        case inr =>
+        case neg =>
           simp [mergeIdem_head2, h₃, evalList] at *
           rw [ih]
         assumption

src/Init/Tactics.lean

@@ -816,6 +816,41 @@ while `congr 2` produces the intended `⊢ x + y = y + x`.
 -/
 syntax (name := congr) "congr" (ppSpace num)? : tactic
 
+
+/--
+In tactic mode, `if h : t then tac1 else tac2` can be used as alternative syntax for:
+```
+by_cases h : t
+· tac1
+· tac2
+```
+It performs case distinction on `h : t` or `h : ¬t` and `tac1` and `tac2` are the subproofs.
+
+You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but
+if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed
+by the end of the block.
+-/
+syntax (name := tacDepIfThenElse)
+  ppRealGroup(ppRealFill(ppIndent("if " binderIdent " : " term " then") ppSpace matchRhsTacticSeq)
+    ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic
+
+/--
+In tactic mode, `if t then tac1 else tac2` is alternative syntax for:
+```
+by_cases t
+· tac1
+· tac2
+```
+It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous
+hypothesis, and `tac1` and `tac2` are the subproofs. (It doesn't actually use
+nondependent `if`, since this wouldn't add anything to the context and hence would be
+useless for proving theorems. To actually insert an `ite` application use
+`refine if t then ?_ else ?_`.)
+-/
+syntax (name := tacIfThenElse)
+  ppRealGroup(ppRealFill(ppIndent("if " term " then") ppSpace matchRhsTacticSeq)
+    ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic
+
 end Tactic
 
 namespace Attr

src/Init/TacticsExtra.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Mario Carneiro
+-/
+prelude
+import Init.Tactics
+import Init.NotationExtra
+
+/-!
+Extra tactics and implementation for some tactics defined at `Init/Tactic.lean`
+-/
+namespace Lean.Parser.Tactic
+
+private def expandIfThenElse
+    (ifTk thenTk elseTk pos neg : Syntax)
+    (mkIf : Term → Term → MacroM Term) : MacroM (TSyntax `tactic) := do
+  let mkCase tk holeOrTacticSeq mkName : MacroM (Term × Array (TSyntax `tactic)) := do
+    if holeOrTacticSeq.isOfKind `Lean.Parser.Term.syntheticHole then
+      pure (⟨holeOrTacticSeq⟩, #[])
+    else if holeOrTacticSeq.isOfKind `Lean.Parser.Term.hole then
+      pure (← mkName, #[])
+    else
+      let hole ← withFreshMacroScope mkName
+      let holeId := hole.raw[1]
+      let case ← (open TSyntax.Compat in `(tactic|
+          case $holeId:ident =>%$tk
+            -- annotate `then/else` with state after `case`
+            with_annotate_state $tk skip
+            $holeOrTacticSeq))
+      pure (hole, #[case])
+  let (posHole, posCase) ← mkCase thenTk pos `(?pos)
+  let (negHole, negCase) ← mkCase elseTk neg `(?neg)
+  `(tactic| (open Classical in refine%$ifTk $(← mkIf posHole negHole); $[$(posCase ++ negCase)]*))
+
+macro_rules
+  | `(tactic| if%$tk $h : $c then%$ttk $pos else%$etk $neg) =>
+    expandIfThenElse tk ttk etk pos neg fun pos neg => `(if $h : $c then $pos else $neg)
+
+macro_rules
+  | `(tactic| if%$tk $c then%$ttk $pos else%$etk $neg) =>
+    expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg)
+
+end Lean.Parser.Tactic

src/Lean/Parser/Tactic.lean

@@ -92,6 +92,9 @@ example : (List.range 1000).length = 1000 := by native_decide
 @[builtin_tactic_parser] def nativeDecide := leading_parser
   nonReservedSymbol "native_decide"
 
+builtin_initialize
+  register_parser_alias "matchRhsTacticSeq" matchRhs
+
 end Tactic
 end Parser
 end Lean

tests/lean/bintreeGoal.lean

@@ -63,5 +63,5 @@ theorem BinTree.find_insert (b : BinTree β) (k : Nat) (v : β)
   induction t with simp
   | node left key value right ihl ihr =>
     by_cases k < key <;> simp [*]
-    . cases h; apply ihl; done
+    · cases h; apply ihl; assumption
     . sorry

tests/lean/bintreeGoal.lean.expected.out

@@ -1,19 +1,2 @@
 bintreeGoal.lean:53:4-53:18: warning: declaration uses 'sorry'
-bintreeGoal.lean:66:26-66:30: error: unsolved goals
-case node.inl.node
-β : Type u_1
-b : BinTree β
-k : Nat
-v : β
-left : Tree β
-key : Nat
-value : β
-right : Tree β
-ihl : BST left → Tree.find? (Tree.insert left k v) k = some v
-ihr : BST right → Tree.find? (Tree.insert right k v) k = some v
-h✝ : k < key
-a✝³ : BST left
-a✝² : ForallTree (fun k v => k < key) left
-a✝¹ : BST right
-a✝ : ForallTree (fun k v => key < k) right
-⊢ BST left
+bintreeGoal.lean:60:8-60:27: warning: declaration uses 'sorry'

tests/lean/run/by_cases.lean

@@ -0,0 +1,9 @@
+example : True := by
+  if 1 + 1 = 2 then _ else ?_
+  case pos => trivial
+  fail_if_success case neg => contradiction
+  · contradiction
+
+example (p : Prop) : True := by
+  if p then ?foo else trivial
+  case foo => trivial