feat: add theorems for tutorial

leodemoura · leodemoura · commit 00193fb9538c · 2021-08-26T12:13:15.000-07:00
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
@@ -112,10 +112,18 @@ theorem reverseAux_eq_append (as bs : List α) : reverseAux as bs = reverseAux a
     rw [ih (a :: bs), ih [a], append_assoc]
     rfl
 
-theorem reverse_cons (a : α) (as : List α) : reverse (a :: as) = reverse as ++ [a] := by
+@[simp] theorem reverse_nil : reverse ([] : List α) = [] :=
+  rfl
+
+@[simp] theorem reverse_cons (a : α) (as : List α) : reverse (a :: as) = reverse as ++ [a] := by
   simp [reverse, reverseAux]
   rw [← reverseAux_eq_append]
 
+@[simp] theorem reverse_append (as bs : List α) : (as ++ bs).reverse = bs.reverse ++ as.reverse := by
+  induction as generalizing bs with
+  | nil => simp
+  | cons a as ih => simp [ih]; rw [append_assoc]
+
 theorem mapTRAux_eq (f : α → β) (as : List α) (bs : List β) : mapTRAux f as bs =  bs.reverse ++ map f as := by
   induction as generalizing bs with
   | nil => simp [mapTRAux, map]
@@ -127,7 +135,6 @@ theorem mapTRAux_eq (f : α → β) (as : List α) (bs : List β) : mapTRAux f a
 @[csimp] theorem map_eq_mapTR : @map = @mapTR := by
   apply funext; intro α; apply funext; intro β; apply funext; intro f; apply funext; intro as
   simp [mapTR, mapTRAux_eq]
-  rfl
 
 @[specialize] def map₂ (f : α → β → γ) : List α → List β → List γ
   | [],    _     => []
@@ -418,6 +425,17 @@ def dropLast {α} : List α → List α
     simp[dropLast, ih]
     rfl
 
+@[simp] theorem length_append (as bs : List α) : (as ++ bs).length = as.length + bs.length := by
+  induction as with
+  | nil => simp
+  | cons a as ih => simp [ih, Nat.succ_add]
+
+
+@[simp] theorem length_reverse (as : List α) : (as.reverse).length = as.length := by
+  induction as with
+  | nil => rfl
+  | cons a as ih => simp [ih]
+
 def maximum? [LT α] [DecidableRel (@LT.lt α _)] : List α → Option α
   | []    => none
   | a::as => some <| as.foldl max a
diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
@@ -143,6 +143,9 @@ protected theorem mul_assoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k)
     have h₆ : n * (m * k + m) = n * (m * succ k)            := Nat.mul_succ m k ▸ rfl
     ((((h₁.trans h₂).trans h₃).trans h₄).trans h₅).trans h₆
 
+protected theorem mul_left_comm (n m k : Nat) : n * (m * k) = m * (n * k) := by
+  rw [← Nat.mul_assoc, Nat.mul_comm n m, Nat.mul_assoc]
+
 /- Inequalities -/
 
 theorem succ_lt_succ {n m : Nat} : n < m → succ n < succ m :=
