More

Author: TwoFX

src/Init/Data/BitVec/Bitblast.lean

@@ -17,6 +17,7 @@ import all Init.Data.BitVec.Basic
 public import Init.Data.BitVec.Decidable
 public import Init.Data.BitVec.Lemmas
 public import Init.Data.BitVec.Folds
+import Init.BinderPredicates
 
 @[expose] public section
 

src/Init/Data/BitVec/Lemmas.lean

@@ -22,6 +22,9 @@ public import Init.Data.Int.Pow
 public import Init.Data.Int.LemmasAux
 public import Init.Data.BitVec.Bootstrap
 public import Init.Data.Order.Factories
+public import Init.Data.List.BasicAux
+import Init.Data.List.Lemmas
+import Init.Data.BEq
 
 public section
 

src/Init/Data/List/Find.lean

@@ -30,15 +30,6 @@ namespace List
 
 open Nat
 
-/-! ### Results about `List.sum` specialized to `Nat` -/
-
-protected theorem sum_pos_iff_exists_pos {l : List Nat} : 0 < l.sum ↔ ∃ x ∈ l, 0 < x := by
-  induction l with
-  | nil => simp
-  | cons x xs ih =>
-    simp [← ih]
-    omega
-
 /-! ### findSome? -/
 
 @[simp] theorem findSome?_cons_of_isSome {l} (h : (f a).isSome) : findSome? f (a :: l) = f a := by

src/Init/Data/List/Nat/Find.lean

@@ -14,10 +14,19 @@ public section
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
+protected theorem Nat.sum_pos_iff_exists_pos {l : List Nat} : 0 < l.sum ↔ ∃ x ∈ l, 0 < x := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp [← ih]
+    omega
+
 namespace List
 
 open Nat
 
+/-! ### Results about `List.sum` specialized to `Nat` -/
+
 theorem find?_eq_some_iff_getElem {xs : List α} {p : α → Bool} {b : α} :
     xs.find? p = some b ↔ p b ∧ ∃ i h, xs[i] = b ∧ ∀ j : Nat, (hj : j < i) → !p xs[j] := by
   rw [find?_eq_some_iff_append]

src/Init/Data/List/OfFn.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.Fin.Fold
-import Init.Data.List.Lemmas
+public import Init.Data.List.Lemmas
 
 public section
 

src/Init/Omega/IntList.lean

@@ -39,7 +39,7 @@ private theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Na
 private theorem map_id (l : List α) : map (id : α → α) l = l := by
   induction l <;> simp_all
 
-[simp] private theorem map_id' (l : List α) : map (fun (a : α) => a) l = l := map_id l
+private theorem map_id' (l : List α) : map (fun (a : α) => a) l = l := map_id l
 
 private theorem getElem?_zipWith {f : α → β → γ} {i : Nat} :
     (zipWith f as bs)[i]? = match as[i]?, bs[i]? with
@@ -52,9 +52,9 @@ private theorem getElem?_zipWith {f : α → β → γ} {i : Nat} :
     | nil => simp
     | cons b bs => cases i <;> simp_all [getElem?_cons_succ]
 
-@[simp] private theorem mem_cons_self {a : α} {l : List α} : a ∈ a :: l := .head ..
+private theorem mem_cons_self {a : α} {l : List α} : a ∈ a :: l := .head ..
 
-@[simp] private theorem mem_cons_of_mem (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l := .tail _
+private theorem mem_cons_of_mem (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l := .tail _
 
 private theorem length_map {as : List α} (f : α → β) : (as.map f).length = as.length := by
   induction as with
@@ -314,7 +314,7 @@ theorem dot_of_left_zero (w : ∀ x, x ∈ xs → x = 0) : dot xs ys = 0 := by
     cases ys with
     | nil => simp
     | cons y ys =>
-      rw [dot_cons₂, w x (by simp), ih]
+      rw [dot_cons₂, w x (by simp [List.mem_cons_self]), ih]
       · simp
       · intro x m
         apply w
@@ -363,7 +363,7 @@ theorem dvd_gcd (xs : IntList) (c : Nat) (w : ∀ {a : Int}, a ∈ xs → (c : I
     simp
     apply Nat.dvd_gcd
     · apply w
-      simp
+      simp [List.mem_cons_self]
     · apply ih
       intro b m
       apply w

src/Std/Tactic/BVDecide/Normalize/Bool.lean

@@ -10,6 +10,7 @@ public import Init.SimpLemmas
 public import Init.Data.Bool
 public import Init.Data.BitVec.Lemmas
 public import Init.Data.BitVec.Decidable
+import Init.Data.BEq
 
 @[expose] public section