update to Lean 4.22.0-rc3 and fixed linter warnings

Author: arademaker

Fad/Assignment02.lean

@@ -54,7 +54,7 @@ theorem sum_snoc (ms : List Nat) (n : Nat) :
   unfold sum
   induction ms with
   | nil =>
-    simp [snoc, sum]
+    simp [snoc]
   | cons m ms ih =>
     simp[snoc, ih]
     rw [<- Nat.add_assoc, Nat.add_comm m n, Nat.add_assoc]
@@ -72,9 +72,9 @@ theorem sum_append (ms ns : List Nat) :
   unfold sum
   induction ms with
   | nil =>
-    simp [sum, List.foldr]
+    simp [List.foldr]
   | cons m ms ih =>
-    simp[sum]
+    simp
     rw [<- foldr_append, ih, Nat.add_assoc]
 
 -- sum (reverse ns) = sum ns --

Fad/Chapter1-Ex.lean

@@ -189,7 +189,7 @@ termination_by xs.length
 
 
 def last₁ {a : Type} (as : List a) (ok : as ≠ []) : a :=
-  as.reverse.head (by simp [List.length_reverse]; assumption)
+  as.reverse.head (by simp ; assumption)
 
 def init₁ {a : Type} : List a → List a :=
   List.reverse ∘ List.tail ∘ List.reverse
@@ -229,7 +229,7 @@ example {a b : Type} (f : b → a → b) (e : b) :
   List.map (List.foldl f e) ∘ inits = scanl f e := by
   funext xs
   induction xs generalizing e with
-  | nil => simp [map, inits, foldl, scanl]
+  | nil => simp [inits, scanl]
   | cons x xs ih =>
     rw [Function.comp, inits]; simp
     rw [foldl_comp, scanl]
@@ -242,9 +242,9 @@ example {α β : Type} (f : α → β → β) (e : β) :
   induction xs with
   | nil =>
     simp [Function.comp]
-    simp [tails, map, List.scanr, List.foldr]
+    simp [tails, List.foldr]
   | cons y ys ih =>
-    simp [List.map, tails]
+    simp [tails]
     rw [Function.comp] at ih
     rw [ih]
 

Fad/Chapter1.lean

@@ -350,15 +350,15 @@ theorem map_map {α β γ : Type} (f : β → γ) (g : α → β) :
   induction as with
   | nil => rfl
   | cons x xs ih =>
-    simp [List.map, ih]
+    simp [List.map]
 
 
 theorem concatMap_map {α β : Type} (f : α → List β) (g : β → α) :
   concatMap f ∘ List.map g = concatMap (f ∘ g) := by
   funext as
   induction as with
   | nil => rfl
-  | cons x xs ih => simp [concatMap, ih]
+  | cons x xs ih => simp [concatMap]
 
 
 theorem foldr_map {α β : Type} (f : α → β → β) (e : β) (g : β → α) :
@@ -390,7 +390,7 @@ example {a : Type} : ∀ xs : List a, [] ++ xs = xs := by
  intro h1
  induction h1 with
  | nil => rfl
- | cons ha hs => simp [List.append]
+ | cons ha hs => grind
 
 
 example {a b : Type} (xs ys : List a) (f : a → b → b) (e : b)
@@ -517,11 +517,11 @@ def collapse₃ (xss : List (List Int)) : List Int :=
   help (0, id) (labelsum xss) []
 
 
-/-
-#eval collapse₃ [[1],[-3],[2,4]]
-#eval collapse₃ [[-2,1],[-3],[2,4]]
-#eval collapse₃ [[-2,1],[3],[2,4]]
--/
+example : collapse₃ [[1],[-3],[2,4]] = [1] :=
+  rfl
+
+example : collapse₃ [[-2,1],[3],[2,4]] = [-2, 1, 3] :=
+  rfl
 
 
 end Chapter1

Fad/Chapter12-Ex.lean

@@ -64,7 +64,7 @@ example
   simp [Function.comp]
   induction xs with
   | nil =>
-    simp [List.foldr, concatMap, flip]
+    simp [List.foldr, flip]
   | cons a as ih =>
     have h1 := h a
     sorry

Fad/Chapter12.lean

@@ -32,7 +32,7 @@ theorem length_lt_of_cons_split {α : Type} (xs ys zs : List α)
   | nil =>
     simp [splits] at h
   | cons x xs ih =>
-    simp only [splits, List.map, List.flatMap, List.mem_cons, List.mem_map] at h
+    simp only [splits, List.mem_cons, List.mem_map] at h
     cases h with
     | inl h' =>
       simp at h'

Fad/Chapter3-Ex.lean

@@ -192,11 +192,11 @@ example : ∀ (xs : List a), xs = fromRA (toRA xs) := by
     match toRA xs with
     | [] => rfl
     | (Digit.zero :: ds) =>
-      simp [fromRA, fromT, Tree.mk]
+      simp [fromRA]
       rw [concatMap]
       sorry
     | (Digit.one t :: ds) =>
-      simp [fromRA, fromT, Tree.mk]
+      simp [fromRA]
       rw [concatMap]
       sorry
 

Fad/Chapter3.lean

@@ -124,7 +124,7 @@ example (x : a) : snoc x ∘ fromSL = fromSL ∘ snocSL x := by
   unfold snoc snocSL fromSL
   match h: lhs with
   | [] =>
-    simp [h]
+    simp
     simp at ok
     apply ok.elim <;> intro h2; simp [h2]
     have a :: [] := rhs
