46 lines
1.6 KiB
Text
46 lines
1.6 KiB
Text
inductive LE : Nat → Nat → Prop
|
|
| refl : LE n n
|
|
| succ : LE n m → LE n m.succ
|
|
|
|
theorem LE.trans : LE m n → LE n o → LE m o := by
|
|
intro h1 h2
|
|
induction h2 with
|
|
| refl => assumption
|
|
| succ h2 ih => exact succ (ih h1)
|
|
|
|
theorem LE.trans' : LE m n → LE n o → LE m o
|
|
| h1, refl => h1
|
|
| h1, succ h2 => succ (trans' h1 h2) -- the structural recursion in being performed on the implicit `Nat` parameter
|
|
|
|
inductive Even : Nat → Prop
|
|
| zero : Even 0
|
|
| ss : Even n → Even n.succ.succ
|
|
|
|
theorem Even.add : Even n → Even m → Even (n+m) := by
|
|
intro h1 h2
|
|
induction h2 with
|
|
| zero => exact h1
|
|
| ss h2 ih => exact ss ih
|
|
|
|
theorem Even.add' : Even n → Even m → Even (n+m)
|
|
| h1, zero => h1
|
|
| h1, ss h2 => ss (add' h1 h2) -- the structural recursion in being performed on the implicit `Nat` parameter
|
|
|
|
theorem mul_left_comm (n m o : Nat) : n * (m * o) = m * (n * o) := by
|
|
rw [← Nat.mul_assoc, Nat.mul_comm n m, Nat.mul_assoc]
|
|
|
|
inductive Power2 : Nat → Prop
|
|
| base : Power2 1
|
|
| ind : Power2 n → Power2 (2*n) -- Note that index here is not a constructor
|
|
|
|
theorem Power2.mul : Power2 n → Power2 m → Power2 (n*m) := by
|
|
intro h1 h2
|
|
induction h2 with
|
|
| base => simp_all
|
|
| ind h2 ih => exact mul_left_comm .. ▸ ind ih
|
|
|
|
/- The following example fails because the structural recursion cannot be performed on the `Nat`s and
|
|
the `brecOn` construction doesn't work for inductive predicates -/
|
|
-- theorem Power2.mul' : Power2 n → Power2 m → Power2 (n*m)
|
|
-- | h1, base => by simp_all
|
|
-- | h1, ind h2 => mul_left_comm .. ▸ ind (mul' h1 h2)
|