feat: fix BitVec.abs, prove toInt produces the expected value

src/Init.lean

@@ -35,3 +35,4 @@ import Init.Ext
 import Init.Omega
 import Init.MacroTrace
 import Init.Grind
+import Init.While

src/Init/Data/Array/Basic.lean

@@ -80,6 +80,26 @@ theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
 
 @[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
 
+@[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
+
+end Array
+
+namespace List
+
+@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
+
+@[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
+    a.toArray[i] = a[i]'(by simpa using h) := rfl
+
+@[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
+
+@[simp] theorem getElem!_toArray [Inhabited α] {a : List α} {i : Nat} :
+    a.toArray[i]! = a[i]! := rfl
+
+end List
+
+namespace Array
+
 @[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
 
 @[deprecated Array.toList (since := "2024-09-10")] abbrev Array.data := @Array.toList
@@ -398,20 +418,25 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α 
   decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
+/-- Variant of `mapIdxM` which receives the index as a `Fin as.size`. -/
 @[inline]
-def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Fin as.size → α → m β) : m (Array β) :=
+def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
+    (as : Array α) (f : Fin as.size → α → m β) : m (Array β) :=
   let rec @[specialize] map (i : Nat) (j : Nat) (inv : i + j = as.size) (bs : Array β) : m (Array β) := do
     match i, inv with
     | 0,    _  => pure bs
     | i+1, inv =>
-      have : j < as.size := by
+      have j_lt : j < as.size := by
         rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_comm]
         apply Nat.le_add_right
-      let idx : Fin as.size := ⟨j, this⟩
       have : i + (j + 1) = as.size := by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
-      map i (j+1) this (bs.push (← f idx (as.get idx)))
+      map i (j+1) this (bs.push (← f ⟨j, j_lt⟩ (as.get ⟨j, j_lt⟩)))
   map as.size 0 rfl (mkEmpty as.size)
 
+@[inline]
+def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Nat → α → m β) : m (Array β) :=
+  as.mapFinIdxM fun i a => f i a
+
 @[inline]
 def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) : m (Option β) := do
   for a in as do
@@ -517,8 +542,13 @@ def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : A
 def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β :=
   Id.run <| as.mapM f
 
+/-- Variant of `mapIdx` which receives the index as a `Fin as.size`. -/
+@[inline]
+def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β :=
+  Id.run <| as.mapFinIdxM f
+
 @[inline]
-def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β :=
+def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Nat → α → β) : Array β :=
   Id.run <| as.mapIdxM f
 
 /-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/

src/Init/Data/Array/Bootstrap.lean

@@ -42,7 +42,7 @@ theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
   unfold foldrM.fold
   match i with
   | 0 => simp [List.foldlM, List.take]
-  | i+1 => rw [← List.take_concat_get _ _ h]; simp [← (aux f arr · i)]; rfl
+  | i+1 => rw [← List.take_concat_get _ _ h]; simp [← (aux f arr · i)]
 
 theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init : β) (arr : Array α) :
     arr.foldrM f init = arr.toList.reverse.foldlM (fun x y => f y x) init := by

src/Init/Data/Array/DecidableEq.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.Basic
 import Init.Data.BEq
+import Init.Data.Nat.Lemmas
+import Init.Data.List.Nat.BEq
 import Init.ByCases
 
 namespace Array
@@ -26,13 +28,44 @@ theorem rel_of_isEqvAux
       subst hj'
       exact heqv.left
 
+theorem isEqvAux_of_rel (r : α → α → Bool) (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size)
+    (w : ∀ j, (hj : j < i) → r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi)))) : Array.isEqvAux a b hsz r i hi := by
+  induction i with
+  | zero => simp [Array.isEqvAux]
+  | succ i ih =>
+    simp only [isEqvAux, Bool.and_eq_true]
+    exact ⟨w i (Nat.lt_add_one i), ih _ fun j hj => w j (Nat.lt_add_right 1 hj)⟩
+
 theorem rel_of_isEqv (r : α → α → Bool) (a b : Array α) :
     Array.isEqv a b r → ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) := by
   simp only [isEqv]
   split <;> rename_i h
   · exact fun h' => ⟨h, rel_of_isEqvAux r a b h a.size (Nat.le_refl ..) h'⟩
   · intro; contradiction
 
+theorem isEqv_iff_rel (a b : Array α) (r) :
+    Array.isEqv a b r ↔ ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) :=
+  ⟨rel_of_isEqv r a b, fun ⟨h, w⟩ => by
+    simp only [isEqv, ← h, ↓reduceDIte]
+    exact isEqvAux_of_rel r a b h a.size (by simp [h]) w⟩
+
+theorem isEqv_eq_decide (a b : Array α) (r) :
+    Array.isEqv a b r =
+      if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h'))) else false := by
+  by_cases h : Array.isEqv a b r
+  · simp only [h, Bool.true_eq]
+    simp only [isEqv_iff_rel] at h
+    obtain ⟨h, w⟩ := h
+    simp [h, w]
+  · let h' := h
+    simp only [Bool.not_eq_true] at h
+    simp only [h, Bool.false_eq, dite_eq_right_iff, decide_eq_false_iff_not, Classical.not_forall,
+      Bool.not_eq_true]
+    simpa [isEqv_iff_rel] using h'
+
+@[simp] theorem isEqv_toList [BEq α] (a b : Array α) : (a.toList.isEqv b.toList r) = (a.isEqv b r) := by
+  simp [isEqv_eq_decide, List.isEqv_eq_decide]
+
 theorem eq_of_isEqv [DecidableEq α] (a b : Array α) (h : Array.isEqv a b (fun x y => x = y)) : a = b := by
   have ⟨h, h'⟩ := rel_of_isEqv (fun x y => x = y) a b h
   exact ext _ _ h (fun i lt _ => by simpa using h' i lt)
@@ -56,4 +89,22 @@ instance [DecidableEq α] : DecidableEq (Array α) :=
     | true  => isTrue (eq_of_isEqv a b h)
     | false => isFalse fun h' => by subst h'; rw [isEqv_self] at h; contradiction
 
+theorem beq_eq_decide [BEq α] (a b : Array α) :
+    (a == b) = if h : a.size = b.size then
+      decide (∀ (i : Nat) (h' : i < a.size), a[i] == b[i]'(h ▸ h')) else false := by
+  simp [BEq.beq, isEqv_eq_decide]
+
+@[simp] theorem beq_toList [BEq α] (a b : Array α) : (a.toList == b.toList) = (a == b) := by
+  simp [beq_eq_decide, List.beq_eq_decide]
+
 end Array
+
+namespace List
+
+@[simp] theorem isEqv_toArray [BEq α] (a b : List α) : (a.toArray.isEqv b.toArray r) = (a.isEqv b r) := by
+  simp [isEqv_eq_decide, Array.isEqv_eq_decide]
+
+@[simp] theorem beq_toArray [BEq α] (a b : List α) : (a.toArray == b.toArray) = (a == b) := by
+  simp [beq_eq_decide, Array.beq_eq_decide]
+
+end List

src/Init/Data/Array/GetLit.lean

@@ -41,6 +41,6 @@ where
   getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
     rfl
   go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
-    induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
+    induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.get_drop_eq_drop, *]
 
 end Array