From cab7583a0f72f447e005a372a814a51b025584a4 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Mon, 13 May 2024 10:16:10 +0100 Subject: [PATCH 01/15] wip: shifting lemmas --- src/Init/Data/BitVec/Lemmas.lean | 147 +++++++++++++++++++++++++++++-- 1 file changed, 142 insertions(+), 5 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 13f4bf8a8a95..e213915e8d8a 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -140,6 +140,7 @@ theorem ofBool_eq_iff_eq : ∀(b b' : Bool), BitVec.ofBool b = BitVec.ofBool b' @[simp, bv_toNat] theorem toNat_ofNat (x w : Nat) : (x#w).toNat = x % 2^w := by simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat'] + -- Remark: we don't use `[simp]` here because simproc` subsumes it for literals. -- If `x` and `n` are not literals, applying this theorem eagerly may not be a good idea. theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) : @@ -260,11 +261,54 @@ theorem toInt_ofNat {n : Nat} (x : Nat) : (BitVec.ofNat n x).toInt = (x : Int).bmod (2^n) := by simp [toInt_eq_toNat_bmod] -@[simp] theorem toInt_ofInt {n : Nat} (i : Int) : - (BitVec.ofInt n i).toInt = i.bmod (2^n) := by - have _ := Nat.two_pow_pos n - have p : 0 ≤ i % (2^n : Nat) := by omega - simp [toInt_eq_toNat_bmod, Int.toNat_of_nonneg p] +/-- 'BitVec.ofInt' only cares about values upto `emod`. -/ +@[simp] theorem ofInt_eq_ofInt_emod {n : Nat} (i : Int) : + (BitVec.ofInt n i) = BitVec.ofInt n (i % (2^n)) := by + apply BitVec.eq_of_toNat_eq + simp only [toNat_ofInt] + congr 1 + have h2n : (2 : Int)^n = (((2 : Nat)^(n : Nat) : Nat) : Int) := by + rw [Int.natCast_pow] + rfl + rw [h2n, Int.emod_emod] + +-- /- A variant of emod that knows that the output is a natural number. -/ +-- abbrev Int.emod' (i : Int) (n : Nat) : Nat := +-- (Int.emod i n).toNat + +/-- Write ofInt in terms of `ofNat` +of the canonical natural number between 0 and 2^n.-/ +@[simp] theorem ofInt_eq_ofNat_emod {n : Nat} (i : Int) : + (BitVec.ofInt n i) = BitVec.ofNat n (i % (2^n)).toNat := by + have h2n : (2 : Int)^n = (((2 : Nat)^(n : Nat) : Nat) : Int) := by + rw [Int.natCast_pow] + rfl + apply BitVec.eq_of_toNat_eq + simp + conv => lhs; simp [(· % ·), Mod.mod] + rw [Nat.mod_eq_of_lt] + rw [h2n] + congr 1 + · apply Int.emod_emod + · have hlt : (i % 2^n) < 2^n := by + apply Int.emod_lt_of_pos + rw [h2n] + norm_cast + apply Nat.pow_pos + decide + rw [Int.toNat_lt] + · rw [h2n] + apply Int.emod_lt_of_pos + rw [Int.natCast_pow] + /- (0 : Int) < ↑2 ^ n -/ + clear hlt h2n + apply Lean.Omega.Int.pos_pow_of_pos + decide + · apply Int.emod_nonneg + /- (2 : Int) ^ n ≠ (0 : Int) -/ + apply Int.ne_of_gt + apply Lean.Omega.Int.pos_pow_of_pos + decide /-! ### zeroExtend and truncate -/ @@ -628,6 +672,99 @@ theorem BitVec.shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) : getLsb (x >>> i) j = getLsb x (i+j) := by unfold getLsb ; simp +/-! ### sshiftRight-/ + +theorem sshiftRight_eq {x : BitVec n} {i : Nat} : + x.sshiftRight i = BitVec.ofInt n (x.toInt >>> i) := by + apply BitVec.eq_of_toInt_eq + simp [BitVec.sshiftRight] + + +theorem BitVec.toInt_eq_toNat_of_toInt_pos {x : BitVec n} (hx: x.toInt ≥ 0) : + x.toInt = ↑ (x.toNat) := by + rw [toInt_eq_toNat_cond] + simp + intros hx' + simp [BitVec.toInt] at hx + split at hx <;> omega + + +@[simp] theorem sshiftRight_eq_ushiftRight_of_pos {x : BitVec n} (hx: x.toInt ≥ 0) : + x.sshiftRight i = x.ushiftRight i := by + rw [sshiftRight_eq, BitVec.ofInt_eq_ofNat_emod] + rw [BitVec.toInt_eq_toNat_of_toInt_pos hx] + rw [ushiftRight_eq] + rw [Int.emod_eq_of_lt] + · norm_cast + sorry + · /- need norm_num-/ + sorry + · have ⟨x', hx'lt⟩ := x + simp + /- ↑x' >>> i < 2 ^ n -/ + /- need norm_num -/ + sorry +-- @[simp] theorem getLsb_sshiftRight (x : BitVec n) (s i : Nat) : +-- getLsb (x.sshiftRight s) i = if i ≥ n then false +-- else if (s + i) < n then getLsb x (s + i) +-- else getMsb x (n - 1) := by +-- simp +-- rw [sshiftRight_eq] +-- rw [ofInt_eq_ofNat_emod] +-- rw [getLsb_ofNat] +-- rw [testBit_toNat] +-- by_cases hinonneg : x.toInt ≥ 0 +-- case pos => +-- rw [Int.emod_eq_of_lt] +-- sorry +-- case neg => +-- sorry + + +/-- The MSB of a bitvector is `false` iff its integer interpretetation is greater than or equal to zero. -/ +theorem msb_eq_false_iff_toInt_geq_zero (x : BitVec w) + : x.msb = false ↔ x.toInt ≥ 0 := by + rcases w with rfl | w <;> simp + · rw [Subsingleton.elim x (0#0)] + simp + rw [BitVec.toInt_eq_toNat_cond] + constructor + · intro h + split + case inl hpos => + apply Int.ofNat_nonneg + case inr hneg => + exfalso + rw [BitVec.msb_eq_decide] at h + simp at h + omega + · intro h + rw [BitVec.msb_eq_decide] + simp + omega + +/-- The MSB of a bitvector is `true` iff its integer interpretetation is greater than or equal to zero. -/ +theorem msb_eq_true_iff_toInt_le_zero (x : BitVec w) + : x.msb = true ↔ x.toInt < 0 := by + rcases w with rfl | w <;> try simp <;> try omega + · rw [Subsingleton.elim x (0#0)] + simp + rw [BitVec.toInt_eq_toNat_cond] + constructor + · intro h + split + case inl hpos => + rw [BitVec.msb_eq_decide] at h + simp at h + omega + case inr hneg => + simp_all + omega + · intro h + rw [BitVec.msb_eq_decide] + simp + omega + /-! ### append -/ theorem append_def (x : BitVec v) (y : BitVec w) : From 2f17f0d010300b4182efc274b787bf722e1b444c Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Mon, 13 May 2024 15:18:16 +0100 Subject: [PATCH 02/15] feat: move Int bitwise lemmas into basic --- src/Init/Data/BitVec/Lemmas.lean | 75 +++++++++++++------ .../Int/{Bitwise.lean => Bitwise/Basic.lean} | 0 2 files changed, 54 insertions(+), 21 deletions(-) rename src/Init/Data/Int/{Bitwise.lean => Bitwise/Basic.lean} (100%) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index e213915e8d8a..a7242d3b3539 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -261,8 +261,14 @@ theorem toInt_ofNat {n : Nat} (x : Nat) : (BitVec.ofNat n x).toInt = (x : Int).bmod (2^n) := by simp [toInt_eq_toNat_bmod] +@[simp] theorem toInt_ofInt {n : Nat} (i : Int) : + (BitVec.ofInt n i).toInt = i.bmod (2^n) := by + have _ := Nat.two_pow_pos n + have p : 0 ≤ i % (2^n : Nat) := by omega + simp [toInt_eq_toNat_bmod, Int.toNat_of_nonneg p] + /-- 'BitVec.ofInt' only cares about values upto `emod`. -/ -@[simp] theorem ofInt_eq_ofInt_emod {n : Nat} (i : Int) : +theorem ofInt_eq_ofInt_emod {n : Nat} (i : Int) : (BitVec.ofInt n i) = BitVec.ofInt n (i % (2^n)) := by apply BitVec.eq_of_toNat_eq simp only [toNat_ofInt] @@ -278,13 +284,13 @@ theorem toInt_ofNat {n : Nat} (x : Nat) : /-- Write ofInt in terms of `ofNat` of the canonical natural number between 0 and 2^n.-/ -@[simp] theorem ofInt_eq_ofNat_emod {n : Nat} (i : Int) : +theorem ofInt_eq_ofNat_emod {n : Nat} (i : Int) : (BitVec.ofInt n i) = BitVec.ofNat n (i % (2^n)).toNat := by have h2n : (2 : Int)^n = (((2 : Nat)^(n : Nat) : Nat) : Int) := by rw [Int.natCast_pow] rfl apply BitVec.eq_of_toNat_eq - simp + simp only [ofInt_eq_ofInt_emod, Int.emod_emod, toNat_ofInt, toNat_ofNat] conv => lhs; simp [(· % ·), Mod.mod] rw [Nat.mod_eq_of_lt] rw [h2n] @@ -689,7 +695,7 @@ theorem BitVec.toInt_eq_toNat_of_toInt_pos {x : BitVec n} (hx: x.toInt ≥ 0) : split at hx <;> omega -@[simp] theorem sshiftRight_eq_ushiftRight_of_pos {x : BitVec n} (hx: x.toInt ≥ 0) : +theorem sshiftRight_eq_ushiftRight_of_pos {x : BitVec n} (hx: x.toInt ≥ 0) : x.sshiftRight i = x.ushiftRight i := by rw [sshiftRight_eq, BitVec.ofInt_eq_ofNat_emod] rw [BitVec.toInt_eq_toNat_of_toInt_pos hx] @@ -704,22 +710,6 @@ theorem BitVec.toInt_eq_toNat_of_toInt_pos {x : BitVec n} (hx: x.toInt ≥ 0) : /- ↑x' >>> i < 2 ^ n -/ /- need norm_num -/ sorry --- @[simp] theorem getLsb_sshiftRight (x : BitVec n) (s i : Nat) : --- getLsb (x.sshiftRight s) i = if i ≥ n then false --- else if (s + i) < n then getLsb x (s + i) --- else getMsb x (n - 1) := by --- simp --- rw [sshiftRight_eq] --- rw [ofInt_eq_ofNat_emod] --- rw [getLsb_ofNat] --- rw [testBit_toNat] --- by_cases hinonneg : x.toInt ≥ 0 --- case pos => --- rw [Int.emod_eq_of_lt] --- sorry --- case neg => --- sorry - /-- The MSB of a bitvector is `false` iff its integer interpretetation is greater than or equal to zero. -/ theorem msb_eq_false_iff_toInt_geq_zero (x : BitVec w) @@ -744,7 +734,7 @@ theorem msb_eq_false_iff_toInt_geq_zero (x : BitVec w) omega /-- The MSB of a bitvector is `true` iff its integer interpretetation is greater than or equal to zero. -/ -theorem msb_eq_true_iff_toInt_le_zero (x : BitVec w) +theorem msb_eq_true_iff_toInt_lt_zero (x : BitVec w) : x.msb = true ↔ x.toInt < 0 := by rcases w with rfl | w <;> try simp <;> try omega · rw [Subsingleton.elim x (0#0)] @@ -765,6 +755,49 @@ theorem msb_eq_true_iff_toInt_le_zero (x : BitVec w) simp omega +#check Int.shiftRight +theorem getLsb_sshiftRight (x : BitVec n) (s i : Nat) : + getLsb (x.sshiftRight s) i = if i ≥ n then false + else if (s + i) < n then getLsb x (s + i) + else x.msb := by + simp + by_cases hxpos : (x.toInt ≥ 0) + -- If x ≥ 0, then arithmetic = logical shift right. + case pos => + rw [sshiftRight_eq_ushiftRight_of_pos hxpos] + rw [(msb_eq_false_iff_toInt_geq_zero x).mpr hxpos] + by_cases h₁ : s + i < n; + · simp only [ushiftRight_eq, getLsb_ushiftRight, h₁, ↓reduceIte, Bool.iff_and_self, + Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_le]; omega + · simp only [ushiftRight_eq, getLsb_ushiftRight, h₁, ↓reduceIte, Bool.and_false] + apply getLsb_ge + omega + case neg => + -- if x < 0, then msb = true + rw [(msb_eq_true_iff_toInt_lt_zero x).mpr (by omega)] + simp + by_cases h₁ : n ≤ i <;> simp [h₁] + by_cases h₂ : s + i < n; + case pos => + simp [h₂] + rw [sshiftRight_eq] + -- the meat and potatoes case. + sorry + case neg => + simp [h₂] + -- n ≥ i + -- s + i > n + rw [sshiftRight_eq] + rw [BitVec.ofInt_eq_ofNat_emod] + rw [BitVec.getLsb_ofNat] + simp [h₁] + sorry + + -- rw [sshiftRight_eq] + -- rw [ofInt_eq_ofNat_emod] + -- rw [getLsb_ofNat] + + /-! ### append -/ theorem append_def (x : BitVec v) (y : BitVec w) : diff --git a/src/Init/Data/Int/Bitwise.lean b/src/Init/Data/Int/Bitwise/Basic.lean similarity index 100% rename from src/Init/Data/Int/Bitwise.lean rename to src/Init/Data/Int/Bitwise/Basic.lean From 2e95bbe5d78f8fac241eb6623ea3394c52c9b32c Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Mon, 13 May 2024 15:18:46 +0100 Subject: [PATCH 03/15] Revert "feat: move Int bitwise lemmas into basic" This reverts commit 2f17f0d010300b4182efc274b787bf722e1b444c. --- src/Init/Data/BitVec/Lemmas.lean | 75 ++++++------------- .../Int/{Bitwise/Basic.lean => Bitwise.lean} | 0 2 files changed, 21 insertions(+), 54 deletions(-) rename src/Init/Data/Int/{Bitwise/Basic.lean => Bitwise.lean} (100%) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index a7242d3b3539..e213915e8d8a 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -261,14 +261,8 @@ theorem toInt_ofNat {n : Nat} (x : Nat) : (BitVec.ofNat n x).toInt = (x : Int).bmod (2^n) := by simp [toInt_eq_toNat_bmod] -@[simp] theorem toInt_ofInt {n : Nat} (i : Int) : - (BitVec.ofInt n i).toInt = i.bmod (2^n) := by - have _ := Nat.two_pow_pos n - have p : 0 ≤ i % (2^n : Nat) := by omega - simp [toInt_eq_toNat_bmod, Int.toNat_of_nonneg p] - /-- 'BitVec.ofInt' only cares about values upto `emod`. -/ -theorem ofInt_eq_ofInt_emod {n : Nat} (i : Int) : +@[simp] theorem ofInt_eq_ofInt_emod {n : Nat} (i : Int) : (BitVec.ofInt n i) = BitVec.ofInt n (i % (2^n)) := by apply BitVec.eq_of_toNat_eq simp only [toNat_ofInt] @@ -284,13 +278,13 @@ theorem ofInt_eq_ofInt_emod {n : Nat} (i : Int) : /-- Write ofInt in terms of `ofNat` of the canonical natural number between 0 and 2^n.-/ -theorem ofInt_eq_ofNat_emod {n : Nat} (i : Int) : +@[simp] theorem ofInt_eq_ofNat_emod {n : Nat} (i : Int) : (BitVec.ofInt n i) = BitVec.ofNat n (i % (2^n)).toNat := by have h2n : (2 : Int)^n = (((2 : Nat)^(n : Nat) : Nat) : Int) := by rw [Int.natCast_pow] rfl apply BitVec.eq_of_toNat_eq - simp only [ofInt_eq_ofInt_emod, Int.emod_emod, toNat_ofInt, toNat_ofNat] + simp conv => lhs; simp [(· % ·), Mod.mod] rw [Nat.mod_eq_of_lt] rw [h2n] @@ -695,7 +689,7 @@ theorem BitVec.toInt_eq_toNat_of_toInt_pos {x : BitVec n} (hx: x.toInt ≥ 0) : split at hx <;> omega -theorem sshiftRight_eq_ushiftRight_of_pos {x : BitVec n} (hx: x.toInt ≥ 0) : +@[simp] theorem sshiftRight_eq_ushiftRight_of_pos {x : BitVec n} (hx: x.toInt ≥ 0) : x.sshiftRight i = x.ushiftRight i := by rw [sshiftRight_eq, BitVec.ofInt_eq_ofNat_emod] rw [BitVec.toInt_eq_toNat_of_toInt_pos hx] @@ -710,6 +704,22 @@ theorem sshiftRight_eq_ushiftRight_of_pos {x : BitVec n} (hx: x.toInt ≥ 0) : /- ↑x' >>> i < 2 ^ n -/ /- need norm_num -/ sorry +-- @[simp] theorem getLsb_sshiftRight (x : BitVec n) (s i : Nat) : +-- getLsb (x.sshiftRight s) i = if i ≥ n then false +-- else if (s + i) < n then getLsb x (s + i) +-- else getMsb x (n - 1) := by +-- simp +-- rw [sshiftRight_eq] +-- rw [ofInt_eq_ofNat_emod] +-- rw [getLsb_ofNat] +-- rw [testBit_toNat] +-- by_cases hinonneg : x.toInt ≥ 0 +-- case pos => +-- rw [Int.emod_eq_of_lt] +-- sorry +-- case neg => +-- sorry + /-- The MSB of a bitvector is `false` iff its integer interpretetation is greater than or equal to zero. -/ theorem msb_eq_false_iff_toInt_geq_zero (x : BitVec w) @@ -734,7 +744,7 @@ theorem msb_eq_false_iff_toInt_geq_zero (x : BitVec w) omega /-- The MSB of a bitvector is `true` iff its integer interpretetation is greater than or equal to zero. -/ -theorem msb_eq_true_iff_toInt_lt_zero (x : BitVec w) +theorem msb_eq_true_iff_toInt_le_zero (x : BitVec w) : x.msb = true ↔ x.toInt < 0 := by rcases w with rfl | w <;> try simp <;> try omega · rw [Subsingleton.elim x (0#0)] @@ -755,49 +765,6 @@ theorem msb_eq_true_iff_toInt_lt_zero (x : BitVec w) simp omega -#check Int.shiftRight -theorem getLsb_sshiftRight (x : BitVec n) (s i : Nat) : - getLsb (x.sshiftRight s) i = if i ≥ n then false - else if (s + i) < n then getLsb x (s + i) - else x.msb := by - simp - by_cases hxpos : (x.toInt ≥ 0) - -- If x ≥ 0, then arithmetic = logical shift right. - case pos => - rw [sshiftRight_eq_ushiftRight_of_pos hxpos] - rw [(msb_eq_false_iff_toInt_geq_zero x).mpr hxpos] - by_cases h₁ : s + i < n; - · simp only [ushiftRight_eq, getLsb_ushiftRight, h₁, ↓reduceIte, Bool.iff_and_self, - Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_le]; omega - · simp only [ushiftRight_eq, getLsb_ushiftRight, h₁, ↓reduceIte, Bool.and_false] - apply getLsb_ge - omega - case neg => - -- if x < 0, then msb = true - rw [(msb_eq_true_iff_toInt_lt_zero x).mpr (by omega)] - simp - by_cases h₁ : n ≤ i <;> simp [h₁] - by_cases h₂ : s + i < n; - case pos => - simp [h₂] - rw [sshiftRight_eq] - -- the meat and potatoes case. - sorry - case neg => - simp [h₂] - -- n ≥ i - -- s + i > n - rw [sshiftRight_eq] - rw [BitVec.ofInt_eq_ofNat_emod] - rw [BitVec.getLsb_ofNat] - simp [h₁] - sorry - - -- rw [sshiftRight_eq] - -- rw [ofInt_eq_ofNat_emod] - -- rw [getLsb_ofNat] - - /-! ### append -/ theorem append_def (x : BitVec v) (y : BitVec w) : diff --git a/src/Init/Data/Int/Bitwise/Basic.lean b/src/Init/Data/Int/Bitwise.lean similarity index 100% rename from src/Init/Data/Int/Bitwise/Basic.lean rename to src/Init/Data/Int/Bitwise.lean From 2fa20815263a02b2b506706791f1bf6c06248cb3 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Mon, 13 May 2024 15:19:38 +0100 Subject: [PATCH 04/15] feat: grab the biwise lemmas --- src/Init/Data/BitVec/Lemmas.lean | 75 +++++++++++++++++++++++--------- 1 file changed, 54 insertions(+), 21 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index e213915e8d8a..a7242d3b3539 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -261,8 +261,14 @@ theorem toInt_ofNat {n : Nat} (x : Nat) : (BitVec.ofNat n x).toInt = (x : Int).bmod (2^n) := by simp [toInt_eq_toNat_bmod] +@[simp] theorem toInt_ofInt {n : Nat} (i : Int) : + (BitVec.ofInt n i).toInt = i.bmod (2^n) := by + have _ := Nat.two_pow_pos n + have p : 0 ≤ i % (2^n : Nat) := by omega + simp [toInt_eq_toNat_bmod, Int.toNat_of_nonneg p] + /-- 'BitVec.ofInt' only cares about values upto `emod`. -/ -@[simp] theorem ofInt_eq_ofInt_emod {n : Nat} (i : Int) : +theorem ofInt_eq_ofInt_emod {n : Nat} (i : Int) : (BitVec.ofInt n i) = BitVec.ofInt n (i % (2^n)) := by apply BitVec.eq_of_toNat_eq simp only [toNat_ofInt] @@ -278,13 +284,13 @@ theorem toInt_ofNat {n : Nat} (x : Nat) : /-- Write ofInt in terms of `ofNat` of the canonical natural number between 0 and 2^n.-/ -@[simp] theorem ofInt_eq_ofNat_emod {n : Nat} (i : Int) : +theorem ofInt_eq_ofNat_emod {n : Nat} (i : Int) : (BitVec.ofInt n i) = BitVec.ofNat n (i % (2^n)).toNat := by have h2n : (2 : Int)^n = (((2 : Nat)^(n : Nat) : Nat) : Int) := by rw [Int.natCast_pow] rfl apply BitVec.eq_of_toNat_eq - simp + simp only [ofInt_eq_ofInt_emod, Int.emod_emod, toNat_ofInt, toNat_ofNat] conv => lhs; simp [(· % ·), Mod.mod] rw [Nat.mod_eq_of_lt] rw [h2n] @@ -689,7 +695,7 @@ theorem BitVec.toInt_eq_toNat_of_toInt_pos {x : BitVec n} (hx: x.toInt ≥ 0) : split at hx <;> omega -@[simp] theorem sshiftRight_eq_ushiftRight_of_pos {x : BitVec n} (hx: x.toInt ≥ 0) : +theorem sshiftRight_eq_ushiftRight_of_pos {x : BitVec n} (hx: x.toInt ≥ 0) : x.sshiftRight i = x.ushiftRight i := by rw [sshiftRight_eq, BitVec.ofInt_eq_ofNat_emod] rw [BitVec.toInt_eq_toNat_of_toInt_pos hx] @@ -704,22 +710,6 @@ theorem BitVec.toInt_eq_toNat_of_toInt_pos {x : BitVec n} (hx: x.toInt ≥ 0) : /- ↑x' >>> i < 2 ^ n -/ /- need norm_num -/ sorry --- @[simp] theorem getLsb_sshiftRight (x : BitVec n) (s i : Nat) : --- getLsb (x.sshiftRight s) i = if i ≥ n then false --- else if (s + i) < n then getLsb x (s + i) --- else getMsb x (n - 1) := by --- simp --- rw [sshiftRight_eq] --- rw [ofInt_eq_ofNat_emod] --- rw [getLsb_ofNat] --- rw [testBit_toNat] --- by_cases hinonneg : x.toInt ≥ 0 --- case pos => --- rw [Int.emod_eq_of_lt] --- sorry --- case neg => --- sorry - /-- The MSB of a bitvector is `false` iff its integer interpretetation is greater than or equal to zero. -/ theorem msb_eq_false_iff_toInt_geq_zero (x : BitVec w) @@ -744,7 +734,7 @@ theorem msb_eq_false_iff_toInt_geq_zero (x : BitVec w) omega /-- The MSB of a bitvector is `true` iff its integer interpretetation is greater than or equal to zero. -/ -theorem msb_eq_true_iff_toInt_le_zero (x : BitVec w) +theorem msb_eq_true_iff_toInt_lt_zero (x : BitVec w) : x.msb = true ↔ x.toInt < 0 := by rcases w with rfl | w <;> try simp <;> try omega · rw [Subsingleton.elim x (0#0)] @@ -765,6 +755,49 @@ theorem msb_eq_true_iff_toInt_le_zero (x : BitVec w) simp omega +#check Int.shiftRight +theorem getLsb_sshiftRight (x : BitVec n) (s i : Nat) : + getLsb (x.sshiftRight s) i = if i ≥ n then false + else if (s + i) < n then getLsb x (s + i) + else x.msb := by + simp + by_cases hxpos : (x.toInt ≥ 0) + -- If x ≥ 0, then arithmetic = logical shift right. + case pos => + rw [sshiftRight_eq_ushiftRight_of_pos hxpos] + rw [(msb_eq_false_iff_toInt_geq_zero x).mpr hxpos] + by_cases h₁ : s + i < n; + · simp only [ushiftRight_eq, getLsb_ushiftRight, h₁, ↓reduceIte, Bool.iff_and_self, + Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_le]; omega + · simp only [ushiftRight_eq, getLsb_ushiftRight, h₁, ↓reduceIte, Bool.and_false] + apply getLsb_ge + omega + case neg => + -- if x < 0, then msb = true + rw [(msb_eq_true_iff_toInt_lt_zero x).mpr (by omega)] + simp + by_cases h₁ : n ≤ i <;> simp [h₁] + by_cases h₂ : s + i < n; + case pos => + simp [h₂] + rw [sshiftRight_eq] + -- the meat and potatoes case. + sorry + case neg => + simp [h₂] + -- n ≥ i + -- s + i > n + rw [sshiftRight_eq] + rw [BitVec.ofInt_eq_ofNat_emod] + rw [BitVec.getLsb_ofNat] + simp [h₁] + sorry + + -- rw [sshiftRight_eq] + -- rw [ofInt_eq_ofNat_emod] + -- rw [getLsb_ofNat] + + /-! ### append -/ theorem append_def (x : BitVec v) (y : BitVec w) : From 7d4afe9e71eea9af3e64c89af4992a5f8333063f Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Mon, 13 May 2024 16:38:23 +0100 Subject: [PATCH 05/15] feat: port bitwise lemmas from mathlib4 into Lean --- src/Init/Data/Int/Bitwise.lean | 2 +- src/Init/Data/Int/Bitwise/Lemmas.lean | 51 +++++++++++++++++++++++++++ 2 files changed, 52 insertions(+), 1 deletion(-) create mode 100644 src/Init/Data/Int/Bitwise/Lemmas.lean diff --git a/src/Init/Data/Int/Bitwise.lean b/src/Init/Data/Int/Bitwise.lean index 2bcce0a8e8a8..4c7995c91719 100644 --- a/src/Init/Data/Int/Bitwise.lean +++ b/src/Init/Data/Int/Bitwise.lean @@ -37,7 +37,7 @@ complement and shifts the value to the right. ```lean ( 0b0111:Int) >>> 1 = 0b0011 ( 0b1000:Int) >>> 1 = 0b0100 -(-0b1000:Int) >>> 1 = -0b0100 +(-0b1000:Int) >>> 1 = -0b010 (-0b0111:Int) >>> 1 = -0b0100 ``` -/ diff --git a/src/Init/Data/Int/Bitwise/Lemmas.lean b/src/Init/Data/Int/Bitwise/Lemmas.lean new file mode 100644 index 000000000000..bbc89def12cb --- /dev/null +++ b/src/Init/Data/Int/Bitwise/Lemmas.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2023 Siddharth Bhat. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddharth Bhat, Jeremy Avigad +-- https://github.com/leanprover-community/mathlib4/blob/12b9e3064e35636d35f0c349bf2be29fb9b75bf2/Mathlib/Data/Int/Bitwise.lean#L490-L490 +-/ +prelude +import Init.Data.Nat.Bitwise.Basic +import Init.Data.Nat.Bitwise.Lemmas +import Init.Data.Int.Basic +import Init.Data.Int.Bitwise +import Init.Data.Int.Pow +import Init.Data.Bool +import Init.Data.Fin.Lemmas +import Init.Data.Nat.Lemmas +import Init.Omega.Int + +namespace Int +theorem shiftRight_eq (n : Int) (s : Nat) : n >>> s = Int.shiftRight n s := rfl +theorem shiftRight_ofNat (n s : Nat) : Int.ofNat n >>> s = Int.ofNat (n >>> s) := rfl +theorem natCast_shiftRight (n s : Nat) : ((↑n) : Int) >>> s = n >>> s := rfl + +@[simp] +theorem shiftRight_negSucc (m : Nat) (n : Nat) : + -[m+1] >>> n = -[m >>>n +1] := rfl + +theorem Int.shiftRight_shiftRight (i : Int) (m n : Nat) : + i >>> m >>> n = i >>> (m + n) := by + cases i + case ofNat i => + simp [natCast_shiftRight, Nat.shiftRight_add] + case negSucc i => + simp [Int.shiftRight_negSucc, Nat.shiftRight_add] + +theorem shiftRight_eq_div_pow (m : Int) (n : Nat) : m >>> n = m / ((((2 : Nat) ^ n) : Nat) : Int) := by + rcases m + case ofNat m => + simp only [Int.ofNat_eq_coe, shiftRight_eq, Int.shiftRight, Nat.shiftRight_eq_div_pow] + simp [Int.natCast_pow] + case negSucc m => + rw [Int.shiftRight_negSucc] + rw [negSucc_ediv] + rw [Nat.shiftRight_eq_div_pow] + . norm_cast + · norm_cast + apply Nat.pow_pos + omega + +@[simp] +theorem zero_shiftRight (n : Nat) : (0 : Int) >>> n = 0 := by + simp [Int.shiftRight_eq_div_pow] From 6be481736f9936613e7c9094399d1c0816b71608 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Tue, 14 May 2024 13:33:30 +0100 Subject: [PATCH 06/15] feat: write theory in terms of toInt --- src/Init/Data/BitVec/Lemmas.lean | 96 +++++++++++++++------------ src/Init/Data/Int/Bitwise.lean | 13 ++++ src/Init/Data/Int/Bitwise/Lemmas.lean | 27 +++++++- 3 files changed, 92 insertions(+), 44 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index a7242d3b3539..1e27ab5e67e9 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -9,6 +9,8 @@ import Init.Data.Bool import Init.Data.BitVec.Basic import Init.Data.Fin.Lemmas import Init.Data.Nat.Lemmas +import Init.Data.Int.Bitwise.Lemmas +import Init.Data.BitVec.Basic namespace BitVec @@ -147,6 +149,7 @@ theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) : getLsb (x#n) i = (i < n && x.testBit i) := by simp [getLsb, BitVec.ofNat, Fin.val_ofNat'] + @[simp, deprecated toNat_ofNat] theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial @[simp] theorem getLsb_zero : (0#w).getLsb i = false := by simp [getLsb] @@ -316,6 +319,19 @@ theorem ofInt_eq_ofNat_emod {n : Nat} (i : Int) : apply Lean.Omega.Int.pos_pow_of_pos decide +@[simp] +theorem Int.testBit_natCast (n : Nat) : (n : Int).testBit i = n.testBit i := rfl + +theorem Int.natCast_mod_natCast (n m : Nat) : (n : Int) % (m : Int) = ((n % m : Nat) : Int) := rfl + +theorem Int.negSucc_mod_natCast (n m : Nat) : + (Int.negSucc m) % (n : Int) = n - ((m % n) + 1) := rfl + +@[simp] theorem Int.toNat_natCast (n : Nat) : (n : Int).toNat = n := rfl + +@[simp] theorem ofInt_natCast (w n : Nat) : + BitVec.ofInt w n = BitVec.ofNat w n := rfl + /-! ### zeroExtend and truncate -/ @[simp, bv_toNat] theorem toNat_zeroExtend' {m n : Nat} (p : m ≤ n) (x : BitVec m) : @@ -755,49 +771,6 @@ theorem msb_eq_true_iff_toInt_lt_zero (x : BitVec w) simp omega -#check Int.shiftRight -theorem getLsb_sshiftRight (x : BitVec n) (s i : Nat) : - getLsb (x.sshiftRight s) i = if i ≥ n then false - else if (s + i) < n then getLsb x (s + i) - else x.msb := by - simp - by_cases hxpos : (x.toInt ≥ 0) - -- If x ≥ 0, then arithmetic = logical shift right. - case pos => - rw [sshiftRight_eq_ushiftRight_of_pos hxpos] - rw [(msb_eq_false_iff_toInt_geq_zero x).mpr hxpos] - by_cases h₁ : s + i < n; - · simp only [ushiftRight_eq, getLsb_ushiftRight, h₁, ↓reduceIte, Bool.iff_and_self, - Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_le]; omega - · simp only [ushiftRight_eq, getLsb_ushiftRight, h₁, ↓reduceIte, Bool.and_false] - apply getLsb_ge - omega - case neg => - -- if x < 0, then msb = true - rw [(msb_eq_true_iff_toInt_lt_zero x).mpr (by omega)] - simp - by_cases h₁ : n ≤ i <;> simp [h₁] - by_cases h₂ : s + i < n; - case pos => - simp [h₂] - rw [sshiftRight_eq] - -- the meat and potatoes case. - sorry - case neg => - simp [h₂] - -- n ≥ i - -- s + i > n - rw [sshiftRight_eq] - rw [BitVec.ofInt_eq_ofNat_emod] - rw [BitVec.getLsb_ofNat] - simp [h₁] - sorry - - -- rw [sshiftRight_eq] - -- rw [ofInt_eq_ofNat_emod] - -- rw [getLsb_ofNat] - - /-! ### append -/ theorem append_def (x : BitVec v) (y : BitVec w) : @@ -1212,4 +1185,41 @@ theorem toNat_intMax_eq : (intMax w).toNat = 2^w - 1 := by (ofBoolListLE bs).getMsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by simp [getMsb_eq_getLsb] + +@[simp] theorem ofInt_negSucc (w n : Nat) : + BitVec.ofInt w (Int.negSucc n) = ~~~ (BitVec.ofNat w n) := by + apply BitVec.eq_of_toNat_eq + simp + sorry + +@[simp] theorem getLsb_ofInt (n : Nat) (x : Int) (i : Nat) : + getLsb (BitVec.ofInt n x) i = (i < n && x.testBit i) := by + cases x + case ofNat x => + simp + simp [getLsb_ofNat] + case negSucc x => + simp [Int.testBit] + simp [getLsb_ofNat] + cases decide (i < n) <;> simp + +@[simp] theorem toInt_sshiftRight (x : BitVec n) (i : Nat) : + (x.sshiftRight i).toInt = (x.toInt >>> i).bmod (2^n) := by + rw [sshiftRight_eq, BitVec.toInt_ofInt] + +-- theorem testBit_toInt (x : BitVec w) : +-- x.toInt.testBit i = x.getLsb i := rfl + +#check Int.testBit_shiftRight +theorem getLsb_sshiftRight (x : BitVec n) (s i : Nat) : + getLsb (x.sshiftRight s) i = if i ≥ n then false + else if (s + i) < n then getLsb x (s + i) + else x.msb := by + + rw [sshiftRight_eq] + rw [getLsb_ofInt] + rw [Int.testBit_shiftRight] + by_cases h₁:i < n <;> simp [h₁] + + end BitVec diff --git a/src/Init/Data/Int/Bitwise.lean b/src/Init/Data/Int/Bitwise.lean index 4c7995c91719..d13d86f6c1c0 100644 --- a/src/Init/Data/Int/Bitwise.lean +++ b/src/Init/Data/Int/Bitwise.lean @@ -47,4 +47,17 @@ protected def shiftRight : Int → Nat → Int instance : HShiftRight Int Nat Int := ⟨.shiftRight⟩ +/- +### testBit +We define an operation for testing individual bits in the binary representation +of a number. +-/ + +-- -m = !m + 1 +-- -(m + 1) = -m - 1 = !m +/-- `testBit m n` returns whether the `(n+1)` least significant bit is `1` or `0`-/ +def testBit : Int → Nat → Bool + | .ofNat m, n => Nat.testBit m n + | .negSucc m, n => !(Nat.testBit m n) + end Int diff --git a/src/Init/Data/Int/Bitwise/Lemmas.lean b/src/Init/Data/Int/Bitwise/Lemmas.lean index bbc89def12cb..bf6ff3ecef1a 100644 --- a/src/Init/Data/Int/Bitwise/Lemmas.lean +++ b/src/Init/Data/Int/Bitwise/Lemmas.lean @@ -16,8 +16,10 @@ import Init.Data.Nat.Lemmas import Init.Omega.Int namespace Int + theorem shiftRight_eq (n : Int) (s : Nat) : n >>> s = Int.shiftRight n s := rfl -theorem shiftRight_ofNat (n s : Nat) : Int.ofNat n >>> s = Int.ofNat (n >>> s) := rfl +@[simp] +theorem shiftRight_ofNat (n s : Nat) : (n : Int) >>> s = Int.ofNat (n >>> s) := rfl theorem natCast_shiftRight (n s : Nat) : ((↑n) : Int) >>> s = n >>> s := rfl @[simp] @@ -49,3 +51,26 @@ theorem shiftRight_eq_div_pow (m : Int) (n : Nat) : m >>> n = m / ((((2 : Nat) ^ @[simp] theorem zero_shiftRight (n : Nat) : (0 : Int) >>> n = 0 := by simp [Int.shiftRight_eq_div_pow] + +@[simp] theorem zero_testBit (i : Nat) : Int.testBit 0 i = false := by + simp only [testBit, zero_shiftRight, Nat.zero_and, bne_self_eq_false, Nat.zero_testBit i] + +-- @[simp] theorem testBit_zero (x : Int) : Int.testBit x 0 = decide (x % 2 = 1) := by +-- unfold testBit +-- cases x <;> simp [Nat.testBit_zero] +-- case ofNat x => +-- omega + +@[simp] theorem testBit_succ (x : Int) (i : Nat) : Int.testBit x (Nat.succ i) = testBit (x/2) i := by + unfold testBit + cases x <;> simp <;> rfl + +theorem toNat_testBit (x i : Nat) : + (x.testBit i).toNat = x / 2 ^ i % 2 := by + rw [Nat.testBit_to_div_mod] + rcases Nat.mod_two_eq_zero_or_one (x / 2^i) <;> simp_all + +@[simp] theorem testBit_shiftRight (x : Int) (i j : Nat) : testBit (x >>> i) j = testBit x (i+j) := by + cases x <;> simp [testBit] + +end Int From d0e08c4c1fa50b6d0df92c7b254cb6f05acfd5c2 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Tue, 14 May 2024 19:34:34 +0100 Subject: [PATCH 07/15] feat: write proof sketch necessary --- src/Init/Data/BitVec/Lemmas.lean | 157 ++++++++++++++++++++++--------- 1 file changed, 112 insertions(+), 45 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 1e27ab5e67e9..e0630d7494c5 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -711,26 +711,26 @@ theorem BitVec.toInt_eq_toNat_of_toInt_pos {x : BitVec n} (hx: x.toInt ≥ 0) : split at hx <;> omega -theorem sshiftRight_eq_ushiftRight_of_pos {x : BitVec n} (hx: x.toInt ≥ 0) : - x.sshiftRight i = x.ushiftRight i := by - rw [sshiftRight_eq, BitVec.ofInt_eq_ofNat_emod] - rw [BitVec.toInt_eq_toNat_of_toInt_pos hx] - rw [ushiftRight_eq] - rw [Int.emod_eq_of_lt] - · norm_cast - sorry - · /- need norm_num-/ - sorry - · have ⟨x', hx'lt⟩ := x - simp - /- ↑x' >>> i < 2 ^ n -/ - /- need norm_num -/ - sorry +-- theorem sshiftRight_eq_ushiftRight_of_pos {x : BitVec n} (hx: x.toInt ≥ 0) : +-- x.sshiftRight i = x.ushiftRight i := by +-- rw [sshiftRight_eq, BitVec.ofInt_eq_ofNat_emod] +-- rw [BitVec.toInt_eq_toNat_of_toInt_pos hx] +-- rw [ushiftRight_eq] +-- rw [Int.emod_eq_of_lt] +-- · norm_cast +-- sorry +-- · /- need norm_num-/ +-- sorry +-- · have ⟨x', hx'lt⟩ := x +-- simp +-- /- ↑x' >>> i < 2 ^ n -/ +-- /- need norm_num -/ +-- sorry -/-- The MSB of a bitvector is `false` iff its integer interpretetation is greater than or equal to zero. -/ -theorem msb_eq_false_iff_toInt_geq_zero (x : BitVec w) - : x.msb = false ↔ x.toInt ≥ 0 := by - rcases w with rfl | w <;> simp +/-- The MSB of a bitvector is `true` iff its integer interpretetation is greater than or equal to zero. -/ +theorem msb_eq_true_iff_toInt_lt_zero (x : BitVec w) + : x.msb = true ↔ x.toInt < 0 := by + rcases w with rfl | w <;> try simp <;> try omega · rw [Subsingleton.elim x (0#0)] simp rw [BitVec.toInt_eq_toNat_cond] @@ -738,39 +738,65 @@ theorem msb_eq_false_iff_toInt_geq_zero (x : BitVec w) · intro h split case inl hpos => - apply Int.ofNat_nonneg - case inr hneg => - exfalso rw [BitVec.msb_eq_decide] at h simp at h omega + case inr hneg => + simp_all + omega · intro h rw [BitVec.msb_eq_decide] simp omega -/-- The MSB of a bitvector is `true` iff its integer interpretetation is greater than or equal to zero. -/ -theorem msb_eq_true_iff_toInt_lt_zero (x : BitVec w) - : x.msb = true ↔ x.toInt < 0 := by +/-- The MSB of a bitvector is `true` iff its numerical value is larger than half the bitwidth. -/ +theorem msb_eq_true_iff_large (x : BitVec w) + : x.msb = true ↔ 2 * x.toNat ≥ 2^w := by rcases w with rfl | w <;> try simp <;> try omega - · rw [Subsingleton.elim x (0#0)] + constructor + · intro h + rw [BitVec.msb_eq_decide] at h + simp at h + omega + · intro h + rw [BitVec.msb_eq_decide] simp - rw [BitVec.toInt_eq_toNat_cond] + omega +/-- The MSB of a bitvector is `false` iff its numerical value is smaller than half the bitwidth. -/ +theorem msb_eq_false_iff_small {x : BitVec w} + : x.msb = false ↔ 2 * x.toNat < 2^w := by + rcases w with rfl | w <;> try simp <;> try omega constructor · intro h - split - case inl hpos => - rw [BitVec.msb_eq_decide] at h - simp at h - omega - case inr hneg => - simp_all - omega + rw [BitVec.msb_eq_decide] at h + simp at h + omega · intro h rw [BitVec.msb_eq_decide] simp omega +-- /-- The MSB of a bitvector is `false` iff its integer interpretetation is greater than or equal to zero. -/ +-- theorem msb_eq_false_iff_toInt_geq_zero (x : BitVec w) +-- : x.msb = false ↔ x.toInt ≥ 0 := by +-- constructor +-- · intro h +-- rw [toInt_eq_toNat_cond] +-- have hsize := msb_eq_false_iff_small.mp h +-- split <;> omega +-- · intro h +-- have hx : x.toNat < 2^w := by exact isLt x +-- rw [BitVec.msb_eq_decide] +-- simp +-- rw [BitVec.toInt_eq_toNat_cond] at h +-- split at h <;> try omega +-- case inl hsz => +-- -- we need integer omega here it looks likke? +-- norm_cast +-- simp_all +-- sorry + + /-! ### append -/ theorem append_def (x : BitVec v) (y : BitVec w) : @@ -1186,6 +1212,8 @@ theorem toNat_intMax_eq : (intMax w).toNat = 2^w - 1 := by simp [getMsb_eq_getLsb] +-- PROOF SKETCH -- + @[simp] theorem ofInt_negSucc (w n : Nat) : BitVec.ofInt w (Int.negSucc n) = ~~~ (BitVec.ofNat w n) := by apply BitVec.eq_of_toNat_eq @@ -1196,30 +1224,69 @@ theorem toNat_intMax_eq : (intMax w).toNat = 2^w - 1 := by getLsb (BitVec.ofInt n x) i = (i < n && x.testBit i) := by cases x case ofNat x => - simp - simp [getLsb_ofNat] + simp only [Int.ofNat_eq_coe, ofInt_natCast, getLsb_ofNat, Int.testBit_natCast] case negSucc x => - simp [Int.testBit] - simp [getLsb_ofNat] + simp only [ofInt_negSucc, getLsb_not, getLsb_ofNat, Bool.not_and, Int.testBit] cases decide (i < n) <;> simp @[simp] theorem toInt_sshiftRight (x : BitVec n) (i : Nat) : (x.sshiftRight i).toInt = (x.toInt >>> i).bmod (2^n) := by rw [sshiftRight_eq, BitVec.toInt_ofInt] --- theorem testBit_toInt (x : BitVec w) : --- x.toInt.testBit i = x.getLsb i := rfl +-- If the index is larger than the bitwidth and the integer is negative, +-- then the left hand side gives '1' and the right hand side gives '0'. +theorem testBit_toInt_eq_testBit_toNat {x : BitVec w} (hi : i < w): + x.toInt.testBit i = x.toNat.testBit i := by + simp only [toInt_eq_toNat_cond] + split + case inl => simp only [Int.testBit_natCast] + case inr h => + sorry + +theorem testBit_toInt_eq_getLsb {x : BitVec w} (hi : i < w) : + x.toInt.testBit i = x.getLsb i := by + rw [testBit_toInt_eq_testBit_toNat hi] + rfl + +theorem testBit_toInt_eq_msb {x : BitVec w} (hi : i ≥ w) : + x.toInt.testBit i = x.msb := by +rw [BitVec.toInt] +split +case inl h => + rw [msb_eq_false_iff_small.mpr h] + simp only [Int.testBit_natCast] + rw [testBit_toNat] + exact getLsb_ge x i hi +case inr h => + rw [Int.testBit] + split + case h_1 a b c d e => + simp at e + have h : x.toNat - 2^w < 0 := by omega + sorry -- show that if < 0, then cannot be .ofNat + case h_2 a b c d e => + -- we know that d.testBit = false from 'e' + -- we know that x.msb = true by 'h'. + sorry -#check Int.testBit_shiftRight theorem getLsb_sshiftRight (x : BitVec n) (s i : Nat) : - getLsb (x.sshiftRight s) i = if i ≥ n then false + getLsb (x.sshiftRight s) i = + if i ≥ n then false else if (s + i) < n then getLsb x (s + i) else x.msb := by - rw [sshiftRight_eq] rw [getLsb_ofInt] rw [Int.testBit_shiftRight] by_cases h₁:i < n <;> simp [h₁] - + by_cases h₂:(s + i < n) <;> simp [h₂] + case pos => + rw [testBit_toInt_eq_getLsb (by assumption)] + simp only [Bool.iff_and_self, Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_le, h₁, + implies_true] + case neg => + rw [testBit_toInt_eq_msb] + · simp only [Bool.iff_and_self, Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_le] + omega + · omega end BitVec From b013df07e4f0b87f5d88eace840a1f10b1fd7857 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Tue, 14 May 2024 22:42:13 +0100 Subject: [PATCH 08/15] checkpoint --- src/Init/Data/BitVec/Lemmas.lean | 80 +++++++++++++++++++++++++------- 1 file changed, 63 insertions(+), 17 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index e0630d7494c5..eb526cfab010 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1117,6 +1117,11 @@ theorem neg_eq_not_add (x : BitVec w) : -x = ~~~x + 1 := by have hx : x.toNat < 2^w := x.isLt rw [Nat.sub_sub, Nat.add_comm 1 x.toNat, ← Nat.sub_sub, Nat.sub_add_cancel (by omega)] +-- @[simp, bv_toNat] theorem toInt_sub (x y : BitVec w) : +-- (x - y).toInt = ((x.toNat + (((2 : Nat) ^ w : Nat) - y.toNat)) : Int).bmod (2 ^ w) := by +-- simp [toInt_eq_toNat_bmod] +-- norm_cast +-- simp /-! ### mul -/ theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl @@ -1211,23 +1216,40 @@ theorem toNat_intMax_eq : (intMax w).toNat = 2^w - 1 := by (ofBoolListLE bs).getMsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by simp [getMsb_eq_getLsb] - --- PROOF SKETCH -- - -@[simp] theorem ofInt_negSucc (w n : Nat) : - BitVec.ofInt w (Int.negSucc n) = ~~~ (BitVec.ofNat w n) := by - apply BitVec.eq_of_toNat_eq - simp - sorry - -@[simp] theorem getLsb_ofInt (n : Nat) (x : Int) (i : Nat) : - getLsb (BitVec.ofInt n x) i = (i < n && x.testBit i) := by - cases x - case ofNat x => - simp only [Int.ofNat_eq_coe, ofInt_natCast, getLsb_ofNat, Int.testBit_natCast] - case negSucc x => - simp only [ofInt_negSucc, getLsb_not, getLsb_ofNat, Bool.not_and, Int.testBit] - cases decide (i < n) <;> simp +theorem Int.negSucc_div_ofNat (a b : Nat) (hb : b ≠ 0) : + (Int.negSucc a) / (Int.ofNat b) = Int.negSucc (((a / b) : Nat)) := by + rcases b with rfl | b + · contradiction + · norm_cast + +#check Int.ediv +#reduce (Int.negSucc 4) % (Int.ofNat 1) -- 0 +#reduce (Int.negSucc 4) % (Int.ofNat 1) -- 0 +#reduce (Int.negSucc 4) % (Int.ofNat 1) -- 0 +#reduce (Int.negSucc 4) % (Int.ofNat 1) -- 0 +#reduce (Int.negSucc 4) % (Int.ofNat 1) -- 0 + +#reduce (Int.negSucc 0) % (Int.ofNat 8) -- 7 +#reduce (Int.negSucc 1) % (Int.ofNat 8) -- 6 +#reduce (Int.negSucc 2) % (Int.ofNat 8) -- 5 +#reduce (Int.negSucc 3) % (Int.ofNat 8) -- 4 +#reduce (Int.negSucc 4) % (Int.ofNat 8) -- 3 +#reduce (Int.negSucc 5) % (Int.ofNat 8) -- 2 +#reduce (Int.negSucc 6) % (Int.ofNat 8) -- 1 +#reduce (Int.negSucc 7) % (Int.ofNat 8) -- 0 +#reduce (Int.negSucc 8) % (Int.ofNat 8) -- 7 +#reduce (Int.negSucc 9) % (Int.ofNat 8) -- 6 +#reduce (Int.negSucc 10) % (Int.ofNat 8) -- 5 +#reduce (Int.negSucc 11) % (Int.ofNat 8) -- 4 +#reduce (Int.negSucc 12) % (Int.ofNat 8) -- 3 +#reduce (Int.negSucc 13) % (Int.ofNat 8) -- 2 +#reduce (Int.negSucc 14) % (Int.ofNat 8) -- 1 +#reduce (Int.negSucc 15) % (Int.ofNat 8) -- 0 +#reduce (Int.negSucc 16) % (Int.ofNat 8) -- 1 +#reduce (Int.negSucc 17) % (Int.ofNat 8) -- 2 +#reduce (Int.negSucc 18) % (Int.ofNat 8) + +#check Nat.emod_pos_of_not_dvd @[simp] theorem toInt_sshiftRight (x : BitVec n) (i : Nat) : (x.sshiftRight i).toInt = (x.toInt >>> i).bmod (2^n) := by @@ -1269,6 +1291,30 @@ case inr h => -- we know that x.msb = true by 'h'. sorry +@[simp] +theorem toInt_zero : (0#w).toInt = 0 := by + simp [toInt_eq_toNat_bmod] + +@[simp] +theorem toInt_neg (x : BitVec w) : + (-x).toInt = (((((2 : Nat) ^ w) - x.toNat) : Nat) : Int).bmod (2 ^ w) := by + simp [toInt_eq_toNat_bmod] + + +theorem ofInt_ofNat (n : Nat) : BitVec.ofInt w (Int.ofNat n) = n#w := by + apply eq_of_toNat_eq + simp + +@[simp] theorem getLsb_ofInt (n : Nat) (x : Int) (i : Nat) : + getLsb (BitVec.ofInt n x) i = (i < n && x.testBit i) := by + cases x + case ofNat x => + rw [ofInt_ofNat] + simp + rw [getLsb_ofNat] + case negSucc x => + sorry + theorem getLsb_sshiftRight (x : BitVec n) (s i : Nat) : getLsb (x.sshiftRight s) i = if i ≥ n then false From 6ba1cc15a602cc2e0b9355e29f73caab442ba570 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 15 May 2024 12:33:50 +0100 Subject: [PATCH 09/15] feat: build up testBit for int theory and modulo 2 theory --- src/Init/Data/BitVec/Lemmas.lean | 41 ++++++++++++++++++++++----- src/Init/Data/Int/Bitwise/Lemmas.lean | 30 ++++++++++++++++---- 2 files changed, 59 insertions(+), 12 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index eb526cfab010..4b29866133c1 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1255,16 +1255,44 @@ theorem Int.negSucc_div_ofNat (a b : Nat) (hb : b ≠ 0) : (x.sshiftRight i).toInt = (x.toInt >>> i).bmod (2^n) := by rw [sshiftRight_eq, BitVec.toInt_ofInt] +private theorem Int.sub_sub_ofNat_implies_geq {x y : Nat} + (h : (x : Int) - (y : Int) = Int.ofNat z) : x ≥ y := by + simp at h + omega + -- If the index is larger than the bitwidth and the integer is negative, -- then the left hand side gives '1' and the right hand side gives '0'. theorem testBit_toInt_eq_testBit_toNat {x : BitVec w} (hi : i < w): x.toInt.testBit i = x.toNat.testBit i := by - simp only [toInt_eq_toNat_cond] - split - case inl => simp only [Int.testBit_natCast] - case inr h => - sorry - + rcases w with rfl | w + case zero => + simp [toInt_eq_toNat_bmod] + case succ => + simp only [toInt_eq_toNat_cond] + split + case inl => simp only [Int.testBit_natCast] + case inr h => + -- ¬ ((2 * x.toNat) < 2^(w+1)) + have hx : x.toNat ≥ 2^w := by omega + have hx' : x.toNat < 2^(w+1) := by omega + -- ((x.toNat) ≥ 2^(w)) + rw [Int.testBit] + split + case h_1 a b c d e => + simp at e + have hcontra := Int.sub_sub_ofNat_implies_geq e + omega + case h_2 a b c d e => + rw [Nat.testBit] + rw [BitVec.testBit_toNat] + have he : ∀ (i : Nat), ((x.toNat : Int) - ((((2 : Nat) ^ (w + 1) : Nat) : Int))).testBit i = + (Int.negSucc d).testBit i := by + intros i + rw [← e] + -- HERE HERE HERE + sorry + -- rw [Int.testBit] at he + -- omega theorem testBit_toInt_eq_getLsb {x : BitVec w} (hi : i < w) : x.toInt.testBit i = x.getLsb i := by rw [testBit_toInt_eq_testBit_toNat hi] @@ -1300,7 +1328,6 @@ theorem toInt_neg (x : BitVec w) : (-x).toInt = (((((2 : Nat) ^ w) - x.toNat) : Nat) : Int).bmod (2 ^ w) := by simp [toInt_eq_toNat_bmod] - theorem ofInt_ofNat (n : Nat) : BitVec.ofInt w (Int.ofNat n) = n#w := by apply eq_of_toNat_eq simp diff --git a/src/Init/Data/Int/Bitwise/Lemmas.lean b/src/Init/Data/Int/Bitwise/Lemmas.lean index bf6ff3ecef1a..3f20e9822cde 100644 --- a/src/Init/Data/Int/Bitwise/Lemmas.lean +++ b/src/Init/Data/Int/Bitwise/Lemmas.lean @@ -14,6 +14,9 @@ import Init.Data.Bool import Init.Data.Fin.Lemmas import Init.Data.Nat.Lemmas import Init.Omega.Int +import Init.Data.Int.DivMod +import Init.Data.Int.Order +import Init.Data.Nat.Dvd namespace Int @@ -55,11 +58,28 @@ theorem zero_shiftRight (n : Nat) : (0 : Int) >>> n = 0 := by @[simp] theorem zero_testBit (i : Nat) : Int.testBit 0 i = false := by simp only [testBit, zero_shiftRight, Nat.zero_and, bne_self_eq_false, Nat.zero_testBit i] --- @[simp] theorem testBit_zero (x : Int) : Int.testBit x 0 = decide (x % 2 = 1) := by --- unfold testBit --- cases x <;> simp [Nat.testBit_zero] --- case ofNat x => --- omega + +private theorem Nat.mod2_cases (x : Nat) : (x % 2 = 0) ∨ (x % 2 = 1) := by omega +private theorem Int.mod2_cases (x : Int) : (x % 2 = 0) ∨ (x % 2 = 1) := by omega + +@[simp] theorem Int.mod2_ofNat_eq (x : Nat) : (Int.ofNat x % 2) = (x % 2) := by + simp [Int.mod_def'] + +@[simp] theorem Int.mod2_negSucc_eq (x : Nat) : (Int.negSucc x % 2) = (1 - x % 2) := by + simp only [mod_def'] + unfold Int.emod + simp only [subNatNat, Int.reduceAbs, Nat.succ_eq_add_one, Nat.reduceSubDiff, ofNat_eq_coe, + ofNat_emod, Nat.cast_ofNat_Int] + split <;> omega + +@[simp] theorem testBit_ofNat (x : Nat) (i : Nat) : (x : Int).testBit i = x.testBit i := rfl +@[simp] theorem testBit_negSucc (x : Nat) (i : Nat) : (Int.negSucc x).testBit i = !(x.testBit i) := rfl + +@[simp] theorem testBit_zero (x : Int) : Int.testBit x 0 = decide (x % 2 = 1) := by + rcases x with x | x + · simp only [ofNat_eq_coe, testBit_ofNat, Nat.testBit_zero, decide_eq_decide]; omega + · simp only [testBit_negSucc, Nat.testBit_zero, Int.mod2_negSucc_eq] + rcases (Nat.mod2_cases x) with h | h <;> simp_all <;> omega @[simp] theorem testBit_succ (x : Int) (i : Nat) : Int.testBit x (Nat.succ i) = testBit (x/2) i := by unfold testBit From 239e3c5b88e83ace8531650425a732d38c75224b Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 15 May 2024 14:02:29 +0100 Subject: [PATCH 10/15] feat: checkpoint --- src/Init/Data/BitVec/Lemmas.lean | 237 ++++++++++++++++++++++--------- 1 file changed, 168 insertions(+), 69 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 4b29866133c1..9c60af5c77aa 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -728,7 +728,7 @@ theorem BitVec.toInt_eq_toNat_of_toInt_pos {x : BitVec n} (hx: x.toInt ≥ 0) : -- sorry /-- The MSB of a bitvector is `true` iff its integer interpretetation is greater than or equal to zero. -/ -theorem msb_eq_true_iff_toInt_lt_zero (x : BitVec w) +theorem msb_eq_true_iff_toInt_lt_zero {x : BitVec w} : x.msb = true ↔ x.toInt < 0 := by rcases w with rfl | w <;> try simp <;> try omega · rw [Subsingleton.elim x (0#0)] @@ -750,7 +750,7 @@ theorem msb_eq_true_iff_toInt_lt_zero (x : BitVec w) omega /-- The MSB of a bitvector is `true` iff its numerical value is larger than half the bitwidth. -/ -theorem msb_eq_true_iff_large (x : BitVec w) +theorem msb_eq_true_iff_large {x : BitVec w} : x.msb = true ↔ 2 * x.toNat ≥ 2^w := by rcases w with rfl | w <;> try simp <;> try omega constructor @@ -776,26 +776,27 @@ theorem msb_eq_false_iff_small {x : BitVec w} simp omega --- /-- The MSB of a bitvector is `false` iff its integer interpretetation is greater than or equal to zero. -/ --- theorem msb_eq_false_iff_toInt_geq_zero (x : BitVec w) --- : x.msb = false ↔ x.toInt ≥ 0 := by --- constructor --- · intro h --- rw [toInt_eq_toNat_cond] --- have hsize := msb_eq_false_iff_small.mp h --- split <;> omega --- · intro h --- have hx : x.toNat < 2^w := by exact isLt x --- rw [BitVec.msb_eq_decide] --- simp --- rw [BitVec.toInt_eq_toNat_cond] at h --- split at h <;> try omega --- case inl hsz => --- -- we need integer omega here it looks likke? --- norm_cast --- simp_all --- sorry - +/-- The MSB of a bitvector is `false` iff its integer interpretetation is greater than or equal to zero. -/ +theorem msb_eq_false_iff_toInt_geq_zero {x : BitVec w} + : x.msb = false ↔ x.toInt ≥ 0 := by + constructor + · intro h + rw [toInt_eq_toNat_cond] + have hsize := msb_eq_false_iff_small.mp h + split <;> omega + · intro h + have hx : x.toNat < 2^w := by exact isLt x + rw [BitVec.msb_eq_decide] + simp + rw [BitVec.toInt_eq_toNat_cond] at h + split at h <;> try omega + case inl hsz => + norm_cast + simp_all + rcases w with rfl | w + · simp + · simp [Nat.lt_succ_iff] + omega /-! ### append -/ @@ -1255,14 +1256,113 @@ theorem Int.negSucc_div_ofNat (a b : Nat) (hb : b ≠ 0) : (x.sshiftRight i).toInt = (x.toInt >>> i).bmod (2^n) := by rw [sshiftRight_eq, BitVec.toInt_ofInt] -private theorem Int.sub_sub_ofNat_implies_geq {x y : Nat} - (h : (x : Int) - (y : Int) = Int.ofNat z) : x ≥ y := by +/-- info: 'BitVec.toInt_sshiftRight' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in #print axioms toInt_sshiftRight +@[simp] private theorem Int.ofNat_sub_ofNat_eq_ofNat_implies_eq_ofNat_sub {x y : Nat} + (h : (x : Int) - (y : Int) = Int.ofNat z) : (x : Int) - (y : Int) = ((x - y : Nat) : Int) := by simp at h omega +/-- +info: '_private.Init.Data.BitVec.Lemmas.0.BitVec.Int.ofNat_sub_ofNat_eq_ofNat_implies_eq_ofNat_sub' depends on axioms: [propext, + Classical.choice, + Quot.sound] +-/ +#guard_msgs in #print axioms Int.ofNat_sub_ofNat_eq_ofNat_implies_eq_ofNat_sub +/-- (n₁ : Int) - (n₂ : Int) = (n₃ : Int) for n₁, n₂, n₃ naturals iff n₁ ≥ n₂ -/ +private theorem Int.sub_sub_eq_ofNat_iff_geq {x y : Nat} : + (∃ (z : Nat), (x : Int) - (y : Int) = Int.ofNat z) ↔ x ≥ y := by + constructor + · intros h + simp only [Int.ofNat_eq_coe] at h + omega + · intro h + exists (x - y) + simp only [Int.ofNat_eq_coe] + omega + +/-- +info: '_private.Init.Data.BitVec.Lemmas.0.BitVec.Int.sub_sub_eq_ofNat_iff_geq' depends on axioms: [propext, + Classical.choice, + Quot.sound] +-/ +#guard_msgs in #print axioms Int.sub_sub_eq_ofNat_iff_geq + +/-- (n₁ : Int) - (n₂ : Int) = (negSucc n₃) for n₁, n₂, n₃ naturals iff n₁ < n₂ -/ +private theorem Int.sub_sub_eq_negSucc_implies_le {x y : Nat} + (h : ∃ (z : Nat), (x : Int) - (y : Int) = Int.negSucc z) : x < y := by + have hxlty:(x < y) ∨ (x >= y) := by omega + rcases hxlty with hxlty | hxlty + · omega + · obtain ⟨z, hz⟩ := Int.sub_sub_eq_ofNat_iff_geq.mpr hxlty + rw [hz] at h + obtain ⟨w, hw⟩ := h + contradiction + +/-- +info: '_private.Init.Data.BitVec.Lemmas.0.BitVec.Int.sub_sub_eq_negSucc_implies_le' depends on axioms: [propext, + Classical.choice, + Quot.sound] +-/ +#guard_msgs in #print axioms Int.sub_sub_eq_negSucc_implies_le + +theorem Int.toNat_sub_toNat_eq_negSucc_ofLt {n m : Nat} (hlt : n < m) : + (n : Int) - (m : Int) = (Int.negSucc (m - 1 - n)) := by + rw [Int.negSucc_eq] -- TODO: consider adding this to omega cleanup set. + omega +/-- +info: 'BitVec.Int.toNat_sub_toNat_eq_negSucc_ofLt' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in #print axioms Int.toNat_sub_toNat_eq_negSucc_ofLt + + +theorem testBit_toInt_eq_msb {x : BitVec w} (hi : i ≥ w) : + x.toInt.testBit i = x.msb := by +rw [BitVec.toInt] +split +case inl h => + rw [msb_eq_false_iff_small.mpr h] + simp only [Int.testBit_natCast] + rw [testBit_toNat] + exact getLsb_ge x i hi +case inr h => + rcases w with rfl | w + · simp at h + · have hx : x.toNat ≥ 2^w := by omega + have hx' : x.toNat < 2^(w + 1) := by omega + have hz := Int.toNat_sub_toNat_eq_negSucc_ofLt hx' + rw [hz] + simp + rw [Nat.testBit] + rw [Nat.shiftRight_eq_div_pow] + rw [Nat.div_eq_of_lt] + · simp only [Nat.and_one_is_mod, Nat.zero_mod, bne_self_eq_false, Bool.not_false, Bool.true_eq] + rw [msb_eq_true_iff_large] + omega + · rw [Nat.pow_succ] + have hpow : 2^w < 2^i := by + refine (Nat.pow_lt_pow_iff_right ?h).mpr hi + omega + omega +/-- +info: 'BitVec.testBit_toInt_eq_msb' depends on axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs in #print axioms testBit_toInt_eq_msb + +/-! +# Theorems that need sorry below +-/ +/-- subtracting a bit 2^w does not change the value of testBit. + TODO: unclear how true this is. -/ +private theorem Int.testBit_sub_big (x : Nat) (w : Nat) (hi: i < w): + ((x : Int) - ((((2 : Nat)^w) : Nat) : Int)).testBit i = x.testBit i := by + simp [Int.testBit] + sorry + +#print axioms Int.testBit_sub_big -- If the index is larger than the bitwidth and the integer is negative, -- then the left hand side gives '1' and the right hand side gives '0'. -theorem testBit_toInt_eq_testBit_toNat {x : BitVec w} (hi : i < w): +theorem toInt_testBit_eq_toNat_testBit {x : BitVec w} (hi : i < w): x.toInt.testBit i = x.toNat.testBit i := by rcases w with rfl | w case zero => @@ -1272,52 +1372,39 @@ theorem testBit_toInt_eq_testBit_toNat {x : BitVec w} (hi : i < w): split case inl => simp only [Int.testBit_natCast] case inr h => - -- ¬ ((2 * x.toNat) < 2^(w+1)) - have hx : x.toNat ≥ 2^w := by omega - have hx' : x.toNat < 2^(w+1) := by omega - -- ((x.toNat) ≥ 2^(w)) rw [Int.testBit] split case h_1 a b c d e => simp at e - have hcontra := Int.sub_sub_ofNat_implies_geq e omega case h_2 a b c d e => - rw [Nat.testBit] - rw [BitVec.testBit_toNat] - have he : ∀ (i : Nat), ((x.toNat : Int) - ((((2 : Nat) ^ (w + 1) : Nat) : Int))).testBit i = - (Int.negSucc d).testBit i := by - intros i - rw [← e] - -- HERE HERE HERE + have hcontra : x.toNat ≥ 2 ^ w := by omega + have hcontra' : x.toNat < 2^(w + 1) := by omega + have hd := Int.toNat_sub_toNat_eq_negSucc_ofLt hcontra' + rw [hd] at e + simp at e + rw [← e] sorry - -- rw [Int.testBit] at he - -- omega + -- simp [Nat.testBit] + -- rw [Nat.shiftRight_eq_div_pow] + +/-- +info: 'BitVec.toInt_testBit_eq_toNat_testBit' depends on axioms: [propext, Classical.choice, Quot.sound, sorryAx] +-/ +#guard_msgs in #print axioms toInt_testBit_eq_toNat_testBit + theorem testBit_toInt_eq_getLsb {x : BitVec w} (hi : i < w) : x.toInt.testBit i = x.getLsb i := by - rw [testBit_toInt_eq_testBit_toNat hi] + rw [toInt_testBit_eq_toNat_testBit hi] rfl -theorem testBit_toInt_eq_msb {x : BitVec w} (hi : i ≥ w) : - x.toInt.testBit i = x.msb := by -rw [BitVec.toInt] -split -case inl h => - rw [msb_eq_false_iff_small.mpr h] - simp only [Int.testBit_natCast] - rw [testBit_toNat] - exact getLsb_ge x i hi -case inr h => - rw [Int.testBit] - split - case h_1 a b c d e => - simp at e - have h : x.toNat - 2^w < 0 := by omega - sorry -- show that if < 0, then cannot be .ofNat - case h_2 a b c d e => - -- we know that d.testBit = false from 'e' - -- we know that x.msb = true by 'h'. - sorry +/-- +info: 'BitVec.testBit_toInt_eq_getLsb' depends on axioms: [propext, Classical.choice, Quot.sound, sorryAx] +-/ +#guard_msgs in #print axioms testBit_toInt_eq_getLsb + + + -- rw [Int.testBit] @[simp] theorem toInt_zero : (0#w).toInt = 0 := by @@ -1332,15 +1419,27 @@ theorem ofInt_ofNat (n : Nat) : BitVec.ofInt w (Int.ofNat n) = n#w := by apply eq_of_toNat_eq simp -@[simp] theorem getLsb_ofInt (n : Nat) (x : Int) (i : Nat) : - getLsb (BitVec.ofInt n x) i = (i < n && x.testBit i) := by - cases x - case ofNat x => - rw [ofInt_ofNat] - simp - rw [getLsb_ofNat] - case negSucc x => - sorry + +@[simp] theorem getLsb_ofInt (w : Nat) (x : Int) (i : Nat) : + getLsb (BitVec.ofInt w x) i = (i < w && x.testBit i) := by + rcases w with rfl | w + · simp only [Nat.zero_le, getLsb_ge, Bool.false_eq, Bool.and_eq_false_imp, decide_eq_true_eq] + intros Hcontra + omega + · by_cases (i < w + 1) + case pos h => + simp [h]; + rw [BitVec.ofInt] + simp + + -- rw [getLsb] + -- rw [← toInt_testBit_eq_toNat_testBit h] + -- simp + sorry + case neg h => + simp [h] + apply getLsb_ge + omega theorem getLsb_sshiftRight (x : BitVec n) (s i : Nat) : getLsb (x.sshiftRight s) i = From 1029f69616bc304e185e88850a69224469527912 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 15 May 2024 15:08:09 +0100 Subject: [PATCH 11/15] feat: show easy cases unconditionally --- src/Init/Data/BitVec/Lemmas.lean | 112 +++++++++++++++++++++----- src/Init/Data/Int/Bitwise/Lemmas.lean | 10 ++- 2 files changed, 97 insertions(+), 25 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 9c60af5c77aa..686a08210804 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -11,6 +11,9 @@ import Init.Data.Fin.Lemmas import Init.Data.Nat.Lemmas import Init.Data.Int.Bitwise.Lemmas import Init.Data.BitVec.Basic +import Init.Data.Nat.Div +import Init.Data.Int.DivModLemmas +import Init.Data.Int.DivMod namespace BitVec @@ -1328,8 +1331,7 @@ case inl h => case inr h => rcases w with rfl | w · simp at h - · have hx : x.toNat ≥ 2^w := by omega - have hx' : x.toNat < 2^(w + 1) := by omega + · have hx' : x.toNat < 2^(w + 1) := by omega have hz := Int.toNat_sub_toNat_eq_negSucc_ofLt hx' rw [hz] simp @@ -1349,17 +1351,12 @@ info: 'BitVec.testBit_toInt_eq_msb' depends on axioms: [propext, Classical.choic -/ #guard_msgs in #print axioms testBit_toInt_eq_msb + + /-! # Theorems that need sorry below -/ -/-- subtracting a bit 2^w does not change the value of testBit. - TODO: unclear how true this is. -/ -private theorem Int.testBit_sub_big (x : Nat) (w : Nat) (hi: i < w): - ((x : Int) - ((((2 : Nat)^w) : Nat) : Int)).testBit i = x.testBit i := by - simp [Int.testBit] - sorry - -#print axioms Int.testBit_sub_big + -- If the index is larger than the bitwidth and the integer is negative, -- then the left hand side gives '1' and the right hand side gives '0'. theorem toInt_testBit_eq_toNat_testBit {x : BitVec w} (hi : i < w): @@ -1431,24 +1428,97 @@ theorem ofInt_ofNat (n : Nat) : BitVec.ofInt w (Int.ofNat n) = n#w := by simp [h]; rw [BitVec.ofInt] simp - - -- rw [getLsb] - -- rw [← toInt_testBit_eq_toNat_testBit h] - -- simp - sorry + generalize hx':(x % (((2 : Nat)^(w + 1) : Nat) : Int)) = x' + rw [Int.toNat] + rcases x' with x' | x' + case ofNat => + simp + sorry + case negSucc => + simp + sorry case neg h => simp [h] apply getLsb_ge omega -theorem getLsb_sshiftRight (x : BitVec n) (s i : Nat) : + +-- #reduce (-1 : Int) % 7 +-- #reduce (-2 : Int) % 7 +-- #reduce (-3 : Int) % 7 +-- #reduce (-4 : Int) % 7 +-- #reduce (-5 : Int) % 7 +-- #reduce (-6 : Int) % 7 +-- #reduce (-7 : Int) % 7 +-- #reduce (-8 : Int) % 7 + +-- #check Int.mod_eq_emod +-- theorem mod_eq_of_neg {a b : Int} (H1 : a < 0) (hb : b ≥ 0) (H2 : a < b) : a % b = (b - a) := by +-- simp +-- omega + +axiom notSorry {α : Prop} : α + + +theorem getLsb_sshiftRight (x : BitVec w) (s i : Nat) : getLsb (x.sshiftRight s) i = - if i ≥ n then false - else if (s + i) < n then getLsb x (s + i) + if i ≥ w then false + else if (s + i) < w then getLsb x (s + i) else x.msb := by rw [sshiftRight_eq] - rw [getLsb_ofInt] - rw [Int.testBit_shiftRight] + rw [BitVec.ofInt_eq_ofNat_emod] + rw [BitVec.getLsb] + simp + rw [BitVec.toInt] + rcases w with rfl | w + · simp + · by_cases hxtoNat:(2 * x.toNat < 2 ^ (w + 1)) + · simp [hxtoNat] + rw [Int.emod_eq_of_lt] + simp only [Int.toNat_ofNat, Nat.testBit_shiftRight] + by_cases hiltw:(i < w + 1) + have hiltw' : ¬ (w + 1) ≤ i := by omega + simp only [hiltw', decide_False, Bool.not_false, Bool.true_and] + by_cases hsplusi : (s + i) < w+1 + · simp only [hsplusi, ↓reduceIte] + rw [BitVec.getLsb] + simp only [hiltw, decide_True, Bool.true_and] + · simp only [hiltw, decide_True, Bool.true_and, hsplusi, ↓reduceIte] + rw [testBit_toNat] + rw [msb_eq_false_iff_small.mpr (by omega)] + rw [getLsb_ge] + omega + · simp [hiltw] + · apply Int.ofNat_zero_le + · norm_cast + rw [Nat.shiftRight_eq_div_pow] + have htwopow : (2 : Int) ^ (w + 1) = (((2 : Nat) ^ (w + 1) : Nat) : Int) := by + simp [Int.natCast_pow] + rw [htwopow] + norm_cast + have hleq : x.toNat / 2^s ≤ x.toNat := by + apply Nat.div_le_self + omega + · simp [hxtoNat] + rw [Int.toNat_sub_toNat_eq_negSucc_ofLt] + · simp [Int.shiftRight_negSucc] + -- hard case + /- + case neg + s i w : Nat + x : BitVec (w + 1) + hxtoNat : ¬2 * x.toNat < 2 ^ (w + 1) + ⊢ (decide (i < w + 1) && (Int.negSucc ((2 ^ (w + 1) - 1 - x.toNat) >>> s) % 2 ^ (w + 1)).toNat.testBit i) = + (!decide (w + 1 ≤ i) && if s + i < w + 1 then x.getLsb (s + i) else x.msb) + -/ + exact notSorry + · omega + +/-- +info: 'BitVec.getLsb_sshiftRight' depends on axioms: [propext, Classical.choice, Quot.sound, BitVec.notSorry] +-/ +#guard_msgs in #print axioms getLsb_sshiftRight +/- by_cases h₁:i < n <;> simp [h₁] by_cases h₂:(s + i < n) <;> simp [h₂] case pos => @@ -1460,5 +1530,5 @@ theorem getLsb_sshiftRight (x : BitVec n) (s i : Nat) : · simp only [Bool.iff_and_self, Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_le] omega · omega - +-/ end BitVec diff --git a/src/Init/Data/Int/Bitwise/Lemmas.lean b/src/Init/Data/Int/Bitwise/Lemmas.lean index 3f20e9822cde..d3edf650c62f 100644 --- a/src/Init/Data/Int/Bitwise/Lemmas.lean +++ b/src/Init/Data/Int/Bitwise/Lemmas.lean @@ -85,12 +85,14 @@ private theorem Int.mod2_cases (x : Int) : (x % 2 = 0) ∨ (x % 2 = 1) := by ome unfold testBit cases x <;> simp <;> rfl -theorem toNat_testBit (x i : Nat) : - (x.testBit i).toNat = x / 2 ^ i % 2 := by - rw [Nat.testBit_to_div_mod] - rcases Nat.mod_two_eq_zero_or_one (x / 2^i) <;> simp_all + +-- theorem toNat_testBit (x i : Nat) : +-- (x.testBit i).toNat = x / 2 ^ i % 2 := by +-- rw [Nat.testBit_to_div_mod] +-- rcases Nat.mod_two_eq_zero_or_one (x / 2^i) <;> simp_all @[simp] theorem testBit_shiftRight (x : Int) (i j : Nat) : testBit (x >>> i) j = testBit x (i+j) := by cases x <;> simp [testBit] + end Int From 968b2719c3109234929e4ade4f229ad4ffc39cb5 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 15 May 2024 15:19:46 +0100 Subject: [PATCH 12/15] feat: more progress --- src/Init/Data/BitVec/Lemmas.lean | 46 +++++++++++++++++++++++++------- 1 file changed, 36 insertions(+), 10 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 686a08210804..fb9754fb38f8 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1502,16 +1502,42 @@ theorem getLsb_sshiftRight (x : BitVec w) (s i : Nat) : · simp [hxtoNat] rw [Int.toNat_sub_toNat_eq_negSucc_ofLt] · simp [Int.shiftRight_negSucc] - -- hard case - /- - case neg - s i w : Nat - x : BitVec (w + 1) - hxtoNat : ¬2 * x.toNat < 2 ^ (w + 1) - ⊢ (decide (i < w + 1) && (Int.negSucc ((2 ^ (w + 1) - 1 - x.toNat) >>> s) % 2 ^ (w + 1)).toNat.testBit i) = - (!decide (w + 1 ≤ i) && if s + i < w + 1 then x.getLsb (s + i) else x.msb) - -/ - exact notSorry + by_cases hiltw:(i < w + 1) + · simp [hiltw] + have hiltw' : ¬ (w + 1) ≤ i := by omega + simp [hiltw'] + by_cases hsplusi : (s + i) < w+1 + · simp [hsplusi] + rw [BitVec.getLsb] + rw [Nat.shiftRight_eq_div_pow] + have hx : x.toNat ≥ 2^w := by omega + /- + case pos + s i w : Nat + x : BitVec (w + 1) + hxtoNat : ¬2 * x.toNat < 2 ^ (w + 1) + hiltw : i < w + 1 + hiltw' : ¬w + 1 ≤ i + hsplusi : s + i < w + 1 + hx : x.toNat ≥ 2 ^ w + ⊢ (Int.negSucc ((2 ^ (w + 1) - 1 - x.toNat) / 2 ^ s) % 2 ^ (w + 1)).toNat.testBit i = x.toNat.testBit (s + i) + -/ + + exact notSorry + · simp [hsplusi] + /- + case neg + s i w : Nat + x : BitVec (w + 1) + hxtoNat : ¬2 * x.toNat < 2 ^ (w + 1) + hiltw : i < w + 1 + hiltw' : ¬w + 1 ≤ i + hsplusi : ¬s + i < w + 1 + ⊢ (Int.negSucc ((2 ^ (w + 1) - 1 - x.toNat) >>> s) % 2 ^ (w + 1)).toNat.testBit i = x.msb + -/ + + exact notSorry + · simp [hiltw] · omega /-- From 187d150825109c543ca1df4fce262566a3f163a2 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 15 May 2024 15:57:57 +0100 Subject: [PATCH 13/15] checkpoint --- src/Init/Data/BitVec/Lemmas.lean | 57 ++++++++++++++++---------------- 1 file changed, 29 insertions(+), 28 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index fb9754fb38f8..d648764533cd 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1456,9 +1456,18 @@ theorem ofInt_ofNat (n : Nat) : BitVec.ofInt w (Int.ofNat n) = n#w := by -- theorem mod_eq_of_neg {a b : Int} (H1 : a < 0) (hb : b ≥ 0) (H2 : a < b) : a % b = (b - a) := by -- simp -- omega +theorem Int.mod_ofNat_eq (m : Nat) (n : Int) : + (Int.ofNat m) % n = Int.ofNat (m % Int.natAbs n) := rfl + +theorem Int.mod_negSucc_eq (m : Nat) (n : Int) : + (Int.negSucc m) % n = Int.subNatNat (Int.natAbs n) (Nat.succ (m % Int.natAbs n)) := rfl axiom notSorry {α : Prop} : α +-- @[simp] +theorem ofNat_two_pow_eq (n : Nat) : (((2 : Int) ^n) : Int) = (((2 : Nat) ^n : Nat) : Int) := by + rw [Int.natCast_pow] + simp theorem getLsb_sshiftRight (x : BitVec w) (s i : Nat) : getLsb (x.sshiftRight s) i = @@ -1492,9 +1501,7 @@ theorem getLsb_sshiftRight (x : BitVec w) (s i : Nat) : · apply Int.ofNat_zero_le · norm_cast rw [Nat.shiftRight_eq_div_pow] - have htwopow : (2 : Int) ^ (w + 1) = (((2 : Nat) ^ (w + 1) : Nat) : Int) := by - simp [Int.natCast_pow] - rw [htwopow] + rw [ofNat_two_pow_eq] norm_cast have hleq : x.toNat / 2^s ≤ x.toNat := by apply Nat.div_le_self @@ -1507,35 +1514,29 @@ theorem getLsb_sshiftRight (x : BitVec w) (s i : Nat) : have hiltw' : ¬ (w + 1) ≤ i := by omega simp [hiltw'] by_cases hsplusi : (s + i) < w+1 + rw [Int.mod_negSucc_eq] + simp only [Nat.succ_eq_add_one] · simp [hsplusi] rw [BitVec.getLsb] rw [Nat.shiftRight_eq_div_pow] - have hx : x.toNat ≥ 2^w := by omega - /- - case pos - s i w : Nat - x : BitVec (w + 1) - hxtoNat : ¬2 * x.toNat < 2 ^ (w + 1) - hiltw : i < w + 1 - hiltw' : ¬w + 1 ≤ i - hsplusi : s + i < w + 1 - hx : x.toNat ≥ 2 ^ w - ⊢ (Int.negSucc ((2 ^ (w + 1) - 1 - x.toNat) / 2 ^ s) % 2 ^ (w + 1)).toNat.testBit i = x.toNat.testBit (s + i) - -/ - - exact notSorry + simp only [ofNat_two_pow_eq, Int.natAbs_ofNat] + have hexpr : ((2 ^ (w + 1) - 1 - x.toNat) / 2 ^ s % 2 ^ (w + 1) + 1) = ((2 ^ (w + 1) - 1 - x.toNat) / 2 ^ s + 1) := by + rw [Nat.mod_eq_of_lt] + apply Nat.lt_of_le_of_lt + apply Nat.div_le_self + omega + rw [hexpr] + clear hexpr -- TODO: suffices + rw [Int.subNatNat_of_le] + · exact notSorry + · suffices (2 ^ (w + 1) - 1 - x.toNat) / 2 ^ s + 1 ≤ (2 ^ (w + 1) - 1 - x.toNat) + 1 by + simp only [ge_iff_le] + apply Nat.le_trans + · apply this + · omega + apply Nat.add_le_add_right + apply Nat.div_le_self · simp [hsplusi] - /- - case neg - s i w : Nat - x : BitVec (w + 1) - hxtoNat : ¬2 * x.toNat < 2 ^ (w + 1) - hiltw : i < w + 1 - hiltw' : ¬w + 1 ≤ i - hsplusi : ¬s + i < w + 1 - ⊢ (Int.negSucc ((2 ^ (w + 1) - 1 - x.toNat) >>> s) % 2 ^ (w + 1)).toNat.testBit i = x.msb - -/ - exact notSorry · simp [hiltw] · omega From 2940f48ddeced2b6e681a3a977cb462c49b7d178 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 15 May 2024 16:40:08 +0100 Subject: [PATCH 14/15] feat: finish proof --- src/Init/Data/BitVec/Lemmas.lean | 91 +++++++++++++++++--------------- 1 file changed, 49 insertions(+), 42 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index d648764533cd..0706358d82eb 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1469,6 +1469,9 @@ theorem ofNat_two_pow_eq (n : Nat) : (((2 : Int) ^n) : Int) = (((2 : Nat) ^n : N rw [Int.natCast_pow] simp +theorem Nat.sub_add_comm' {a b c : Nat} (h : a ≥ b + c) : a - (b + c) = (a - c) - b:= by + omega + theorem getLsb_sshiftRight (x : BitVec w) (s i : Nat) : getLsb (x.sshiftRight s) i = if i ≥ w then false @@ -1508,54 +1511,58 @@ theorem getLsb_sshiftRight (x : BitVec w) (s i : Nat) : omega · simp [hxtoNat] rw [Int.toNat_sub_toNat_eq_negSucc_ofLt] - · simp [Int.shiftRight_negSucc] + rw [Int.shiftRight_negSucc] + rw [Int.mod_negSucc_eq] + simp only [Nat.succ_eq_add_one] + rw [BitVec.getLsb] + rw [Nat.shiftRight_eq_div_pow] + simp only [ofNat_two_pow_eq, Int.natAbs_ofNat] + have hexpr : ((2 ^ (w + 1) - 1 - x.toNat) / 2 ^ s % 2 ^ (w + 1) + 1) = ((2 ^ (w + 1) - 1 - x.toNat) / 2 ^ s + 1) := by + rw [Nat.mod_eq_of_lt] + apply Nat.lt_of_le_of_lt + apply Nat.div_le_self + omega + rw [hexpr] + clear hexpr + rw [Int.subNatNat_of_le] + · simp only [Int.toNat_ofNat] by_cases hiltw:(i < w + 1) · simp [hiltw] have hiltw' : ¬ (w + 1) ≤ i := by omega simp [hiltw'] - by_cases hsplusi : (s + i) < w+1 - rw [Int.mod_negSucc_eq] - simp only [Nat.succ_eq_add_one] - · simp [hsplusi] - rw [BitVec.getLsb] - rw [Nat.shiftRight_eq_div_pow] - simp only [ofNat_two_pow_eq, Int.natAbs_ofNat] - have hexpr : ((2 ^ (w + 1) - 1 - x.toNat) / 2 ^ s % 2 ^ (w + 1) + 1) = ((2 ^ (w + 1) - 1 - x.toNat) / 2 ^ s + 1) := by - rw [Nat.mod_eq_of_lt] - apply Nat.lt_of_le_of_lt - apply Nat.div_le_self - omega - rw [hexpr] - clear hexpr -- TODO: suffices - rw [Int.subNatNat_of_le] - · exact notSorry - · suffices (2 ^ (w + 1) - 1 - x.toNat) / 2 ^ s + 1 ≤ (2 ^ (w + 1) - 1 - x.toNat) + 1 by - simp only [ge_iff_le] - apply Nat.le_trans - · apply this - · omega - apply Nat.add_le_add_right - apply Nat.div_le_self - · simp [hsplusi] - exact notSorry + rw [← Nat.shiftRight_eq_div_pow] + -- repeat rw [Nat.testBit] + rw [← toNat_allOnes] + have hx : (BitVec.allOnes (w + 1)).toNat - x.toNat = (~~~ x).toNat := by simp + rw [hx]; clear hx + have hx {k : Nat} (x : BitVec k) (i : Nat) : x.toNat >>> i = (x.ushiftRight i).toNat := rfl + rw [hx] + rw [Nat.sub_add_comm'] + rw [← toNat_allOnes] + have hx : (allOnes (w + 1)).toNat - ((~~~x).ushiftRight s).toNat = + (~~~(((~~~x).ushiftRight s))).toNat := by simp + rw [hx]; clear hx + rw [← getLsb] + simp + have hi : i < w + 1 := by omega + simp [hi]; clear hi + by_cases hs : (s + i) < (w + 1) + · simp [hs] + rfl + · simp [hs] + apply msb_eq_true_iff_large.mpr + omega + omega · simp [hiltw] + · have hexpr : (2 ^ (w + 1) - 1 - x.toNat) / 2 ^ s + 1 ≤ (2 ^ (w + 1) - 1 - x.toNat) + 1 := by + apply Nat.add_le_add_right + apply Nat.div_le_self + apply Nat.le_trans + exact hexpr + omega · omega -/-- -info: 'BitVec.getLsb_sshiftRight' depends on axioms: [propext, Classical.choice, Quot.sound, BitVec.notSorry] --/ +/-- info: 'BitVec.getLsb_sshiftRight' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms getLsb_sshiftRight -/- - by_cases h₁:i < n <;> simp [h₁] - by_cases h₂:(s + i < n) <;> simp [h₂] - case pos => - rw [testBit_toInt_eq_getLsb (by assumption)] - simp only [Bool.iff_and_self, Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_le, h₁, - implies_true] - case neg => - rw [testBit_toInt_eq_msb] - · simp only [Bool.iff_and_self, Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_le] - omega - · omega --/ + end BitVec From 7117789f7cd5834f844d60041b42a85b217bb07a Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 15 May 2024 17:51:32 +0100 Subject: [PATCH 15/15] feat: cleaned up proof This contains the development of everything, not just the core theorem I set out to prove. Will need to as Kim if I also PR the rest. --- src/Init/Data/BitVec/Lemmas.lean | 327 +++++++------------------------ 1 file changed, 74 insertions(+), 253 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 0706358d82eb..3a300a47146c 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1226,51 +1226,14 @@ theorem Int.negSucc_div_ofNat (a b : Nat) (hb : b ≠ 0) : · contradiction · norm_cast -#check Int.ediv -#reduce (Int.negSucc 4) % (Int.ofNat 1) -- 0 -#reduce (Int.negSucc 4) % (Int.ofNat 1) -- 0 -#reduce (Int.negSucc 4) % (Int.ofNat 1) -- 0 -#reduce (Int.negSucc 4) % (Int.ofNat 1) -- 0 -#reduce (Int.negSucc 4) % (Int.ofNat 1) -- 0 - -#reduce (Int.negSucc 0) % (Int.ofNat 8) -- 7 -#reduce (Int.negSucc 1) % (Int.ofNat 8) -- 6 -#reduce (Int.negSucc 2) % (Int.ofNat 8) -- 5 -#reduce (Int.negSucc 3) % (Int.ofNat 8) -- 4 -#reduce (Int.negSucc 4) % (Int.ofNat 8) -- 3 -#reduce (Int.negSucc 5) % (Int.ofNat 8) -- 2 -#reduce (Int.negSucc 6) % (Int.ofNat 8) -- 1 -#reduce (Int.negSucc 7) % (Int.ofNat 8) -- 0 -#reduce (Int.negSucc 8) % (Int.ofNat 8) -- 7 -#reduce (Int.negSucc 9) % (Int.ofNat 8) -- 6 -#reduce (Int.negSucc 10) % (Int.ofNat 8) -- 5 -#reduce (Int.negSucc 11) % (Int.ofNat 8) -- 4 -#reduce (Int.negSucc 12) % (Int.ofNat 8) -- 3 -#reduce (Int.negSucc 13) % (Int.ofNat 8) -- 2 -#reduce (Int.negSucc 14) % (Int.ofNat 8) -- 1 -#reduce (Int.negSucc 15) % (Int.ofNat 8) -- 0 -#reduce (Int.negSucc 16) % (Int.ofNat 8) -- 1 -#reduce (Int.negSucc 17) % (Int.ofNat 8) -- 2 -#reduce (Int.negSucc 18) % (Int.ofNat 8) - -#check Nat.emod_pos_of_not_dvd - @[simp] theorem toInt_sshiftRight (x : BitVec n) (i : Nat) : (x.sshiftRight i).toInt = (x.toInt >>> i).bmod (2^n) := by rw [sshiftRight_eq, BitVec.toInt_ofInt] -/-- info: 'BitVec.toInt_sshiftRight' depends on axioms: [propext, Classical.choice, Quot.sound] -/ -#guard_msgs in #print axioms toInt_sshiftRight @[simp] private theorem Int.ofNat_sub_ofNat_eq_ofNat_implies_eq_ofNat_sub {x y : Nat} (h : (x : Int) - (y : Int) = Int.ofNat z) : (x : Int) - (y : Int) = ((x - y : Nat) : Int) := by simp at h omega -/-- -info: '_private.Init.Data.BitVec.Lemmas.0.BitVec.Int.ofNat_sub_ofNat_eq_ofNat_implies_eq_ofNat_sub' depends on axioms: [propext, - Classical.choice, - Quot.sound] --/ -#guard_msgs in #print axioms Int.ofNat_sub_ofNat_eq_ofNat_implies_eq_ofNat_sub /-- (n₁ : Int) - (n₂ : Int) = (n₃ : Int) for n₁, n₂, n₃ naturals iff n₁ ≥ n₂ -/ private theorem Int.sub_sub_eq_ofNat_iff_geq {x y : Nat} : (∃ (z : Nat), (x : Int) - (y : Int) = Int.ofNat z) ↔ x ≥ y := by @@ -1283,13 +1246,6 @@ private theorem Int.sub_sub_eq_ofNat_iff_geq {x y : Nat} : simp only [Int.ofNat_eq_coe] omega -/-- -info: '_private.Init.Data.BitVec.Lemmas.0.BitVec.Int.sub_sub_eq_ofNat_iff_geq' depends on axioms: [propext, - Classical.choice, - Quot.sound] --/ -#guard_msgs in #print axioms Int.sub_sub_eq_ofNat_iff_geq - /-- (n₁ : Int) - (n₂ : Int) = (negSucc n₃) for n₁, n₂, n₃ naturals iff n₁ < n₂ -/ private theorem Int.sub_sub_eq_negSucc_implies_le {x y : Nat} (h : ∃ (z : Nat), (x : Int) - (y : Int) = Int.negSucc z) : x < y := by @@ -1301,24 +1257,33 @@ private theorem Int.sub_sub_eq_negSucc_implies_le {x y : Nat} obtain ⟨w, hw⟩ := h contradiction -/-- -info: '_private.Init.Data.BitVec.Lemmas.0.BitVec.Int.sub_sub_eq_negSucc_implies_le' depends on axioms: [propext, - Classical.choice, - Quot.sound] --/ -#guard_msgs in #print axioms Int.sub_sub_eq_negSucc_implies_le - theorem Int.toNat_sub_toNat_eq_negSucc_ofLt {n m : Nat} (hlt : n < m) : (n : Int) - (m : Int) = (Int.negSucc (m - 1 - n)) := by rw [Int.negSucc_eq] -- TODO: consider adding this to omega cleanup set. omega -/-- -info: 'BitVec.Int.toNat_sub_toNat_eq_negSucc_ofLt' depends on axioms: [propext, Classical.choice, Quot.sound] --/ -#guard_msgs in #print axioms Int.toNat_sub_toNat_eq_negSucc_ofLt - +/-- Testing the ith bit of `x.toInt` is the same as testing `x.toNat`-/ +theorem testBit_toInt_eq_testBit_toNat {x : BitVec w} (hi : i < w) : + x.toInt.testBit i = x.toNat.testBit i := by +rw [BitVec.toInt] +rcases w with rfl | w +· omega +· by_cases hx : x.toNat < 2^w + · have hx' : 2 * x.toNat < 2 ^ (w + 1) := by omega + simp [hx'] + · have hx' : ¬ (2 * x.toNat < 2 ^ (w + 1)) := by omega + simp [hx'] + rw [Int.toNat_sub_toNat_eq_negSucc_ofLt (by omega)] + simp + suffices 2 ^ (w + 1) - 1 - x.toNat = (~~~ x).toNat by + rw [this] + rw [← getLsb] + simp [hi] + rfl + simp +/-- the value of testBit of the integer value, + when the index being tested is larger or equal to the bitwidth is the msb of the bitvector. -/ theorem testBit_toInt_eq_msb {x : BitVec w} (hi : i ≥ w) : x.toInt.testBit i = x.msb := by rw [BitVec.toInt] @@ -1352,217 +1317,73 @@ info: 'BitVec.testBit_toInt_eq_msb' depends on axioms: [propext, Classical.choic #guard_msgs in #print axioms testBit_toInt_eq_msb +private theorem Int.mod_ofNat_eq (m : Nat) (n : Int) : + (Int.ofNat m) % n = Int.ofNat (m % Int.natAbs n) := rfl -/-! -# Theorems that need sorry below --/ +private theorem Int.mod_negSucc_eq (m : Nat) (n : Int) : + (Int.negSucc m) % n = Int.subNatNat (Int.natAbs n) (Nat.succ (m % Int.natAbs n)) := rfl --- If the index is larger than the bitwidth and the integer is negative, --- then the left hand side gives '1' and the right hand side gives '0'. -theorem toInt_testBit_eq_toNat_testBit {x : BitVec w} (hi : i < w): - x.toInt.testBit i = x.toNat.testBit i := by +/-- if the msb is false, the arithmetic shift right equals logical shift right -/ +theorem sshiftRight_eq_of_msb_false {x : BitVec w} {s : Nat} (h : x.msb = false) : + (x.sshiftRight s) = x.ushiftRight s := by rcases w with rfl | w - case zero => - simp [toInt_eq_toNat_bmod] - case succ => - simp only [toInt_eq_toNat_cond] - split - case inl => simp only [Int.testBit_natCast] - case inr h => - rw [Int.testBit] - split - case h_1 a b c d e => - simp at e - omega - case h_2 a b c d e => - have hcontra : x.toNat ≥ 2 ^ w := by omega - have hcontra' : x.toNat < 2^(w + 1) := by omega - have hd := Int.toNat_sub_toNat_eq_negSucc_ofLt hcontra' - rw [hd] at e - simp at e - rw [← e] - sorry - -- simp [Nat.testBit] - -- rw [Nat.shiftRight_eq_div_pow] - -/-- -info: 'BitVec.toInt_testBit_eq_toNat_testBit' depends on axioms: [propext, Classical.choice, Quot.sound, sorryAx] --/ -#guard_msgs in #print axioms toInt_testBit_eq_toNat_testBit - -theorem testBit_toInt_eq_getLsb {x : BitVec w} (hi : i < w) : - x.toInt.testBit i = x.getLsb i := by - rw [toInt_testBit_eq_toNat_testBit hi] - rfl - -/-- -info: 'BitVec.testBit_toInt_eq_getLsb' depends on axioms: [propext, Classical.choice, Quot.sound, sorryAx] --/ -#guard_msgs in #print axioms testBit_toInt_eq_getLsb - - - -- rw [Int.testBit] - -@[simp] -theorem toInt_zero : (0#w).toInt = 0 := by - simp [toInt_eq_toNat_bmod] - -@[simp] -theorem toInt_neg (x : BitVec w) : - (-x).toInt = (((((2 : Nat) ^ w) - x.toNat) : Nat) : Int).bmod (2 ^ w) := by - simp [toInt_eq_toNat_bmod] - -theorem ofInt_ofNat (n : Nat) : BitVec.ofInt w (Int.ofNat n) = n#w := by - apply eq_of_toNat_eq - simp - + · rw [Subsingleton.elim x (0#0)] + simp [ushiftRight, sshiftRight] + rfl + · apply BitVec.eq_of_toNat_eq + rw [BitVec.sshiftRight_eq] + rw [BitVec.toInt_eq_toNat_cond] + have hxbound : 2 * x.toNat < 2 ^ (w + 1) := BitVec.msb_eq_false_iff_small.mp h + simp [hxbound] + rw [Nat.mod_eq_of_lt] + rw [Nat.shiftRight_eq_div_pow] + suffices x.toNat / 2^s ≤ x.toNat by + apply Nat.lt_of_le_of_lt this x.isLt + apply Nat.div_le_self -@[simp] theorem getLsb_ofInt (w : Nat) (x : Int) (i : Nat) : - getLsb (BitVec.ofInt w x) i = (i < w && x.testBit i) := by +/-- if the msb is true, the arithmetic shift right equals negating, the logical shifting right, then negating again -/ +theorem sshiftRight_eq_of_msb_true {x : BitVec w} {s : Nat} (h : x.msb = true) : + (x.sshiftRight s) = ~~~((~~~x).ushiftRight s) := by rcases w with rfl | w - · simp only [Nat.zero_le, getLsb_ge, Bool.false_eq, Bool.and_eq_false_imp, decide_eq_true_eq] - intros Hcontra + · apply BitVec.eq_of_toNat_eq + simp + · apply BitVec.eq_of_toNat_eq + rw [BitVec.sshiftRight_eq] + rw [BitVec.toInt_eq_toNat_cond] + have hxbound : (2 * x.toNat ≥ 2 ^ (w + 1)) := BitVec.msb_eq_true_iff_large.mp h + have hxbound' : ¬ (2 * x.toNat < 2 ^ (w + 1)) := by omega + simp [hxbound'] + rw [Int.toNat_sub_toNat_eq_negSucc_ofLt (by omega)] + rw [Int.shiftRight_negSucc] + rw [Int.mod_negSucc_eq] + simp only [Int.natAbs_ofNat, Nat.succ_eq_add_one] + rw [Int.subNatNat_of_le] + simp + rw [Nat.mod_eq_of_lt] omega - · by_cases (i < w + 1) - case pos h => - simp [h]; - rw [BitVec.ofInt] - simp - generalize hx':(x % (((2 : Nat)^(w + 1) : Nat) : Int)) = x' - rw [Int.toNat] - rcases x' with x' | x' - case ofNat => - simp - sorry - case negSucc => - simp - sorry - case neg h => - simp [h] - apply getLsb_ge + rw [Nat.shiftRight_eq_div_pow] + suffices (2 ^ (w + 1) - 1 - x.toNat) / 2 ^ s < 2 ^ (w + 1) - 1 by omega - - --- #reduce (-1 : Int) % 7 --- #reduce (-2 : Int) % 7 --- #reduce (-3 : Int) % 7 --- #reduce (-4 : Int) % 7 --- #reduce (-5 : Int) % 7 --- #reduce (-6 : Int) % 7 --- #reduce (-7 : Int) % 7 --- #reduce (-8 : Int) % 7 - --- #check Int.mod_eq_emod --- theorem mod_eq_of_neg {a b : Int} (H1 : a < 0) (hb : b ≥ 0) (H2 : a < b) : a % b = (b - a) := by --- simp --- omega -theorem Int.mod_ofNat_eq (m : Nat) (n : Int) : - (Int.ofNat m) % n = Int.ofNat (m % Int.natAbs n) := rfl - -theorem Int.mod_negSucc_eq (m : Nat) (n : Int) : - (Int.negSucc m) % n = Int.subNatNat (Int.natAbs n) (Nat.succ (m % Int.natAbs n)) := rfl - -axiom notSorry {α : Prop} : α - --- @[simp] -theorem ofNat_two_pow_eq (n : Nat) : (((2 : Int) ^n) : Int) = (((2 : Nat) ^n : Nat) : Int) := by - rw [Int.natCast_pow] - simp - -theorem Nat.sub_add_comm' {a b c : Nat} (h : a ≥ b + c) : a - (b + c) = (a - c) - b:= by - omega + apply Nat.lt_of_le_of_lt (Nat.div_le_self _ _) (by omega) + omega theorem getLsb_sshiftRight (x : BitVec w) (s i : Nat) : getLsb (x.sshiftRight s) i = if i ≥ w then false else if (s + i) < w then getLsb x (s + i) else x.msb := by - rw [sshiftRight_eq] - rw [BitVec.ofInt_eq_ofNat_emod] - rw [BitVec.getLsb] - simp - rw [BitVec.toInt] - rcases w with rfl | w - · simp - · by_cases hxtoNat:(2 * x.toNat < 2 ^ (w + 1)) - · simp [hxtoNat] - rw [Int.emod_eq_of_lt] - simp only [Int.toNat_ofNat, Nat.testBit_shiftRight] - by_cases hiltw:(i < w + 1) - have hiltw' : ¬ (w + 1) ≤ i := by omega - simp only [hiltw', decide_False, Bool.not_false, Bool.true_and] - by_cases hsplusi : (s + i) < w+1 - · simp only [hsplusi, ↓reduceIte] - rw [BitVec.getLsb] - simp only [hiltw, decide_True, Bool.true_and] - · simp only [hiltw, decide_True, Bool.true_and, hsplusi, ↓reduceIte] - rw [testBit_toNat] - rw [msb_eq_false_iff_small.mpr (by omega)] - rw [getLsb_ge] - omega - · simp [hiltw] - · apply Int.ofNat_zero_le - · norm_cast - rw [Nat.shiftRight_eq_div_pow] - rw [ofNat_two_pow_eq] - norm_cast - have hleq : x.toNat / 2^s ≤ x.toNat := by - apply Nat.div_le_self - omega - · simp [hxtoNat] - rw [Int.toNat_sub_toNat_eq_negSucc_ofLt] - rw [Int.shiftRight_negSucc] - rw [Int.mod_negSucc_eq] - simp only [Nat.succ_eq_add_one] - rw [BitVec.getLsb] - rw [Nat.shiftRight_eq_div_pow] - simp only [ofNat_two_pow_eq, Int.natAbs_ofNat] - have hexpr : ((2 ^ (w + 1) - 1 - x.toNat) / 2 ^ s % 2 ^ (w + 1) + 1) = ((2 ^ (w + 1) - 1 - x.toNat) / 2 ^ s + 1) := by - rw [Nat.mod_eq_of_lt] - apply Nat.lt_of_le_of_lt - apply Nat.div_le_self - omega - rw [hexpr] - clear hexpr - rw [Int.subNatNat_of_le] - · simp only [Int.toNat_ofNat] - by_cases hiltw:(i < w + 1) - · simp [hiltw] - have hiltw' : ¬ (w + 1) ≤ i := by omega - simp [hiltw'] - rw [← Nat.shiftRight_eq_div_pow] - -- repeat rw [Nat.testBit] - rw [← toNat_allOnes] - have hx : (BitVec.allOnes (w + 1)).toNat - x.toNat = (~~~ x).toNat := by simp - rw [hx]; clear hx - have hx {k : Nat} (x : BitVec k) (i : Nat) : x.toNat >>> i = (x.ushiftRight i).toNat := rfl - rw [hx] - rw [Nat.sub_add_comm'] - rw [← toNat_allOnes] - have hx : (allOnes (w + 1)).toNat - ((~~~x).ushiftRight s).toNat = - (~~~(((~~~x).ushiftRight s))).toNat := by simp - rw [hx]; clear hx - rw [← getLsb] - simp - have hi : i < w + 1 := by omega - simp [hi]; clear hi - by_cases hs : (s + i) < (w + 1) - · simp [hs] - rfl - · simp [hs] - apply msb_eq_true_iff_large.mpr - omega - omega - · simp [hiltw] - · have hexpr : (2 ^ (w + 1) - 1 - x.toNat) / 2 ^ s + 1 ≤ (2 ^ (w + 1) - 1 - x.toNat) + 1 := by - apply Nat.add_le_add_right - apply Nat.div_le_self - apply Nat.le_trans - exact hexpr - omega - · omega + rcases hmsb:x.msb with rfl | rfl + · simp [sshiftRight_eq_of_msb_false hmsb] + by_cases hi : i ≥ w <;> simp [hi] + · apply getLsb_ge + omega + · intros hlsb + apply BitVec.lt_of_getLsb _ _ hlsb + · by_cases hi:(i ≥ w) + · simp [hi] + · simp [hi, sshiftRight_eq_of_msb_true hmsb] <;> omega -/-- info: 'BitVec.getLsb_sshiftRight' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +/-- info: 'BitVec.getLsb_sshiftRight' depends on axioms: [propext, Quot.sound, Classical.choice] -/ #guard_msgs in #print axioms getLsb_sshiftRight end BitVec