feat: improve Nat simp lemma confluence (#5148)

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -86,6 +86,12 @@ noncomputable def div2Induction {motive : Nat → Sort u}
 @[simp] theorem testBit_zero (x : Nat) : testBit x 0 = decide (x % 2 = 1) := by
   cases mod_two_eq_zero_or_one x with | _ p => simp [testBit, p]
 
+theorem mod_two_eq_one_iff_testBit_zero : (x % 2 = 1) ↔ x.testBit 0 = true := by
+  cases mod_two_eq_zero_or_one x <;> simp_all
+
+theorem mod_two_eq_zero_iff_testBit_zero : (x % 2 = 0) ↔ x.testBit 0 = false := by
+  cases mod_two_eq_zero_or_one x <;> simp_all
+
 theorem testBit_succ (x i : Nat) : testBit x (succ i) = testBit (x/2) i := by
   unfold testBit
   simp [shiftRight_succ_inside]
@@ -94,6 +100,9 @@ theorem testBit_succ (x i : Nat) : testBit x (succ i) = testBit (x/2) i := by
   unfold testBit
   simp [shiftRight_succ_inside]
 
+theorem testBit_div_two (x i : Nat) : testBit (x / 2) i = testBit x (i + 1) := by
+  simp
+
 theorem testBit_to_div_mod {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1) := by
   induction i generalizing x with
   | zero =>
@@ -315,6 +324,17 @@ theorem testBit_one_eq_true_iff_self_eq_zero {i : Nat} :
     Nat.testBit 1 i = true ↔ i = 0 := by
   cases i <;> simp
 
+@[simp] theorem two_pow_sub_one_mod_two : (2 ^ n - 1) % 2 = 1 % 2 ^ n := by
+  cases n with
+  | zero => simp
+  | succ n =>
+    rw [mod_eq_of_lt (a := 1) (Nat.one_lt_two_pow (by omega)), mod_two_eq_one_iff_testBit_zero, testBit_two_pow_sub_one ]
+    simp only [zero_lt_succ, decide_True]
+
+@[simp] theorem mod_two_pos_mod_two_eq_one : x % 2 ^ j % 2 = 1 ↔ (0 < j) ∧ x % 2 = 1 := by
+  rw [mod_two_eq_one_iff_testBit_zero, testBit_mod_two_pow]
+  simp
+
 /-! ### bitwise -/
 
 theorem testBit_bitwise
@@ -417,6 +437,11 @@ theorem and_pow_two_identity {x : Nat} (lt : x < 2^n) : x &&& 2^n-1 = x := by
   rw [and_pow_two_is_mod]
   apply Nat.mod_eq_of_lt lt
 
+@[simp] theorem and_mod_two_eq_one : (a &&& b) % 2 = 1 ↔ a % 2 = 1 ∧ b % 2 = 1 := by
+  simp only [mod_two_eq_one_iff_testBit_zero]
+  rw [testBit_and]
+  simp
+
 /-! ### lor -/
 
 @[simp] theorem zero_or (x : Nat) : 0 ||| x = x := by
@@ -435,6 +460,11 @@ theorem and_pow_two_identity {x : Nat} (lt : x < 2^n) : x &&& 2^n-1 = x := by
 theorem or_lt_two_pow {x y n : Nat} (left : x < 2^n) (right : y < 2^n) : x ||| y < 2^n :=
   bitwise_lt_two_pow left right
 
+@[simp] theorem or_mod_two_eq_one : (a ||| b) % 2 = 1 ↔ a % 2 = 1 ∨ b % 2 = 1 := by
+  simp only [mod_two_eq_one_iff_testBit_zero]
+  rw [testBit_or]
+  simp
+
 /-! ### xor -/
 
 @[simp] theorem testBit_xor (x y i : Nat) :
@@ -452,6 +482,11 @@ theorem and_xor_distrib_left {a b c : Nat} : a &&& (b ^^^ c) = (a &&& b) ^^^ (a
   apply Nat.eq_of_testBit_eq
   simp [Bool.and_xor_distrib_left]
 
+@[simp] theorem xor_mod_two_eq_one : ((a ^^^ b) % 2 = 1) ↔ ¬ ((a % 2 = 1) ↔ (b % 2 = 1)) := by
+  simp only [mod_two_eq_one_iff_testBit_zero]
+  rw [testBit_xor]
+  simp
+
 /-! ### Arithmetic -/
 
 theorem testBit_mul_pow_two_add (a : Nat) {b i : Nat} (b_lt : b < 2^i) (j : Nat) :
@@ -513,6 +548,15 @@ theorem mul_add_lt_is_or {b : Nat} (b_lt : b < 2^i) (a : Nat) : 2^i * a + b = 2^
 @[simp] theorem testBit_shiftRight (x : Nat) : testBit (x >>> i) j = testBit x (i+j) := by
   simp [testBit, ←shiftRight_add]
 
+@[simp] theorem shiftLeft_mod_two_eq_one : x <<< i % 2 = 1 ↔ i = 0 ∧ x % 2 = 1 := by
+  rw [mod_two_eq_one_iff_testBit_zero, testBit_shiftLeft]
+  simp
+
+@[simp] theorem decide_shiftRight_mod_two_eq_one :
+    decide (x >>> i % 2 = 1) = x.testBit i := by
+  simp only [testBit, one_and_eq_mod_two, mod_two_bne_zero]
+  exact (Bool.beq_eq_decide_eq _ _).symm
+
 /-! ### le -/
 
 theorem le_of_testBit {n m : Nat} (h : ∀ i, n.testBit i = true → m.testBit i = true) : n ≤ m := by

src/Init/Data/Nat/Lemmas.lean

@@ -544,6 +544,11 @@ theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
   | 0, _ => .inl rfl
   | 1, _ => .inr rfl
 
+@[simp] theorem mod_two_bne_zero : ((a % 2) != 0) = (a % 2 == 1) := by
+  cases mod_two_eq_zero_or_one a <;> simp_all
+@[simp] theorem mod_two_bne_one : ((a % 2) != 1) = (a % 2 == 0) := by
+  cases mod_two_eq_zero_or_one a <;> simp_all
+
 theorem le_of_mod_lt {a b : Nat} (h : a % b < a) : b ≤ a :=
   Nat.not_lt.1 fun hf => (ne_of_lt h).elim (Nat.mod_eq_of_lt hf)
 
@@ -654,6 +659,13 @@ protected theorem one_le_two_pow : 1 ≤ 2 ^ n :=
   else
     Nat.le_of_lt (Nat.one_lt_two_pow h)
 
+@[simp] theorem one_mod_two_pow_eq_one : 1 % 2 ^ n = 1 ↔ 0 < n := by
+  cases n with
+  | zero => simp
+  | succ n =>
+    rw [mod_eq_of_lt (a := 1) (Nat.one_lt_two_pow (by omega))]
+    simp
+
 protected theorem pow_pos (h : 0 < a) : 0 < a^n :=
   match n with
   | 0 => Nat.zero_lt_one