fix: ambiguity at induction/cases

See efc3a320fe

doc/tactics.md

@@ -31,7 +31,7 @@ The tactic `assumption` tries to fill a hole by searching the local context for
 ```lean
 theorem ex1 : p ∨ q → q ∨ p := by
   intro h
-  cases h
+  cases h with
   | inl h1 =>
     apply Or.inr
     exact h1
@@ -172,7 +172,7 @@ theorem Nat.mod.inductionOn
 -/
 
 theorem ex (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by
-  induction x, y using Nat.mod.inductionOn generalizing h
+  induction x, y using Nat.mod.inductionOn generalizing h with
   | ind x y h₁ ih =>
     rw [Nat.modEqSubMod h₁.2]
     exact ih h

lean4-mode/lean4-syntax.el

@@ -20,7 +20,7 @@
     "try" "catch" "finally" "where" "rec" "mut" "forall" "fun"
     "exists" "if" "then" "else" "from" "init_quot" "return"
     "mutual" "def" "run_cmd" "declare_syntax_cat" "syntax" "macro_rules" "macro"
-    "initialize" "builtin_initialize")
+    "initialize" "builtin_initialize" "induction" "cases" "generalizing")
   "lean keywords ending with 'word' (not symbol)")
 (defconst lean4-keywords1-regexp
   (eval `(rx word-start (or ,@lean4-keywords1) word-end)))

src/Init/Classical.lean

@@ -114,7 +114,7 @@ theorem skolem {α : Sort u} {b : α → Sort v} {p : ∀ x, b x → Prop} : (
   ⟨axiomOfChoice, fun ⟨f, hw⟩ (x) => ⟨f x, hw x⟩⟩
 
 theorem propComplete (a : Prop) : a = True ∨ a = False := by
-  cases em a
+  cases em a with
   | inl _  => apply Or.inl; apply propext; apply Iff.intro; { intros; apply True.intro }; { intro; assumption }
   | inr hn => apply Or.inr; apply propext; apply Iff.intro; { intro h; exact hn h }; { intro h; apply False.elim h }
 

src/Init/Data/Array/Basic.lean

@@ -570,13 +570,13 @@ theorem ext (a b : Array α)
       (h₁ : a.length = b.length)
       (h₂ : (i : Nat) → (hi₁ : i < a.length) → (hi₂ : i < b.length) → a.get i hi₁ = b.get i hi₂)
       : a = b := by
-    induction a generalizing b
+    induction a generalizing b with
     | nil =>
-      cases b
+      cases b with
       | nil       => rfl
       | cons b bs => rw [List.lengthConsEq] at h₁; injection h₁
     | cons a as ih =>
-      cases b
+      cases b with
       | nil => rw [List.lengthConsEq] at h₁; injection h₁
       | cons b bs =>
         have hz₁ : 0 < (a::as).length by rw [List.lengthConsEq]; apply Nat.zeroLtSucc

src/Init/Data/List/Basic.lean

@@ -336,7 +336,7 @@ def dropLast {α} : List α → List α
 
 def lengthReplicateEq {α} (n : Nat) (a : α) : (replicate n a).length = n :=
   let rec aux (n : Nat) (as : List α) : (replicate.loop a n as).length = n + as.length := by
-    induction n generalizing as
+    induction n generalizing as with
     | zero => rw [Nat.zeroAdd]; rfl
     | succ n ih =>
       show length (replicate.loop a n (a::as)) = Nat.succ n + length as
@@ -345,7 +345,7 @@ def lengthReplicateEq {α} (n : Nat) (a : α) : (replicate n a).length = n :=
   aux n []
 
 def lengthConcatEq {α} (as : List α) (a : α) : (concat as a).length = as.length + 1 := by
-  induction as
+  induction as with
   | nil => rfl
   | cons x xs ih =>
     show length (x :: concat xs a) = length (x :: xs) + 1
@@ -353,10 +353,10 @@ def lengthConcatEq {α} (as : List α) (a : α) : (concat as a).length = as.leng
     rfl
 
 def lengthSetEq {α} (as : List α) (i : Nat) (a : α) : (as.set i a).length = as.length := by
-  induction as generalizing i
+  induction as generalizing i with
   | nil => rfl
   | cons x xs ih =>
-    cases i
+    cases i with
     | zero => rfl
     | succ i =>
       show length (x :: set xs i a) = length (x :: xs)

src/Init/Data/Nat/Basic.lean

@@ -164,12 +164,12 @@ protected theorem subZero (n : Nat) : n - 0 = n :=
   rfl
 
 theorem succSubSuccEqSub (n m : Nat) : succ n - succ m = n - m := by
-  induction m
+  induction m with
   | zero      => exact rfl
   | succ m ih => apply congrArg pred ih
 
 theorem notSuccLeSelf (n : Nat) : ¬succ n ≤ n := by
-  induction n
+  induction n with
   | zero      => intro h; apply notSuccLeZero 0 h
   | succ n ih => intro h; exact ih (leOfSuccLeSucc h)
 
@@ -185,7 +185,7 @@ theorem predLt : ∀ {n : Nat}, n ≠ 0 → pred n < n
   | succ n, h => ltSuccOfLe (Nat.leRefl _)
 
 theorem subLe (n m : Nat) : n - m ≤ n := by
-  induction m
+  induction m with
   | zero      => exact Nat.leRefl (n - 0)
   | succ m ih => apply Nat.leTrans (predLe (n - m)) ih
 

src/Init/Notation.lean

@@ -165,7 +165,7 @@ syntax[«let!»] "let! " letDecl : tactic
 syntax[letrec] withPosition(atomic(group("let " &"rec ")) letRecDecls) : tactic
 
 syntax inductionAlt  := (ident <|> "_") (ident <|> "_")* " => " (hole <|> syntheticHole <|> tacticSeq)
-syntax inductionAlts := withPosition("| " sepBy1(inductionAlt, colGe "| "))
+syntax inductionAlts := "with " withPosition("| " sepBy1(inductionAlt, colGe "| "))
 syntax[induction] "induction " sepBy1(term, ", ") (" using " ident)?  ("generalizing " ident+)? (inductionAlts)? : tactic
 syntax casesTarget := atomic(ident " : ")? term
 syntax[cases] "cases " sepBy1(casesTarget, ", ") (" using " ident)? (inductionAlts)? : tactic

src/Init/WF.lean

@@ -50,7 +50,7 @@ section
 variables {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r)
 
 theorem recursion {C : α → Sort v} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a := by
-  induction (apply hwf a)
+  induction (apply hwf a) with
   | intro x₁ ac₁ ih => exact h x₁ ih
 
 theorem induction {C : α → Prop} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a :=
@@ -60,11 +60,11 @@ variable {C : α → Sort v}
 variable (F : ∀ x, (∀ y, r y x → C y) → C x)
 
 def fixF (x : α) (a : Acc r x) : C x := by
-  induction a
+  induction a with
   | intro x₁ ac₁ ih => exact F x₁ ih
 
 def fixFEq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p)) := by
