45fccc5906
Replaces `@[eliminator]` with two attributes `@[induction_eliminator]` and `@[cases_eliminator]` for defining custom eliminators for the `induction` and `cases` tactics, respectively. Adds `Nat.recAux` and `Nat.casesAuxOn`, which are eliminators that are defeq to `Nat.rec` and `Nat.casesOn`, but these use `0` and `n + 1` rather than `Nat.zero` and `Nat.succ n`. For example, using `induction` to prove that the factorial function is positive now has the following goal states (thanks also to #3616 for the goal state after unfolding). ```lean example : 0 < fact x := by induction x with | zero => decide | succ x ih => /- x : Nat ih : 0 < fact x ⊢ 0 < fact (x + 1) -/ unfold fact /- ... ⊢ 0 < (x + 1) * fact x -/ simpa using ih ``` Thanks to @adamtopaz for initial work on splitting the `@[eliminator]` attribute.
45 lines
1 KiB
Text
45 lines
1 KiB
Text
unsolvedIndCases.lean:3:11-3:18: error: unsolved goals
|
|
case zero
|
|
⊢ 0 + 0 = 0
|
|
unsolvedIndCases.lean:4:11-4:18: error: unsolved goals
|
|
case succ
|
|
y : Nat
|
|
⊢ 0 + (y + 1) = y + 1
|
|
unsolvedIndCases.lean:8:14-8:21: error: unsolved goals
|
|
case zero
|
|
⊢ 0 + 0 = 0
|
|
unsolvedIndCases.lean:9:14-9:21: error: unsolved goals
|
|
case succ
|
|
y : Nat
|
|
ih : 0 + y = y
|
|
⊢ 0 + (y + 1) = y + 1
|
|
unsolvedIndCases.lean:14:11-14:18: error: unsolved goals
|
|
case succ
|
|
y : Nat
|
|
⊢ 0 + (y + 1) = y + 1
|
|
unsolvedIndCases.lean:18:18-18:25: error: unsolved goals
|
|
case ind
|
|
x y : Nat
|
|
h₁ : 0 < y ∧ y ≤ x
|
|
ih : y > 0 → (x - y) % y < y
|
|
h : y > 0
|
|
⊢ x % y < y
|
|
unsolvedIndCases.lean:19:18-19:25: error: unsolved goals
|
|
case base
|
|
x y : Nat
|
|
h₁ : ¬(0 < y ∧ y ≤ x)
|
|
h : y > 0
|
|
⊢ x % y < y
|
|
unsolvedIndCases.lean:23:18-23:25: error: unsolved goals
|
|
case ind
|
|
x y : Nat
|
|
h : y > 0
|
|
h₁ : 0 < y ∧ y ≤ x
|
|
ih : x = x - y → y = y → x % y < y
|
|
⊢ x % y < y
|
|
unsolvedIndCases.lean:24:18-24:25: error: unsolved goals
|
|
case base
|
|
x y : Nat
|
|
h : y > 0
|
|
h₁ : ¬(0 < y ∧ y ≤ x)
|
|
⊢ x % y < y
|