chore: consolidate decide_True and decide_true_eq_true (#5949)

leanprover · Nov 6, 2024 · 910b20f · 910b20f
1 parent 4df71ed
commit 910b20f
Show file tree

Hide file tree

Showing 11 changed files with 92 additions and 84 deletions.
diff --git 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
@@ -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