From 5a9d7ae9253a3ccb126d47bb0c4fc44da8bcdcae Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Tue, 24 Jun 2025 15:16:21 +1000 Subject: [PATCH] feat: revise grind annotations for bitwise operations (#8965) This PR revises @[grind] annotations on Nat bitwise operations. --- src/Init/Data/Bool.lean | 8 ++++---- src/Init/Data/Int/Bitwise/Lemmas.lean | 1 + src/Init/Data/Nat/Bitwise/Basic.lean | 2 +- src/Init/Data/Nat/Bitwise/Lemmas.lean | 21 ++++++++------------- src/Init/Data/Nat/Lemmas.lean | 9 +++++---- 5 files changed, 19 insertions(+), 22 deletions(-) diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean index 7a06aa99a8..af696ed4c1 100644 --- a/src/Init/Data/Bool.lean +++ b/src/Init/Data/Bool.lean @@ -434,9 +434,9 @@ Converts `true` to `1` and `false` to `0`. -/ @[expose] def toNat (b : Bool) : Nat := cond b 1 0 -@[simp, bitvec_to_nat] theorem toNat_false : false.toNat = 0 := rfl +@[simp, bitvec_to_nat, grind =] theorem toNat_false : false.toNat = 0 := rfl -@[simp, bitvec_to_nat] theorem toNat_true : true.toNat = 1 := rfl +@[simp, bitvec_to_nat, grind =] theorem toNat_true : true.toNat = 1 := rfl theorem toNat_le (c : Bool) : c.toNat ≤ 1 := by cases c <;> trivial @@ -457,9 +457,9 @@ Converts `true` to `1` and `false` to `0`. -/ @[expose] def toInt (b : Bool) : Int := cond b 1 0 -@[simp] theorem toInt_false : false.toInt = 0 := rfl +@[simp, grind =] theorem toInt_false : false.toInt = 0 := rfl -@[simp] theorem toInt_true : true.toInt = 1 := rfl +@[simp, grind =] theorem toInt_true : true.toInt = 1 := rfl /-! ### ite -/ diff --git a/src/Init/Data/Int/Bitwise/Lemmas.lean b/src/Init/Data/Int/Bitwise/Lemmas.lean index 57a160db0d..6e0b81ee55 100644 --- a/src/Init/Data/Int/Bitwise/Lemmas.lean +++ b/src/Init/Data/Int/Bitwise/Lemmas.lean @@ -21,6 +21,7 @@ theorem natCast_shiftRight (n s : Nat) : (n : Int) >>> s = n >>> s := rfl theorem negSucc_shiftRight (m n : Nat) : -[m+1] >>> n = -[m >>>n +1] := rfl +@[grind _=_] theorem shiftRight_add (i : Int) (m n : Nat) : i >>> (m + n) = i >>> m >>> n := by simp only [shiftRight_eq, Int.shiftRight] diff --git a/src/Init/Data/Nat/Bitwise/Basic.lean b/src/Init/Data/Nat/Bitwise/Basic.lean index 3815e297b8..9cce6bf936 100644 --- a/src/Init/Data/Nat/Bitwise/Basic.lean +++ b/src/Init/Data/Nat/Bitwise/Basic.lean @@ -105,7 +105,7 @@ theorem shiftLeft_eq (a b : Nat) : a <<< b = a * 2 ^ b := | b+1 => (shiftLeft_eq _ b).trans <| by simp [Nat.pow_succ, Nat.mul_assoc, Nat.mul_comm] -@[simp] theorem shiftRight_zero : n >>> 0 = n := rfl +@[simp, grind =] theorem shiftRight_zero : n >>> 0 = n := rfl theorem shiftRight_succ (m n) : m >>> (n + 1) = (m >>> n) / 2 := rfl diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean index 30329eebe9..db32ab4981 100644 --- a/src/Init/Data/Nat/Bitwise/Lemmas.lean +++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean @@ -81,10 +81,10 @@ noncomputable def div2Induction {motive : Nat → Sort u} /-! ### testBit -/ -@[simp] theorem zero_testBit (i : Nat) : testBit 0 i = false := by +@[simp, grind =] theorem zero_testBit (i : Nat) : testBit 0 i = false := by simp only [testBit, zero_shiftRight, and_zero, bne_self_eq_false] -@[simp] theorem testBit_zero (x : Nat) : testBit x 0 = decide (x % 2 = 1) := by +@[simp, grind =] 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 @@ -349,12 +349,16 @@ theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) : · simp · exact Nat.two_pow_pos _ -theorem testBit_bool_to_nat (b : Bool) (i : Nat) : +@[grind =] +theorem testBit_bool_toNat (b : Bool) (i : Nat) : testBit (Bool.toNat b) i = (decide (i = 0) && b) := by cases b <;> cases i <;> - simp [testBit_eq_decide_div_mod_eq, + simp [testBit_eq_decide_div_mod_eq, Nat.mod_eq_of_lt] +@[deprecated testBit_bool_toNat (since := "2025-06-22")] +abbrev testBit_bool_to_nat := @testBit_bool_toNat + /-- `testBit 1 i` is true iff the index `i` equals 0. -/ theorem testBit_one_eq_true_iff_self_eq_zero {i : Nat} : Nat.testBit 1 i = true ↔ i = 0 := by @@ -543,15 +547,12 @@ abbrev and_pow_two_sub_one_of_lt_two_pow := @and_two_pow_sub_one_of_lt_two_pow rw [testBit_and] simp -@[grind _=_] theorem and_div_two_pow : (a &&& b) / 2 ^ n = a / 2 ^ n &&& b / 2 ^ n := bitwise_div_two_pow -@[grind _=_] theorem and_div_two : (a &&& b) / 2 = a / 2 &&& b / 2 := and_div_two_pow (n := 1) -@[grind _=_] theorem and_mod_two_pow : (a &&& b) % 2 ^ n = (a % 2 ^ n) &&& (b % 2 ^ n) := bitwise_mod_two_pow @@ -625,15 +626,12 @@ theorem or_lt_two_pow {x y n : Nat} (left : x < 2^n) (right : y < 2^n) : x ||| y rw [testBit_or] simp -@[grind _=_] theorem or_div_two_pow : (a ||| b) / 2 ^ n = a / 2 ^ n ||| b / 2 ^ n := bitwise_div_two_pow -@[grind _=_] theorem or_div_two : (a ||| b) / 2 = a / 2 ||| b / 2 := or_div_two_pow (n := 1) -@[grind _=_] theorem or_mod_two_pow : (a ||| b) % 2 ^ n = a % 2 ^ n ||| b % 2 ^ n := bitwise_mod_two_pow @@ -693,15 +691,12 @@ theorem and_xor_distrib_left {a b c : Nat} : a &&& (b ^^^ c) = (a &&& b) ^^^ (a rw [testBit_xor] simp -@[grind _=_] theorem xor_div_two_pow : (a ^^^ b) / 2 ^ n = a / 2 ^ n ^^^ b / 2 ^ n := bitwise_div_two_pow -@[grind _=_] theorem xor_div_two : (a ^^^ b) / 2 = a / 2 ^^^ b / 2 := xor_div_two_pow (n := 1) -@[grind _=_] theorem xor_mod_two_pow : (a ^^^ b) % 2 ^ n = a % 2 ^ n ^^^ b % 2 ^ n := bitwise_mod_two_pow diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index 6b4568a1d2..0ec01cc651 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -1320,7 +1320,7 @@ theorem le_log2 (h : n ≠ 0) : k ≤ n.log2 ↔ 2 ^ k ≤ n := by | k+1 => rw [log2]; split · have n0 : 0 < n / 2 := (Nat.le_div_iff_mul_le (by decide)).2 ‹_› - simp only [Nat.add_le_add_iff_right, le_log2 (Nat.ne_of_gt n0), + simp only [Nat.add_le_add_iff_right, le_log2 (Nat.ne_of_gt n0), Nat.pow_succ] exact Nat.le_div_iff_mul_le (by decide) · simp only [le_zero_eq, succ_ne_zero, false_iff] @@ -1686,7 +1686,7 @@ theorem div_lt_div_of_lt_of_dvd {a b d : Nat} (hdb : d ∣ b) (h : a < b) : a / /-! ### shiftLeft and shiftRight -/ -@[simp] theorem shiftLeft_zero : n <<< 0 = n := rfl +@[simp, grind =] theorem shiftLeft_zero : n <<< 0 = n := rfl /-- Shiftleft on successor with multiple moved inside. -/ theorem shiftLeft_succ_inside (m n : Nat) : m <<< (n+1) = (2*m) <<< n := rfl @@ -1705,14 +1705,15 @@ theorem shiftRight_succ_inside : ∀m n, m >>> (n+1) = (m/2) >>> n rw [shiftRight_succ _ (k+1)] rw [shiftRight_succ_inside _ k, shiftRight_succ] -@[simp] theorem zero_shiftLeft : ∀ n, 0 <<< n = 0 +@[simp, grind =] theorem zero_shiftLeft : ∀ n, 0 <<< n = 0 | 0 => by simp | n + 1 => by simp [zero_shiftLeft n, shiftLeft_succ] -@[simp] theorem zero_shiftRight : ∀ n, 0 >>> n = 0 +@[simp, grind =] theorem zero_shiftRight : ∀ n, 0 >>> n = 0 | 0 => by simp | n + 1 => by simp [zero_shiftRight n, shiftRight_succ] +@[grind _=_] theorem shiftLeft_add (m n : Nat) : ∀ k, m <<< (n + k) = (m <<< n) <<< k | 0 => rfl | k + 1 => by simp [← Nat.add_assoc, shiftLeft_add _ _ k, shiftLeft_succ]