Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

chore: move Nat theorems into namespace in ForLean #543

Merged
merged 1 commit into from
Aug 17, 2024
Merged

chore: move Nat theorems into namespace in ForLean #543

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 17 additions & 14 deletions SSA/Projects/InstCombine/ForLean.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand All @@ -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

Expand Down Expand Up @@ -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 :=
Expand Down Expand Up @@ -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]
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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
Expand All @@ -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]
Expand All @@ -401,15 +404,15 @@ 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
have h_if_nat : ¬ (2 ^ (w - 1) < (2 ^ w + 1) / 2) := 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
Expand All @@ -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
Expand Down
Loading