@@ -270,7 +270,7 @@ example : ∀ (as : SymList a), fromSL (tailSL as) = tail (fromSL as) := by
     | nil => simp [tailSL, fromSL, nil]
     | cons b bs ih =>
       simp [fromSL, tailSL, nil]
-      simp [ok] at *
+      simp at *
       rw [ok]
       rw [List.reverse_nil, List.nil_append, List.tail]
   | cons a as =>
@@ -302,7 +302,7 @@ theorem length_tail_lt_length (sl : SymList a) (h : sl ≠ nil)
     cases ok with
     | intro h1 h2 =>
       simp [k] at h1
-      cases h1 with 
+      cases h1 with
       | inl l => simp_all; contradiction
       | inr m => simp [m]
   · simp [k]
@@ -315,7 +315,7 @@ theorem length_tail_lt_length (sl : SymList a) (h : sl ≠ nil)
       omega
     simp [l]
     apply Nat.sub_lt_self
-    simp [k]
+    simp
     have h : 0 < lsl.length := by
       cases lsl with
       | nil => contradiction
@@ -328,7 +328,7 @@ theorem headSL_none_iff_nilSL {sl : SymList a} : headSL sl = none ↔ sl = nil :
   split at h
   unfold nil
   exact rfl
-  repeat simp [eq_comm, <-Option.isNone_iff_eq_none] at h
+  repeat simp [eq_comm] at h
   rw [h]
   unfold headSL nil
   simp
@@ -455,7 +455,7 @@ theorem tails_append_singleton (xs : List α) (x : α) :
   induction xs with
   | nil      => simp
   | cons y ys ih =>
-      simp [List.tails, ih, List.map_append]
+      simp [List.tails, ih]
 
 theorem map_reverse_tails_snoc (x : α) (xs : List α) :
     List.map reverse (snoc x xs).tails =
@@ -510,11 +510,9 @@ theorem inits_eq {a : Type} : ∀ xs : List a, inits₁ xs = inits₂ xs
     simp
   | x :: xs => by
     have ih := inits_eq xs
-    simp [ inits₁, inits₂,
-            List.reverse_cons,
-            map_reverse_tails_snoc,
-            scanl_cons, fromSL_snoc, ih,
-            Function.comp, flip, map_reverse] at *
+    simp [inits₁, inits₂,
+          List.reverse_cons,
+          Function.comp, flip] at *
     sorry
 
 

Fad/Chapter5-Ex.lean

@@ -179,7 +179,7 @@ example (xs : List Nat) : expression₂ xs = reverse xs := by
   | nil => rfl
   | cons x xs ih =>
     simp [expression₂, reverse] at *
-    simp [List.foldr_cons, List.foldl_cons, flip] at *
+    simp [List.foldr_cons, flip] at *
     sorry
 
 

Fad/Chapter6.lean

@@ -180,23 +180,23 @@ theorem partition3_length {a : Type} [LT a] [DecidableRel (α := a) (· < ·)]
     by_cases l: x > y
     · simp at *
       repeat rw [← partition3]
-      repeat simp [k, l]
+      repeat simp [k]
       rw [← ih]
       by_cases m: x = y
       · simp [m]
         rw [← add_assoc]
         rw[add_assoc]
         nth_rewrite 3 [add_comm]
         rfl
-      simp [k, l, m]
+      simp [m]
       nth_rewrite 2 [add_assoc]
       nth_rewrite 3 [add_comm]
       rw [← add_assoc]
       rw[add_assoc]
       nth_rewrite 3 [add_comm]
       rw [← add_assoc]
     by_cases m: x = y
-    · simp [k, l]
+    · simp [k]
       simp at *
       simp [m]
       repeat rw [← partition3]
@@ -205,7 +205,7 @@ theorem partition3_length {a : Type} [LT a] [DecidableRel (α := a) (· < ·)]
       nth_rewrite 3 [add_comm]
       rw [← add_assoc]
       rw [ih]
-    simp [k, l, m]
+    simp [k, m]
     repeat rw [← partition3]
     nth_rewrite 2 [add_assoc]
     nth_rewrite 3 [add_comm]
@@ -216,7 +216,7 @@ theorem partition3_length {a : Type} [LT a] [DecidableRel (α := a) (· < ·)]
     rw [ih]
 
 /- may not be necessary -/
-def select' (k : Nat) (xs : List a) (q: k ≤ xs.length): a := 
+def select' (k : Nat) (xs : List a) (q: k ≤ xs.length): a :=
   let rec help (k : Nat) (xs : List a) (q: k ≤ xs.length) (fuel: Nat) : a :=
    match fuel with
    | 0 => panic!"Never here"
@@ -229,8 +229,8 @@ def select' (k : Nat) (xs : List a) (q: k ≤ xs.length): a :=
      if      h₁:  k ≤ m     then   help k us (by omega) fuel
      else if h₂:  k ≤ m + n then vs[k - m - 1]
      else                        help (k-m-n) ws (by
-     simp [m, n]; rw [partition3_length]; simp [q]) fuel    
-  termination_by fuel 
+     simp [m, n]; rw [partition3_length]; simp [q]) fuel
+  termination_by fuel
   help k xs q xs.length
-  
+
 end Chapter6

Fad/Chapter7-Ex.lean

@@ -119,7 +119,7 @@ example (x : Nat) : ∀ xs, xs ≠ [] →
  minimum (xs.map (x :: ·)) = (x :: ·) (minimum xs)
  := by
  intro xs h
- simp [Function.comp]
+ simp
  induction xs with
  | nil => contradiction
  | cons a as ih =>