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: drop unused theorems #712

Merged
merged 6 commits into from
Oct 23, 2024
Merged

chore: drop unused theorems #712

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
f7857fd
chore: drop unused theorems
tobiasgrosser Oct 17, 2024
c9d2991
fix
tobiasgrosser Oct 23, 2024
d8ae3d1
Drop more unused theorems
tobiasgrosser Oct 23, 2024
ce262c0
drop another one
tobiasgrosser Oct 23, 2024
eb0270d
remove one more
tobiasgrosser Oct 23, 2024
0865742
drop another one
tobiasgrosser Oct 23, 2024
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
2 changes: 1 addition & 1 deletion SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@ def alive_simplifyMulDivRem805 (w : Nat) :
case zero =>
simp only [Nat.zero_eq, toNat_add, toNat_ofNat, Nat.reduceSucc, pow_one,
Nat.mod_succ, Nat.reduceMod, Nat.lt_one_iff]
have hxcases := BitVec.width_one_cases x
have hxcases := eq_zero_or_eq_one x
have hxone : x = 1 := by
cases hxcases
case inl => contradiction
Expand Down
42 changes: 1 addition & 41 deletions SSA/Projects/InstCombine/ForLean.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,10 +82,6 @@ theorem add_odd_iff_neq (n m : Nat) :
<;> cases' Nat.mod_two_eq_zero_or_one m with mparity mparity
<;> simp [mparity, nparity, Nat.add_mod]

theorem mod_eq_of_eq {a b c : Nat} (h : a = b) : a % c = b % c := by
subst h
simp

end Nat

namespace BitVec
Expand Down Expand Up @@ -126,9 +122,6 @@ lemma one_shiftLeft_mul_eq_shiftLeft {A B : BitVec w} :
simp only [bv_toNat, Nat.mod_mul_mod, one_mul]
rw [Nat.mul_comm]

@[simp]
lemma msb_one_of_width_one : BitVec.msb 1#1 = true := rfl

def msb_allOnes {w : Nat} (h : 0 < w) : BitVec.msb (allOnes w) = true := by
simp only [BitVec.msb, getMsbD, allOnes]
simp only [getLsbD_ofNatLt, Nat.testBit_two_pow_sub_one, Bool.and_eq_true,
Expand Down Expand Up @@ -170,16 +163,6 @@ def sdiv_one_allOnes {w : Nat} (h : 1 < w) :
have : ¬ (w = 1) := by omega
simp [this]

theorem width_one_cases (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
obtain ⟨a, ha⟩ := a
simp only [pow_one] at ha
have acases : a = 0 ∨ a = 1 := by omega
rcases acases with ⟨rfl | rfl⟩
· simp
case inr h =>
subst h
simp

theorem sub_eq_add_neg {w : Nat} {x y : BitVec w} : x - y = x + (- y) := by
simp only [HAdd.hAdd, HSub.hSub, Neg.neg, Sub.sub, BitVec.sub, Add.add, BitVec.add]
simp [BitVec.ofNat, Fin.ofNat', add_comm]
Expand Down Expand Up @@ -219,8 +202,7 @@ def one_sdiv { w : Nat} {a : BitVec w} (ha0 : a ≠ 0) (ha1 : a ≠ 1)
case succ w' =>
cases w'
case zero =>
have ha' : a = 0#1 ∨ a = 1#1 := BitVec.width_one_cases a
rcases ha' with ⟨rfl | rfl⟩ <;> (simp only [Nat.reduceAdd, ofNat_eq_ofNat, ne_eq,
rcases eq_zero_or_eq_one a with ⟨rfl | rfl⟩ <;> (simp only [Nat.reduceAdd, ofNat_eq_ofNat, ne_eq,
not_true_eq_false] at ha0)
case inr h => subst h; contradiction
case succ w' =>
Expand Down Expand Up @@ -287,12 +269,6 @@ theorem intMin_neq_one {w : Nat} (h : w > 1): BitVec.intMin w ≠ 1 := by
rw [← Nat.two_pow_pred_add_two_pow_pred (by omega)]
omega

theorem width_one_cases' (x : BitVec 1) :
x = 0 ∨ x = 1 := by
obtain ⟨x, hx⟩ := x
simp [BitVec.toNat_eq]
omega

/- Not a simp lemma by default because we may want toFin or toInt in the future. -/
theorem ult_toNat (x y : BitVec n) :
(BitVec.ult (n := n) x y) = decide (x.toNat < y.toNat) := by
Expand Down Expand Up @@ -370,22 +346,6 @@ theorem intMin_not_gt_zero : ¬ (intMin w >ₛ (0#w)):= by
apply intMin_lt_zero
omega

theorem zero_sub_eq_neg {w : Nat} { A : BitVec w}: BitVec.ofInt w 0 - A = -A:= by
simp

-- Any bitvec of width 0 is equal to the zero bitvector
theorem width_zero_eq_zero (x : BitVec 0) : x = BitVec.ofNat 0 0 :=
Subsingleton.allEq ..

@[simp]
theorem toInt_width_zero (x : BitVec 0) : BitVec.toInt x = 0 := by
rw [BitVec.width_zero_eq_zero x]
simp

@[simp]
theorem neg_of_ofNat_0_minus_self (x : BitVec w) : (BitVec.ofNat w 0) - x = -x := by
simp

@[simp]
lemma carry_and_xor_false : carry i (a &&& b) (a ^^^ b) false = false := by
induction i
Expand Down
Loading