From 910b20fb2ccb9e0316db7c7b5ea95324379276f8 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 6 Nov 2024 16:12:25 +1100 Subject: [PATCH] chore: consolidate `decide_True` and `decide_true_eq_true` (#5949) --- src/Init/Core.lean | 9 +- src/Init/Data/BitVec/Bitblast.lean | 20 ++-- src/Init/Data/BitVec/Lemmas.lean | 99 ++++++++++--------- src/Init/Data/Nat/Bitwise/Lemmas.lean | 2 +- src/Init/SimpLemmas.lean | 8 +- .../Bitblast/BVExpr/Circuit/Lemmas/Expr.lean | 12 +-- .../BVExpr/Circuit/Lemmas/Operations/Neg.lean | 2 +- .../Circuit/Lemmas/Operations/ShiftLeft.lean | 2 +- .../BVExpr/Circuit/Lemmas/Operations/Ult.lean | 2 +- .../LRAT/Internal/Formula/RatAddSound.lean | 2 +- .../LRAT/Internal/Formula/RupAddSound.lean | 18 ++-- 11 files changed, 92 insertions(+), 84 deletions(-) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 46b3644d19..e424a131be 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -861,16 +861,21 @@ theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop} /-! # Decidable -/ -theorem decide_true_eq_true (h : Decidable True) : @decide True h = true := +@[simp] theorem decide_true (h : Decidable True) : @decide True h = true := match h with | isTrue _ => rfl | isFalse h => False.elim <| h ⟨⟩ -theorem decide_false_eq_false (h : Decidable False) : @decide False h = false := +@[simp] theorem decide_false (h : Decidable False) : @decide False h = false := match h with | isFalse _ => rfl | isTrue h => False.elim h +set_option linter.missingDocs false in +@[deprecated decide_true (since := "2024-11-05")] abbrev decide_true_eq_true := decide_true +set_option linter.missingDocs false in +@[deprecated decide_false (since := "2024-11-05")] abbrev decide_false_eq_false := decide_false + /-- Similar to `decide`, but uses an explicit instance -/ @[inline] def toBoolUsing {p : Prop} (d : Decidable p) : Bool := decide (h := d) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 174a5832a8..67227cae1b 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -180,7 +180,7 @@ theorem carry_succ_one (i : Nat) (x : BitVec w) (h : 0 < w) : | zero => simp [carry_succ, h] | succ i ih => rw [carry_succ, ih] - simp only [getLsbD_one, add_one_ne_zero, decide_False, Bool.and_false, atLeastTwo_false_mid] + simp only [getLsbD_one, add_one_ne_zero, decide_false, Bool.and_false, atLeastTwo_false_mid] cases hx : x.getLsbD (i+1) case false => have : ∃ j ≤ i + 1, x.getLsbD j = false := @@ -249,7 +249,7 @@ theorem getLsbD_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool [ Nat.testBit_mod_two_pow, Nat.testBit_mul_two_pow_add_eq, i_lt, - decide_True, + decide_true, Bool.true_and, Nat.add_assoc, Nat.add_left_comm (_%_) (_ * _) _, @@ -392,7 +392,7 @@ theorem getLsbD_neg {i : Nat} {x : BitVec w} : by_cases hi : i < w · rw [getLsbD_add hi] have : 0 < w := by omega - simp only [getLsbD_not, hi, decide_True, Bool.true_and, getLsbD_one, this, not_bne, + simp only [getLsbD_not, hi, decide_true, Bool.true_and, getLsbD_one, this, not_bne, _root_.true_and, not_eq_eq_eq_not] cases i with | zero => @@ -401,7 +401,7 @@ theorem getLsbD_neg {i : Nat} {x : BitVec w} : simp [hi, carry_zero] | succ => rw [carry_succ_one _ _ (by omega), ← Bool.xor_not, ← decide_not] - simp only [add_one_ne_zero, decide_False, getLsbD_not, and_eq_true, decide_eq_true_eq, + simp only [add_one_ne_zero, decide_false, getLsbD_not, and_eq_true, decide_eq_true_eq, not_eq_eq_eq_not, Bool.not_true, false_bne, not_exists, _root_.not_and, not_eq_true, bne_left_inj, decide_eq_decide] constructor @@ -419,7 +419,7 @@ theorem getMsbD_neg {i : Nat} {x : BitVec w} : simp [hi]; omega case pos => have h₁ : w - 1 - i < w := by omega - simp only [hi, decide_True, h₁, Bool.true_and, Bool.bne_left_inj, decide_eq_decide] + simp only [hi, decide_true, h₁, Bool.true_and, Bool.bne_left_inj, decide_eq_decide] constructor · rintro ⟨j, hj, h⟩ refine ⟨w - 1 - j, by omega, by omega, by omega, _root_.cast ?_ h⟩ @@ -455,7 +455,7 @@ theorem msb_neg {w : Nat} {x : BitVec w} : apply hmin apply eq_of_getMsbD_eq rintro ⟨i, hi⟩ - simp only [getMsbD_intMin, w_pos, decide_True, Bool.true_and] + simp only [getMsbD_intMin, w_pos, decide_true, Bool.true_and] cases i case zero => exact hmsb case succ => exact getMsbD_x _ hi (by omega) @@ -476,7 +476,7 @@ theorem msb_abs {w : Nat} {x : BitVec w} : by_cases h₀ : 0 < w · by_cases h₁ : x = intMin w · simp [h₁, msb_intMin] - · simp only [neg_eq, h₁, decide_False] + · simp only [neg_eq, h₁, decide_false] by_cases h₂ : x.msb · simp [h₂, msb_neg] and_intros @@ -566,18 +566,18 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow (x : BitVec w) (i setWidth w (x.setWidth i) + (x &&& twoPow w i) := by rw [add_eq_or_of_and_eq_zero] · ext k - simp only [getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and] + simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or, getLsbD_and] by_cases hik : i = k · subst hik simp - · simp only [getLsbD_twoPow, hik, decide_False, Bool.and_false, Bool.or_false] + · 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 simp [hik', hik''] · have hik'' : ¬ (k < i) := by omega simp [hik', hik''] · ext k - simp only [and_twoPow, getLsbD_and, getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and, + simp only [and_twoPow, getLsbD_and, getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and, getLsbD_zero, and_eq_false_imp, and_eq_true, decide_eq_true_eq, and_imp] by_cases hi : x.getLsbD i <;> simp [hi] <;> omega diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index eeb62f76c4..2e358c75e6 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -123,7 +123,7 @@ theorem getMsbD_eq_getLsbD (x : BitVec w) (i : Nat) : x.getMsbD i = (decide (i < theorem getLsbD_eq_getMsbD (x : BitVec w) (i : Nat) : x.getLsbD i = (decide (i < w) && x.getMsbD (w - 1 - i)) := by rw [getMsbD] by_cases h₁ : i < w <;> by_cases h₂ : w - 1 - i < w <;> - simp only [h₁, h₂] <;> simp only [decide_True, decide_False, Bool.false_and, Bool.and_false, Bool.true_and, Bool.and_true] + simp only [h₁, h₂] <;> simp only [decide_true, decide_false, Bool.false_and, Bool.and_false, Bool.true_and, Bool.and_true] · congr omega all_goals @@ -386,7 +386,7 @@ theorem msb_eq_getLsbD_last (x : BitVec w) : · simp [Nat.div_eq_of_lt h, h] · simp only [h] rw [Nat.div_eq_sub_div (Nat.two_pow_pos w) h, Nat.div_eq_of_lt] - · decide + · simp · omega @[bv_toNat] theorem getLsbD_succ_last (x : BitVec (w + 1)) : @@ -633,7 +633,7 @@ theorem getElem?_setWidth (m : Nat) (x : BitVec n) (i : Nat) : @[simp] theorem setWidth_setWidth_of_le (x : BitVec w) (h : k ≤ l) : (x.setWidth l).setWidth k = x.setWidth k := by ext i - simp only [getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and] + simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and] have p := lt_of_getLsbD (x := x) (i := i) revert p cases getLsbD x i <;> simp; omega @@ -663,7 +663,7 @@ theorem setWidth_one_eq_ofBool_getLsb_zero (x : BitVec w) : 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, hilt⟩ - simp only [getLsbD_setWidth, hilt, decide_True, getLsbD_ofNat, Bool.true_and, + 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₁ @@ -735,9 +735,9 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h @[simp] theorem ofFin_add_rev (x : Fin (2^n)) : ofFin (x + x.rev) = allOnes n := by ext - simp only [Fin.rev, getLsbD_ofFin, getLsbD_allOnes, Fin.is_lt, decide_True] + simp only [Fin.rev, getLsbD_ofFin, getLsbD_allOnes, Fin.is_lt, decide_true] rw [Fin.add_def] - simp only [Nat.testBit_mod_two_pow, Fin.is_lt, decide_True, Bool.true_and] + simp only [Nat.testBit_mod_two_pow, Fin.is_lt, decide_true, Bool.true_and] have h : (x : Nat) + (2 ^ n - (x + 1)) = 2 ^ n - 1 := by omega rw [h, Nat.testBit_two_pow_sub_one] simp @@ -1089,21 +1089,21 @@ 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 - simp only [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, getLsbD_xor] + 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 - simp only [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, getLsbD_and] + 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 - simp only [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or] + simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or] by_cases h : i < n <;> simp [h] @@ -1114,9 +1114,9 @@ theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) : · subst h; simp have t : w - 1 - k < w := by omega simp only [t] - simp only [decide_True, Nat.sub_sub, Bool.true_and, Nat.add_assoc] + 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 only [h₁, h₂, h₃, decide_False, h₂, decide_True, Bool.not_true, Bool.false_and, Bool.and_self, + <;> 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 @@ -1160,7 +1160,7 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} : theorem shiftLeft_add {w : Nat} (x : BitVec w) (n m : Nat) : x <<< (n + m) = (x <<< n) <<< m := by ext i - simp only [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and] + simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and] rw [show i - (n + m) = (i - m - n) by omega] cases h₂ : decide (i < m) <;> cases h₃ : decide (i - m < w) <;> @@ -1258,7 +1258,8 @@ theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} : · simp [getLsbD_ge, show w ≤ (n + (w - 1 - i)) by omega] omega · by_cases h₁ : i < w - · simp only [h, ushiftRight_eq, getLsbD_ushiftRight, show i - n < w by omega] + · simp only [h, decide_false, Bool.not_false, show i - n < w by omega, decide_true, + Bool.true_and] congr omega · simp [h, h₁] @@ -1327,17 +1328,17 @@ theorem getLsbD_sshiftRight (x : BitVec w) (s i : Nat) : rcases hmsb : x.msb with rfl | rfl · simp only [sshiftRight_eq_of_msb_false hmsb, getLsbD_ushiftRight, Bool.if_false_right] by_cases hi : i ≥ w - · simp only [hi, decide_True, Bool.not_true, Bool.false_and] + · simp only [hi, decide_true, Bool.not_true, Bool.false_and] apply getLsbD_ge omega - · simp only [hi, decide_False, Bool.not_false, Bool.true_and, Bool.iff_and_self, + · simp only [hi, decide_false, Bool.not_false, Bool.true_and, Bool.iff_and_self, decide_eq_true_eq] intros hlsb apply BitVec.lt_of_getLsbD hlsb · by_cases hi : i ≥ w · simp [hi] · simp only [sshiftRight_eq_of_msb_true hmsb, getLsbD_not, getLsbD_ushiftRight, Bool.not_and, - Bool.not_not, hi, decide_False, Bool.not_false, Bool.if_true_right, Bool.true_and, + Bool.not_not, hi, decide_false, Bool.not_false, Bool.if_true_right, Bool.true_and, Bool.and_iff_right_iff_imp, Bool.or_eq_true, Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, decide_eq_true_eq] omega @@ -1382,7 +1383,7 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} : rw [msb_eq_getLsbD_last, getLsbD_sshiftRight, msb_eq_getLsbD_last] by_cases hw₀ : w = 0 · simp [hw₀] - · simp only [show ¬(w ≤ w - 1) by omega, decide_False, Bool.not_false, Bool.true_and, + · simp only [show ¬(w ≤ w - 1) by omega, decide_false, Bool.not_false, Bool.true_and, ite_eq_right_iff] intros h simp [show n = 0 by omega] @@ -1401,7 +1402,7 @@ theorem sshiftRight_add {x : BitVec w} {m n : Nat} : simp only [getLsbD_sshiftRight, Nat.add_assoc] by_cases h₁ : w ≤ (i : Nat) · simp [h₁] - · simp only [h₁, decide_False, Bool.not_false, Bool.true_and] + · simp only [h₁, decide_false, Bool.not_false, Bool.true_and] by_cases h₂ : n + ↑i < w · simp [h₂] · simp only [h₂, ↓reduceIte] @@ -1413,7 +1414,7 @@ theorem sshiftRight_add {x : BitVec w} {m n : Nat} : theorem not_sshiftRight {b : BitVec w} : ~~~b.sshiftRight n = (~~~b).sshiftRight n := by ext i - simp only [getLsbD_not, Fin.is_lt, decide_True, getLsbD_sshiftRight, Bool.not_and, Bool.not_not, + simp only [getLsbD_not, Fin.is_lt, decide_true, getLsbD_sshiftRight, Bool.not_and, Bool.not_not, Bool.true_and, msb_not] by_cases h : w ≤ i <;> by_cases h' : n + i < w @@ -1431,15 +1432,15 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} : getMsbD (x.sshiftRight n) i = (decide (i < w) && if i < n then x.msb else getMsbD x (i - n)) := by simp only [getMsbD, BitVec.getLsbD_sshiftRight] by_cases h : i < w - · simp only [h, decide_True, Bool.true_and] + · simp only [h, decide_true, Bool.true_and] by_cases h₁ : w ≤ w - 1 - i · simp [h₁] omega - · simp only [h₁, decide_False, Bool.not_false, Bool.true_and] + · simp only [h₁, decide_false, Bool.not_false, Bool.true_and] by_cases h₂ : i < n · simp only [h₂, ↓reduceIte, ite_eq_right_iff] omega - · simp only [show i - n < w by omega, h₂, ↓reduceIte, decide_True, Bool.true_and] + · simp only [show i - n < w by omega, h₂, ↓reduceIte, decide_true, Bool.true_and] by_cases h₄ : n + (w - 1 - i) < w <;> (simp only [h₄, ↓reduceIte]; congr; omega) · simp [h] @@ -1459,15 +1460,15 @@ theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} : (x.sshiftRight y.toNat).getMsbD i = (decide (i < w) && if i < y.toNat then x.msb else x.getMsbD (i - y.toNat)) := by simp only [BitVec.sshiftRight', getMsbD, BitVec.getLsbD_sshiftRight] by_cases h : i < w - · simp only [h, decide_True, Bool.true_and] + · simp only [h, decide_true, Bool.true_and] by_cases h₁ : w ≤ w - 1 - i · simp [h₁] omega - · simp only [h₁, decide_False, Bool.not_false, Bool.true_and] + · simp only [h₁, decide_false, Bool.not_false, Bool.true_and] by_cases h₂ : i < y.toNat · simp only [h₂, ↓reduceIte, ite_eq_right_iff] omega - · simp only [show i - y.toNat < w by omega, h₂, ↓reduceIte, decide_True, Bool.true_and] + · simp only [show i - y.toNat < w by omega, h₂, ↓reduceIte, decide_true, Bool.true_and] by_cases h₄ : y.toNat + (w - 1 - i) < w <;> (simp only [h₄, ↓reduceIte]; congr; omega) · simp [h] @@ -1492,11 +1493,11 @@ theorem signExtend_eq_not_setWidth_not_of_msb_false {x : BitVec w} {v : Nat} (hm x.signExtend v = x.setWidth v := by ext i by_cases hv : i < v - · simp only [signExtend, getLsbD, getLsbD_setWidth, hv, decide_True, Bool.true_and, toNat_ofInt, + · simp only [signExtend, getLsbD, getLsbD_setWidth, hv, decide_true, Bool.true_and, toNat_ofInt, BitVec.toInt_eq_msb_cond, hmsb, ↓reduceIte, reduceCtorEq] rw [Int.ofNat_mod_ofNat, Int.toNat_ofNat, Nat.testBit_mod_two_pow] simp [BitVec.testBit_toNat] - · simp only [getLsbD_setWidth, hv, decide_False, Bool.false_and] + · simp only [getLsbD_setWidth, hv, decide_false, Bool.false_and] apply getLsbD_ge omega @@ -1538,7 +1539,7 @@ theorem getElem_signExtend {x : BitVec w} {v i : Nat} (h : i < v) : theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w): x.signExtend v = x.setWidth v := by ext i - simp only [getLsbD_signExtend, Fin.is_lt, decide_True, Bool.true_and, getLsbD_setWidth, + simp only [getLsbD_signExtend, Fin.is_lt, decide_true, Bool.true_and, getLsbD_setWidth, ite_eq_left_iff, Nat.not_lt] omega @@ -1622,7 +1623,7 @@ 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 apply eq_of_getLsbD_eq intro i - simp only [getLsbD_setWidth, Fin.is_lt, decide_True, getLsbD_append, Bool.true_and] + simp only [getLsbD_setWidth, Fin.is_lt, decide_true, getLsbD_append, Bool.true_and] split · have t : i < v := by omega simp [t] @@ -1634,7 +1635,7 @@ theorem setWidth_append {x : BitVec w} {y : BitVec v} : @[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 - simp only [getLsbD_setWidth, Fin.is_lt, decide_True, getLsbD_append, cond_eq_if, + 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 @@ -1705,13 +1706,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 only [getLsbD, Fin.val_rev, getMsbD, Fin.is_lt, decide_True, Bool.true_and] + 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 only [Fin.getElem_fin, Fin.val_rev, getMsbD, Fin.is_lt, decide_True, Bool.true_and] + simp only [Fin.getElem_fin, Fin.val_rev, getMsbD, Fin.is_lt, decide_true, Bool.true_and] congr 1 omega @@ -1741,7 +1742,7 @@ theorem getLsbD_cons (b : Bool) {n} (x : BitVec n) (i : Nat) : · have p1 : ¬(n ≤ i) := by omega have p2 : i ≠ n := by omega simp [p1, p2] - · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_True, Nat.sub_self, Nat.testBit_zero, + · 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 @@ -1756,7 +1757,7 @@ 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 only [i_eq_n, ge_iff_le, Nat.le_refl, decide_True, Nat.sub_self, Nat.testBit_zero, + · 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 @@ -1776,7 +1777,7 @@ theorem setWidth_succ (x : BitVec w) : setWidth (i+1) x = cons (getLsbD x i) (setWidth i x) := by apply eq_of_getLsbD_eq intro j - simp only [getLsbD_setWidth, getLsbD_cons, j.isLt, decide_True, Bool.true_and] + simp only [getLsbD_setWidth, getLsbD_cons, j.isLt, decide_true, Bool.true_and] if j_eq : j.val = i then simp [j_eq] else @@ -1884,7 +1885,7 @@ 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 - simp only [getLsbD_ushiftRight, getLsbD_shiftConcat, Fin.is_lt, decide_True, Bool.true_and] + simp only [getLsbD_ushiftRight, getLsbD_shiftConcat, Fin.is_lt, decide_true, Bool.true_and] split · simp [*] · congr 1; omega @@ -1925,7 +1926,7 @@ theorem getMsbD_concat {i w : Nat} {b : Bool} {x : BitVec w} : · simp [h₀] · by_cases h₁ : i < w · simp [h₀, h₁, show ¬ w - i = 0 by omega, show i < w + 1 by omega, Nat.sub_sub, Nat.add_comm] - · simp only [show w - i = 0 by omega, ↓reduceIte, h₁, h₀, decide_False, Bool.false_and, + · simp only [show w - i = 0 by omega, ↓reduceIte, h₁, h₀, decide_false, Bool.false_and, Bool.and_eq_false_imp, decide_eq_true_eq] intro omega @@ -1933,10 +1934,10 @@ theorem getMsbD_concat {i w : Nat} {b : Bool} {x : BitVec w} : @[simp] theorem msb_concat {w : Nat} {b : Bool} {x : BitVec w} : (x.concat b).msb = if 0 < w then x.msb else b := by - simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.zero_lt_succ, decide_True, Nat.add_one_sub_one, + simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.zero_lt_succ, decide_true, Nat.add_one_sub_one, Nat.sub_zero, Bool.true_and] by_cases h₀ : 0 < w - · simp only [Nat.lt_add_one, getLsbD_eq_getElem, getElem_concat, h₀, ↓reduceIte, decide_True, + · simp only [Nat.lt_add_one, getLsbD_eq_getElem, getElem_concat, h₀, ↓reduceIte, decide_true, Bool.true_and, ite_eq_right_iff] intro omega @@ -2506,7 +2507,7 @@ theorem smod_zero {x : BitVec n} : x.smod 0#n = x := by @[simp] theorem getElem_ofBoolListBE (h : i < bs.length) : (ofBoolListBE bs)[i] = bs[bs.length - 1 - i] := by rw [← getLsbD_eq_getElem, getLsbD_ofBoolListBE] - simp only [h, decide_True, List.getD_eq_getElem?_getD, Bool.true_and] + simp only [h, decide_true, List.getD_eq_getElem?_getD, Bool.true_and] rw [List.getElem?_eq_getElem (by omega)] simp @@ -2708,7 +2709,7 @@ theorem getLsbD_twoPow (i j : Nat) : (twoPow w i).getLsbD j = ((i < w) && (i = j · simp · simp only [twoPow, getLsbD_shiftLeft, getLsbD_ofNat] by_cases hj : j < i - · simp only [hj, decide_True, Bool.not_true, Bool.and_false, Bool.false_and, Bool.false_eq, + · simp only [hj, decide_true, Bool.not_true, Bool.and_false, Bool.false_and, Bool.false_eq, Bool.and_eq_false_imp, decide_eq_true_eq, decide_eq_false_iff_not] omega · by_cases hi : Nat.testBit 1 (j - i) @@ -2771,7 +2772,7 @@ theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w := by theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) : x <<< n = x * (BitVec.twoPow w n) := by ext i - simp [getLsbD_shiftLeft, Fin.is_lt, decide_True, Bool.true_and, mul_twoPow_eq_shiftLeft] + simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft] /- ### cons -/ @@ -2799,7 +2800,7 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false setWidth w (x.setWidth (i + 1)) = setWidth w (x.setWidth i) := by ext k - simp only [getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and] + 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] @@ -2815,7 +2816,7 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true setWidth w (x.setWidth (i + 1)) = setWidth w (x.setWidth i) ||| (twoPow w i) := by ext k - simp only [getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and] + 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] @@ -2825,7 +2826,7 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} : (x &&& 1#w) = setWidth w (ofBool (x.getLsbD 0)) := by ext i - simp only [getLsbD_and, getLsbD_one, getLsbD_setWidth, Fin.is_lt, decide_True, getLsbD_ofBool, + 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 @@ -2862,13 +2863,13 @@ theorem getLsbD_replicate {n w : Nat} (x : BitVec w) : case succ n ih => simp only [replicate_succ_eq, getLsbD_cast, getLsbD_append] by_cases hi : i < w * (n + 1) - · simp only [hi, decide_True, Bool.true_and] + · simp only [hi, decide_true, Bool.true_and] by_cases hi' : i < w * n · simp [hi', ih] - · simp only [hi', decide_False, cond_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] + simp only [show ¬i < w * n by omega, decide_false, cond_false, hi, Bool.false_and] apply BitVec.getLsbD_ge (x := x) (i := i - w * n) (ge := by omega) @[simp] @@ -2929,7 +2930,7 @@ theorem toInt_intMin_le (x : BitVec w) : apply Int.le_bmod (by omega) theorem intMin_sle (x : BitVec w) : (intMin w).sle x := by - simp only [BitVec.sle, toInt_intMin_le x, decide_True] + simp only [BitVec.sle, toInt_intMin_le x, decide_true] @[simp] theorem neg_intMin {w : Nat} : -intMin w = intMin w := by diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean index a34dccf187..67c8525c9b 100644 --- a/src/Init/Data/Nat/Bitwise/Lemmas.lean +++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean @@ -357,7 +357,7 @@ theorem testBit_two_pow_of_ne {n m : Nat} (hm : n ≠ m) : testBit (2 ^ n) m = f | 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 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] diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index d75a4a6bc7..3cab2e7cac 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -263,7 +263,7 @@ theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true) := by simp ⟨of_decide_eq_false, decide_eq_false⟩ @[simp] theorem decide_not [g : Decidable p] [h : Decidable (Not p)] : decide (Not p) = !(decide p) := by - cases g <;> (rename_i gp; simp [gp]; rfl) + cases g <;> (rename_i gp; simp [gp]) theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by simp @[simp] theorem heq_eq_eq (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq @@ -277,8 +277,10 @@ theorem beq_self_eq_true' [DecidableEq α] (a : α) : (a == a) = true := by simp @[simp] theorem bne_self_eq_false [BEq α] [LawfulBEq α] (a : α) : (a != a) = false := by simp [bne] theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by simp -@[simp] theorem decide_False : decide False = false := rfl -@[simp] theorem decide_True : decide True = true := rfl +set_option linter.missingDocs false in +@[deprecated decide_false (since := "2024-11-05")] abbrev decide_False := decide_false +set_option linter.missingDocs false in +@[deprecated decide_true (since := "2024-11-05")] abbrev decide_True := decide_true @[simp] theorem bne_iff_ne [BEq α] [LawfulBEq α] {a b : α} : a != b ↔ a ≠ b := by simp [bne]; rw [← beq_iff_eq (a := a) (b := b)]; simp [-beq_iff_eq] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean index 6c7d5e29f6..f36108271e 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean @@ -69,7 +69,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) : simp [go, hidx, denote_blastVar] | zeroExtend v inner ih => simp only [go, denote_blastZeroExtend, ih, dite_eq_ite, Bool.if_false_right, - eval_zeroExtend, BitVec.getLsbD_setWidth, hidx, decide_True, Bool.true_and, + eval_zeroExtend, BitVec.getLsbD_setWidth, hidx, decide_true, Bool.true_and, Bool.and_iff_right_iff_imp, decide_eq_true_eq] apply BitVec.lt_of_getLsbD | append lhs rhs lih rih => @@ -78,10 +78,10 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) : BitVec.getLsbD_append] split · next hsplit => - simp only [hsplit, decide_True, cond_true] + simp only [hsplit, decide_true, cond_true] rw [rih] · next hsplit => - simp only [hsplit, decide_False, cond_false] + 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 => @@ -97,7 +97,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) : simp only [eval_signExtend] 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, + BitVec.getLsbD_setWidth, hidx, decide_true, Bool.true_and, Bool.and_iff_right_iff_imp, decide_eq_true_eq] apply BitVec.lt_of_getLsbD · subst heq @@ -108,7 +108,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) : rw [denote_blastSignExtend] simp only [eval_signExtend] rw [BitVec.getLsbD_signExtend] - · simp only [hidx, decide_True, Bool.true_and] + · simp only [hidx, decide_true, Bool.true_and] split · rw [ih] · rw [BitVec.msb_eq_getLsbD_last] @@ -116,7 +116,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) : · dsimp only; omega | @extract w start len inner ih => simp only [go, denote_blastExtract, Bool.if_false_right, eval_extract, - BitVec.getLsbD_extractLsb', hidx, decide_True, Bool.true_and] + BitVec.getLsbD_extractLsb', hidx, decide_true, Bool.true_and] split · next hsplit => rw [ih] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean index 3fc3664410..e05ec1ac91 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean @@ -39,7 +39,7 @@ theorem denote_blastNeg (aig : AIG α) (value : BitVec w) (target : RefVec aig w rw [denote_blastAdd] · intro idx hidx rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)] - · simp only [RefVec.get_cast, Ref.gate_cast, BitVec.getLsbD_not, hidx, decide_True, + · simp only [RefVec.get_cast, Ref.gate_cast, BitVec.getLsbD_not, hidx, decide_true, Bool.true_and] rw [denote_blastNot, htarget] · simp [Ref.hgate] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean index c10d0ad71c..e7145d2efa 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean @@ -210,7 +210,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : omega · rw [hleft] simp only [BitVec.shiftLeft_eq', BitVec.toNat_twoPow, hmod, BitVec.getLsbD_shiftLeft, hidx, - decide_True, Bool.true_and, Bool.iff_and_self, Bool.not_eq_true', decide_eq_false_iff_not, + decide_true, Bool.true_and, Bool.iff_and_self, Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt] omega · next hif1 => diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean index 56e31838f5..8ea81d4847 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean @@ -42,7 +42,7 @@ theorem mkUlt_denote_eq (aig : AIG α) (lhs rhs : BitVec w) (input : BinaryRefVe · dsimp only intro idx hidx rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)] - · simp only [RefVec.get_cast, Ref.gate_cast, BitVec.getLsbD_not, hidx, decide_True, + · simp only [RefVec.get_cast, Ref.gate_cast, BitVec.getLsbD_not, hidx, decide_true, Bool.true_and] rw [BVExpr.bitblast.denote_blastNot] congr 1 diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean index 88c6392a8a..1e5dca56a1 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean @@ -306,7 +306,7 @@ theorem sat_of_insertRat {n : Nat} (f : DefaultFormula n) simp +decide only [hasAssignment, hasPosAssignment, heq] have p_entails_i := hf.2.2 i false hasNegAssignment_fi p pf simp only [(· ⊨ ·)] at p_entails_i - simp only [p_entails_i, decide_True] + simp only [p_entails_i, decide_true] · next heq => exfalso rw [heq] at h3 diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean index 16a860faee..052238e472 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean @@ -171,7 +171,7 @@ theorem sat_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : Re decide have p_entails_i := (assignmentsInvariant_of_strongAssignmentsInvariant f f_readyForRupAdd.2).2 i false hasNegAssignment_fi p pf simp only [(· ⊨ ·)] at p_entails_i - simp only [p_entails_i, decide_True] + simp only [p_entails_i, decide_true] · next heq => exfalso rw [heq] at h3 @@ -424,7 +424,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi · simp only [(· ⊨ ·), i_eq_idx, c_arr_idx_eq_false] at p_entails_c_arr_i simp only [(· ⊨ ·), Bool.not_eq_true] at p_entails_assignment specialize p_entails_assignment c_arr[idx.1].1 - simp +decide only [p_entails_c_arr_i, decide_True, heq] at p_entails_assignment + simp +decide only [p_entails_c_arr_i, decide_true, heq] at p_entails_assignment · next h => exact Or.inr h · exact Or.inr ih1 @@ -443,7 +443,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi · simp only [(· ⊨ ·), i_eq_idx, c_arr_idx_eq_false] at p_entails_c_arr_i simp only [(· ⊨ ·), Bool.not_eq_true] at p_entails_assignment specialize p_entails_assignment c_arr[idx.1].1 - simp +decide only [p_entails_c_arr_i, decide_True, heq] at p_entails_assignment + simp +decide only [p_entails_c_arr_i, decide_true, heq] at p_entails_assignment · next h => exact Or.inr h · exact Or.inr ih1 @@ -519,7 +519,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi · simp only [j_eq_idx, (· ⊨ ·), c_arr_idx_eq_false] at p_entails_c_arr_j simp only [(· ⊨ ·), Bool.not_eq_true] at hp specialize hp c_arr[idx.1].1 - simp +decide only [p_entails_c_arr_j, decide_True, heq] at hp + simp +decide only [p_entails_c_arr_j, decide_true, heq] at hp · next heq => split at h · simp at h @@ -534,7 +534,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi · simp only [j_eq_idx, (· ⊨ ·), c_arr_idx_eq_true] at p_entails_c_arr_j simp only [(· ⊨ ·), Bool.not_eq_true] at hp specialize hp c_arr[idx.1].1 - simp +decide only [p_entails_c_arr_j, decide_True, heq] at hp + simp +decide only [p_entails_c_arr_j, decide_true, heq] at hp · simp at h · simp at h · simp at h @@ -683,8 +683,8 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin Array.get_eq_getElem, l_eq_i, Array.getElem_modify_self (addAssignment b), decidableGetElem?] simp only [getElem!, i_in_bounds, dite_true, Array.get_eq_getElem, decidableGetElem?] at pacc by_cases pi : p i - · simp only [pi, decide_False] - simp only [hasAssignment, pi, decide_False, ite_false] at pacc + · simp only [pi, decide_false] + simp only [hasAssignment, pi, decide_false, ite_false] at pacc by_cases hb : b · simp only [hasAssignment, ↓reduceIte, addAssignment] simp only [hb] @@ -694,8 +694,8 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin simp only [Bool.not_eq_true] at hb simp [(· ⊨ ·), hb, Subtype.ext l_eq_i, pi] at plb · simp only [Bool.not_eq_true] at pi - simp only [pi, decide_True] - simp only [pi, decide_True] at pacc + simp only [pi, decide_true] + simp only [pi, decide_true] at pacc by_cases hb : b · simp [(· ⊨ ·), hb, Subtype.ext l_eq_i, pi] at plb · simp only [Bool.not_eq_true] at hb