chore: update mathlib nightly 2024-10-17 (#711)

Co-authored-by: Tobias Grosser <[email protected]>

SSA/Experimental/Bits/AutoStructs/FiniteStateMachine.lean

@@ -21,7 +21,7 @@ variable {α β α' β' : Type} {γ : β → Type}
 where `n` is the number of `BitStream` arguments,
 as a finite state machine.
 -/
-structure FSM (arity : Type) : Type 1 :=
+structure FSM (arity : Type) : Type 1 where
   /--
   The arity of the (finite) type `α` determines how many bits the internal carry state of this
   FSM has -/
@@ -307,7 +307,7 @@ def sub : FSM Bool :=
 theorem carry_sub (x : Bool → BitStream) : ∀ (n : ℕ), sub.carry x (n+1) =
     fun _ => (BitStream.subAux (x true) (x false) n).2
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, BitStream.subAux, sub]
+    simp [carry, nextBit, BitStream.subAux, sub]
   | n+1 => by
     rw [carry, carry_sub _ n]
     simp [nextBit, eval, sub, BitStream.sub, BitStream.subAux, Bool.xor_not_left']
@@ -333,7 +333,7 @@ def neg : FSM Unit :=
 theorem carry_neg (x : Unit → BitStream) : ∀ (n : ℕ), neg.carry x (n+1) =
     fun _ => (BitStream.negAux (x ()) n).2
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, BitStream.negAux, neg]
+    simp [carry, nextBit, BitStream.negAux, neg]
   | n+1 => by
     rw [carry, carry_neg _ n]
     simp [nextBit, eval, neg, BitStream.neg, BitStream.negAux, Bool.xor_not_left']
@@ -401,7 +401,7 @@ def ls (b : Bool) : FSM Unit :=
 theorem carry_ls (b : Bool) (x : Unit → BitStream) : ∀ (n : ℕ),
     (ls b).carry x (n+1) = fun _ => x () n
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, ls]
+    simp [carry, nextBit, ls]
   | n+1 => by
     rw [carry, carry_ls _ _ n]
     simp [nextBit, eval, ls]
@@ -433,7 +433,7 @@ def incr : FSM Unit :=
 theorem carry_incr (x : Unit → BitStream) : ∀ (n : ℕ),
     incr.carry x (n+1) = fun _ => (BitStream.incrAux (x ()) n).2
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, BitStream.incrAux, incr]
+    simp [carry, nextBit, BitStream.incrAux, incr]
   | n+1 => by
     rw [carry, carry_incr _ n]
     simp [nextBit, eval, incr, incr, BitStream.incrAux]
@@ -456,7 +456,7 @@ def decr : FSM Unit :=
 theorem carry_decr (x : Unit → BitStream) : ∀ (n : ℕ), decr.carry x (n+1) =
     fun _ => (BitStream.decrAux (x ()) n).2
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, BitStream.decrAux, decr]
+    simp [carry, nextBit, BitStream.decrAux, decr]
   | n+1 => by
     rw [carry, carry_decr _ n]
     simp [nextBit, eval, decr, BitStream.decrAux]
@@ -508,7 +508,7 @@ def repeatBit : FSM Unit where
 
 end FSM
 
-structure FSMSolution (t : Term) extends FSM (Fin t.arity) :=
+structure FSMSolution (t : Term) extends FSM (Fin t.arity) where
   ( good : t.evalFinStream = toFSM.eval )
 
 def composeUnary

SSA/Experimental/Bits/Fast/BitStream.lean

@@ -500,6 +500,8 @@ theorem ofBitVec_one_eqTo_ofNat : @ofBitVec w 1 ≈ʷ ofNat 1 := by
   · simp [EqualUpTo ,h]
   · intros n a
     simp [ofNat_one n, ofBitVec, a]
+    rw [← Bool.decide_and]
+    rw [decide_eq_decide]
     omega
 
 theorem ofBitVec_neg : ofBitVec (- x) ≈ʷ - (ofBitVec x) := by

SSA/Experimental/Bits/Fast/Decide.lean

@@ -8,7 +8,7 @@ instance (t₁ t₂ : Term) : Decidable (t₁.eval = t₂.eval) :=
     ← (termEvalEqFSM (t₁.xor t₂)).good]
   simp only [eval_eq_iff_xor_eq_zero]
   rw [forall_swap]
