From ca6e9270edc081f47386b3868113297ee4e5200b Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Thu, 8 Aug 2024 07:06:15 +0100 Subject: [PATCH] feat: add sshiftRight/shiftLeft_*_distrib --- src/Init/Data/BitVec/Lemmas.lean | 51 ++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 3d4a7d3445d3..f983830d0215 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -559,6 +559,15 @@ theorem and_comm (x y : BitVec w) : rw [← testBit_toNat, getLsb, getLsb] simp +@[simp] theorem getMsb_xor {x y : BitVec w} : + (x ^^^ y).getMsb i = (xor (x.getMsb i) (y.getMsb i)) := by + simp only [getMsb] + by_cases h : i < w <;> simp [h] + +@[simp] theorem msb_xor {x y : BitVec w} : + (x ^^^ y).msb = (xor x.msb y.msb) := by + simp [BitVec.msb] + @[simp] theorem truncate_xor {x y : BitVec w} : (x ^^^ y).truncate k = x.truncate k ^^^ y.truncate k := by ext @@ -651,6 +660,24 @@ theorem zero_shiftLeft (n : Nat) : 0#w <<< n = 0#w := by cases h₁ : decide (i < m) <;> cases h₂ : decide (n ≤ i) <;> cases h₃ : decide (i < n) all_goals { simp_all <;> omega } +theorem shiftLeft_xor_distrib (x y : BitVec w) (n : Nat) : + (x ^^^ y) <<< n = (x <<< n) ^^^ (y <<< n) := by + ext i + simp + by_cases h : (i < n) <;> simp [h] + +theorem shiftLeft_and_distrib (x y : BitVec w) (n : Nat) : + (x &&& y) <<< n = (x <<< n) &&& (y <<< n) := by + ext i + simp + by_cases h : (i < n) <;> simp [h] + +theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) : + (x ||| y) <<< n = (x <<< n) ||| (y <<< n) := by + ext i + simp + by_cases h : (i < n) <;> simp [h] + @[simp] theorem getMsb_shiftLeft (x : BitVec w) (i) : (x <<< i).getMsb k = x.getMsb (k + i) := by simp only [getMsb, getLsb_shiftLeft] @@ -822,6 +849,30 @@ theorem sshiftRight_eq_of_msb_true {x : BitVec w} {s : Nat} (h : x.msb = true) : Nat.not_lt, decide_eq_true_eq] omega +theorem sshiftRight_xor_distrib (x y : BitVec w) (n : Nat) : + (x ^^^ y).sshiftRight n = (x.sshiftRight n) ^^^ (y.sshiftRight n) := by + ext i + simp + split <;> + by_cases w ≤ i <;> + simp [*] + +theorem sshiftRight_and_distrib (x y : BitVec w) (n : Nat) : + (x &&& y).sshiftRight n = (x.sshiftRight n) &&& (y.sshiftRight n) := by + ext i + simp + split <;> + by_cases w ≤ i <;> + simp [*] + +theorem sshiftRight_or_distrib (x y : BitVec w) (n : Nat) : + (x ||| y).sshiftRight n = (x.sshiftRight n) ||| (y.sshiftRight n) := by + ext i + simp + split <;> + by_cases w ≤ i <;> + simp [*] + /-- The msb after arithmetic shifting right equals the original msb. -/ theorem sshiftRight_msb_eq_msb {n : Nat} {x : BitVec w} : (x.sshiftRight n).msb = x.msb := by