From f7857fd3772ef21f286921a99c4d102aa527a479 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Thu, 17 Oct 2024 20:55:04 +0100 Subject: [PATCH 1/6] chore: drop unused theorems --- SSA/Projects/InstCombine/ForLean.lean | 19 +------------------ 1 file changed, 1 insertion(+), 18 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index dfe33e624..937de30be 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -170,16 +170,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] @@ -219,8 +209,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' => @@ -287,12 +276,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 From c9d29917bf3e0f0bcea60f62a7d870c6858b0883 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Wed, 23 Oct 2024 08:39:44 -0700 Subject: [PATCH 2/6] fix --- SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean index 64e510da2..cbe6bd3d0 100644 --- a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean +++ b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean @@ -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 From d8ae3d1b46e60a0c6c7fd6c9f025df3de181e434 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Wed, 23 Oct 2024 08:48:22 -0700 Subject: [PATCH 3/6] Drop more unused theorems --- SSA/Projects/InstCombine/ForLean.lean | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 937de30be..b5da71851 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -353,18 +353,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 From ce262c0121daea951e6345d8cd1503adb9b664cd Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Wed, 23 Oct 2024 08:49:59 -0700 Subject: [PATCH 4/6] drop another one --- SSA/Projects/InstCombine/ForLean.lean | 4 ---- 1 file changed, 4 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index b5da71851..11f62121f 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -353,10 +353,6 @@ theorem intMin_not_gt_zero : ¬ (intMin w >ₛ (0#w)):= by apply intMin_lt_zero omega -@[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 From eb0270de99613e52f816cfb53dfeda630c2ff9e1 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Wed, 23 Oct 2024 08:51:38 -0700 Subject: [PATCH 5/6] remove one more --- SSA/Projects/InstCombine/ForLean.lean | 4 ---- 1 file changed, 4 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 11f62121f..61580d25c 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -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 From 08657425a75ddd7b4406565ebdbb4403aed09fe4 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Wed, 23 Oct 2024 08:52:41 -0700 Subject: [PATCH 6/6] drop another one --- SSA/Projects/InstCombine/ForLean.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 61580d25c..b1c8e9779 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -122,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,