-  simp only [← Function.funext_iff]
+  simp only [← funext_iff]
 
 
 open Term

SSA/Experimental/Bits/Fast/FiniteStateMachine.lean

@@ -303,7 +303,7 @@ def sub : FSM Bool :=
 theorem carry_sub (x : Bool → BitStream) : ∀ (n : ℕ), sub.carry x (n+1) =
     fun _ => (BitStream.subAux (x true) (x false) n).2
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, BitStream.subAux, sub]
+    simp [carry, nextBit, funext_iff, BitStream.subAux, sub]
   | n+1 => by
     rw [carry, carry_sub _ n]
     simp [nextBit, eval, sub, BitStream.sub, BitStream.subAux, Bool.xor_not_left']
@@ -329,7 +329,7 @@ def neg : FSM Unit :=
 theorem carry_neg (x : Unit → BitStream) : ∀ (n : ℕ), neg.carry x (n+1) =
     fun _ => (BitStream.negAux (x ()) n).2
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, BitStream.negAux, neg]
+    simp [carry, nextBit, funext_iff, BitStream.negAux, neg]
   | n+1 => by
     rw [carry, carry_neg _ n]
     simp [nextBit, eval, neg, BitStream.neg, BitStream.negAux, Bool.xor_not_left']
@@ -397,7 +397,7 @@ def ls (b : Bool) : FSM Unit :=
 theorem carry_ls (b : Bool) (x : Unit → BitStream) : ∀ (n : ℕ),
     (ls b).carry x (n+1) = fun _ => x () n
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, ls]
+    simp [carry, nextBit, funext_iff, ls]
   | n+1 => by
     rw [carry, carry_ls _ _ n]
     simp [nextBit, eval, ls]
@@ -429,7 +429,7 @@ def incr : FSM Unit :=
 theorem carry_incr (x : Unit → BitStream) : ∀ (n : ℕ),
     incr.carry x (n+1) = fun _ => (BitStream.incrAux (x ()) n).2
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, BitStream.incrAux, incr]
+    simp [carry, nextBit, funext_iff, BitStream.incrAux, incr]
   | n+1 => by
     rw [carry, carry_incr _ n]
     simp [nextBit, eval, incr, incr, BitStream.incrAux]
@@ -452,7 +452,7 @@ def decr : FSM Unit :=
 theorem carry_decr (x : Unit → BitStream) : ∀ (n : ℕ), decr.carry x (n+1) =
     fun _ => (BitStream.decrAux (x ()) n).2
   | 0 => by
-    simp [carry, nextBit, Function.funext_iff, BitStream.decrAux, decr]
+    simp [carry, nextBit, funext_iff, BitStream.decrAux, decr]
   | n+1 => by
     rw [carry, carry_decr _ n]
     simp [nextBit, eval, decr, BitStream.decrAux]

SSA/Experimental/Bits/Fast/Lemmas.lean

@@ -19,11 +19,11 @@ lemma evalFin_eq_eval (t : Term) (vars : Nat → BitStream) :
 
 lemma eq_iff_xor_eq_zero (seq₁ seq₂ : BitStream) :
     (∀ i, seq₁ i = seq₂ i) ↔ (∀ i, (seq₁ ^^^ seq₂) i = BitStream.zero i) := by
-  simp [Function.funext_iff]
+  simp [funext_iff]
 
 lemma eval_eq_iff_xor_eq_zero (t₁ t₂ : Term) :
     t₁.eval = t₂.eval ↔ (t₁.xor t₂).evalFin = fun _ => BitStream.zero := by
-  simp only [Function.funext_iff, Term.eval, Term.evalFin,
+  simp only [funext_iff, Term.eval, Term.evalFin,
     ← eq_iff_xor_eq_zero, ← evalFin_eq_eval]
   constructor
   · intro h seq

SSA/Experimental/Bits/SafeNativeDecide.lean

@@ -26,7 +26,7 @@ private def mkNativeAuxDecl (baseName : Name) (type value : Expr) : TermElabM Na
   pure auxName
 
 elab "safe_native_decide" : tactic =>
-  Lean.Elab.Tactic.closeMainGoalUsing `safeNativeDecide fun expectedType => do
+  Lean.Elab.Tactic.closeMainGoalUsing `safeNativeDecide fun expectedType _ => do
     let expectedType ← preprocessPropToDecide expectedType
     let d ← mkDecide expectedType
     let auxDeclName ← mkNativeAuxDecl `_nativeDecide (Lean.mkConst `Bool) d

SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean

@@ -177,6 +177,8 @@ def alive_simplifyMulDivRem805 (w : Nat) :
                 rw [Nat.mod_eq_of_lt (by omega)]
               subst h1
               simp [BitVec.sdiv_one_one]
+              intro h
+              simp [h]
             · have hcases : (1 + BitVec.toNat x = 2 ^ Nat.succ (Nat.succ w'') ∨
                   1 + BitVec.toNat x = 2 ^ Nat.succ (Nat.succ w'') + 1) := by
                 omega
@@ -240,12 +242,20 @@ def alive_simplifyMulDivRem805' (w : Nat) :
   · simp only [h, ofBool_true, ofNat_eq_ofNat, Refinement.some_some]
     by_cases a_0 : a = 0; subst a_0; simp at c
     by_cases a_1 : a = 1; subst a_1; simp [sdiv_one_one]
-    rw [BitVec.toNat_eq] at a_0 a_1
+    rw [BitVec.toNat_eq] at a_0
+    intro h
+    simp [h]
     simp only [ofNat_eq_ofNat, toNat_ofNat, Nat.zero_mod] at a_0 a_1
-    by_cases w_1 : w = 1; subst w_1; omega
+    by_cases w_1 : w = 1
+    · subst w_1
+      have hh := BitVec.eq_zero_or_eq_one a
+      simp [a_0] at hh
+      simp [a_1] at hh
     have w_gt_1 : 1 < w := by omega
-    have el_one: 1 % 2^w = 1 := by rw [Nat.mod_eq_of_lt]; omega
-    rw [el_one] at a_1
+    have el_one: 1 % 2^w = 1 := by
+      rw [Nat.mod_eq_of_lt]
+      have aa := Nat.lt_two_pow w
+      omega
     have el_three: 3 % 2^w = 3 := by
       rw [Nat.mod_eq_of_lt];
       have x := @Nat.pow_le_pow_of_le 2 2 w (by omega) (by omega);
@@ -259,6 +269,9 @@ def alive_simplifyMulDivRem805' (w : Nat) :
       simp [x]
     · rw [Nat.add_mod_of_add_mod_lt] at h
       simp only [el_one, toNat_mod_cancel] at h
+      simp_all
+      simp [bv_toNat] at a_0
+      simp [bv_toNat, show 0 < w by omega] at a_1
       omega
       simp only [el_one, toNat_mod_cancel]
       rw [BitVec.toNat_eq] at a_allones

SSA/Projects/InstCombine/ForLean.lean

@@ -1,6 +1,7 @@
 import Mathlib.Data.Nat.Size -- TODO: remove and get rid of shiftLeft_eq_mul_pow use
-import SSA.Projects.InstCombine.ForMathlib
 import SSA.Projects.InstCombine.LLVM.Semantics
+import Mathlib.Tactic.Ring
+import Mathlib.Data.BitVec
 
 namespace Nat
 
@@ -125,12 +126,6 @@ lemma one_shiftLeft_mul_eq_shiftLeft {A B : BitVec w} :
   simp only [bv_toNat, Nat.mod_mul_mod, one_mul]
   rw [Nat.mul_comm]
 
-@[simp]
-def msb_one (h : 1 < w) : BitVec.msb 1#w = false := by
-  simp only [BitVec.msb_eq_decide, decide_eq_false_iff_not, not_le, toNat_ofInt,
-    toNat_ofNat]
-  rw [Nat.mod_eq_of_lt] <;> simp <;> omega
-
 @[simp]
 lemma msb_one_of_width_one : BitVec.msb 1#1 = true := rfl
 
