feat: Float32

This PR adds support for `Float32` to the Lean runtime.

We need an update stage0, and then remove `#exit` from new
`Float32.lean` file.

src/Init/Data/Array/Basic.lean

@@ -663,7 +663,7 @@ def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool
   Id.run <| as.allM p start stop
 
 def contains [BEq α] (as : Array α) (a : α) : Bool :=
-  as.any (a == ·)
+  as.any (· == a)
 
 def elem [BEq α] (a : α) (as : Array α) : Bool :=
   as.contains a

src/Init/Data/Array/Lemmas.lean

@@ -379,22 +379,6 @@ theorem isEmpty_iff_size_eq_zero {l : Array α} : l.isEmpty ↔ l.size = 0 := by
 @[simp] theorem isEmpty_eq_false {l : Array α} : l.isEmpty = false ↔ l ≠ #[] := by
   cases l <;> simp
 
-/-! ### Decidability of bounded quantifiers -/
-
-instance {xs : Array α} {p : α → Prop} [DecidablePred p] :
-    Decidable (∀ x, x ∈ xs → p x) :=
-  decidable_of_iff (∀ (i : Nat) h, p (xs[i]'h)) (by
-    simp only [mem_iff_getElem, forall_exists_index]
-    exact
-      ⟨by rintro w _ i h rfl; exact w i h, fun w i h => w _ i h rfl⟩)
-
-instance {xs : Array α} {p : α → Prop} [DecidablePred p] :
-    Decidable (∃ x, x ∈ xs ∧ p x) :=
-  decidable_of_iff (∃ (i : Nat), ∃ (h : i < xs.size), p (xs[i]'h)) (by
-    simp [mem_iff_getElem]
-    exact
-      ⟨by rintro ⟨i, h, w⟩; exact ⟨_, ⟨i, h, rfl⟩, w⟩, fun ⟨_, ⟨i, h, rfl⟩, w⟩ => ⟨i, h, w⟩⟩)
-
 /-! ### any / all -/
 
 theorem anyM_eq_anyM_loop [Monad m] (p : α → m Bool) (as : Array α) (start stop) :
@@ -405,15 +389,14 @@ theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start
     (h : min stop as.size ≤ start) : anyM p as start stop = pure false := by
   rw [anyM_eq_anyM_loop, anyM.loop, dif_neg (Nat.not_lt.2 h)]
 
-theorem anyM_loop_cons [Monad m] (p : α → m Bool) (a : α) (as : List α) (stop start : Nat)
-    (h : stop + 1 ≤ (a :: as).length) :
-    anyM.loop p ⟨a :: as⟩ (stop + 1) h (start + 1) =
-      anyM.loop p ⟨as⟩ stop (by simpa using h) start := by
+theorem anyM_loop_cons [Monad m] (p : α → m Bool) (a : α) (as : List α) (stop start : Nat) (h : stop + 1 ≤ (a :: as).length) :
+    anyM.loop p ⟨a :: as⟩ (stop + 1) h (start + 1) = anyM.loop p ⟨as⟩ stop (by simpa using h) start := by
   rw [anyM.loop]
   conv => rhs; rw [anyM.loop]
   split <;> rename_i h'
   · simp only [Nat.add_lt_add_iff_right] at h'
-    rw [dif_pos h', anyM_loop_cons]
+    rw [dif_pos h']
+    rw [anyM_loop_cons]
     simp
   · rw [dif_neg]
     omega
@@ -468,15 +451,10 @@ theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
     · rintro ⟨i, hi, ge, _, h⟩
       exact ⟨i, by omega, by omega, by omega, h⟩
 
-@[simp] theorem any_eq_true {p : α → Bool} {as : Array α} :
-    as.any p = true ↔ ∃ (i : Nat) (_ : i < as.size), p as[i] := by
+theorem any_eq_true {p : α → Bool} {as : Array α} :
+    as.any p ↔ ∃ (i : Nat) (_ : i < as.size), p as[i] := by
   simp [any_iff_exists]
 
-@[simp] theorem any_eq_false {p : α → Bool} {as : Array α} :
-    as.any p = false ↔ ∀ (i : Nat) (_ : i < as.size), ¬p as[i] := by
-  rw [Bool.eq_false_iff, Ne, any_eq_true]
-  simp
-
 theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p := by
   rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]
   simp only [List.mem_iff_getElem, getElem_toList]
@@ -507,15 +485,10 @@ theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
   simp only [any_iff_exists, Bool.not_eq_eq_eq_not, Bool.not_true, not_exists, not_and,
     Bool.not_eq_false, and_imp]
 
-@[simp] theorem all_eq_true {p : α → Bool} {as : Array α} :
-    as.all p = true ↔ ∀ (i : Nat) (_ : i < as.size), p as[i] := by
+theorem all_eq_true {p : α → Bool} {as : Array α} :
+    as.all p ↔ ∀ (i : Nat) (_ : i < as.size), p as[i] := by
   simp [all_iff_forall]
 
-@[simp] theorem all_eq_false {p : α → Bool} {as : Array α} :
-    as.all p = false ↔ ∃ (i : Nat) (_ : i < as.size), ¬p as[i] := by
-  rw [Bool.eq_false_iff, Ne, all_eq_true]
-  simp
-
 theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p := by
   rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]
   simp only [List.mem_iff_getElem, getElem_toList]
@@ -528,188 +501,6 @@ theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all
 theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
   simp only [← all_toList, List.all_eq_true, mem_def]
 
-theorem _root_.List.anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
-    l.toArray.anyM p = l.anyM p := by
-  rw [← anyM_toList]
-
-theorem _root_.List.any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
-  rw [any_toList]
-
-theorem _root_.List.allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
-    l.toArray.allM p = l.allM p := by
-  rw [← allM_toList]
-
-theorem _root_.List.all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
-  rw [all_toList]
-
-/-- Variant of `anyM_toArray` with a side condition on `stop`. -/
-@[simp] theorem _root_.List.anyM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
-    (h : stop = l.toArray.size) :
-    l.toArray.anyM p 0 stop = l.anyM p := by
-  subst h
-  rw [← anyM_toList]
-
-/-- Variant of `any_toArray` with a side condition on `stop`. -/
-@[simp] theorem _root_.List.any_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
-    l.toArray.any p 0 stop = l.any p := by
-  subst h
-  rw [any_toList]
-
-/-- Variant of `allM_toArray` with a side condition on `stop`. -/
-@[simp] theorem _root_.List.allM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
-    (h : stop = l.toArray.size) :
-    l.toArray.allM p 0 stop = l.allM p := by
-  subst h
-  rw [← allM_toList]
-
-/-- Variant of `all_toArray` with a side condition on `stop`. -/
-@[simp] theorem _root_.List.all_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
-    l.toArray.all p 0 stop = l.all p := by
-  subst h
-  rw [all_toList]
-
-/-- Variant of `any_eq_true` in terms of membership rather than an array index. -/
-theorem any_eq_true' {p : α → Bool} {as : Array α} :
-    as.any p = true ↔ (∃ x, x ∈ as ∧ p x) := by
-  cases as
-  simp
-
-/-- Variant of `any_eq_false` in terms of membership rather than an array index. -/
-theorem any_eq_false' {p : α → Bool} {as : Array α} :
-    as.any p = false ↔ ∀ x, x ∈ as → ¬p x := by
-  rw [Bool.eq_false_iff, Ne, any_eq_true']
-  simp
-
-/-- Variant of `all_eq_true` in terms of membership rather than an array index. -/
-theorem all_eq_true' {p : α → Bool} {as : Array α} :
-    as.all p = true ↔ (∀ x, x ∈ as → p x) := by
-  cases as
-  simp
-
-/-- Variant of `all_eq_false` in terms of membership rather than an array index. -/
-theorem all_eq_false' {p : α → Bool} {as : Array α} :
-    as.all p = false ↔ ∃ x, x ∈ as ∧ ¬p x := by
-  rw [Bool.eq_false_iff, Ne, all_eq_true']
-  simp
-
-theorem any_eq {xs : Array α} {p : α → Bool} : xs.any p = decide (∃ i : Nat, ∃ h, p (xs[i]'h)) := by
-  by_cases h : xs.any p
-  · simp_all [any_eq_true]
-  · simp_all [any_eq_false]
-
-/-- Variant of `any_eq` in terms of membership rather than an array index. -/
-theorem any_eq' {xs : Array α} {p : α → Bool} : xs.any p = decide (∃ x, x ∈ xs ∧ p x) := by
-  by_cases h : xs.any p
-  · simp_all [any_eq_true', -any_eq_true]
-  · simp only [Bool.not_eq_true] at h
-    simp only [h]
-    simp only [any_eq_false'] at h
-    simpa using h
-
-theorem all_eq {xs : Array α} {p : α → Bool} : xs.all p = decide (∀ i, (_ : i < xs.size) → p xs[i]) := by
-  by_cases h : xs.all p
-  · simp_all [all_eq_true]
-  · simp only [Bool.not_eq_true] at h
-    simp only [h]
-    simp only [all_eq_false] at h
-    simpa using h
-
-/-- Variant of `all_eq` in terms of membership rather than an array index. -/
-theorem all_eq' {xs : Array α} {p : α → Bool} : xs.all p = decide (∀ x, x ∈ xs → p x) := by
-  by_cases h : xs.all p
-  · simp_all [all_eq_true', -all_eq_true]
-  · simp only [Bool.not_eq_true] at h
-    simp only [h]
-    simp only [all_eq_false'] at h
-    simpa using h
-
-theorem decide_exists_mem {xs : Array α} {p : α → Prop} [DecidablePred p] :
-    decide (∃ x, x ∈ xs ∧ p x) = xs.any p := by
-  simp [any_eq']
-
-theorem decide_forall_mem {xs : Array α} {p : α → Prop} [DecidablePred p] :
-    decide (∀ x, x ∈ xs → p x) = xs.all p := by
-  simp [all_eq']
-
-@[simp] theorem _root_.List.contains_toArray [BEq α] {l : List α} {a : α} :
-    l.toArray.contains a = l.contains a := by
-  simp [Array.contains, List.any_beq]
-
-@[simp] theorem _root_.List.elem_toArray [BEq α] {l : List α} {a : α} :
-    Array.elem a l.toArray = List.elem a l := by
-  simp [Array.elem]
-
-theorem any_beq [BEq α] {xs : Array α} {a : α} : (xs.any fun x => a == x) = xs.contains a := by
-  cases xs
-  simp [List.any_beq]
-
-/-- Variant of `any_beq` with `==` reversed. -/
-theorem any_beq' [BEq α] [PartialEquivBEq α] {xs : Array α} :
-    (xs.any fun x => x == a) = xs.contains a := by
-  simp only [BEq.comm, any_beq]
-
-theorem all_bne [BEq α] {xs : Array α} : (xs.all fun x => a != x) = !xs.contains a := by
-  cases xs
-  simp [List.all_bne]
-
-/-- Variant of `all_bne` with `!=` reversed. -/
-theorem all_bne' [BEq α] [PartialEquivBEq α] {xs : Array α} :
-    (xs.all fun x => x != a) = !xs.contains a := by
-  simp only [bne_comm, all_bne]
-
-theorem mem_of_elem_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Array α} : elem a as = true → a ∈ as := by
-  cases as
-  simp
-
-theorem elem_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a ∈ as) : elem a as = true := by
-  cases as
-  simpa using h
-
-instance [BEq α] [LawfulBEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
-  decidable_of_decidable_of_iff (Iff.intro mem_of_elem_eq_true elem_eq_true_of_mem)
-
-@[simp] theorem elem_eq_contains [BEq α] {a : α} {l : Array α} :
-    elem a l = l.contains a := by
-  simp [elem]
-
-theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {as : Array α} :
-    elem a as = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
-
-theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : Array α} :
-    as.contains a = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
-
-theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : Array α) :
-    elem a as = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
-
-@[simp] theorem contains_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : Array α) :
-    as.contains a = decide (a ∈ as) := by rw [← elem_eq_contains, elem_eq_mem]
-
-/-- Variant of `any_push` with a side condition on `stop`. -/
-@[simp] theorem any_push' [BEq α] {as : Array α} {a : α} {p : α → Bool} (h : stop = as.size + 1) :
-    (as.push a).any p 0 stop = (as.any p || p a) := by
-  cases as
-  rw [List.push_toArray]
-  simp [h]
-
-theorem any_push [BEq α] {as : Array α} {a : α} {p : α → Bool} :
-    (as.push a).any p = (as.any p || p a) :=
-  any_push' (by simp)
-
-/-- Variant of `all_push` with a side condition on `stop`. -/
-@[simp] theorem all_push' [BEq α] {as : Array α} {a : α} {p : α → Bool} (h : stop = as.size + 1) :
-    (as.push a).all p 0 stop = (as.all p && p a) := by
-  cases as
-  rw [List.push_toArray]
-  simp [h]
-
-theorem all_push [BEq α] {as : Array α} {a : α} {p : α → Bool} :
-    (as.push a).all p = (as.all p && p a) :=
-  all_push' (by simp)
-
-@[simp] theorem contains_push [BEq α] {l : Array α} {a : α} {b : α} :
-    (l.push a).contains b = (l.contains b || b == a) := by
-  simp [contains]
-
 theorem singleton_inj : #[a] = #[b] ↔ a = b := by
   simp
 
@@ -2006,6 +1797,46 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   · simp
   · simp_all [List.set_eq_of_length_le]
 
+theorem anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
+    l.toArray.anyM p = l.anyM p := by
+  rw [← anyM_toList]
+
+theorem any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
+  rw [any_toList]
+
+theorem allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
+    l.toArray.allM p = l.allM p := by
+  rw [← allM_toList]
+
+theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
+  rw [all_toList]
+
+/-- Variant of `anyM_toArray` with a side condition on `stop`. -/
+@[simp] theorem anyM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
+    (h : stop = l.toArray.size) :
+    l.toArray.anyM p 0 stop = l.anyM p := by
+  subst h
+  rw [← anyM_toList]
+
+/-- Variant of `any_toArray` with a side condition on `stop`. -/
+@[simp] theorem any_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
+    l.toArray.any p 0 stop = l.any p := by
+  subst h
+  rw [any_toList]
+
+/-- Variant of `allM_toArray` with a side condition on `stop`. -/
+@[simp] theorem allM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
+    (h : stop = l.toArray.size) :
+    l.toArray.allM p 0 stop = l.allM p := by
+  subst h
+  rw [← allM_toList]
+
+/-- Variant of `all_toArray` with a side condition on `stop`. -/
+@[simp] theorem all_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
+    l.toArray.all p 0 stop = l.all p := by
+  subst h
+  rw [all_toList]
+
 @[simp] theorem swap_toArray (l : List α) (i j : Nat) {hi hj}:
     l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray := by
   apply ext'

src/Init/Data/BEq.lean

@@ -40,9 +40,6 @@ theorem BEq.symm [BEq α] [PartialEquivBEq α] {a b : α} : a == b → b == a :=
 theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
   Bool.eq_iff_iff.2 ⟨BEq.symm, BEq.symm⟩
 
-theorem bne_comm [BEq α] [PartialEquivBEq α] {a b : α} : (a != b) = (b != a) := by
-  rw [bne, BEq.comm, bne]
-
 theorem BEq.symm_false [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = false → (b == a) = false :=
   BEq.comm (α := α) ▸ id
 

src/Init/Data/BitVec/Bitblast.lean

@@ -462,7 +462,7 @@ theorem msb_neg {w : Nat} {x : BitVec w} :
       case true =>
         apply hmin
         apply eq_of_getMsbD_eq
-        intro i hi
+        rintro ⟨i, hi⟩
         simp only [getMsbD_intMin, w_pos, decide_true, Bool.true_and]
         cases i
         case zero => exact hmsb
@@ -470,7 +470,7 @@ theorem msb_neg {w : Nat} {x : BitVec w} :
       case false =>
         apply hzero
         apply eq_of_getMsbD_eq
-        intro i hi
+        rintro ⟨i, hi⟩
         simp only [getMsbD_zero]
         cases i
         case zero => exact hmsb
@@ -573,11 +573,11 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow (x : BitVec w) (i
     setWidth w (x.setWidth (i + 1)) =
       setWidth w (x.setWidth i) + (x &&& twoPow w i) := by
   rw [add_eq_or_of_and_eq_zero]
-  · ext k h
-    simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
+  · ext k
+    simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
     by_cases hik : i = k
     · subst hik
-      simp [h]
+      simp
     · simp only [getLsbD_twoPow, hik, decide_false, Bool.and_false, Bool.or_false]
       by_cases hik' : k < (i + 1)
       · have hik'' : k < i := by omega

src/Init/Data/BitVec/Lemmas.lean

@@ -173,21 +173,21 @@ theorem getMsbD_eq_getMsb?_getD (x : BitVec w) (i : Nat) :
 -- We choose `eq_of_getLsbD_eq` as the `@[ext]` theorem for `BitVec`
 -- somewhat arbitrarily over `eq_of_getMsbD_eq`.
 @[ext] theorem eq_of_getLsbD_eq {x y : BitVec w}
-    (pred : ∀ i, i < w → x.getLsbD i = y.getLsbD i) : x = y := by
+    (pred : ∀(i : Fin w), x.getLsbD i.val = y.getLsbD i.val) : x = y := by
   apply eq_of_toNat_eq
   apply Nat.eq_of_testBit_eq
   intro i
   if i_lt : i < w then
-    exact pred i i_lt
+    exact pred ⟨i, i_lt⟩
   else
     have p : i ≥ w := Nat.le_of_not_gt i_lt
     simp [testBit_toNat, getLsbD_ge _ _ p]
 
 theorem eq_of_getMsbD_eq {x y : BitVec w}
-    (pred : ∀ i, i < w → x.getMsbD i = y.getMsbD i) : x = y := by
+    (pred : ∀(i : Fin w), x.getMsbD i.val = y.getMsbD i.val) : x = y := by
   simp only [getMsbD] at pred
   apply eq_of_getLsbD_eq
-  intro i i_lt
+  intro ⟨i, i_lt⟩
   if w_zero : w = 0 then
     simp [w_zero]
   else
@@ -199,7 +199,7 @@ theorem eq_of_getMsbD_eq {x y : BitVec w}
       simp only [Nat.sub_sub]
       apply Nat.sub_lt w_pos
       simp [Nat.succ_add]
-    have q := pred (w - 1 - i) q_lt
+    have q := pred ⟨w - 1 - i, q_lt⟩
     simpa [q_lt, Nat.sub_sub_self, r] using q
 
 -- This cannot be a `@[simp]` lemma, as it would be tried at every term.
@@ -498,9 +498,6 @@ theorem toInt_ofNat {n : Nat} (x : Nat) :
 @[simp] theorem ofInt_ofNat (w n : Nat) :
   BitVec.ofInt w (no_index (OfNat.ofNat n)) = BitVec.ofNat w (OfNat.ofNat n) := rfl
 
-@[simp] theorem ofInt_toInt {x : BitVec w} : BitVec.ofInt w x.toInt = x := by
-  by_cases h : 2 * x.toNat < 2^w <;> ext <;> simp [getLsbD, h, BitVec.toInt]
-
 theorem toInt_neg_iff {w : Nat} {x : BitVec w} :
     BitVec.toInt x < 0 ↔ 2 ^ w ≤ 2 * x.toNat := by
   simp [toInt_eq_toNat_cond]; omega
@@ -572,10 +569,6 @@ theorem zeroExtend_eq_setWidth {v : Nat} {x : BitVec w} :
     (x.setWidth v).toInt = Int.bmod x.toNat (2^v) := by
   simp [toInt_eq_toNat_bmod, toNat_setWidth, Int.emod_bmod]
 
-@[simp] theorem toFin_setWidth {x : BitVec w} :
-    (x.setWidth v).toFin = Fin.ofNat' (2^v) x.toNat := by
-  ext; simp
-
 theorem setWidth'_eq {x : BitVec w} (h : w ≤ v) : x.setWidth' h = x.setWidth v := by
   apply eq_of_toNat_eq
   rw [toNat_setWidth, toNat_setWidth']
@@ -652,20 +645,6 @@ theorem getElem?_setWidth (m : Nat) (x : BitVec n) (i : Nat) :
     getLsbD (setWidth m x) i = (decide (i < m) && getLsbD x i) := by
   simp [getLsbD, toNat_setWidth, Nat.testBit_mod_two_pow]
 
-theorem getMsbD_setWidth {m : Nat} {x : BitVec n} {i : Nat} :
-    getMsbD (setWidth m x) i = (decide (m - n ≤ i) && getMsbD x (i + n - m)) := by
-  unfold setWidth
-  by_cases h : n ≤ m <;> simp only [h]
-  · by_cases h' : m - n ≤ i
-    <;> simp [h', show i - (m - n) = i + n - m by omega]
-  · simp only [show m - n = 0 by omega, getMsbD, getLsbD_setWidth]
-    by_cases h' : i < m
-    · simp [show m - 1 - i < m by omega, show i + n - m < n by omega,
-        show n - 1 - (i + n - m) = m - 1 - i by omega]
-      omega
-    · simp [h']
-      omega
-
 @[simp] theorem getMsbD_setWidth_add {x : BitVec w} (h : k ≤ i) :
     (x.setWidth (w + k)).getMsbD i = x.getMsbD (i - k) := by
   by_cases h : w = 0
@@ -710,15 +689,14 @@ theorem msb_setWidth'' (x : BitVec w) : (x.setWidth (k + 1)).msb = x.getLsbD k :
 /-- zero extending a bitvector to width 1 equals the boolean of the lsb. -/
 theorem setWidth_one_eq_ofBool_getLsb_zero (x : BitVec w) :
     x.setWidth 1 = BitVec.ofBool (x.getLsbD 0) := by
-  ext i h
-  simp at h
-  simp [getLsbD_setWidth, h]
+  ext i
+  simp [getLsbD_setWidth, Fin.fin_one_eq_zero i]
 
 /-- Zero extending `1#v` to `1#w` equals `1#w` when `v > 0`. -/
 theorem setWidth_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
     (BitVec.ofNat v 1).setWidth w = BitVec.ofNat w 1 := by
-  ext i h
-  simp only [getLsbD_setWidth, h, decide_true, getLsbD_ofNat, Bool.true_and,
+  ext ⟨i, hilt⟩
+  simp only [getLsbD_setWidth, hilt, decide_true, getLsbD_ofNat, Bool.true_and,
     Bool.and_iff_right_iff_imp, decide_eq_true_eq]
   intros hi₁
   have hv := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi₁
@@ -745,7 +723,8 @@ protected theorem extractLsb_ofFin {n} (x : Fin (2^n)) (hi lo : Nat) :
 @[simp]
 protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
   extractLsb hi lo (BitVec.ofNat n x) = .ofNat (hi - lo + 1) ((x % 2^n) >>> lo) := by
-  ext i
+  apply eq_of_getLsbD_eq
+  intro ⟨i, _lt⟩
   simp [BitVec.ofNat]
 
 @[simp] theorem extractLsb'_toNat (s m : Nat) (x : BitVec n) :
@@ -832,8 +811,8 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
 
 @[simp] theorem setWidth_or {x y : BitVec w} :
     (x ||| y).setWidth k = x.setWidth k ||| y.setWidth k := by
-  ext i h
-  simp [h]
+  ext
+  simp
 
 theorem or_assoc (x y z : BitVec w) :
     x ||| y ||| z = x ||| (y ||| z) := by
@@ -866,12 +845,12 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· ||| · ) (0#n) where
   simp
 
 @[simp] theorem or_allOnes {x : BitVec w} : x ||| allOnes w = allOnes w := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 @[simp] theorem allOnes_or {x : BitVec w} : allOnes w ||| x = allOnes w := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 /-! ### and -/
 
@@ -905,8 +884,8 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· ||| · ) (0#n) where
 
 @[simp] theorem setWidth_and {x y : BitVec w} :
     (x &&& y).setWidth k = x.setWidth k &&& y.setWidth k := by
-  ext i h
-  simp [h]
+  ext
+  simp
 
 theorem and_assoc (x y z : BitVec w) :
     x &&& y &&& z = x &&& (y &&& z) := by
@@ -936,15 +915,15 @@ instance : Std.IdempotentOp (α := BitVec n) (· &&& · ) where
   simp
 
 @[simp] theorem and_allOnes {x : BitVec w} : x &&& allOnes w = x := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 instance : Std.LawfulCommIdentity (α := BitVec n) (· &&& · ) (allOnes n) where
   right_id _ := BitVec.and_allOnes
 
 @[simp] theorem allOnes_and {x : BitVec w} : allOnes w &&& x = x := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 /-! ### xor -/
 
@@ -981,8 +960,8 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· &&& · ) (allOnes n) wher
 
 @[simp] theorem setWidth_xor {x y : BitVec w} :
     (x ^^^ y).setWidth k = x.setWidth k ^^^ y.setWidth k := by
-  ext i h
-  simp [h]
+  ext
+  simp
 
 theorem xor_assoc (x y z : BitVec w) :
     x ^^^ y ^^^ z = x ^^^ (y ^^^ z) := by
@@ -1075,9 +1054,9 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   rw [Nat.testBit_two_pow_sub_succ x.isLt]
   simp [h]
 
-@[simp] theorem setWidth_not {x : BitVec w} (_ : k ≤ w) :
+@[simp] theorem setWidth_not {x : BitVec w} (h : k ≤ w) :
     (~~~x).setWidth k = ~~~(x.setWidth k) := by
-  ext i h
+  ext
   simp [h]
   omega
 
@@ -1090,17 +1069,17 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   simp
 
 @[simp] theorem xor_allOnes {x : BitVec w} : x ^^^ allOnes w = ~~~ x := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 @[simp] theorem allOnes_xor {x : BitVec w} : allOnes w ^^^ x = ~~~ x := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 @[simp]
 theorem not_not {b : BitVec w} : ~~~(~~~b) = b := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
   constructor
@@ -1175,21 +1154,24 @@ theorem zero_shiftLeft (n : Nat) : 0#w <<< n = 0#w := by
 
 theorem shiftLeft_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y) <<< n = (x <<< n) ^^^ (y <<< n) := by
-  ext i h
-  simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_xor]
-  by_cases h' : i < n <;> simp [h']
+  ext i
+  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, getLsbD_xor]
+  by_cases h : i < n
+    <;> simp [h]
 
 theorem shiftLeft_and_distrib (x y : BitVec w) (n : Nat) :
     (x &&& y) <<< n = (x <<< n) &&& (y <<< n) := by
-  ext i h
-  simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_and]
-  by_cases h' : i < n <;> simp [h']
+  ext i
+  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, getLsbD_and]
+  by_cases h : i < n
+    <;> simp [h]
 
 theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) :
     (x ||| y) <<< n = (x <<< n) ||| (y <<< n) := by
-  ext i h
-  simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_or]
-  by_cases h' : i < n <;> simp [h']
+  ext i
+  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or]
+  by_cases h : i < n
+    <;> simp [h]
 
 @[simp] theorem getMsbD_shiftLeft (x : BitVec w) (i) :
     (x <<< i).getMsbD k = x.getMsbD (k + i) := by
@@ -1528,12 +1510,12 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
     simp [show n = 0 by omega]
 
 @[simp] theorem sshiftRight_zero {x : BitVec w} : x.sshiftRight 0 = x := by
-  ext i h
-  simp [getLsbD_sshiftRight, h]
+  ext i
+  simp [getLsbD_sshiftRight]
 
 @[simp] theorem zero_sshiftRight {n : Nat} : (0#w).sshiftRight n = 0#w := by
-  ext i h
-  simp [getLsbD_sshiftRight, h]
+  ext i
+  simp [getLsbD_sshiftRight]
 
 theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
     x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by
@@ -1634,7 +1616,7 @@ private theorem Int.negSucc_emod (m : Nat) (n : Int) :
     -(m + 1) % n = Int.subNatNat (Int.natAbs n) ((m % Int.natAbs n) + 1) := rfl
 
 /-- The sign extension is the same as zero extending when `msb = false`. -/
-theorem signExtend_eq_setWidth_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
+theorem signExtend_eq_not_setWidth_not_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
     x.signExtend v = x.setWidth v := by
   ext i
   by_cases hv : i < v
@@ -1670,36 +1652,21 @@ theorem signExtend_eq_not_setWidth_not_of_msb_true {x : BitVec w} {v : Nat} (hms
 theorem getLsbD_signExtend (x  : BitVec w) {v i : Nat} :
     (x.signExtend v).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else x.msb) := by
   rcases hmsb : x.msb with rfl | rfl
-  · rw [signExtend_eq_setWidth_of_msb_false hmsb]
+  · rw [signExtend_eq_not_setWidth_not_of_msb_false hmsb]
     by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega
   · rw [signExtend_eq_not_setWidth_not_of_msb_true hmsb]
     by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega
 
-theorem getMsbD_signExtend {x : BitVec w} {v i : Nat} :
-    (x.signExtend v).getMsbD i =
-      (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else x.msb) := by
-  rcases hmsb : x.msb with rfl | rfl
-  · simp only [signExtend_eq_setWidth_of_msb_false hmsb, getMsbD_setWidth]
-    by_cases h : v - w ≤ i <;> simp [h, getMsbD] <;> omega
-  · simp only [signExtend_eq_not_setWidth_not_of_msb_true hmsb, getMsbD_not, getMsbD_setWidth]
-    by_cases h : i < v <;> by_cases h' : v - w ≤ i <;> simp [h, h'] <;> omega
-
 theorem getElem_signExtend {x  : BitVec w} {v i : Nat} (h : i < v) :
     (x.signExtend v)[i] = if i < w then x.getLsbD i else x.msb := by
   rw [←getLsbD_eq_getElem, getLsbD_signExtend]
   simp [h]
 
-theorem msb_signExtend {x : BitVec w} :
-    (x.signExtend v).msb = (decide (0 < v) && if w ≥ v then x.getMsbD (w - v) else x.msb) := by
-  by_cases h : w ≥ v
-  · simp [h, BitVec.msb, getMsbD_signExtend, show v - w = 0 by omega]
-  · simp [h, BitVec.msb, getMsbD_signExtend, show ¬ (v - w = 0) by omega]
-
 /-- Sign extending to a width smaller than the starting width is a truncation. -/
 theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
   x.signExtend v = x.setWidth v := by
-  ext i h
-  simp only [getLsbD_signExtend, h, decide_true, Bool.true_and, getLsbD_setWidth,
+  ext i
+  simp only [getLsbD_signExtend, Fin.is_lt, decide_true, Bool.true_and, getLsbD_setWidth,
     ite_eq_left_iff, Nat.not_lt]
   omega
 
@@ -1793,34 +1760,35 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
   rfl
 
 theorem getLsbD_append {x : BitVec n} {y : BitVec m} :
-    getLsbD (x ++ y) i = if i < m then getLsbD y i else getLsbD x (i - m) := by
+    getLsbD (x ++ y) i = bif i < m then getLsbD y i else getLsbD x (i - m) := by
   simp only [append_def, getLsbD_or, getLsbD_shiftLeftZeroExtend, getLsbD_setWidth']
   by_cases h : i < m
   · simp [h]
   · simp_all [h]
 
 theorem getElem_append {x : BitVec n} {y : BitVec m} (h : i < n + m) :
-    (x ++ y)[i] = if i < m then getLsbD y i else getLsbD x (i - m) := by
+    (x ++ y)[i] = bif i < m then getLsbD y i else getLsbD x (i - m) := by
   simp only [append_def, getElem_or, getElem_shiftLeftZeroExtend, getElem_setWidth']
   by_cases h' : i < m
   · simp [h']
   · simp_all [h']
 
 @[simp] theorem getMsbD_append {x : BitVec n} {y : BitVec m} :
-    getMsbD (x ++ y) i = if n ≤ i then getMsbD y (i - n) else getMsbD x i := by
+    getMsbD (x ++ y) i = bif n ≤ i then getMsbD y (i - n) else getMsbD x i := by
   simp only [append_def]
   by_cases h : n ≤ i
   · simp [h]
   · simp [h]
 
 theorem msb_append {x : BitVec w} {y : BitVec v} :
-    (x ++ y).msb = if w = 0 then y.msb else x.msb := by
+    (x ++ y).msb = bif (w == 0) then (y.msb) else (x.msb) := by
   rw [← append_eq, append]
   simp only [msb_or, msb_shiftLeftZeroExtend, msb_setWidth']
   by_cases h : w = 0
   · subst h
     simp [BitVec.msb, getMsbD]
-  · have q : 0 < w + v := by omega
+  · rw [cond_eq_if]
+    have q : 0 < w + v := by omega
     have t : y.getLsbD (w + v - 1) = false := getLsbD_ge _ _ (by omega)
     simp [h, q, t, BitVec.msb, getMsbD]
 
@@ -1836,7 +1804,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 
 @[simp] theorem zero_append_zero : 0#v ++ 0#w = 0#(v + w) := by
   ext
-  simp only [getLsbD_append, getLsbD_zero, ite_self]
+  simp only [getLsbD_append, getLsbD_zero, Bool.cond_self]
 
 @[simp] theorem cast_append_right (h : w + v = w + v') (x : BitVec w) (y : BitVec v) :
     (x ++ y).cast h = x ++ y.cast (by omega) := by
@@ -1856,19 +1824,21 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 
 theorem setWidth_append {x : BitVec w} {y : BitVec v} :
     (x ++ y).setWidth k = if h : k ≤ v then y.setWidth k else (x.setWidth (k - v) ++ y).cast (by omega) := by
-  ext i h
-  simp only [getLsbD_setWidth, h, getLsbD_append]
-  split <;> rename_i h₁ <;> split <;> rename_i h₂
-  · simp [h]
-  · simp [getLsbD_append, h₁]
-  · omega
-  · simp [getLsbD_append, h₁]
-    omega
+  apply eq_of_getLsbD_eq
+  intro i
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, getLsbD_append, Bool.true_and]
+  split
+  · have t : i < v := by omega
+    simp [t]
+  · by_cases t : i < v
+    · simp [t, getLsbD_append]
+    · have t' : i - v < k - v := by omega
+      simp [t, t', getLsbD_append]
 
 @[simp] theorem setWidth_append_of_eq {x : BitVec v} {y : BitVec w} (h : w' = w) : setWidth (v' + w') (x ++ y) = setWidth v' x ++ setWidth w' y := by
   subst h
-  ext i h
-  simp only [getLsbD_setWidth, h, decide_true, getLsbD_append, cond_eq_if,
+  ext i
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, getLsbD_append, cond_eq_if,
     decide_eq_true_eq, Bool.true_and, setWidth_eq]
   split
   · simp_all
@@ -1918,12 +1888,12 @@ theorem shiftLeft_ushiftRight {x : BitVec w} {n : Nat}:
   case succ n ih =>
     rw [BitVec.shiftLeft_add, Nat.add_comm, BitVec.shiftRight_add, ih,
        Nat.add_comm, BitVec.shiftLeft_add, BitVec.shiftLeft_and_distrib]
-    ext i h
+    ext i
     by_cases hw : w = 0
     · simp [hw]
-    · by_cases hi₂ : i = 0
+    · by_cases hi₂ : i.val = 0
       · simp [hi₂]
-      · simp [Nat.lt_one_iff, hi₂, h, show 1 + (i - 1) = i by omega]
+      · simp [Nat.lt_one_iff, hi₂, show 1 + (i.val - 1) = i by omega]
 
 @[simp]
 theorem msb_shiftLeft {x : BitVec w} {n : Nat} :
@@ -2008,12 +1978,13 @@ theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
 
 theorem setWidth_succ (x : BitVec w) :
     setWidth (i+1) x = cons (getLsbD x i) (setWidth i x) := by
-  ext j h
-  simp only [getLsbD_setWidth, getLsbD_cons, h, decide_true, Bool.true_and]
-  if j_eq : j = i then
+  apply eq_of_getLsbD_eq
+  intro j
+  simp only [getLsbD_setWidth, getLsbD_cons, j.isLt, decide_true, Bool.true_and]
+  if j_eq : j.val = i then
     simp [j_eq]
   else
-    have j_lt : j < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ h) j_eq
+    have j_lt : j.val < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ j.isLt) j_eq
     simp [j_eq, j_lt]
 
 @[simp] theorem cons_msb_setWidth (x : BitVec (w+1)) : (cons x.msb (x.setWidth w)) = x := by
@@ -2127,19 +2098,19 @@ theorem msb_concat {w : Nat} {b : Bool} {x : BitVec w} :
   simp [← Fin.val_inj]
 
 @[simp] theorem not_concat (x : BitVec w) (b : Bool) : ~~~(concat x b) = concat (~~~x) !b := by
-  ext (_ | i) h <;> simp [getLsbD_concat]
+  ext i; cases i using Fin.succRecOn <;> simp [*, Nat.succ_lt_succ]
 
 @[simp] theorem concat_or_concat (x y : BitVec w) (a b : Bool) :
     (concat x a) ||| (concat y b) = concat (x ||| y) (a || b) := by
-  ext (_ | i) h <;> simp [getLsbD_concat]
+  ext i; cases i using Fin.succRecOn <;> simp
 
 @[simp] theorem concat_and_concat (x y : BitVec w) (a b : Bool) :
     (concat x a) &&& (concat y b) = concat (x &&& y) (a && b) := by
-  ext (_ | i) h <;> simp [getLsbD_concat]
+  ext i; cases i using Fin.succRecOn <;> simp
 
 @[simp] theorem concat_xor_concat (x y : BitVec w) (a b : Bool) :
     (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (a ^^ b) := by
-  ext (_ | i) h <;> simp [getLsbD_concat]
+  ext i; cases i using Fin.succRecOn <;> simp
 
 @[simp] theorem zero_concat_false : concat 0#w false = 0#(w + 1) := by
   ext
@@ -2160,8 +2131,8 @@ theorem getLsbD_shiftConcat_eq_decide (x : BitVec w) (b : Bool) (i : Nat) :
 
 theorem shiftRight_sub_one_eq_shiftConcat (n : BitVec w) (hwn : 0 < wn) :
     n >>> (wn - 1) = (n >>> wn).shiftConcat (n.getLsbD (wn - 1)) := by
-  ext i h
-  simp only [getLsbD_ushiftRight, getLsbD_shiftConcat, h, decide_true, Bool.true_and]
+  ext i
+  simp only [getLsbD_ushiftRight, getLsbD_shiftConcat, Fin.is_lt, decide_true, Bool.true_and]
   split
   · simp [*]
   · congr 1; omega
@@ -3172,8 +3143,8 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false
   {x : BitVec w} {i : Nat} (hx : x.getLsbD i = false) :
     setWidth w (x.setWidth (i + 1)) =
       setWidth w (x.setWidth i) := by
-  ext k h
-  simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
+  ext k
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
   by_cases hik : i = k
   · subst hik
     simp [hx]
@@ -3188,17 +3159,20 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true
     {x : BitVec w} {i : Nat} (hx : x.getLsbD i = true) :
     setWidth w (x.setWidth (i + 1)) =
       setWidth w (x.setWidth i) ||| (twoPow w i) := by
-  ext k h
-  simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
+  ext k
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
   by_cases hik : i = k
   · subst hik
-    simp [hx, h]
+    simp [hx]
   · by_cases hik' : k < i + 1 <;> simp [hik, hik'] <;> omega
 
 /-- Bitwise and of `(x : BitVec w)` with `1#w` equals zero extending `x.lsb` to `w`. -/
 theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
     (x &&& 1#w) = setWidth w (ofBool (x.getLsbD 0)) := by
-  ext (_ | i) h <;> simp [Bool.and_comm]
+  ext i
+  simp only [getLsbD_and, getLsbD_one, getLsbD_setWidth, Fin.is_lt, decide_true, getLsbD_ofBool,
+    Bool.true_and]
+  by_cases h : ((i : Nat) = 0) <;> simp [h] <;> omega
 
 @[simp]
 theorem replicate_zero_eq {x : BitVec w} : x.replicate 0 = 0#0 := by
@@ -3222,7 +3196,7 @@ theorem getLsbD_replicate {n w : Nat} (x : BitVec w) :
     · simp only [hi, decide_true, Bool.true_and]
       by_cases hi' : i < w * n
       · simp [hi', ih]
-      · simp [hi', decide_false]
+      · simp only [hi', decide_false, cond_false]
         rw [Nat.sub_mul_eq_mod_of_lt_of_le] <;> omega
     · rw [Nat.mul_succ] at hi ⊢
       simp only [show ¬i < w * n by omega, decide_false, cond_false, hi, Bool.false_and]
@@ -3528,7 +3502,7 @@ theorem forall_zero_iff {P : BitVec 0 → Prop} :
   · intro h
     apply h
   · intro h v
-    obtain (rfl : v = 0#0) := (by ext i ⟨⟩)
+    obtain (rfl : v = 0#0) := (by ext ⟨i, h⟩; simp at h)
     apply h
 
 theorem forall_cons_iff {P : BitVec (n + 1) → Prop} :
@@ -3544,7 +3518,7 @@ theorem forall_cons_iff {P : BitVec (n + 1) → Prop} :
 instance instDecidableForallBitVecZero (P : BitVec 0 → Prop) :
     ∀ [Decidable (P 0#0)], Decidable (∀ v, P v)
   | .isTrue h => .isTrue fun v => by
-    obtain (rfl : v = 0#0) := (by ext i ⟨⟩)
+    obtain (rfl : v = 0#0) := (by ext ⟨i, h⟩; cases h)
     exact h
   | .isFalse h => .isFalse (fun w => h (w _))
 
@@ -3589,9 +3563,6 @@ instance instDecidableExistsBitVec :
 
 set_option linter.missingDocs false
 
-@[deprecated signExtend_eq_setWidth_of_msb_false (since := "2024-12-08")]
-abbrev signExtend_eq_not_setWidth_not_of_msb_false := @signExtend_eq_setWidth_of_msb_false
-
 @[deprecated truncate_eq_setWidth (since := "2024-09-18")]
 abbrev truncate_eq_zeroExtend := @truncate_eq_setWidth
 
@@ -3694,8 +3665,8 @@ abbrev truncate_xor := @setWidth_xor
 @[deprecated setWidth_not (since := "2024-09-18")]
 abbrev truncate_not := @setWidth_not
 
-@[deprecated signExtend_eq_setWidth_of_msb_false  (since := "2024-09-18")]
-abbrev signExtend_eq_not_zeroExtend_not_of_msb_false  := @signExtend_eq_setWidth_of_msb_false
+@[deprecated signExtend_eq_not_setWidth_not_of_msb_false  (since := "2024-09-18")]
+abbrev signExtend_eq_not_zeroExtend_not_of_msb_false  := @signExtend_eq_not_setWidth_not_of_msb_false
 
 @[deprecated signExtend_eq_not_setWidth_not_of_msb_true (since := "2024-09-18")]
 abbrev signExtend_eq_not_zeroExtend_not_of_msb_true := @signExtend_eq_not_setWidth_not_of_msb_true

src/Init/Data/List/Basic.lean

@@ -666,14 +666,10 @@ def isEmpty : List α → Bool
 /-! ### elem -/
 
 /--
-`O(|l|)`.
-`l.contains a` or `elem a l` is true if there is an element in `l` equal (according to `==`) to `a`.
+`O(|l|)`. `elem a l` or `l.contains a` is true if there is an element in `l` equal to `a`.
 
-* `[1, 4, 2, 3, 3, 7].contains 3 = true`
-* `[1, 4, 2, 3, 3, 7].contains 5 = false`
-
-The preferred simp normal form is `l.contains a`, and when `LawfulBEq α` is available,
-`l.contains a = true ↔ a ∈ l` and `l.contains a = false ↔ a ∉ l`.
+* `elem 3 [1, 4, 2, 3, 3, 7] = true`
+* `elem 5 [1, 4, 2, 3, 3, 7] = false`
 -/
 def elem [BEq α] (a : α) : List α → Bool
   | []    => false

src/Init/Data/List/Lemmas.lean

@@ -451,10 +451,6 @@ theorem forall_getElem {l : List α} {p : α → Prop} :
         simp only [getElem_cons_succ]
         exact getElem_mem (lt_of_succ_lt_succ h)
 
-@[simp] theorem elem_eq_contains [BEq α] {a : α} {l : List α} :
-    elem a l = l.contains a := by
-  simp [contains]
-
 @[simp] theorem decide_mem_cons [BEq α] [LawfulBEq α] {l : List α} :
     decide (y ∈ a :: l) = (y == a || decide (y ∈ l)) := by
   cases h : y == a <;> simp_all
@@ -462,20 +458,9 @@ theorem forall_getElem {l : List α} {p : α → Prop} :
 theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {as : List α} :
     elem a as = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
 
-theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : List α} :
-    as.contains a = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
-
-theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
+@[simp] theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
     elem a as = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
 
-@[simp] theorem contains_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
-    as.contains a = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
-
-@[simp] theorem contains_cons [BEq α] {a : α} {b : α} {l : List α} :
-    (a :: l).contains b = (b == a || l.contains b) := by
-  simp only [contains, elem_cons]
-  split <;> simp_all
-
 /-! ### `isEmpty` -/
 
 theorem isEmpty_iff {l : List α} : l.isEmpty ↔ l = [] := by
@@ -520,21 +505,17 @@ theorem decide_forall_mem {l : List α} {p : α → Prop} [DecidablePred p] :
 @[simp] theorem all_eq_false {l : List α} : l.all p = false ↔ ∃ x, x ∈ l ∧ ¬p x := by
   simp [all_eq]
 
-theorem any_beq [BEq α] {l : List α} {a : α} : (l.any fun x => a == x) = l.contains a := by
-  induction l <;> simp_all [contains_cons]
+theorem any_beq [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => a == x) ↔ a ∈ l := by
+  simp
 
-/-- Variant of `any_beq` with `==` reversed. -/
-theorem any_beq' [BEq α] [PartialEquivBEq α] {l : List α} :
-    (l.any fun x => x == a) = l.contains a := by
-  simp only [BEq.comm, any_beq]
+theorem any_beq' [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => x == a) ↔ a ∈ l := by
+  simp
 
-theorem all_bne [BEq α] {l : List α} : (l.all fun x => a != x) = !l.contains a := by
-  induction l <;> simp_all [bne]
+theorem all_bne [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => a != x) ↔ a ∉ l := by
+  induction l <;> simp_all
 
-/-- Variant of `all_bne` with `!=` reversed. -/
-theorem all_bne' [BEq α] [PartialEquivBEq α] {l : List α} :
-    (l.all fun x => x != a) = !l.contains a := by
-  simp only [bne_comm, all_bne]
+theorem all_bne' [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => x != a) ↔ a ∉ l := by
+  induction l <;> simp_all [eq_comm (a := a)]
 
 /-! ### set -/
 
@@ -2847,6 +2828,11 @@ theorem leftpad_suffix (n : Nat) (a : α) (l : List α) : l <:+ (leftpad n a l)
 
 theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by simp
 
+@[simp] theorem contains_cons [BEq α] :
+    (a :: as : List α).contains x = (x == a || as.contains x) := by
+  simp only [contains, elem]
+  split <;> simp_all
+
 theorem contains_eq_any_beq [BEq α] (l : List α) (a : α) : l.contains a = l.any (a == ·) := by
   induction l with simp | cons b l => cases b == a <;> simp [*]
 

src/Init/Data/Nat/Lemmas.lean

@@ -1046,25 +1046,6 @@ instance decidableExistsLE [DecidablePred p] : DecidablePred fun n => ∃ m : Na
   fun n => decidable_of_iff (∃ m, m < n + 1 ∧ p m)
     (exists_congr fun _ => and_congr_left' Nat.lt_succ_iff)
 
-/-- Dependent version of `decidableExistsLT`. -/
-instance decidableExistsLT' {p : (m : Nat) → m < k → Prop} [I : ∀ m h, Decidable (p m h)] :
-    Decidable (∃ m : Nat, ∃ h : m < k, p m h) :=
-  match k, p, I with
-  | 0, _, _ => isFalse (by simp)
-  | (k + 1), p, I => @decidable_of_iff _ ((∃ m, ∃ h : m < k, p m (by omega)) ∨ p k (by omega))
-      ⟨by rintro (⟨m, h, w⟩ | w); exact ⟨m, by omega, w⟩; exact ⟨k, by omega, w⟩,
-        fun ⟨m, h, w⟩ => if h' : m < k then .inl ⟨m, h', w⟩ else
-          by obtain rfl := (by omega : m = k); exact .inr w⟩
-      (@instDecidableOr _ _
-        (decidableExistsLT' (p := fun m h => p m (by omega)) (I := fun m h => I m (by omega)))
-        inferInstance)
-
-/-- Dependent version of `decidableExistsLE`. -/
-instance decidableExistsLE' {p : (m : Nat) → m ≤ k → Prop} [I : ∀ m h, Decidable (p m h)] :
-    Decidable (∃ m : Nat, ∃ h : m ≤ k, p m h) :=
-  decidable_of_iff (∃ m, ∃ h : m < k + 1, p m (by omega)) (exists_congr fun _ =>
-    ⟨fun ⟨h, w⟩ => ⟨le_of_lt_succ h, w⟩, fun ⟨h, w⟩ => ⟨lt_add_one_of_le h, w⟩⟩)
-
 /-! ### 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

src/Lean/Compiler/IR/Basic.lean

@@ -81,9 +81,9 @@ then one of the following must hold in each (execution) branch.
 inductive IRType where
   | float | uint8 | uint16 | uint32 | uint64 | usize
   | irrelevant | object | tobject
-  | float32
   | struct (leanTypeName : Option Name) (types : Array IRType) : IRType
   | union (leanTypeName : Name) (types : Array IRType) : IRType
+  | float32
   deriving Inhabited, Repr
 
 namespace IRType

src/Lean/Expr.lean

@@ -1235,9 +1235,6 @@ def getRevArg!' : Expr → Nat → Expr
 @[inline] def getArgD (e : Expr) (i : Nat) (v₀ : Expr) (n := e.getAppNumArgs) : Expr :=
   getRevArgD e (n - i - 1) v₀
 
-/-- Return `true` if `e` contains any loose bound variables.
-
-This is a constant time operation. -/
 def hasLooseBVars (e : Expr) : Bool :=
   e.looseBVarRange > 0
 
@@ -1250,11 +1247,6 @@ def isArrow (e : Expr) : Bool :=
   | forallE _ _ b _ => !b.hasLooseBVars
   | _ => false
 
-/--
-Return `true` if `e` contains the specified loose bound variable with index `bvarIdx`.
-
-This operation traverses the expression tree.
--/
 @[extern "lean_expr_has_loose_bvar"]
 opaque hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool
 

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean

@@ -77,8 +77,12 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
     simp only [go, denote_blastAppend, RefVec.get_cast, Ref.cast_eq, eval_append,
       BitVec.getLsbD_append]
     split
-    · next hsplit => rw [rih]
-    · next hsplit => rw [go_denote_mem_prefix, lih]
+    · next hsplit =>
+      simp only [hsplit, decide_true, cond_true]
+      rw [rih]
+    · next hsplit =>
+      simp only [hsplit, decide_false, cond_false]
+      rw [go_denote_mem_prefix, lih]
   | replicate n expr ih => simp [go, ih, hidx]
   | signExtend v inner ih =>
     rename_i originalWidth
@@ -91,7 +95,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
       rw [blastSignExtend_empty_eq_zeroExtend] at hgo
       · rw [← hgo]
         simp only [eval_signExtend]
-        rw [BitVec.signExtend_eq_setWidth_of_msb_false]
+        rw [BitVec.signExtend_eq_not_setWidth_not_of_msb_false]
         · simp only [denote_blastZeroExtend, ih, dite_eq_ite, Bool.if_false_right,
             BitVec.getLsbD_setWidth, hidx, decide_true, Bool.true_and, Bool.and_iff_right_iff_imp,
             decide_eq_true_eq]

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Eq.lean

@@ -30,9 +30,9 @@ theorem mkEq_denote_eq (aig : AIG α) (pair : AIG.BinaryRefVec aig w) (assign :
   simp only [RefVec.denote_fold_and, RefVec.denote_zip, denote_mkBEqCached, beq_iff_eq]
   constructor
   · intro h
-    ext i h'
+    ext
     rw [← hleft, ← hright]
-    · simp [h, h']
+    · simp [h]
     · omega
     · omega
   · intro h idx hidx

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

@@ -168,13 +168,13 @@ attribute [bv_normalize] BitVec.and_self
 
 @[bv_normalize]
 theorem BitVec.and_contra (a : BitVec w) : a &&& ~~~a = 0#w := by
-  ext i h
-  simp [h]
+  ext
+  simp
 
 @[bv_normalize]
 theorem BitVec.and_contra' (a : BitVec w) : ~~~a &&& a = 0#w := by
-  ext i h
-  simp [h]
+  ext
+  simp
 
 @[bv_normalize]
 theorem BitVec.add_not (a : BitVec w) : a + ~~~a = (-1#w) := by

src/library/compiler/ir.cpp

@@ -352,16 +352,6 @@ class to_ir_fn {
         return ir::mk_sset(to_var_id(args[0]), n, offset, to_var_id(args[1]), ir::type::Float, b);
     }
 
-    ir::fn_body visit_f32set(local_decl const & decl, ir::fn_body const & b) {
-        expr val = *decl.get_value();
-        buffer<expr> args;
-        expr const & fn = get_app_args(val, args);
-        lean_assert(args.size() == 2);
-        unsigned n, offset;
-        lean_verify(is_llnf_f32set(fn, n, offset));
-        return ir::mk_sset(to_var_id(args[0]), n, offset, to_var_id(args[1]), ir::type::Float32, b);
-    }
-
     ir::fn_body visit_uset(local_decl const & decl, ir::fn_body const & b) {
         expr val = *decl.get_value();
         buffer<expr> args;
@@ -429,8 +419,6 @@ class to_ir_fn {
                 return visit_sset(decl, b);
             else if (is_llnf_fset(fn))
                 return visit_fset(decl, b);
-            else if (is_llnf_f32set(fn))
-                return visit_f32set(decl, b);
             else if (is_llnf_uset(fn))
                 return visit_uset(decl, b);
             else if (is_llnf_proj(fn))
@@ -463,7 +451,7 @@ class to_ir_fn {
                 expr new_fvar   = m_lctx.mk_local_decl(ngen(), n, type, val);
                 fvars.push_back(new_fvar);
                 expr const & op = get_app_fn(val);
-                if (is_llnf_sset(op) || is_llnf_fset(op) || is_llnf_f32set(op) || is_llnf_uset(op)) {
+                if (is_llnf_sset(op) || is_llnf_fset(op) || is_llnf_uset(op)) {
                     /* In the Lean IR, sset and uset are instructions that perform destructive updates. */
                     subst.push_back(app_arg(app_fn(val)));
                 } else {

src/library/compiler/ir.h

@@ -14,13 +14,13 @@ namespace ir {
 inductive IRType
 | float | uint8 | uint16 | uint32 | uint64 | usize
 | irrelevant | object | tobject
-| float32
 | struct (leanTypeName : Option Name) (types : Array IRType) : IRType
 | union (leanTypeName : Name) (types : Array IRType) : IRType
+| float32
 
 Remark: we don't create struct/union types from C++.
 */
-enum class type { Float, UInt8, UInt16, UInt32, UInt64, USize, Irrelevant, Object, TObject, Float32, Struct, Union };
+enum class type { Float, UInt8, UInt16, UInt32, UInt64, USize, Irrelevant, Object, TObject, Float32 };
 
 typedef nat        var_id;
 typedef nat        jp_id;

src/library/compiler/ir_interpreter.cpp

@@ -188,11 +188,6 @@ option_ref<decl> find_ir_decl(environment const & env, name const & n) {
 
 extern "C" double lean_float_of_nat(lean_obj_arg a);
 
-// TODO: define in Lean like `lean_float_of_nat`
-float lean_float32_of_nat(lean_obj_arg a) {
-    return lean_float_of_nat(a);
-}
-
 static string_ref * g_mangle_prefix = nullptr;
 static string_ref * g_boxed_suffix = nullptr;
 static string_ref * g_boxed_mangled_suffix = nullptr;
@@ -232,7 +227,6 @@ union value {
     uint64   m_num; // big enough for any unboxed integral type
     static_assert(sizeof(size_t) <= sizeof(uint64), "uint64 should be the largest unboxed type"); // NOLINT
     double   m_float;
-    float    m_float32;
     object * m_obj;
 
     value() {}
@@ -246,50 +240,36 @@ union value {
         v.m_float = f;
         return v;
     }
-
-    static value from_float32(float f) {
-        value v;
-        v.m_float32 = f;
-        return v;
-    }
 };
 
 object * box_t(value v, type t) {
     switch (t) {
-    case type::Float:   return box_float(v.m_float);
-    case type::Float32: return box_float(v.m_float32);
-    case type::UInt8:   return box(v.m_num);
-    case type::UInt16:  return box(v.m_num);
-    case type::UInt32:  return box_uint32(v.m_num);
-    case type::UInt64:  return box_uint64(v.m_num);
-    case type::USize:   return box_size_t(v.m_num);
-    case type::Object:
-    case type::TObject:
-    case type::Irrelevant:
-        return v.m_obj;
-    case type::Struct:
-    case type::Union:
-        throw exception("not implemented yet");
+        case type::Float: return box_float(v.m_float);
+        case type::UInt8: return box(v.m_num);
+        case type::UInt16: return box(v.m_num);
+        case type::UInt32: return box_uint32(v.m_num);
+        case type::UInt64: return box_uint64(v.m_num);
+        case type::USize: return box_size_t(v.m_num);
+        case type::Object:
+        case type::TObject:
+        case type::Irrelevant:
+            return v.m_obj;
     }
     lean_unreachable();
 }
 
 value unbox_t(object * o, type t) {
     switch (t) {
-    case type::Float:   return value::from_float(unbox_float(o));
-    case type::Float32: return value::from_float32(unbox_float32(o));
-    case type::UInt8:   return unbox(o);
-    case type::UInt16:  return unbox(o);
-    case type::UInt32:  return unbox_uint32(o);
-    case type::UInt64:  return unbox_uint64(o);
-    case type::USize:   return unbox_size_t(o);
-    case type::Irrelevant:
-    case type::Object:
-    case type::TObject:
-        break;
-    case type::Struct:
-    case type::Union:
-        throw exception("not implemented yet");
+        case type::Float: return value::from_float(unbox_float(o));
+        case type::UInt8: return unbox(o);
+        case type::UInt16: return unbox(o);
+        case type::UInt32: return unbox_uint32(o);
+        case type::UInt64: return unbox_uint64(o);
+        case type::USize: return unbox_size_t(o);
+        case type::Irrelevant:
+        case type::Object:
+        case type::TObject:
+            break;
     }
     lean_unreachable();
 }
@@ -298,8 +278,6 @@ value unbox_t(object * o, type t) {
 void print_value(tout & ios, value const & v, type t) {
     if (t == type::Float) {
         ios << v.m_float;
-    } else if (t == type::Float32) {
-        ios << v.m_float32;
     } else if (type_is_scalar(t)) {
         ios << v.m_num;
     } else {
@@ -494,7 +472,6 @@ private:
                 object * o = var(expr_sproj_obj(e)).m_obj;
                 switch (t) {
                     case type::Float: return value::from_float(cnstr_get_float(o, offset));
-                    case type::Float32: return value::from_float32(cnstr_get_float32(o, offset));
                     case type::UInt8: return cnstr_get_uint8(o, offset);
                     case type::UInt16: return cnstr_get_uint16(o, offset);
                     case type::UInt32: return cnstr_get_uint32(o, offset);
@@ -503,8 +480,6 @@ private:
                     case type::Irrelevant:
                     case type::Object:
                     case type::TObject:
-                    case type::Struct:
-                    case type::Union:
                         break;
                 }
                 throw exception("invalid instruction");
@@ -555,9 +530,6 @@ private:
                             case type::Float:
                                 lean_inc(n.raw());
                                 return value::from_float(lean_float_of_nat(n.raw()));
-                            case type::Float32:
-                                lean_inc(n.raw());
-                                return value::from_float32(lean_float32_of_nat(n.raw()));
                             case type::UInt8:
                             case type::UInt16:
                             case type::UInt32:
@@ -571,9 +543,6 @@ private:
                                 return n.to_obj_arg();
                             case type::Irrelevant:
                                 break;
-                            case type::Union:
-                            case type::Struct:
-                                break;
                         }
                         throw exception("invalid instruction");
                     }
@@ -685,7 +654,6 @@ private:
                     lean_assert(is_exclusive(o));
                     switch (fn_body_sset_type(b)) {
                         case type::Float: cnstr_set_float(o, offset, v.m_float); break;
-                        case type::Float32: cnstr_set_float32(o, offset, v.m_float32); break;
                         case type::UInt8: cnstr_set_uint8(o, offset, v.m_num); break;
                         case type::UInt16: cnstr_set_uint16(o, offset, v.m_num); break;
                         case type::UInt32: cnstr_set_uint32(o, offset, v.m_num); break;
@@ -694,8 +662,6 @@ private:
                         case type::Irrelevant:
                         case type::Object:
                         case type::TObject:
-                        case type::Struct:
-                        case type::Union:
                             throw exception(sstream() << "invalid instruction");
                     }
                     b = fn_body_sset_cont(b);
@@ -841,7 +807,6 @@ private:
             // constants do not have boxed wrappers, but we'll survive
             switch (t) {
                 case type::Float: return value::from_float(*static_cast<double *>(e.m_addr));
-                case type::Float32: return value::from_float32(*static_cast<float *>(e.m_addr));
                 case type::UInt8: return *static_cast<uint8 *>(e.m_addr);
                 case type::UInt16: return *static_cast<uint16 *>(e.m_addr);
                 case type::UInt32: return *static_cast<uint32 *>(e.m_addr);
@@ -851,9 +816,6 @@ private:
                 case type::TObject:
                 case type::Irrelevant:
                     return *static_cast<object **>(e.m_addr);
-                case type::Struct:
-                case type::Union:
-                    throw exception("not implemented yet");
             }
         }
 

src/library/compiler/llnf.cpp

@@ -34,7 +34,6 @@ static char const * g_cnstr = "_cnstr";
 static name * g_reuse       = nullptr;
 static name * g_reset       = nullptr;
 static name * g_fset        = nullptr;
-static name * g_f32set      = nullptr;
 static name * g_sset        = nullptr;
 static name * g_uset        = nullptr;
 static name * g_proj        = nullptr;
@@ -163,9 +162,6 @@ bool is_llnf_sset(expr const & e, unsigned & sz, unsigned & n, unsigned & offset
 expr mk_llnf_fset(unsigned n, unsigned offset) { return mk_constant(name(name(*g_fset, n), offset)); }
 bool is_llnf_fset(expr const & e, unsigned & n, unsigned & offset) { return is_llnf_binary_primitive(e, *g_fset, n, offset); }
 
-expr mk_llnf_f32set(unsigned n, unsigned offset) { return mk_constant(name(name(*g_f32set, n), offset)); }
-bool is_llnf_f32set(expr const & e, unsigned & n, unsigned & offset) { return is_llnf_binary_primitive(e, *g_f32set, n, offset); }
-
 /* The `_uset.<n>` instruction sets a `usize` value in a constructor object at offset `sizeof(void*)*n`. */
 expr mk_llnf_uset(unsigned n) { return mk_constant(name(*g_uset, n)); }
 bool is_llnf_uset(expr const & e, unsigned & n) { return is_llnf_unary_primitive(e, *g_uset, n); }
@@ -222,7 +218,6 @@ bool is_llnf_op(expr const & e) {
         is_llnf_reset(e)   ||
         is_llnf_sset(e)    ||
         is_llnf_fset(e)    ||
-        is_llnf_f32set(e)  ||
         is_llnf_uset(e)    ||
         is_llnf_proj(e)    ||
         is_llnf_sproj(e)   ||
@@ -525,10 +520,6 @@ class to_lambda_pure_fn {
         return mk_app(mk_llnf_fset(num, offset), major, v);
     }
 
-    expr mk_f32set(expr const & major, unsigned num, unsigned offset, expr const & v) {
-        return mk_app(mk_llnf_f32set(num, offset), major, v);
-    }
-
     expr mk_uset(expr const & major, unsigned idx, expr const & v) {
         return mk_app(mk_llnf_uset(idx), major, v);
     }
@@ -693,10 +684,8 @@ class to_lambda_pure_fn {
                 if (first) {
                     r = mk_let_decl(mk_enf_object_type(), r);
                 }
-                if (info.is_float()) {
+                if (info.is_float() || info.is_float32()) {
                     r = mk_let_decl(mk_enf_object_type(), mk_fset(r, info.m_idx, info.m_offset, args[j]));
-                } else if (info.is_float32()) {
-                    r = mk_let_decl(mk_enf_object_type(), mk_f32set(r, info.m_idx, info.m_offset, args[j]));
                 } else {
                     r = mk_let_decl(mk_enf_object_type(), mk_sset(r, info.m_size, info.m_idx, info.m_offset, args[j]));
                 }
@@ -845,8 +834,6 @@ void initialize_llnf() {
     mark_persistent(g_sset->raw());
     g_fset      = new name("_fset");
     mark_persistent(g_fset->raw());
-    g_f32set      = new name("_f32set");
-    mark_persistent(g_f32set->raw());
     g_uset      = new name("_uset");
     mark_persistent(g_uset->raw());
     g_proj      = new name("_proj");
@@ -877,7 +864,6 @@ void finalize_llnf() {
     delete g_reset;
     delete g_sset;
     delete g_fset;
-    delete g_f32set;
     delete g_proj;
     delete g_sproj;
     delete g_fproj;

src/library/compiler/llnf.h

@@ -26,7 +26,6 @@ bool is_llnf_fproj(expr const & e, unsigned & n, unsigned & offset);
 bool is_llnf_uproj(expr const & e, unsigned & idx);
 bool is_llnf_sset(expr const & e, unsigned & sz, unsigned & n, unsigned & offset);
 bool is_llnf_fset(expr const & e, unsigned & n, unsigned & offset);
-bool is_llnf_f32set(expr const & e, unsigned & n, unsigned & offset);
 bool is_llnf_uset(expr const & e, unsigned & n);
 bool is_llnf_jmp(expr const & e);
 bool is_llnf_unbox(expr const & e, unsigned & n);
@@ -44,7 +43,6 @@ inline bool is_llnf_fproj(expr const & e) { unsigned d1, d2; return is_llnf_fpro
 inline bool is_llnf_uproj(expr const & e) { unsigned d; return is_llnf_uproj(e, d); }
 inline bool is_llnf_sset(expr const & e) { unsigned d1, d2, d3; return is_llnf_sset(e, d1, d2, d3); }
 inline bool is_llnf_fset(expr const & e) { unsigned d1, d2; return is_llnf_fset(e, d1, d2); }
-inline bool is_llnf_f32set(expr const & e) { unsigned d1, d2; return is_llnf_f32set(e, d1, d2); }
 inline bool is_llnf_uset(expr const & e) { unsigned d; return is_llnf_uset(e, d); }
 inline bool is_llnf_box(expr const & e) { unsigned n; return is_llnf_box(e, n); }
 inline bool is_llnf_unbox(expr const & e) { unsigned n; return is_llnf_unbox(e, n); }

src/runtime/object.h

@@ -85,13 +85,11 @@ inline uint16 cnstr_get_uint16(b_obj_arg o, unsigned offset) { return lean_ctor_
 inline uint32 cnstr_get_uint32(b_obj_arg o, unsigned offset) { return lean_ctor_get_uint32(o, offset); }
 inline uint64 cnstr_get_uint64(b_obj_arg o, unsigned offset) { return lean_ctor_get_uint64(o, offset); }
 inline double cnstr_get_float(b_obj_arg o, unsigned offset) { return lean_ctor_get_float(o, offset); }
-inline float cnstr_get_float32(b_obj_arg o, unsigned offset) { return lean_ctor_get_float32(o, offset); }
 inline void cnstr_set_uint8(b_obj_arg o, unsigned offset, uint8 v) { lean_ctor_set_uint8(o, offset, v); }
 inline void cnstr_set_uint16(b_obj_arg o, unsigned offset, uint16 v) { lean_ctor_set_uint16(o, offset, v); }
 inline void cnstr_set_uint32(b_obj_arg o, unsigned offset, uint32 v) { lean_ctor_set_uint32(o, offset, v); }
 inline void cnstr_set_uint64(b_obj_arg o, unsigned offset, uint64 v) { lean_ctor_set_uint64(o, offset, v); }
 inline void cnstr_set_float(b_obj_arg o, unsigned offset, double v) { lean_ctor_set_float(o, offset, v); }
-inline void cnstr_set_float32(b_obj_arg o, unsigned offset, float v) { lean_ctor_set_float32(o, offset, v); }
 
 // =======================================
 // Closures
@@ -374,7 +372,6 @@ inline obj_res box_uint64(unsigned long long v) { return lean_box_uint64(v); }
 inline unsigned long long unbox_uint64(b_obj_arg o) { return lean_unbox_uint64(o); }
 inline obj_res box_float(double v) { return lean_box_float(v); }
 inline double unbox_float(b_obj_arg o) { return lean_unbox_float(o); }
-inline float unbox_float32(b_obj_arg o) { return lean_unbox_float32(o); }
 inline obj_res box_size_t(size_t v) { return lean_box_usize(v); }
 inline size_t unbox_size_t(b_obj_arg o) { return lean_unbox_usize(o); }
 

tests/lean/run/bv_uninterpreted.lean

@@ -5,8 +5,8 @@ example {x y z : BitVec w} :
     (x &&& y) ||| (x &&& z) ||| (y &&& z) ||| x ||| y ||| z
       =
     ~~~ ((~~~ x) &&& (~~~ y) &&& (~~~ z)) := by
-  ext i h
-  simp [h]
+  ext
+  simp
   bv_decide
 
 @[irreducible]

tests/lean/run/wfOverapplicationIssue.lean

@@ -1,6 +1,6 @@
 theorem Array.sizeOf_lt_of_mem' [DecidableEq α] [SizeOf α] {as : Array α} (h : as.contains a) : sizeOf a < sizeOf as := by
   simp [Membership.mem, contains, any, Id.run, BEq.beq, anyM] at h
-  let rec aux (j : Nat) : anyM.loop (m := Id) (fun b => decide (a = b)) as as.size (Nat.le_refl ..) j = true → sizeOf a < sizeOf as := by
+  let rec aux (j : Nat) : anyM.loop (m := Id) (fun b => decide (b = a)) as as.size (Nat.le_refl ..) j = true → sizeOf a < sizeOf as := by
     unfold anyM.loop
     intro h
     split at h