From 622b24cb2e4c2a6381d729f1b621eb2f7f9c723b Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 17 Aug 2024 07:22:53 +0100 Subject: [PATCH] chore: move Nat theorems into namespace in ForLean --- SSA/Projects/InstCombine/ForLean.lean | 31 +++++++++++++++------------ 1 file changed, 17 insertions(+), 14 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 7bb736533..512894c1e 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -2,6 +2,8 @@ import Mathlib.Data.Nat.Size -- TODO: remove and get rid of shiftLeft_eq_mul_pow import SSA.Projects.InstCombine.ForMathlib import SSA.Projects.InstCombine.LLVM.Semantics +namespace Nat + lemma two_pow_pred_mul_two (h : 0 < w) : 2 ^ (w - 1) * 2 = 2 ^ w := by simp only [← pow_succ, gt_iff_lt, ne_eq, not_false_eq_true] @@ -26,14 +28,19 @@ lemma two_pow_pred_mod_two_pow (h : 0 < w): rw [Nat.mod_eq_of_lt] apply two_pow_pred_lt_two_pow h -lemma Nat.eq_one_mod_two_of_ne_zero (n : Nat) (h : n % 2 != 0) : n % 2 = 1 := by +lemma eq_one_mod_two_of_ne_zero (n : Nat) (h : n % 2 != 0) : n % 2 = 1 := by simp only [bne_iff_ne, ne_eq, mod_two_ne_zero] at h assumption -lemma Nat.sub_mod_of_lt (n x : Nat) (hxgt0 : x > 0) (hxltn : x < n) : (n - x) % n = n - x := by +lemma sub_mod_of_lt (n x : Nat) (hxgt0 : x > 0) (hxltn : x < n) : (n - x) % n = n - x := by rcases n with rfl | n <;> simp omega +@[simp] +theorem one_mod_two_pow_eq {n : Nat} (hn : n ≠ 0) : 1 % 2 ^ n = 1 := by + rw [Nat.mod_eq_of_lt (Nat.one_lt_pow hn (by decide))] + +end Nat namespace BitVec @@ -71,10 +78,6 @@ def msb_allOnes {w : Nat} (h : 0 < w) : BitVec.msb (allOnes w) = true := by decide_eq_true_eq] rw [Nat.sub_lt_iff_lt_add] <;> omega -@[simp] -theorem Nat.one_mod_two_pow_eq {n : Nat} (hn : n ≠ 0) : 1 % 2 ^ n = 1 := by - rw [Nat.mod_eq_of_lt (Nat.one_lt_pow hn (by decide))] - @[simp] lemma ofInt_ofNat (w n : Nat) : BitVec.ofInt w (no_index (OfNat.ofNat n)) = BitVec.ofNat w n := @@ -305,7 +308,7 @@ private theorem toNat_intMin (w : Nat) : simp only [intMin, toNat_ofNat] by_cases w_0 : w = 0 · simp [w_0] - · rw [two_pow_pred_mod_two_pow (by omega)] + · rw [Nat.two_pow_pred_mod_two_pow (by omega)] simp [w_0, ↓reduceIte] @[simp] @@ -342,7 +345,7 @@ private theorem ofInt_neg {w : Nat} {A : BitVec w} (rs : A ≠ intMin w) : simp only [gt_iff_lt, Nat.ofNat_pos, mul_le_mul_right, le_of_lt (isLt A)] have is_int_min' : BitVec.toNat A = 2^(w-1) := by have h : 2 ^w = (2 ^(w - 1)) * 2 := by - rw [← two_pow_pred_add_two_pow_pred (by omega)] + rw [← Nat.two_pow_pred_add_two_pow_pred (by omega)] omega omega simp [ne_eq, toNat_eq, is_int_min', toNat_intMin, w_0, ↓reduceIte, @@ -374,7 +377,7 @@ theorem sgt_zero_eq_not_neg_sgt_zero (A : BitVec w) (h_ne_intMin : A ≠ intMin simp only [ne_eq] unfold intMin simp only [toNat_eq, toNat_ofNat, Nat.zero_mod] - rw [two_pow_pred_mod_two_pow (by omega)] + rw [Nat.two_pow_pred_mod_two_pow (by omega)] have _ : 0 < 2 ^(w - 1) := by simp [Nat.pow_pos] omega @@ -387,8 +390,8 @@ theorem intMin_eq_neg_intMin (w : Nat) : have w_gt_zero : 0 < w := by omega simp only [toNat_eq, toNat_neg, toNat_intMin] simp only [w_eq_zero, ↓reduceIte] - simp only [two_pow_sub_two_pow_pred w_gt_zero] - simp only [two_pow_pred_mod_two_pow w_gt_zero] + simp only [Nat.two_pow_sub_two_pow_pred w_gt_zero] + simp only [Nat.two_pow_pred_mod_two_pow w_gt_zero] theorem sgt_same (A : BitVec w) : ¬ (A >ₛ A) := by simp [BitVec.slt] @@ -401,7 +404,7 @@ private theorem intMin_lt_zero (h : 0 < w): intMin w <ₛ 0 := by unfold Int.bmod simp only [Nat.cast_pow, Nat.cast_ofNat] norm_cast - simp only [two_pow_pred_mod_two_pow h] + simp only [Nat.two_pow_pred_mod_two_pow h] split_ifs · rename_i hh norm_cast at hh @@ -409,7 +412,7 @@ private theorem intMin_lt_zero (h : 0 < w): intMin w <ₛ 0 := by have hhh : ¬ (2 ^ (w - 1) * 2 + 1 < (2 ^ w + 1) / 2 * 2 + 1) := by rw [Nat.div_two_mul_two_add_one_of_odd] · simp only [add_lt_add_iff_right, not_lt] - rw [← two_pow_pred_add_two_pow_pred h] + rw [← Nat.two_pow_pred_add_two_pow_pred h] omega · apply Even.add_odd · apply Even.pow_of_ne_zero @@ -425,7 +428,7 @@ private theorem intMin_lt_zero (h : 0 < w): intMin w <ₛ 0 := by apply Int.sub_lt_of_sub_lt simp only [Nat.cast_pow, Nat.cast_ofNat, sub_zero] norm_cast - apply two_pow_pred_lt_two_pow + apply Nat.two_pow_pred_lt_two_pow simp [h] private theorem not_gt_eq_le (A B : BitVec w) : (¬ (A >ₛ B)) = (A ≤ₛ B) := by