Backward compatible implementation of lean 3 cases tactic

This tactic is similar to the cases tactic in Lean 4 core, but the syntax for giving names is different:

example (h : p ∨ q) : q ∨ p := by
  cases h with
  | inl hp => exact Or.inr hp
  | inr hq => exact Or.inl hq

example (h : p ∨ q) : q ∨ p := by
  cases' h with hp hq
  · exact Or.inr hp
  · exact Or.inl hq

example (h : p ∨ q) : q ∨ p := by
  rcases h with hp | hq
  · exact Or.inr hp
  · exact Or.inl hq

Prefer cases or rcases when possible, because these tactics promote structured proofs.

def Mathlib.Tactic.ElimApp.evalNames (elimInfo : Lean.Meta.ElimInfo) (alts : Array Lean.Elab.Tactic.ElimApp.Alt) (withArg : Lean.Syntax) (numEqs : Nat := 0) (generalized toClear : Array Lean.FVarId := #[]) (toTag : Array (Lean.Ident × Lean.FVarId) := #[]) : Lean.Elab.TermElabM (Array Lean.MVarId)

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.induction' : Lean.ParserDescr

induction' x applies induction on the variable x of the inductive type t to the main goal, producing one goal for each constructor of t, in which x is replaced by that constructor applied to newly introduced variables. induction' adds an inductive hypothesis for each recursive argument to the constructor. This is a backwards-compatible variant of the induction tactic in Lean 4 core.

Prefer induction when possible, because it promotes structured proofs.

• induction' x with n1 n2 ... names the introduced hypotheses: arguments to constructors and inductive hypotheses. This is the main difference with induction in core Lean.
• induction' e, where e is an expression instead of a variable, generalizes e in the goal, and then performs induction on the resulting variable.
• induction' h : e, where e is an expression instead of a variable, generalizes e in the goal, and then performs induction on the resulting variable, adding to each goal the hypothesis h : e = _ where _ is the constructor instance.
• induction' x using r uses r as the principle of induction. Here r should be a term whose result type is of the form C t1 t2 ..., where C is a bound variable and t1, t2, ... (if present) are bound variables.
• induction' x generalizing z1 z2 ... generalizes over the local variables z1, z2, ... in the inductive hypothesis.

Example:

open Nat

example (n : ℕ) : 0 < factorial n := by
  induction' n with n ih
  · rw [factorial_zero]
    simp
  · rw [factorial_succ]
    apply mul_pos (succ_pos n) ih

-- Though the following equivalent spellings should be preferred
example (n : ℕ) : 0 < factorial n := by
  induction n
  case zero =>
    rw [factorial_zero]
    simp
  case succ n ih =>
    rw [factorial_succ]
    apply mul_pos (succ_pos n) ih

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.cases' : Lean.ParserDescr

cases' x, where the variable x has inductive type t, splits the main goal, producing one goal for each constructor of t, in which x is replaced by that constructor applied to newly introduced variables. This is a backwards-compatible variant of the cases tactic in Lean 4 core.

Prefer cases, rcases, or obtain when possible, because these tactics promote structured proofs.

• cases' x with n1 n2 ... names the arguments to the constructors. This is the main difference with cases in core Lean.
• cases' e, where e is an expression instead of a variable, generalizes e in the goal, and then performs induction on the resulting variable.
• cases' h : e, where e is an expression instead of a variable, generalizes e in the goal, and then splits by cases on the resulting variable, adding to each goal the hypothesis h : e = _ where _ is the constructor instance.
• cases' x using r uses r as the case matching rule. Here r should be a term whose result type is of the form C t1 t2 ..., where C is a bound variable and t1, t2, ... (if present) are bound variables.

Example:

example (h : p ∨ q) : q ∨ p := by
  cases' h with hp hq
  · exact Or.inr hp
  · exact Or.inl hq

-- Though the following equivalent spellings should be preferred
example (h : p ∨ q) : q ∨ p := by
  cases h with
  | inl hp => exact Or.inr hp
  | inr hq => exact Or.inl hq

example (h : p ∨ q) : q ∨ p := by
  rcases h with hp | hq
  · exact Or.inr hp
  · exact Or.inl hq

Equations

• One or more equations did not get rendered due to their size.