From df3a5da46928ef03c2362eb1a660f7d01e343b5f Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 27 Sep 2024 18:54:23 +0100 Subject: [PATCH 1/5] chore: BitVec.Lemmas - drop non-terminal simps --- src/Init/Data/BitVec/Lemmas.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 58a147a6e527..0c6f4d4a44fb 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -303,7 +303,7 @@ theorem getElem?_zero_ofNat_one : (BitVec.ofNat (w+1) 1)[0]? = some true := by -- This does not need to be a `@[simp]` theorem as it is already handled by `getElem?_eq_getElem`. theorem getElem?_zero_ofBool (b : Bool) : (ofBool b)[0]? = some b := by - simp [ofBool, cond_eq_if] + simp only [ofBool, ofNat_eq_ofNat, cond_eq_if] split <;> simp_all @[simp] theorem getElem_zero_ofBool (b : Bool) : (ofBool b)[0] = b := by @@ -332,7 +332,7 @@ theorem getElem_ofBool {b : Bool} {i : Nat} : (ofBool b)[0] = b := by theorem msb_eq_getLsbD_last (x : BitVec w) : x.msb = x.getLsbD (w - 1) := by - simp [BitVec.msb, getMsbD, getLsbD] + simp only [BitVec.msb, getMsbD] rcases w with rfl | w · simp [BitVec.eq_nil x] · simp @@ -360,7 +360,7 @@ theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat | 0 => simp [BitVec.msb, BitVec.getMsbD] at p | n + 1 => - simp [BitVec.msb_eq_decide] at p + simp only [msb_eq_decide, Nat.add_one_sub_one, decide_eq_true_eq] at p simp only [Nat.add_sub_cancel] exact p @@ -420,7 +420,7 @@ theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := /-- Prove equality of bitvectors in terms of nat operations. -/ theorem eq_of_toInt_eq {x y : BitVec n} : x.toInt = y.toInt → x = y := by intro eq - simp [toInt_eq_toNat_cond] at eq + simp only [toInt_eq_toNat_cond] at eq apply eq_of_toNat_eq revert eq have _xlt := x.isLt @@ -901,7 +901,7 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl rw [Nat.testBit_two_pow_sub_succ (isLt _)] · cases w : decide (i < v) · simp at w - simp [w] + simp only [Bool.false_bne, Bool.false_and] rw [Nat.testBit_lt_two_pow] calc BitVec.toNat x < 2 ^ v := isLt _ _ ≤ 2 ^ i := Nat.pow_le_pow_of_le_right Nat.zero_lt_two w @@ -1515,7 +1515,7 @@ theorem getElem_append {x : BitVec n} {y : BitVec m} (h : i < n + m) : theorem msb_append {x : BitVec w} {y : BitVec v} : (x ++ y).msb = bif (w == 0) then (y.msb) else (x.msb) := by rw [← append_eq, append] - simp [msb_setWidth'] + simp only [msb_or, msb_shiftLeftZeroExtend, msb_setWidth'] by_cases h : w = 0 · subst h simp [BitVec.msb, getMsbD] @@ -1636,13 +1636,13 @@ theorem shiftRight_shiftRight {w : Nat} (x : BitVec w) (n m : Nat) : theorem getLsbD_rev (x : BitVec w) (i : Fin w) : x.getLsbD i.rev = x.getMsbD i := by - simp [getLsbD, getMsbD] + simp only [getLsbD, Fin.val_rev, getMsbD, Fin.is_lt, decide_True, Bool.true_and] congr 1 omega theorem getElem_rev {x : BitVec w} {i : Fin w}: x[i.rev] = x.getMsbD i := by - simp [getMsbD] + simp only [Fin.getElem_fin, Fin.val_rev, getMsbD, Fin.is_lt, decide_True, Bool.true_and] congr 1 omega @@ -1952,7 +1952,7 @@ theorem toInt_neg {x : BitVec w} : Int.bmod_add_cancel] by_cases h : x.toNat < ((2 ^ w) + 1) / 2 · rw [Int.bmod_pos (x := x.toNat)] - all_goals simp [toNat_mod_cancel', h] + all_goals simp only [toNat_mod_cancel'] norm_cast · rw [Int.bmod_neg (x := x.toNat)] · simp only [toNat_mod_cancel'] From 121211a08366478813e523e0db86e706705154de Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 28 Sep 2024 10:05:39 +0100 Subject: [PATCH 2/5] chore: fix missing freestanding simp --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 0c6f4d4a44fb..cec0c272733f 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -900,7 +900,7 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl rw [← h] rw [Nat.testBit_two_pow_sub_succ (isLt _)] · cases w : decide (i < v) - · simp at w + · simp only [decide_eq_false_iff_not, Nat.not_lt] at w simp only [Bool.false_bne, Bool.false_and] rw [Nat.testBit_lt_two_pow] calc BitVec.toNat x < 2 ^ v := isLt _ From c11ca6e73b761a6fcbae1e173066f28225e41154 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 28 Sep 2024 10:08:34 +0100 Subject: [PATCH 3/5] chore: fix missing freestanding simp --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index cec0c272733f..958ab02dc843 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1507,7 +1507,7 @@ theorem getElem_append {x : BitVec n} {y : BitVec m} (h : i < n + m) : @[simp] theorem getMsbD_append {x : BitVec n} {y : BitVec m} : getMsbD (x ++ y) i = bif n ≤ i then getMsbD y (i - n) else getMsbD x i := by - simp [append_def] + simp only [append_def] by_cases h : n ≤ i · simp [h] · simp [h] From 57a78993824fe02b4b7f6ede1e155200e6fb1331 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 28 Sep 2024 10:35:52 +0100 Subject: [PATCH 4/5] more missed simps --- src/Init/Data/BitVec/Lemmas.lean | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 958ab02dc843..15be3e365aba 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -165,7 +165,8 @@ theorem getMsbD_eq_getMsb?_getD (x : BitVec w) (i : Nat) : · simp [getMsb?, h] · rw [getLsbD_eq_getElem?_getD, getMsb?_eq_getLsb?] split <;> - · simp + · simp only [getLsb?_eq_getElem?, Bool.and_iff_right_iff_imp, decide_eq_true_eq, + Option.getD_none, Bool.and_eq_false_imp] intros omega @@ -1041,7 +1042,8 @@ theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) : simp only [t] simp only [decide_True, Nat.sub_sub, Bool.true_and, Nat.add_assoc] by_cases h₁ : k < w <;> by_cases h₂ : w - (1 + k) < i <;> by_cases h₃ : k + i < w - <;> simp [h₁, h₂, h₃] + <;> simp only [h₁, h₂, h₃, decide_False, h₂, decide_True, Bool.not_true, Bool.false_and, Bool.and_self, + Bool.true_and, Bool.false_eq, Bool.false_and, Bool.not_false] <;> (first | apply getLsbD_ge | apply Eq.symm; apply getLsbD_ge) <;> omega @@ -1667,13 +1669,13 @@ theorem toNat_cons' {x : BitVec w} : theorem getLsbD_cons (b : Bool) {n} (x : BitVec n) (i : Nat) : getLsbD (cons b x) i = if i = n then b else getLsbD x i := by - simp only [getLsbD, toNat_cons, Nat.testBit_or] - rw [Nat.testBit_shiftLeft] + simp only [getLsbD, toNat_cons, Nat.testBit_or, Nat.testBit_shiftLeft, ge_iff_le] rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i · have p1 : ¬(n ≤ i) := by omega have p2 : i ≠ n := by omega simp [p1, p2] - · simp [i_eq_n, testBit_toNat] + · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_True, Nat.sub_self, Nat.testBit_zero, + Bool.true_and, testBit_toNat, getLsbD_ge, Bool.or_false, ↓reduceIte] cases b <;> trivial · have p1 : i ≠ n := by omega have p2 : i - n ≠ 0 := by omega @@ -1687,7 +1689,8 @@ theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) : · have p1 : ¬(n ≤ i) := by omega have p2 : i ≠ n := by omega simp [p1, p2] - · simp [i_eq_n, testBit_toNat] + · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_True, Nat.sub_self, Nat.testBit_zero, + Bool.true_and, testBit_toNat, getLsbD_ge, Bool.or_false, ↓reduceIte] cases b <;> trivial · have p1 : i ≠ n := by omega have p2 : i - n ≠ 0 := by omega @@ -1966,7 +1969,7 @@ theorem toInt_neg {x : BitVec w} : theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by apply eq_of_toNat_eq - simp + simp only [toNat_sub, toNat_add, toNat_neg, Nat.add_mod_mod] rw [Nat.add_comm] @[simp] theorem neg_zero (n:Nat) : -BitVec.ofNat n 0 = BitVec.ofNat n 0 := by apply eq_of_toNat_eq ; simp From 255c31824359e85640c0866a6c289e1ef6383552 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 28 Sep 2024 11:00:36 +0100 Subject: [PATCH 5/5] chore: two more --- src/Init/Data/BitVec/Lemmas.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 15be3e365aba..c9f479ffda6a 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1498,14 +1498,14 @@ theorem getLsbD_append {x : BitVec n} {y : BitVec m} : simp only [append_def, getLsbD_or, getLsbD_shiftLeftZeroExtend, getLsbD_setWidth'] by_cases h : i < m · simp [h] - · simp [h]; simp_all + · simp_all [h] theorem getElem_append {x : BitVec n} {y : BitVec m} (h : i < n + m) : (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 [h']; simp_all + · simp_all [h'] @[simp] theorem getMsbD_append {x : BitVec n} {y : BitVec m} : getMsbD (x ++ y) i = bif n ≤ i then getMsbD y (i - n) else getMsbD x i := by