@@ -168,10 +163,12 @@ theorem udiv_eq_zero {x y : BitVec w} (h : x < y) : udiv x y = 0#w := by
 def sdiv_one_allOnes {w : Nat} (h : 1 < w) :
     BitVec.sdiv (1#w) (BitVec.allOnes w) = BitVec.allOnes w := by
   simp only [BitVec.sdiv]
-  simp only [msb_one h, neg_eq, @msb_allOnes w (by omega)]
+  simp only [msb_one, neg_eq, @msb_allOnes w (by omega)]
   simp only [neg_allOnes]
   simp only [udiv_one_eq_self]
   simp only [negOne_eq_allOnes]
+  have : ¬ (w = 1) := by omega
+  simp [this]
 
 theorem width_one_cases (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
   obtain ⟨a, ha⟩ := a
@@ -246,14 +243,14 @@ def sdiv_one_one : BitVec.sdiv 1#w 1#w = 1#w := by
   by_cases w_1 : w = 1; subst w_1; rfl
   unfold BitVec.sdiv
   unfold BitVec.udiv
-  simp only [toNat_ofNat, neg_eq, toNat_neg]
-  rw [msb_one (by omega)]
-  simp only []
+  simp only [msb_one, w_1, decide_False, toNat_ofNat, ne_eq, w_0, not_false_eq_true,
+    Nat.one_mod_two_pow_eq, zero_lt_one, Nat.div_self]
+  apply BitVec.eq_of_toNat_eq
+  simp
   have hone : 1 % 2 ^ w = 1 := by
     apply Nat.mod_eq_of_lt
     simp
     omega
-  apply BitVec.eq_of_toNat_eq
   simp [hone]
 
 -- @[simp bv_toNat]
@@ -517,39 +514,6 @@ theorem shiftLeft_and_distrib' {x y : BitVec w} {n m : Nat} :
 theorem zero_sub {x : BitVec w} : 0#w - x = - x := by
     simp [bv_toNat]
 
-theorem getLsbD_sub {i : Nat} {i_lt : i < w} {x y : BitVec w} :
-    (x - y).getLsbD i =
-      (x.getLsbD i ^^ ((~~~y + 1).getLsbD i ^^ carry i x (~~~y + 1) false)) := by
-  rw [BitVec.sub_eq_add_neg, BitVec.neg_eq_not_add, getLsbD_add]
-  rfl
-  omega
-
-
-theorem getMsbD_add {i : Nat} {i_lt : i < w} {x y : BitVec w} :
-    getMsbD (x + y) i =
-      Bool.xor (getMsbD x i) (Bool.xor (getMsbD y i) (carry (w - 1 - i) x y false)) := by
-  simp [getMsbD, getLsbD_add, i_lt, show w - 1 - i < w by omega]
-
-theorem getMsbD_sub {i : Nat} {i_lt : i < w} {x y : BitVec w} :
-    (x - y).getMsbD i =
-      (x.getMsbD i ^^ ((~~~y + 1).getMsbD i ^^ carry (w - 1 - i) x (~~~y + 1) false)) := by
-  rw [BitVec.sub_eq_add_neg, neg_eq_not_add, getMsbD_add]
-  rfl
-  omega
-
-theorem msb_add {w : Nat} {x y: BitVec w} :
-    (x + y).msb =
-      Bool.xor (getMsbD x 0) (Bool.xor (getMsbD y 0) (carry (w - 1) x y false)) := by
-  simp only [BitVec.msb, BitVec.getMsbD]
-  by_cases h : w ≤ 0
-  · simp [h, show w = 0 by omega]
-  · simp [h, getLsbD_add, show w > 0 by omega]
-
-theorem msb_sub {x y: BitVec w} :
-    (x - y).msb
-      = (x.getMsbD 0 ^^ ((~~~y + 1#w).getMsbD 0 ^^ carry (w - 1 - 0) x (~~~y + 1#w) false)) := by
-  simp [sub_eq_add_neg, BitVec.neg_eq_not_add, msb_add]
-
 theorem msb_neg {x : BitVec w} :
     (-x).msb = (~~~x + 1#w).msb := by
   rw [neg_eq_not_add]

SSA/Projects/InstCombine/HackersDelight.lean

@@ -1,4 +1,3 @@
-import SSA.Projects.InstCombine.ForMathlib
 import SSA.Projects.InstCombine.ForStd
 import SSA.Projects.InstCombine.TacticAuto
 import Std.Tactic.BVDecide