From 057c0d376b02cd2162cb6cd0fb494279d674109b Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Tue, 1 Oct 2024 13:36:08 +0100 Subject: [PATCH 01/23] proof in an ugly state but it proves the thing --- SSA/Projects/InstCombine/ForLean.lean | 82 +++++++++++++++++++++++++++ 1 file changed, 82 insertions(+) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 66eaef987..c316f7721 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -543,6 +543,88 @@ theorem shiftLeft_and_distrib' {x y : BitVec w} {n m : Nat} : theorem zero_sub {x : BitVec w} : 0#w - x = - x := by simp [bv_toNat] +@[simp] +theorem potato (a b c d: Nat) : + d - a - (b - c) = d - a - b + c := + by sorry + +@[simp] theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat}: + getMsbD (x.sshiftRight n) i = (!decide (w ≤ i) && if i < n then x.msb else getMsbD x (i - n)) := by + simp only [getMsbD] + rw [BitVec.getLsbD_sshiftRight] + rcases hmsb : x.msb with rfl | rfl + · simp [hmsb] + by_cases h : i < w + · simp [h] + by_cases h1 : (w ≤ w - 1 - i) + · simp [h, h1] + omega + · simp [h, h1] + by_cases h2 : (n + (w - 1 - i) < w) + · simp [h, h1, h2] + by_cases h3 : (w ≤ i) + · simp [h, h1, h2, h3] + omega + · simp [h, h1, h2, h3] + by_cases h4 : (i < n) + · simp [h, h1, h2, h3, h4] + omega + · simp [h, h1, h2, h3, h4] + by_cases h5 : (i - n < w) + · simp [h, h1, h2, h3, h4, h5] + rw [← Nat.add_sub_assoc] + · rw [← Nat.add_sub_assoc] + · -- this is just a matter of commutation + rw [Nat.add_comm] + rw [Nat.sub_add_comm] + · rw [Nat.sub_add_comm] + · omega + · omega + · omega + · omega + · simp [h, h1, h2, h3, h4, h5] + omega + · simp [h, h1, h2] + omega + · simp_all + · simp_all + by_cases h : i < w + · simp [h] + by_cases h1 : (w ≤ w - 1 - i) + · simp [h, h1] + omega + · simp [h, h1] + by_cases h2 : (n + (w - 1 - i) < w) + · simp [h, h1, h2] + by_cases h3 : (w ≤ i) + · simp [h, h1, h2, h3] + omega + · simp [h, h1, h2, h3] + by_cases h4 : (i < n) + · simp [h, h1, h2, h3, h4] + omega + · simp [h, h1, h2, h3, h4] + by_cases h5 : (i - n < w) + · simp [h, h1, h2, h3, h4, h5] + rw [← Nat.add_sub_assoc] + · rw [← Nat.add_sub_assoc] + · -- this is just a matter of commutation + rw [Nat.add_comm] + rw [Nat.sub_add_comm] + · rw [Nat.sub_add_comm] + · omega + · omega + · omega + · omega + · simp [h, h1, h2, h3, h4, h5] + omega + · simp [h, h1, h2] + omega + · simp_all + + + + end BitVec namespace Bool From dc8be1baa537de4f76ecef77d3b8cd6efa60c9fb Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Tue, 1 Oct 2024 15:08:16 +0100 Subject: [PATCH 02/23] trying to el;iminate potato --- SSA/Projects/InstCombine/ForLean.lean | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index c316f7721..f98ceea81 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -545,8 +545,8 @@ theorem zero_sub {x : BitVec w} : 0#w - x = - x := by @[simp] theorem potato (a b c d: Nat) : - d - a - (b - c) = d - a - b + c := - by sorry + d - a - (b - c) = d - a - b + c := by + eq_refl @[simp] theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat}: getMsbD (x.sshiftRight n) i = (!decide (w ≤ i) && if i < n then x.msb else getMsbD x (i - n)) := by @@ -574,8 +574,7 @@ theorem potato (a b c d: Nat) : · simp [h, h1, h2, h3, h4, h5] rw [← Nat.add_sub_assoc] · rw [← Nat.add_sub_assoc] - · -- this is just a matter of commutation - rw [Nat.add_comm] + · rw [Nat.add_comm] rw [Nat.sub_add_comm] · rw [Nat.sub_add_comm] · omega @@ -608,8 +607,7 @@ theorem potato (a b c d: Nat) : · simp [h, h1, h2, h3, h4, h5] rw [← Nat.add_sub_assoc] · rw [← Nat.add_sub_assoc] - · -- this is just a matter of commutation - rw [Nat.add_comm] + · rw [Nat.add_comm] rw [Nat.sub_add_comm] · rw [Nat.sub_add_comm] · omega From 937b150d01cf165ebd51194aa6c207c3a2b9ce6d Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Tue, 1 Oct 2024 16:00:18 +0100 Subject: [PATCH 03/23] more thinking required --- SSA/Projects/InstCombine/ForLean.lean | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index f98ceea81..9b582cf55 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -544,9 +544,18 @@ theorem zero_sub {x : BitVec w} : 0#w - x = - x := by simp [bv_toNat] @[simp] -theorem potato (a b c d: Nat) : - d - a - (b - c) = d - a - b + c := by - eq_refl +theorem sub_sub_eq (a b c : Nat) : a - (b - (c)) = a - b + (c) := by + induction c + case zero => + simp + case succ n ih => + simp only [Nat.add_succ, Nat.sub_succ, ih] + -- rw [Nat.sub_add_eq] + -- rw [Nat.sub_add] + -- rw [← Nat.add_assoc] + -- rw [← ih] + + sorry @[simp] theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat}: getMsbD (x.sshiftRight n) i = (!decide (w ≤ i) && if i < n then x.msb else getMsbD x (i - n)) := by From b720959aed169fa164823efc8266f4f36135754a Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Tue, 1 Oct 2024 19:55:07 +0100 Subject: [PATCH 04/23] cleaned but still very ugly --- SSA/Projects/InstCombine/ForLean.lean | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 9b582cf55..674101fd8 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -545,16 +545,12 @@ theorem zero_sub {x : BitVec w} : 0#w - x = - x := by @[simp] theorem sub_sub_eq (a b c : Nat) : a - (b - (c)) = a - b + (c) := by - induction c + induction c generalizing a case zero => simp case succ n ih => - simp only [Nat.add_succ, Nat.sub_succ, ih] - -- rw [Nat.sub_add_eq] - -- rw [Nat.sub_add] - -- rw [← Nat.add_assoc] - -- rw [← ih] - + rw [Nat.add_succ, Nat.sub_succ] + simp [ih, ← Nat.add_assoc] sorry @[simp] theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat}: From 909e522b32cfffd02f1ba3e36ba2e7b675c6873c Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Tue, 1 Oct 2024 20:13:28 +0100 Subject: [PATCH 05/23] broken again --- SSA/Projects/InstCombine/ForLean.lean | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 674101fd8..cfa6b4198 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -543,16 +543,6 @@ theorem shiftLeft_and_distrib' {x y : BitVec w} {n m : Nat} : theorem zero_sub {x : BitVec w} : 0#w - x = - x := by simp [bv_toNat] -@[simp] -theorem sub_sub_eq (a b c : Nat) : a - (b - (c)) = a - b + (c) := by - induction c generalizing a - case zero => - simp - case succ n ih => - rw [Nat.add_succ, Nat.sub_succ] - simp [ih, ← Nat.add_assoc] - sorry - @[simp] theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat}: getMsbD (x.sshiftRight n) i = (!decide (w ≤ i) && if i < n then x.msb else getMsbD x (i - n)) := by simp only [getMsbD] @@ -582,6 +572,7 @@ theorem sub_sub_eq (a b c : Nat) : a - (b - (c)) = a - b + (c) := by · rw [Nat.add_comm] rw [Nat.sub_add_comm] · rw [Nat.sub_add_comm] + · sorry · omega · omega · omega @@ -614,8 +605,7 @@ theorem sub_sub_eq (a b c : Nat) : a - (b - (c)) = a - b + (c) := by · rw [← Nat.add_sub_assoc] · rw [Nat.add_comm] rw [Nat.sub_add_comm] - · rw [Nat.sub_add_comm] - · omega + · sorry · omega · omega · omega From 67533cb0c74164b9a2884492d1f47386eff98a17 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 2 Oct 2024 00:28:23 +0100 Subject: [PATCH 06/23] even more broken than before --- SSA/Projects/InstCombine/ForLean.lean | 87 ++++++++------------------- 1 file changed, 24 insertions(+), 63 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index cfa6b4198..a6060af40 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -547,73 +547,34 @@ theorem zero_sub {x : BitVec w} : 0#w - x = - x := by getMsbD (x.sshiftRight n) i = (!decide (w ≤ i) && if i < n then x.msb else getMsbD x (i - n)) := by simp only [getMsbD] rw [BitVec.getLsbD_sshiftRight] + have h : i < w + have h1 : (w ≤ w - 1 - i) + have h2 : (n + (w - 1 - i) < w) + have h3 : (w ≤ i) + have h4 : (i < n) + have h5 : (i - n < w) rcases hmsb : x.msb with rfl | rfl - · simp [hmsb] + · simp only [hmsb, Bool.if_false_right, Bool.if_false_left] by_cases h : i < w - · simp [h] - by_cases h1 : (w ≤ w - 1 - i) - · simp [h, h1] - omega - · simp [h, h1] - by_cases h2 : (n + (w - 1 - i) < w) - · simp [h, h1, h2] - by_cases h3 : (w ≤ i) - · simp [h, h1, h2, h3] - omega - · simp [h, h1, h2, h3] - by_cases h4 : (i < n) - · simp [h, h1, h2, h3, h4] - omega - · simp [h, h1, h2, h3, h4] - by_cases h5 : (i - n < w) - · simp [h, h1, h2, h3, h4, h5] - rw [← Nat.add_sub_assoc] - · rw [← Nat.add_sub_assoc] - · rw [Nat.add_comm] - rw [Nat.sub_add_comm] - · rw [Nat.sub_add_comm] - · sorry - · omega - · omega - · omega - · omega - · simp [h, h1, h2, h3, h4, h5] - omega - · simp [h, h1, h2] - omega - · simp_all - · simp_all + · simp [h, h1, h2, h3, h4, h5] + congr 1 + sorry + · omega + sorry + · simp only [hmsb, Bool.if_true_right, Bool.if_true_left] by_cases h : i < w - · simp [h] - by_cases h1 : (w ≤ w - 1 - i) - · simp [h, h1] - omega - · simp [h, h1] - by_cases h2 : (n + (w - 1 - i) < w) - · simp [h, h1, h2] - by_cases h3 : (w ≤ i) - · simp [h, h1, h2, h3] - omega - · simp [h, h1, h2, h3] - by_cases h4 : (i < n) - · simp [h, h1, h2, h3, h4] - omega - · simp [h, h1, h2, h3, h4] - by_cases h5 : (i - n < w) - · simp [h, h1, h2, h3, h4, h5] - rw [← Nat.add_sub_assoc] - · rw [← Nat.add_sub_assoc] - · rw [Nat.add_comm] - rw [Nat.sub_add_comm] - · sorry - · omega - · omega - · omega + · by_cases h1 : (w ≤ w - 1 - i) + · by_cases h2 : (n + (w - 1 - i) < w) + · by_cases h3 : (w ≤ i) + · by_cases h4 : (i < n) + · by_cases h5 : (i - n < w) · simp [h, h1, h2, h3, h4, h5] - omega - · simp [h, h1, h2] - omega - · simp_all + · omega + · omega + · omega + · omega + · sorry + · sorry From ca0af0a5d48eb607053c50933179dc24aee20653 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 2 Oct 2024 08:27:40 +0100 Subject: [PATCH 07/23] very ugly but very much working --- SSA/Projects/InstCombine/ForLean.lean | 57 +++++++++++---------------- 1 file changed, 24 insertions(+), 33 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index a6060af40..f4a8c152d 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -543,41 +543,32 @@ theorem shiftLeft_and_distrib' {x y : BitVec w} {n m : Nat} : theorem zero_sub {x : BitVec w} : 0#w - x = - x := by simp [bv_toNat] -@[simp] theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat}: - getMsbD (x.sshiftRight n) i = (!decide (w ≤ i) && if i < n then x.msb else getMsbD x (i - n)) := by +@[simp] +theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat}: + getMsbD (x.sshiftRight n) i = (decide (i < w) && if i < n then x.msb else getMsbD x (i - n)) := by simp only [getMsbD] rw [BitVec.getLsbD_sshiftRight] - have h : i < w - have h1 : (w ≤ w - 1 - i) - have h2 : (n + (w - 1 - i) < w) - have h3 : (w ≤ i) - have h4 : (i < n) - have h5 : (i - n < w) - rcases hmsb : x.msb with rfl | rfl - · simp only [hmsb, Bool.if_false_right, Bool.if_false_left] - by_cases h : i < w - · simp [h, h1, h2, h3, h4, h5] - congr 1 - sorry - · omega - sorry - · simp only [hmsb, Bool.if_true_right, Bool.if_true_left] - by_cases h : i < w - · by_cases h1 : (w ≤ w - 1 - i) - · by_cases h2 : (n + (w - 1 - i) < w) - · by_cases h3 : (w ≤ i) - · by_cases h4 : (i < n) - · by_cases h5 : (i - n < w) - · simp [h, h1, h2, h3, h4, h5] - · omega - · omega - · omega - · omega - · sorry - · sorry - - - + by_cases h : i < w + · simp [h] + by_cases h₁ : w ≤ w - 1 - i + · simp [h₁] + have h₂ : (i < n) := by omega + simp [h₂] + omega + · simp [h₁] + simp_all + by_cases h₂ : n + (w - 1 - i) < w + · simp [h₂] + have h₃ : ¬(i < n) := by omega + simp [h₃] + have h₄ : (n + (w - 1 - i)) = (w - 1 - (i - n)) := by omega + simp [h₄] + intro + omega + · simp [h₂] + have h₃ : (i < n) := by omega + simp [h₃] + · simp [h] end BitVec From 41c90ae6d83f23a1acebf820c86dad752b484719 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 2 Oct 2024 08:56:59 +0100 Subject: [PATCH 08/23] two ugly but working proofs --- SSA/Projects/InstCombine/ForLean.lean | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index f4a8c152d..bc214a7e3 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -570,6 +570,32 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat}: simp [h₃] · simp [h] +@[simp] +theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat}: + getMsbD (x.ushiftRight n) i = (decide (i < w) && if i < n then x.msb else getMsbD x (i - n)) := by + simp only [getMsbD, ushiftRight_eq] + rw [BitVec.getLsbD_ushiftRight] + rcases hmsb : x.msb with rfl | rfl + by_cases h : i < w + · simp [h] + have h₁ : (i - n < w) := by omega + simp [h₁] + by_cases h₂ : i < n + · simp [h₂] + by_cases h₃ : n = i + · simp [h₃] + simp_all + · by_cases h₄ : n > i + · simp_all + simp [BitVec.getLsbD_eq_getMsbD] + intro + omega + · simp_all + · simp [h₂] + congr + omega + · simp [h] + end BitVec namespace Bool From 56cf83ef5149e093211669ea519e3edaaf78ab79 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 2 Oct 2024 09:43:22 +0100 Subject: [PATCH 09/23] four ugly but working proofs --- SSA/Projects/InstCombine/ForLean.lean | 83 ++++++++++++++++++++------- 1 file changed, 62 insertions(+), 21 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index bc214a7e3..90fefa1e0 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -543,7 +543,6 @@ theorem shiftLeft_and_distrib' {x y : BitVec w} {n m : Nat} : theorem zero_sub {x : BitVec w} : 0#w - x = - x := by simp [bv_toNat] -@[simp] theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat}: getMsbD (x.sshiftRight n) i = (decide (i < w) && if i < n then x.msb else getMsbD x (i - n)) := by simp only [getMsbD] @@ -570,32 +569,74 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat}: simp [h₃] · simp [h] -@[simp] -theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat}: - getMsbD (x.ushiftRight n) i = (decide (i < w) && if i < n then x.msb else getMsbD x (i - n)) := by - simp only [getMsbD, ushiftRight_eq] - rw [BitVec.getLsbD_ushiftRight] +theorem getLsbD_sshiftRight' (x y: BitVec w) (i : Nat) : + getLsbD (x.sshiftRight' y) i = + (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by + simp only [BitVec.sshiftRight'] rcases hmsb : x.msb with rfl | rfl + · simp only [sshiftRight_eq_of_msb_false hmsb, getLsbD_ushiftRight, Bool.if_false_right] + by_cases hi : i ≥ w + · simp only [hi, decide_True, Bool.not_true, Bool.false_and] + apply getLsbD_ge + omega + · simp only [hi, decide_False, Bool.not_false, Bool.true_and, Bool.iff_and_self, + decide_eq_true_eq] + intros hlsb + apply BitVec.lt_of_getLsbD hlsb + · by_cases hi : i ≥ w + · simp [hi] + · simp only [sshiftRight_eq_of_msb_true hmsb, getLsbD_not, getLsbD_ushiftRight, Bool.not_and, + Bool.not_not, hi, decide_False, Bool.not_false, Bool.if_true_right, Bool.true_and, + Bool.and_iff_right_iff_imp, Bool.or_eq_true, Bool.not_eq_true', decide_eq_false_iff_not, + Nat.not_lt, decide_eq_true_eq] + omega + +theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat}: + getMsbD (x.sshiftRight' y) i = (decide (i < w) && if i < y.toNat then x.msb else getMsbD x (i - y.toNat)) := by + simp only [BitVec.sshiftRight'] + simp only [getMsbD] + rw [BitVec.getLsbD_sshiftRight] by_cases h : i < w · simp [h] - have h₁ : (i - n < w) := by omega - simp [h₁] - by_cases h₂ : i < n - · simp [h₂] - by_cases h₃ : n = i - · simp [h₃] - simp_all - · by_cases h₄ : n > i - · simp_all - simp [BitVec.getLsbD_eq_getMsbD] - intro - omega - · simp_all - · simp [h₂] - congr + by_cases h₁ : w ≤ w - 1 - i + · simp [h₁] + have h₂ : (i < y.toNat) := by omega + simp [h₂] omega + · simp [h₁] + simp_all + by_cases h₂ : y.toNat + (w - 1 - i) < w + · simp [h₂] + have h₃ : ¬(i < y.toNat) := by omega + simp [h₃] + have h₄ : (y.toNat + (w - 1 - i)) = (w - 1 - (i - y.toNat)) := by omega + simp [h₄] + intro + omega + · simp [h₂] + have h₃ : (i < y.toNat) := by omega + simp [h₃] · simp [h] +theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat}: + getMsbD (x.ushiftRight n) i = (decide (i < w) && if i < n then false else getMsbD x (i - n)) := by + simp only [getMsbD, Bool.if_false_left] + by_cases h : i < w + · simp [h] + by_cases h₁ : i < n + · simp [h₁] + rw [BitVec.getLsbD_ge] + omega + · simp [h₁] + by_cases h₂ : (i - n < w) + · simp [h₂] + congr + omega + · simp [h₂] + omega + · simp [h] + + end BitVec namespace Bool From 0fdee9e34d09c7d1de2e500ee9eef395c970addc Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 2 Oct 2024 10:21:58 +0100 Subject: [PATCH 10/23] double the theorems double the fun --- SSA/Projects/InstCombine/ForLean.lean | 36 ++++++++++++++++++++++++--- 1 file changed, 32 insertions(+), 4 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 90fefa1e0..7ffd536a6 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -543,7 +543,7 @@ theorem shiftLeft_and_distrib' {x y : BitVec w} {n m : Nat} : theorem zero_sub {x : BitVec w} : 0#w - x = - x := by simp [bv_toNat] -theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat}: +theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} : getMsbD (x.sshiftRight n) i = (decide (i < w) && if i < n then x.msb else getMsbD x (i - n)) := by simp only [getMsbD] rw [BitVec.getLsbD_sshiftRight] @@ -569,7 +569,7 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat}: simp [h₃] · simp [h] -theorem getLsbD_sshiftRight' (x y: BitVec w) (i : Nat) : +theorem getLsbD_sshiftRight' (x y: BitVec w) {i : Nat} : getLsbD (x.sshiftRight' y) i = (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by simp only [BitVec.sshiftRight'] @@ -591,7 +591,7 @@ theorem getLsbD_sshiftRight' (x y: BitVec w) (i : Nat) : Nat.not_lt, decide_eq_true_eq] omega -theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat}: +theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} : getMsbD (x.sshiftRight' y) i = (decide (i < w) && if i < y.toNat then x.msb else getMsbD x (i - y.toNat)) := by simp only [BitVec.sshiftRight'] simp only [getMsbD] @@ -618,7 +618,7 @@ theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat}: simp [h₃] · simp [h] -theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat}: +theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} : getMsbD (x.ushiftRight n) i = (decide (i < w) && if i < n then false else getMsbD x (i - n)) := by simp only [getMsbD, Bool.if_false_left] by_cases h : i < w @@ -636,6 +636,34 @@ theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat}: omega · simp [h] +theorem msb_shiftLeft {x : BitVec w} {n : Nat} : + (x <<< n).msb = x.getMsbD n := by + simp [BitVec.msb] + +theorem msb_ushiftRight {x : BitVec w} {n : Nat} : + (x.ushiftRight n).msb = if n > 0 then false else x.msb := by + induction n + case zero => + simp + case succ n ih => + simp only [gt_iff_lt, lt_add_iff_pos_left, add_pos_iff, zero_lt_one, or_true, + ↓reduceIte, ih, BitVec.msb, getMsbD_ushiftRight, Bool.and_false] + +-- this one exists already but has a different name +theorem msb_sshiftRight {x : BitVec w} {n : Nat} : + (x.sshiftRight n).msb = x.msb := by + rw [sshiftRight_msb_eq_msb] + +-- this one i got the proof from sshiftRight_msb_eq_msb +theorem msb_sshiftRight' {x y: BitVec w} : + (x.sshiftRight' y).msb = x.msb := by + rw [msb_eq_getLsbD_last, getLsbD_sshiftRight', msb_eq_getLsbD_last] + by_cases hw₀ : w = 0 + · simp [hw₀] + · simp only [show ¬(w ≤ w - 1) by omega, decide_False, Bool.not_false, Bool.true_and, + ite_eq_right_iff] + intros h + simp [show y.toNat = 0 by omega] end BitVec From 3d32458ca16c83b2263009a4d07c4cb0bb14723b Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 2 Oct 2024 10:28:14 +0100 Subject: [PATCH 11/23] updated comment --- SSA/Projects/InstCombine/ForLean.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 7ffd536a6..a7e406dae 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -654,7 +654,7 @@ theorem msb_sshiftRight {x : BitVec w} {n : Nat} : (x.sshiftRight n).msb = x.msb := by rw [sshiftRight_msb_eq_msb] --- this one i got the proof from sshiftRight_msb_eq_msb +-- this one has basically the same proof as sshiftRight_msb_eq_msb theorem msb_sshiftRight' {x y: BitVec w} : (x.sshiftRight' y).msb = x.msb := by rw [msb_eq_getLsbD_last, getLsbD_sshiftRight', msb_eq_getLsbD_last] From 4b61c78f4c18590cc9e355d56b0208601d974c42 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 2 Oct 2024 11:00:59 +0100 Subject: [PATCH 12/23] not sure this is any better but seems a bit cleaner --- SSA/Projects/InstCombine/ForLean.lean | 38 ++++++++++++++------------- 1 file changed, 20 insertions(+), 18 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index a7e406dae..3a3f83407 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -548,25 +548,27 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} : simp only [getMsbD] rw [BitVec.getLsbD_sshiftRight] by_cases h : i < w - · simp [h] - by_cases h₁ : w ≤ w - 1 - i - · simp [h₁] - have h₂ : (i < n) := by omega - simp [h₂] - omega - · simp [h₁] - simp_all - by_cases h₂ : n + (w - 1 - i) < w - · simp [h₂] - have h₃ : ¬(i < n) := by omega - simp [h₃] - have h₄ : (n + (w - 1 - i)) = (w - 1 - (i - n)) := by omega - simp [h₄] - intro + · by_cases h₁ : w ≤ w - 1 - i + · by_cases h₂ : n + (w - 1 - i) < w + · by_cases h₃ : ¬(i < n) + · have h₄ : (n + (w - 1 - i)) = (w - 1 - (i - n)) := by omega + simp [h, h₁, h₂, h₃, h₄] + intro + omega + · simp [h, h₁, h₂, h₃] + omega + · simp [h, h₁, h₂] + omega + · simp [h, h₁] + by_cases h₂ : ¬(i < n) + · simp [h, h₁, h₂] + have h₃ : n + (w - 1 - i) < w := by omega + have h₄ : i - n < w := by omega + simp [h, h₁, h₂, h₃, h₄] + congr + omega + · simp_all omega - · simp [h₂] - have h₃ : (i < n) := by omega - simp [h₃] · simp [h] theorem getLsbD_sshiftRight' (x y: BitVec w) {i : Nat} : From a767ba3ed419ee09b445a910dd7bdc3b6159f395 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 2 Oct 2024 11:05:04 +0100 Subject: [PATCH 13/23] much better sshiftright --- SSA/Projects/InstCombine/ForLean.lean | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 3a3f83407..4eff73c99 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -549,16 +549,10 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} : rw [BitVec.getLsbD_sshiftRight] by_cases h : i < w · by_cases h₁ : w ≤ w - 1 - i - · by_cases h₂ : n + (w - 1 - i) < w - · by_cases h₃ : ¬(i < n) - · have h₄ : (n + (w - 1 - i)) = (w - 1 - (i - n)) := by omega - simp [h, h₁, h₂, h₃, h₄] - intro - omega - · simp [h, h₁, h₂, h₃] - omega - · simp [h, h₁, h₂] - omega + · have h₂ : ¬(i < n) := by omega + simp [h, h₁, h₂] + intro + omega · simp [h, h₁] by_cases h₂ : ¬(i < n) · simp [h, h₁, h₂] From 76d451af0ccad7ed55a4f0ef8f7b6b36ddff718b Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 2 Oct 2024 13:31:12 +0100 Subject: [PATCH 14/23] cutee proofs --- SSA/Projects/InstCombine/ForLean.lean | 52 +++++++++++++-------------- 1 file changed, 25 insertions(+), 27 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 4eff73c99..af9325786 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -548,23 +548,25 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} : simp only [getMsbD] rw [BitVec.getLsbD_sshiftRight] by_cases h : i < w - · by_cases h₁ : w ≤ w - 1 - i + · simp [h] + by_cases h₁ : w ≤ w - 1 - i · have h₂ : ¬(i < n) := by omega - simp [h, h₁, h₂] + simp only [h, decide_True, h₁, Bool.not_true, Bool.false_and, Bool.and_false, h₂, ↓reduceIte, + Bool.true_and, Bool.false_eq, Bool.and_eq_false_imp, decide_eq_true_eq] intro omega - · simp [h, h₁] + · simp only [h, decide_True, h₁, decide_False, Bool.not_false, Bool.true_and] by_cases h₂ : ¬(i < n) - · simp [h, h₁, h₂] - have h₃ : n + (w - 1 - i) < w := by omega + · have h₃ : n + (w - 1 - i) < w := by omega have h₄ : i - n < w := by omega - simp [h, h₁, h₂, h₃, h₄] + simp only [h₃, ↓reduceIte, h₂, h₄, decide_True, Bool.true_and] congr omega · simp_all omega · simp [h] +-- this was basically copied from the analogous getLsbD_sshiftRight' theorem getLsbD_sshiftRight' (x y: BitVec w) {i : Nat} : getLsbD (x.sshiftRight' y) i = (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by @@ -595,23 +597,21 @@ theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} : by_cases h : i < w · simp [h] by_cases h₁ : w ≤ w - 1 - i - · simp [h₁] - have h₂ : (i < y.toNat) := by omega - simp [h₂] + · have h₂ : (i < y.toNat) := by omega + simp [h₁, h₂] omega · simp [h₁] simp_all by_cases h₂ : y.toNat + (w - 1 - i) < w - · simp [h₂] - have h₃ : ¬(i < y.toNat) := by omega - simp [h₃] + · have h₃ : ¬(i < y.toNat) := by omega have h₄ : (y.toNat + (w - 1 - i)) = (w - 1 - (i - y.toNat)) := by omega + simp [h₂, h₃] + -- if I put these together it stops working simp [h₄] intro omega - · simp [h₂] - have h₃ : (i < y.toNat) := by omega - simp [h₃] + · have h₃ : (i < y.toNat) := by omega + simp [h₂, h₃] · simp [h] theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} : @@ -623,13 +623,10 @@ theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} : · simp [h₁] rw [BitVec.getLsbD_ge] omega - · simp [h₁] - by_cases h₂ : (i - n < w) - · simp [h₂] - congr - omega - · simp [h₂] - omega + · have h₂ : (i - n < w) := by omega + simp [h₁, h₂] + congr + omega · simp [h] theorem msb_shiftLeft {x : BitVec w} {n : Nat} : @@ -642,15 +639,16 @@ theorem msb_ushiftRight {x : BitVec w} {n : Nat} : case zero => simp case succ n ih => + -- if i remove the only here everything breaks. why? simp only [gt_iff_lt, lt_add_iff_pos_left, add_pos_iff, zero_lt_one, or_true, ↓reduceIte, ih, BitVec.msb, getMsbD_ushiftRight, Bool.and_false] --- this one exists already but has a different name -theorem msb_sshiftRight {x : BitVec w} {n : Nat} : - (x.sshiftRight n).msb = x.msb := by - rw [sshiftRight_msb_eq_msb] +-- this one exists already under the name : sshiftRight_msb_eq_msb +-- theorem msb_sshiftRight {x : BitVec w} {n : Nat} : +-- (x.sshiftRight n).msb = x.msb := by +-- rw [sshiftRight_msb_eq_msb] --- this one has basically the same proof as sshiftRight_msb_eq_msb +-- got the proof from sshiftRight_msb_eq_msb theorem msb_sshiftRight' {x y: BitVec w} : (x.sshiftRight' y).msb = x.msb := by rw [msb_eq_getLsbD_last, getLsbD_sshiftRight', msb_eq_getLsbD_last] From c5ac552d128e8d8b0749858aaf081f35ab1bb04b Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 2 Oct 2024 13:52:01 +0100 Subject: [PATCH 15/23] commenting my confusion --- SSA/Projects/InstCombine/ForLean.lean | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index af9325786..938765899 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -553,7 +553,6 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} : · have h₂ : ¬(i < n) := by omega simp only [h, decide_True, h₁, Bool.not_true, Bool.false_and, Bool.and_false, h₂, ↓reduceIte, Bool.true_and, Bool.false_eq, Bool.and_eq_false_imp, decide_eq_true_eq] - intro omega · simp only [h, decide_True, h₁, decide_False, Bool.not_false, Bool.true_and] by_cases h₂ : ¬(i < n) @@ -600,15 +599,15 @@ theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} : · have h₂ : (i < y.toNat) := by omega simp [h₁, h₂] omega - · simp [h₁] + · -- if i only put simp_all it breaks. i am confused + simp [h₁] simp_all by_cases h₂ : y.toNat + (w - 1 - i) < w · have h₃ : ¬(i < y.toNat) := by omega have h₄ : (y.toNat + (w - 1 - i)) = (w - 1 - (i - y.toNat)) := by omega - simp [h₂, h₃] - -- if I put these together it stops working + -- if I put h₄ in the simp only it stops working. i am confused again + simp only [h, h₁, h₂, ↓reduceIte, h₃, Bool.iff_and_self, decide_eq_true_eq] simp [h₄] - intro omega · have h₃ : (i < y.toNat) := by omega simp [h₂, h₃] From 59cde64287db2f6c34c10e0ba4be765d230e4c28 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 2 Oct 2024 15:21:49 +0100 Subject: [PATCH 16/23] fixed comments --- SSA/Projects/InstCombine/ForLean.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 938765899..492cb4a48 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -599,15 +599,15 @@ theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} : · have h₂ : (i < y.toNat) := by omega simp [h₁, h₂] omega - · -- if i only put simp_all it breaks. i am confused - simp [h₁] + · simp [h₁] simp_all by_cases h₂ : y.toNat + (w - 1 - i) < w · have h₃ : ¬(i < y.toNat) := by omega have h₄ : (y.toNat + (w - 1 - i)) = (w - 1 - (i - y.toNat)) := by omega - -- if I put h₄ in the simp only it stops working. i am confused again - simp only [h, h₁, h₂, ↓reduceIte, h₃, Bool.iff_and_self, decide_eq_true_eq] - simp [h₄] + -- keep separated, otherwise Bool.iff_and_self and decide_eq_true_eq + -- conflict with h₄ and it breaks + simp only [h₂, ↓reduceIte, h₃] + simp only [h₄, Bool.iff_and_self, decide_eq_true_eq] omega · have h₃ : (i < y.toNat) := by omega simp [h₂, h₃] @@ -617,13 +617,13 @@ theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} : getMsbD (x.ushiftRight n) i = (decide (i < w) && if i < n then false else getMsbD x (i - n)) := by simp only [getMsbD, Bool.if_false_left] by_cases h : i < w - · simp [h] + · simp only [h, decide_True, ushiftRight_eq, getLsbD_ushiftRight, Bool.true_and] by_cases h₁ : i < n - · simp [h₁] + · simp only [h₁, decide_True, Bool.not_true, Bool.false_and] rw [BitVec.getLsbD_ge] omega · have h₂ : (i - n < w) := by omega - simp [h₁, h₂] + simp only [h₁, decide_False, Bool.not_false, h₂, decide_True, Bool.true_and] congr omega · simp [h] From a0ac9e1fe55d14675bb3f952262fb185a72c9218 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 2 Oct 2024 15:42:26 +0100 Subject: [PATCH 17/23] fixed non terminal simp only --- SSA/Projects/InstCombine/ForLean.lean | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 492cb4a48..8e0aa19b3 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -565,7 +565,7 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} : omega · simp [h] --- this was basically copied from the analogous getLsbD_sshiftRight' +-- basically copied from getLsbD_sshiftRight theorem getLsbD_sshiftRight' (x y: BitVec w) {i : Nat} : getLsbD (x.sshiftRight' y) i = (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by @@ -638,16 +638,11 @@ theorem msb_ushiftRight {x : BitVec w} {n : Nat} : case zero => simp case succ n ih => - -- if i remove the only here everything breaks. why? - simp only [gt_iff_lt, lt_add_iff_pos_left, add_pos_iff, zero_lt_one, or_true, - ↓reduceIte, ih, BitVec.msb, getMsbD_ushiftRight, Bool.and_false] + simp [ih, ← BitVec.ushiftRight_eq, getMsbD_ushiftRight, BitVec.msb] --- this one exists already under the name : sshiftRight_msb_eq_msb --- theorem msb_sshiftRight {x : BitVec w} {n : Nat} : --- (x.sshiftRight n).msb = x.msb := by --- rw [sshiftRight_msb_eq_msb] +-- msb_sshiftRight exists already under the name : sshiftRight_msb_eq_msb --- got the proof from sshiftRight_msb_eq_msb +-- basically copied sshiftRight_msb_eq_msb theorem msb_sshiftRight' {x y: BitVec w} : (x.sshiftRight' y).msb = x.msb := by rw [msb_eq_getLsbD_last, getLsbD_sshiftRight', msb_eq_getLsbD_last] From 9df5e6218488829b14f9dd83a7f65a3e4be306e0 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 3 Oct 2024 08:41:21 +0100 Subject: [PATCH 18/23] slowly becoming cuter --- SSA/Projects/InstCombine/ForLean.lean | 29 ++++++++++++--------------- 1 file changed, 13 insertions(+), 16 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 8e0aa19b3..f8a98ec5b 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -547,23 +547,20 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} : getMsbD (x.sshiftRight n) i = (decide (i < w) && if i < n then x.msb else getMsbD x (i - n)) := by simp only [getMsbD] rw [BitVec.getLsbD_sshiftRight] - by_cases h : i < w - · simp [h] - by_cases h₁ : w ≤ w - 1 - i - · have h₂ : ¬(i < n) := by omega - simp only [h, decide_True, h₁, Bool.not_true, Bool.false_and, Bool.and_false, h₂, ↓reduceIte, - Bool.true_and, Bool.false_eq, Bool.and_eq_false_imp, decide_eq_true_eq] + by_cases h : i < w <;> by_cases h₁ : w ≤ w - 1 - i <;> by_cases h₂ : ¬(i < n) + all_goals (simp [h, h₁, h₂]; try omega) + · have h₃ : n + (w - 1 - i) < w := by omega + have h₄ : i - n < w := by omega + simp only [h₃, ↓reduceIte, h₂, h₄, decide_True, Bool.true_and] + congr + omega + · have h₄ : i - n < w := by omega + simp only [↓reduceIte, h₂, h₄, decide_True, Bool.true_and] + by_cases h₃ : n + (w - 1 - i) < w + · simp [h₃] omega - · simp only [h, decide_True, h₁, decide_False, Bool.not_false, Bool.true_and] - by_cases h₂ : ¬(i < n) - · have h₃ : n + (w - 1 - i) < w := by omega - have h₄ : i - n < w := by omega - simp only [h₃, ↓reduceIte, h₂, h₄, decide_True, Bool.true_and] - congr - omega - · simp_all - omega - · simp [h] + · simp_all + -- basically copied from getLsbD_sshiftRight theorem getLsbD_sshiftRight' (x y: BitVec w) {i : Nat} : From 3cb67c9bce7c335bb9178f07ec24b1730ac11f19 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 3 Oct 2024 08:48:49 +0100 Subject: [PATCH 19/23] now we're talking --- SSA/Projects/InstCombine/ForLean.lean | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index f8a98ec5b..1aeb39705 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -547,19 +547,14 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} : getMsbD (x.sshiftRight n) i = (decide (i < w) && if i < n then x.msb else getMsbD x (i - n)) := by simp only [getMsbD] rw [BitVec.getLsbD_sshiftRight] - by_cases h : i < w <;> by_cases h₁ : w ≤ w - 1 - i <;> by_cases h₂ : ¬(i < n) + by_cases h : i < w <;> by_cases h₁ : w ≤ w - 1 - i <;> by_cases h₂ : ¬(i < n) <;> by_cases h₃ : n + (w - 1 - i) < w all_goals (simp [h, h₁, h₂]; try omega) - · have h₃ : n + (w - 1 - i) < w := by omega - have h₄ : i - n < w := by omega - simp only [h₃, ↓reduceIte, h₂, h₄, decide_True, Bool.true_and] + all_goals (have h₄ : i - n < w := by omega) + · simp only [h₃, ↓reduceIte, h₂, h₄, decide_True, Bool.true_and] congr omega - · have h₄ : i - n < w := by omega - simp only [↓reduceIte, h₂, h₄, decide_True, Bool.true_and] - by_cases h₃ : n + (w - 1 - i) < w - · simp [h₃] - omega - · simp_all + · simp only [↓reduceIte, h₂, h₃, decide_True, Bool.true_and] + simp_all -- basically copied from getLsbD_sshiftRight From 5abca29ae51fdd89d9a8b36e0c7d3ca2dda097f8 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 3 Oct 2024 08:52:00 +0100 Subject: [PATCH 20/23] cute check --- SSA/Projects/InstCombine/ForLean.lean | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 1aeb39705..a6b5b4788 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -547,14 +547,13 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} : getMsbD (x.sshiftRight n) i = (decide (i < w) && if i < n then x.msb else getMsbD x (i - n)) := by simp only [getMsbD] rw [BitVec.getLsbD_sshiftRight] - by_cases h : i < w <;> by_cases h₁ : w ≤ w - 1 - i <;> by_cases h₂ : ¬(i < n) <;> by_cases h₃ : n + (w - 1 - i) < w - all_goals (simp [h, h₁, h₂]; try omega) - all_goals (have h₄ : i - n < w := by omega) - · simp only [h₃, ↓reduceIte, h₂, h₄, decide_True, Bool.true_and] - congr - omega - · simp only [↓reduceIte, h₂, h₃, decide_True, Bool.true_and] - simp_all + by_cases h : i < w + <;> by_cases h₁ : w ≤ w - 1 - i + <;> by_cases h₂ : ¬(i < n) + <;> by_cases h₃ : n + (w - 1 - i) < w + <;> by_cases h₄ : i - n < w + all_goals (simp [h, h₁, h₂, h₃, h₄]; try congr; try omega) + simp_all -- basically copied from getLsbD_sshiftRight From 412f7f2074cfa34051b8725a37b8762855a97757 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 3 Oct 2024 09:01:16 +0100 Subject: [PATCH 21/23] much better --- SSA/Projects/InstCombine/ForLean.lean | 44 ++++++++------------------- 1 file changed, 13 insertions(+), 31 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index a6b5b4788..0d94903ba 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -581,43 +581,25 @@ theorem getLsbD_sshiftRight' (x y: BitVec w) {i : Nat} : theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} : getMsbD (x.sshiftRight' y) i = (decide (i < w) && if i < y.toNat then x.msb else getMsbD x (i - y.toNat)) := by - simp only [BitVec.sshiftRight'] - simp only [getMsbD] - rw [BitVec.getLsbD_sshiftRight] + simp only [BitVec.sshiftRight', getMsbD, BitVec.getLsbD_sshiftRight] by_cases h : i < w - · simp [h] - by_cases h₁ : w ≤ w - 1 - i - · have h₂ : (i < y.toNat) := by omega - simp [h₁, h₂] - omega - · simp [h₁] - simp_all - by_cases h₂ : y.toNat + (w - 1 - i) < w - · have h₃ : ¬(i < y.toNat) := by omega - have h₄ : (y.toNat + (w - 1 - i)) = (w - 1 - (i - y.toNat)) := by omega - -- keep separated, otherwise Bool.iff_and_self and decide_eq_true_eq - -- conflict with h₄ and it breaks - simp only [h₂, ↓reduceIte, h₃] - simp only [h₄, Bool.iff_and_self, decide_eq_true_eq] - omega - · have h₃ : (i < y.toNat) := by omega - simp [h₂, h₃] - · simp [h] + <;> by_cases h₁ : w ≤ w - 1 - i + <;> by_cases h₂ : i < y.toNat + <;> by_cases h₃ : y.toNat + (w - 1 - i) < w + <;> by_cases h₄ : (y.toNat + (w - 1 - i)) = (w - 1 - (i - y.toNat)) + all_goals (simp [h, h₁, h₂, h₃, h₄]; try omega) + simp_all + omega theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} : getMsbD (x.ushiftRight n) i = (decide (i < w) && if i < n then false else getMsbD x (i - n)) := by simp only [getMsbD, Bool.if_false_left] by_cases h : i < w - · simp only [h, decide_True, ushiftRight_eq, getLsbD_ushiftRight, Bool.true_and] - by_cases h₁ : i < n - · simp only [h₁, decide_True, Bool.not_true, Bool.false_and] - rw [BitVec.getLsbD_ge] - omega - · have h₂ : (i - n < w) := by omega - simp only [h₁, decide_False, Bool.not_false, h₂, decide_True, Bool.true_and] - congr - omega - · simp [h] + <;> by_cases h₁ : i < n + <;> by_cases h₂ : i - n < w + all_goals (simp [h, h₁, h₂]; try congr; try omega) + rw [BitVec.getLsbD_ge] + omega theorem msb_shiftLeft {x : BitVec w} {n : Nat} : (x <<< n).msb = x.getMsbD n := by From 1f7722d267fa05cae942e3c778cd195a75dfd978 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 3 Oct 2024 09:06:54 +0100 Subject: [PATCH 22/23] successful swanification --- SSA/Projects/InstCombine/ForLean.lean | 28 ++------------------------- 1 file changed, 2 insertions(+), 26 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 0d94903ba..84683b047 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -555,29 +555,11 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} : all_goals (simp [h, h₁, h₂, h₃, h₄]; try congr; try omega) simp_all - -- basically copied from getLsbD_sshiftRight theorem getLsbD_sshiftRight' (x y: BitVec w) {i : Nat} : getLsbD (x.sshiftRight' y) i = (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by - simp only [BitVec.sshiftRight'] - rcases hmsb : x.msb with rfl | rfl - · simp only [sshiftRight_eq_of_msb_false hmsb, getLsbD_ushiftRight, Bool.if_false_right] - by_cases hi : i ≥ w - · simp only [hi, decide_True, Bool.not_true, Bool.false_and] - apply getLsbD_ge - omega - · simp only [hi, decide_False, Bool.not_false, Bool.true_and, Bool.iff_and_self, - decide_eq_true_eq] - intros hlsb - apply BitVec.lt_of_getLsbD hlsb - · by_cases hi : i ≥ w - · simp [hi] - · simp only [sshiftRight_eq_of_msb_true hmsb, getLsbD_not, getLsbD_ushiftRight, Bool.not_and, - Bool.not_not, hi, decide_False, Bool.not_false, Bool.if_true_right, Bool.true_and, - Bool.and_iff_right_iff_imp, Bool.or_eq_true, Bool.not_eq_true', decide_eq_false_iff_not, - Nat.not_lt, decide_eq_true_eq] - omega + simp only [BitVec.sshiftRight', BitVec.getLsbD_sshiftRight] theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} : getMsbD (x.sshiftRight' y) i = (decide (i < w) && if i < y.toNat then x.msb else getMsbD x (i - y.toNat)) := by @@ -618,13 +600,7 @@ theorem msb_ushiftRight {x : BitVec w} {n : Nat} : -- basically copied sshiftRight_msb_eq_msb theorem msb_sshiftRight' {x y: BitVec w} : (x.sshiftRight' y).msb = x.msb := by - rw [msb_eq_getLsbD_last, getLsbD_sshiftRight', msb_eq_getLsbD_last] - by_cases hw₀ : w = 0 - · simp [hw₀] - · simp only [show ¬(w ≤ w - 1) by omega, decide_False, Bool.not_false, Bool.true_and, - ite_eq_right_iff] - intros h - simp [show y.toNat = 0 by omega] + simp [BitVec.sshiftRight', BitVec.sshiftRight_msb_eq_msb] end BitVec From 8c1e5be70da805282b931350852f92afc6acdf54 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 3 Oct 2024 09:07:42 +0100 Subject: [PATCH 23/23] removed comments --- SSA/Projects/InstCombine/ForLean.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 84683b047..887dc40a7 100644 --- a/SSA/Projects/InstCombine/ForLean.lean +++ b/SSA/Projects/InstCombine/ForLean.lean @@ -555,7 +555,6 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} : all_goals (simp [h, h₁, h₂, h₃, h₄]; try congr; try omega) simp_all --- basically copied from getLsbD_sshiftRight theorem getLsbD_sshiftRight' (x y: BitVec w) {i : Nat} : getLsbD (x.sshiftRight' y) i = (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by @@ -597,7 +596,6 @@ theorem msb_ushiftRight {x : BitVec w} {n : Nat} : -- msb_sshiftRight exists already under the name : sshiftRight_msb_eq_msb --- basically copied sshiftRight_msb_eq_msb theorem msb_sshiftRight' {x y: BitVec w} : (x.sshiftRight' y).msb = x.msb := by simp [BitVec.sshiftRight', BitVec.sshiftRight_msb_eq_msb]