-  induction acx
+  induction acx with
   | intro x r ih => exact rfl
 
 end
@@ -96,7 +96,7 @@ namespace Subrelation
 variables {α : Sort u} {r q : α → α → Prop}
 
 def accessible {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a := by
-  induction ac
+  induction ac with
   | intro x ax ih =>
     apply Acc.intro
     intro y h
@@ -111,7 +111,7 @@ namespace InvImage
 variables {α : Sort u} {β : Sort v} {r : β → β → Prop}
 
 private def accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x = b → Acc (InvImage r f) x := by
-  induction ac
+  induction ac with
   | intro x acx ih =>
     intro z e
     apply Acc.intro
@@ -131,11 +131,11 @@ namespace TC
 variables {α : Sort u} {r : α → α → Prop}
 
 def accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
-  induction ac
+  induction ac with
   | intro x acx ih =>
     apply Acc.intro x
     intro y rel
-    induction rel generalizing acx ih
+    induction rel generalizing acx ih with
     | base a b rab => exact ih a rab
     | trans a b c rab rbc ih₁ ih₂ => apply Acc.inv (ih₂ acx ih) rab
 
@@ -147,7 +147,7 @@ end TC
 def Nat.ltWf : WellFounded Nat.lt := by
   apply WellFounded.intro
   intro n
-  induction n
+  induction n with
   | zero      =>
     apply Acc.intro 0
     intro _ h
@@ -201,13 +201,13 @@ variables {α : Type u} {β : Type v}
 variables {ra  : α → α → Prop} {rb  : β → β → Prop}
 
 def lexAccessible (aca : (a : α) → Acc ra a) (acb : (b : β) → Acc rb b) (a : α) (b : β) : Acc (Lex ra rb) (a, b) := by
-  induction (aca a) generalizing b
+  induction (aca a) generalizing b with
   | intro xa aca iha =>
-    induction (acb b)
+    induction (acb b) with
     | intro xb acb ihb =>
       apply Acc.intro (xa, xb)
       intro p lt
-      cases lt
+      cases lt with
       | left  a₁ b₁ a₂ b₂ h => apply iha a₁ h
       | right a b₁ b₂ h     => apply ihb b₁ h
 
@@ -217,7 +217,7 @@ def lexWf (ha : WellFounded ra) (hb : WellFounded rb) : WellFounded (Lex ra rb)
 
 -- relational product is a Subrelation of the Lex
 def rprodSubLex (a : α × β) (b : α × β) (h : Rprod ra rb a b) : Lex ra rb a b := by
-  cases h
+  cases h with
   | intro a₁ b₁ a₂ b₂ h₁ h₂ => exact Lex.left b₁ b₂ h₁
 
 -- The relational product of well founded relations is well-founded
@@ -252,13 +252,13 @@ variables {α : Sort u} {β : α → Sort v}
 variables {r  : α → α → Prop} {s : ∀ (a : α), β a → β a → Prop}
 
 def lexAccessible {a} (aca : Acc r a) (acb : (a : α) → WellFounded (s a)) (b : β a) : Acc (Lex r s) ⟨a, b⟩ := by
-  induction aca generalizing b
+  induction aca generalizing b with
   | intro xa aca iha =>
-    induction (WellFounded.apply (acb xa) b)
+    induction (WellFounded.apply (acb xa) b) with
     | intro xb acb ihb =>
       apply Acc.intro
       intro p lt
-      cases lt
+      cases lt with
       | left  => apply iha; assumption
       | right => apply ihb; assumption
 
@@ -292,14 +292,14 @@ variables {α : Sort u} {β : Sort v}
 variables {r  : α → α → Prop} {s : β → β → Prop}
 
 def revLexAccessible {b} (acb : Acc s b) (aca : (a : α) → Acc r a): (a : α) → Acc (RevLex r s) ⟨a, b⟩ := by
-  induction acb
+  induction acb with
   | intro xb acb ihb =>
     intro a
-    induction (aca a)
+    induction (aca a) with
     | intro xa aca iha =>
       apply Acc.intro
       intro p lt
-      cases lt
+      cases lt with
       | left  => apply iha; assumption
       | right => apply ihb; assumption
 

src/Lean/Elab/Tactic/Induction.lean

@@ -240,10 +240,7 @@ private def generalizeVars (stx : Syntax) (targets : Array Expr) : TacticM Nat :
     pure (fvarIds.size, [mvarId'])
 
 private def getAltsOfInductionAlts (inductionAlts : Syntax) : Array Syntax :=
-  if inductionAlts.getNumArgs == 2 then
-    inductionAlts[1].getSepArgs -- TODO remove
-  else
-    inductionAlts[2].getSepArgs
+  inductionAlts[2].getSepArgs
 
 private def getAltsOfOptInductionAlts (optInductionAlts : Syntax) : Array Syntax :=
   if optInductionAlts.isNone then #[] else getAltsOfInductionAlts optInductionAlts[0]

tests/lean/hygienicIntro.lean

@@ -1,4 +1,4 @@
-
+--
 
 set_option hygienicIntro false in
 theorem ex1 {a p q r : Prop} : p → (p → q) → (q → r) → r := by
@@ -32,7 +32,7 @@ exact h
 
 -- Hygienic versions
 example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by
-cases h₂
+cases h₂ with
 | inl h => apply h₁; exact h
 | inr h => exact h
 

tests/lean/inductionErrors.lean

@@ -7,25 +7,25 @@ axiom elimEx (motive : Nat → Nat → Sort u) (x y : Nat)
   : motive y x
 
 theorem ex1 (p q : Nat) : p ≤ q ∨ p > q := by
-  cases p, q using elimEx
+  cases p, q using elimEx with
   | lower d => apply Or.inl -- Error
   | upper d => apply Or.inr -- Error
   | diag    => apply Or.inl; apply Nat.leRefl
 
 theorem ex2 (p q : Nat) : p ≤ q ∨ p > q := by
-  cases p, q using elimEx2 -- Error
+  cases p, q using elimEx2 with -- Error
   | lower d => apply Or.inl
   | upper d => apply Or.inr
   | diag    => apply Or.inl; apply Nat.leRefl
 
 theorem ex3 (p q : Nat) : p ≤ q ∨ p > q := by
-  cases p /- Error -/ using elimEx
+  cases p /- Error -/ using elimEx with
   | lower d => apply Or.inl
   | upper d => apply Or.inr
   | diag    => apply Or.inl; apply Nat.leRefl
 
 theorem ex4 (p q : Nat) : p ≤ q ∨ p > q := by
-  cases p using Nat.add -- Error
+  cases p using Nat.add with -- Error
   | lower d => apply Or.inl
   | upper d => apply Or.inr
   | diag    => apply Or.inl; apply Nat.leRefl
@@ -36,7 +36,7 @@ theorem ex5 (x : Nat) : 0 + x = x := by
   | y+1 => done -- Error
 
 theorem ex5b (x : Nat) : 0 + x = x := by
-  cases x
+  cases x with
   | zero   => done -- Error
   | succ y => done -- Error
 
@@ -45,36 +45,36 @@ inductive Vec : Nat → Type
   | cons : Bool → {n : Nat} → Vec n → Vec (n+1)
 
 theorem ex6 (x : Vec 0) : x = Vec.nil := by
-  cases x using Vec.casesOn
+  cases x using Vec.casesOn with
   | nil  => rfl
   | cons => done -- Error
 
 theorem ex7 (x : Vec 0) : x = Vec.nil := by
-  cases x -- Error: TODO: improve error location
+  cases x with -- Error: TODO: improve error location
   | nil  => rfl
   | cons => done
 
 theorem ex8 (p q : Nat) : p ≤ q ∨ p > q := by
-  cases p, q using elimEx
+  cases p, q using elimEx with
   | lower d => apply Or.inl; admit
   | upper2 /- Error -/ d => apply Or.inr
   | diag    => apply Or.inl; apply Nat.leRefl
 
 theorem ex9 (p q : Nat) : p ≤ q ∨ p > q := by
-  cases p, q using elimEx
+  cases p, q using elimEx with
   | lower d => apply Or.inl; admit
   | _ => apply Or.inr; admit
   | diag    => apply Or.inl; apply Nat.leRefl
 
 theorem ex10 (p q : Nat) : p ≤ q ∨ p > q := by
-  cases p, q using elimEx
+  cases p, q using elimEx with
   | lower d => apply Or.inl; admit
   | upper d => apply Or.inr; admit
   | diag    => apply Or.inl; apply Nat.leRefl
   | _  /- error unused -/ => admit
 
 theorem ex11 (p q : Nat) : p ≤ q ∨ p > q := by
-  cases p, q using elimEx
+  cases p, q using elimEx with
   | lower d => apply Or.inl; admit
   | upper d => apply Or.inr; admit
   | lower d /- error unused -/ => apply Or.inl; admit

tests/lean/run/casesUsing.lean

@@ -12,7 +12,7 @@ axiom elimEx (motive : Nat → Nat → Sort u) (x y : Nat)
   : motive y x
 
 theorem ex1 (p q : Nat) : p ≤ q ∨ p > q := by
-  cases p, q using elimEx
+  cases p, q using elimEx with
   | diag    => apply Or.inl; apply Nat.leRefl
   | lower d => apply Or.inl; show p ≤ p + d.succ; admit
   | upper d => apply Or.inr; show q + d.succ > q; admit
@@ -36,7 +36,7 @@ theorem time2Eq (n : Nat) : 2*n = n + n := by
   rfl
 
 theorem ex3 (n : Nat) : Exists (fun m => n = m + m ∨ n = m + m + 1) := by
-  cases n using parityElim
+  cases n using parityElim with
   | even i =>
     apply Exists.intro i
     apply Or.inl
@@ -49,12 +49,12 @@ theorem ex3 (n : Nat) : Exists (fun m => n = m + m ∨ n = m + m + 1) := by
     rfl
 
 def ex4 {α} (xs : List α) (h : xs = [] → False) : α := by
-  cases he:xs
+  cases he:xs with
   | nil      => apply False.elim; exact h he; done
   | cons x _ => exact x
 
 def ex5 {α} (xs : List α) (h : xs = [] → False) : α := by
-  cases he:xs using List.casesOn
+  cases he:xs using List.casesOn with
   | nil      => apply False.elim; exact h he; done
   | cons x _ => exact x
 
@@ -64,22 +64,22 @@ theorem ex6 {α} (f : List α → Bool) (h₁ : {xs : List α} → f xs = true
   | false => rfl
 
 theorem ex7 {α} (f : List α → Bool) (h₁ : {xs : List α} → f xs = true → xs = []) (xs : List α) (h₂ : xs ≠ []) : f xs = false := by
-  cases he:f xs
+  cases he:f xs with
   | true  => exact False.elim (h₂ (h₁ he))
   | false => rfl
 
 theorem ex8 {α} (f : List α → Bool) (h₁ : {xs : List α} → f xs = true → xs = []) (xs : List α) (h₂ : xs ≠ []) : f xs = false := by
-  cases he:f xs using Bool.casesOn
+  cases he:f xs using Bool.casesOn with
   | true  => exact False.elim (h₂ (h₁ he))
   | false => rfl
 
 theorem ex9 {α} (xs : List α) (h : xs = [] → False) : Nonempty α := by
-  cases xs using List.rec
+  cases xs using List.rec with
   | nil      => apply False.elim; apply h; rfl
   | cons x _ => apply Nonempty.intro; assumption
 
 theorem modLt (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by
-  induction x, y using Nat.mod.inductionOn generalizing h
+  induction x, y using Nat.mod.inductionOn generalizing h with
   | ind x y h₁ ih =>
     rw [Nat.modEqSubMod h₁.2]
     exact ih h
@@ -93,21 +93,21 @@ theorem modLt (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by
       assumption
 
 theorem ex11 {p q : Prop } (h : p ∨ q) : q ∨ p := by
-  induction h using Or.casesOn
+  induction h using Or.casesOn with
   | inr h  => ?myright
   | inl h  => ?myleft
   case myleft  => exact Or.inr h
   case myright => exact Or.inl h
 
 theorem ex12 {p q : Prop } (h : p ∨ q) : q ∨ p := by
-  cases h using Or.casesOn
+  cases h using Or.casesOn with
   | inr h  => ?myright
   | inl h  => ?myleft
   case myleft  => exact Or.inr h
   case myright => exact Or.inl h
 
 theorem ex13 (p q : Nat) : p ≤ q ∨ p > q := by
-  cases p, q using elimEx
+  cases p, q using elimEx with
   | diag    => ?hdiag
   | lower d => ?hlower
   | upper d => ?hupper
@@ -116,7 +116,7 @@ theorem ex13 (p q : Nat) : p ≤ q ∨ p > q := by
   case hupper => apply Or.inr; show q + d.succ > q; admit
 
 theorem ex14 (p q : Nat) : p ≤ q ∨ p > q := by
-  cases p, q using elimEx
+  cases p, q using elimEx with
   | diag    => ?hdiag
   | lower d => _
   | upper d => ?hupper
@@ -125,7 +125,7 @@ theorem ex14 (p q : Nat) : p ≤ q ∨ p > q := by
   case hupper => apply Or.inr; show q + d.succ > q; admit
 
 theorem ex15 (p q : Nat) : p ≤ q ∨ p > q := by
-  cases p, q using elimEx
+  cases p, q using elimEx with
   | diag    => ?hdiag
   | lower d => _
   | upper d => ?hupper

tests/lean/run/concatElim.lean

@@ -51,7 +51,7 @@ theorem dropLastLen {α} (xs : List α) : (n : Nat) → xs.length = n+1 → (dro
     rfl
   | x₁::x₂::xs =>
     intro n h
-    cases n
+    cases n with
     | zero   =>
       rw [lengthCons, lengthCons] at h
       injection h with h

tests/lean/run/induction1.lean

@@ -21,34 +21,34 @@ focus
   assumption
 
 theorem tst1 {p q : Prop } (h : p ∨ q) : q ∨ p := by
-induction h
+induction h with
 | inr h2 => exact Or.inl h2
 | inl h1 => exact Or.inr h1
 
 theorem tst2 {p q : Prop } (h : p ∨ q) : q ∨ p := by
-induction h using elim2
+induction h using elim2 with
 | left _  => apply Or.inr; assumption
 | right _ => apply Or.inl; assumption
 
 theorem tst2b {p q : Prop } (h : p ∨ q) : q ∨ p := by
-induction h using elim2
+induction h using elim2 with
 | left => apply Or.inr; assumption
 | _ => apply Or.inl; assumption
 
 theorem tst3 {p q : Prop } (h : p ∨ q) : q ∨ p := by
-induction h using elim2
+induction h using elim2 with
 | right h => exact Or.inl h
 | left h  => exact Or.inr h
 
 theorem tst4 {p q : Prop } (h : p ∨ q) : q ∨ p := by
-induction h using elim2
+induction h using elim2 with
 | right h => ?myright
 | left h  => ?myleft
 case myleft  => exact Or.inr h
 case myright => exact Or.inl h
 
 theorem tst5 {p q : Prop } (h : p ∨ q) : q ∨ p := by
-induction h using elim2
+induction h using elim2 with
 | right h => _
 | left h  =>
   refine Or.inr ?_
@@ -57,14 +57,14 @@ case right => exact Or.inl h
 
 theorem tst6 {p q : Prop } (h : p ∨ q) : q ∨ p :=
 by {
-  cases h
+  cases h with
   | inr h2 => exact Or.inl h2
   | inl h1 => exact Or.inr h1
 }
 
 theorem tst7 {α : Type} (xs : List α) (h : (a : α) → (as : List α) → xs ≠ a :: as) : xs = [] :=
 by {
-  induction xs
+  induction xs with
   | nil          => exact rfl
   | cons z zs ih => exact absurd rfl (h z zs)
 }
@@ -76,23 +76,23 @@ theorem tst8 {α : Type} (xs : List α) (h : (a : α) → (as : List α) → xs
 }
 
 theorem tst9 {α : Type} (xs : List α) (h : (a : α) → (as : List α) → xs ≠ a :: as) : xs = [] := by
-  cases xs
+  cases xs with
      | nil       => exact rfl
      | cons z zs => exact absurd rfl (h z zs)
 
 theorem tst10 {p q : Prop } (h₁ : p ↔ q) (h₂ : p) : q := by
-  induction h₁
+  induction h₁ with
   | intro h _ => exact h h₂
 
 def Iff2 (m p q : Prop) := p ↔ q
 
 theorem tst11 {p q r : Prop } (h₁ : Iff2 r p q) (h₂ : p) : q := by
-  induction h₁ using Iff.rec
+  induction h₁ using Iff.rec with
   | intro h _ => exact h h₂
 
 theorem tst12 {p q : Prop } (h₁ : p ∨ q) (h₂ : p ↔ q) (h₃ : p) : q := by
   failIfSuccess induction h₁ using Iff.casesOn
-  induction h₂ using Iff.casesOn
+  induction h₂ using Iff.casesOn with
   | intro h _ =>
     exact h h₃
 
@@ -106,12 +106,12 @@ def Tree.isLeaf₁ : Tree → Bool
   | _     => false
 
 theorem tst13 (x : Tree) (h : x = Tree.leaf₁) : x.isLeaf₁ = true := by
-  cases x
+  cases x with
   | leaf₁ => rfl
   | _     => injection h
 
 theorem tst14 (x : Tree) (h : x = Tree.leaf₁) : x.isLeaf₁ = true := by
-  induction x
+  induction x with
   | leaf₁ => rfl
   | _     => injection h
 

tests/lean/run/inj2.lean

@@ -30,9 +30,9 @@ theorem test4 {α} (v : Fin2 0) : α :=
 by cases v
 
 def test5 {α β} {n} (v : Vec2 α β (n+1)) : α := by
-  cases v
+  cases v with
   | cons h1 h2 n tail => exact h1
 
 def test6 {α β} {n} (v : Vec2 α β (n+2)) : α := by
-  cases v
+  cases v with
   | cons h1 h2 n tail => exact h1

tests/lean/run/tacticTests.lean

@@ -9,14 +9,14 @@ theorem ex1 (m : Nat) : Le m 0 → m = 0 := by
 
 theorem ex2 (m n : Nat) : Le m n → Le m.succ n.succ := by
   intro h
-  induction h
+  induction h with
   | base n => apply Le.base
   | succ n m ih =>
     apply Le.succ
     apply ih
 
 theorem ex3 (m : Nat) : Le 0 m := by
-  induction m
+  induction m with
   | zero => apply Le.base
   | succ m ih =>
     apply Le.succ
@@ -28,22 +28,22 @@ theorem ex4 (m : Nat) : ¬ Le m.succ 0 := by
 
 theorem ex5 {m n : Nat} : Le m n.succ → m = n.succ ∨ Le m n := by
   intro h
-  cases h
+  cases h with
   | base => apply Or.inl; rfl
   | succ => apply Or.inr; assumption
 
 theorem ex6 {m n : Nat} : Le m.succ n.succ → Le m n := by
   revert m
-  induction n
+  induction n with
   | zero =>
     intros m h;
-    cases h
+    cases h with
     | base => apply Le.base
     | succ n h => exact absurd h (ex4 _)
   | succ n ih =>
     intros m h
     have aux := ih (m := m)
-    cases ex5 h
+    cases ex5 h with
     | inl h =>
       injection h with h
       subst h
@@ -54,7 +54,7 @@ theorem ex6 {m n : Nat} : Le m.succ n.succ → Le m n := by
 
 theorem ex7 {m n o : Nat} : Le m n → Le n o → Le m o := by
   intro h
-  induction h
+  induction h with
   | base => intros; assumption
   | succ n s ih =>
     intro h₂
@@ -71,7 +71,7 @@ theorem ex8 {m n : Nat} : Le m.succ n → Le m n := by
 
 theorem ex9 {m n : Nat} : Le m n → m = n ∨ Le m.succ n := by
   intro h
-  cases h
+  cases h with
   | base => apply Or.inl; rfl
   | succ n s =>
     apply Or.inr
@@ -86,12 +86,12 @@ theorem ex10 (n : Nat) : ¬ Le n.succ n := by
 -/
 
 theorem ex10 (n : Nat) : n.succ ≠ n := by
-  induction n
+  induction n with
   | zero => intro h; injection h; done
   | succ n ih => intro h; injection h with h; apply ih h
 
 theorem ex11 (n : Nat) : ¬ Le n.succ n := by
-  induction n
+  induction n with
   | zero => intro h; cases h; done
   | succ n ih =>
     intro h
@@ -101,12 +101,12 @@ theorem ex11 (n : Nat) : ¬ Le n.succ n := by
 
 theorem ex12 (m n : Nat) : Le m n → Le n m → m = n := by
   revert m
-  induction n
+  induction n with
   | zero => intro m h1 h2; apply ex1; assumption; done
   | succ n ih =>
     intro m h1 h2
     have ih := ih m
-    cases ex5 h1
+    cases ex5 h1 with
     | inl h => assumption
     | inr h =>
       have ih := ih h

tests/lean/run/where1.lean

@@ -19,7 +19,7 @@ theorem lengthReverse (as : List α) : (reverse as).length = as.length :=
   revLoop as []
 where
   revLoop (as bs : List α) : (reverse.loop as bs).length = as.length + bs.length := by
-    induction as generalizing bs
+    induction as generalizing bs with
     | nil => rw [Nat.zeroAdd]; rfl
     | cons a as ih =>
       show (reverse.loop as (a::bs)).length = (a :: as).length + bs.length

tests/lean/unsolvedIndCases.lean

@@ -1,24 +1,24 @@
 theorem ex1 (x : Nat) : 0 + x = x := by
-  cases x
+  cases x with
   | zero   => skip -- Error: unsolved goals
   | succ y => skip -- Error: unsolved goals
 
 theorem ex2 (x : Nat) : 0 + x = x := by
-  induction x
+  induction x with
   | zero      => skip -- Error: unsolved goals
   | succ y ih => skip -- Error: unsolved goals
 
 theorem ex3 (x : Nat) : 0 + x = x := by
-  cases x
+  cases x with
   | zero   => rfl
   | succ y => skip -- Error: unsolved goals
 
 theorem ex4 (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by
-  induction x, y using Nat.mod.inductionOn generalizing h
+  induction x, y using Nat.mod.inductionOn generalizing h with
   | ind x y h₁ ih => skip -- Error: unsolved goals
   | base x y h₁   => skip -- Error: unsolved goals
 
 theorem ex5 (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by
-  cases x, y using Nat.mod.inductionOn
+  cases x, y using Nat.mod.inductionOn with
   | ind x y h₁ ih => skip -- Error: unsolved goals
   | base x y h₁   => skip -- Error: unsolved goals