From 2b8004101b5509765024efd1c338869696114325 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 20 Feb 2025 17:45:35 +0000 Subject: [PATCH 1/9] feat: theorems --- src/Init/Data/BitVec/Lemmas.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 3f57854a6d22..efe30d4704c2 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -773,6 +773,22 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) : @[simp] theorem extractLsb_toNat (hi lo : Nat) (x : BitVec n) : (extractLsb hi lo x).toNat = (x.toNat >>> lo) % 2^(hi-lo+1) := rfl +@[simp] theorem extractLsb'_toInt (s m : Nat) (x : BitVec n) : + (extractLsb' s m x).toInt = ((x.toNat >>> s) : Int).bmod (2 ^ m) := by + simp [extractLsb', toInt_ofNat] + +@[simp] theorem extractLsb_toInt (hi lo : Nat) (x : BitVec n) : + (extractLsb hi lo x).toInt = ((x.toNat >>> lo) : Int).bmod (2 ^ (hi - lo + 1)) := by + simp [extractLsb, toInt_ofNat] + +@[simp] theorem extractLsb'_toFin (s m : Nat) (x : BitVec n) : + (extractLsb' s m x).toFin = Fin.ofNat' (2 ^ m) (x.toNat >>> s) := by + simp [extractLsb', toInt_ofNat] + +@[simp] theorem extractLsb_toFin (hi lo : Nat) (x : BitVec n) : + (extractLsb hi lo x).toFin = Fin.ofNat' (2 ^ (hi - lo + 1)) (x.toNat >>> lo) := by + simp [extractLsb, toInt_ofNat] + @[simp] theorem getElem_extractLsb' {start len : Nat} {x : BitVec n} {i : Nat} (h : i < len) : (extractLsb' start len x)[i] = x.getLsbD (start+i) := by simp [getElem_eq_testBit_toNat, getLsbD, h] From 2b6dc1845320cb32c11a7ef1cc9822557df1644f Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Thu, 20 Feb 2025 18:47:26 +0000 Subject: [PATCH 2/9] chore: implicit args Co-authored-by: Siddharth --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index efe30d4704c2..78ad1248f3d2 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -773,7 +773,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) : @[simp] theorem extractLsb_toNat (hi lo : Nat) (x : BitVec n) : (extractLsb hi lo x).toNat = (x.toNat >>> lo) % 2^(hi-lo+1) := rfl -@[simp] theorem extractLsb'_toInt (s m : Nat) (x : BitVec n) : +@[simp] theorem extractLsb'_toInt {s m : Nat} {x : BitVec n} : (extractLsb' s m x).toInt = ((x.toNat >>> s) : Int).bmod (2 ^ m) := by simp [extractLsb', toInt_ofNat] From 701c47bb60fed84875ef46b8cdf7c26ea7d8329b Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Thu, 20 Feb 2025 18:47:37 +0000 Subject: [PATCH 3/9] chore: implicit args Co-authored-by: Siddharth --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 78ad1248f3d2..ba145fc662d6 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -777,7 +777,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) : (extractLsb' s m x).toInt = ((x.toNat >>> s) : Int).bmod (2 ^ m) := by simp [extractLsb', toInt_ofNat] -@[simp] theorem extractLsb_toInt (hi lo : Nat) (x : BitVec n) : +@[simp] theorem extractLsb_toInt {hi lo : Nat} {x : BitVec n} : (extractLsb hi lo x).toInt = ((x.toNat >>> lo) : Int).bmod (2 ^ (hi - lo + 1)) := by simp [extractLsb, toInt_ofNat] From 0a4678b1d2638e60d3e779c479d3972434167d92 Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Thu, 20 Feb 2025 18:47:45 +0000 Subject: [PATCH 4/9] chore: implicit args Co-authored-by: Siddharth --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index ba145fc662d6..5dea38efe1fc 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -781,7 +781,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) : (extractLsb hi lo x).toInt = ((x.toNat >>> lo) : Int).bmod (2 ^ (hi - lo + 1)) := by simp [extractLsb, toInt_ofNat] -@[simp] theorem extractLsb'_toFin (s m : Nat) (x : BitVec n) : +@[simp] theorem extractLsb'_toFin {s m : Nat} {x : BitVec n} : (extractLsb' s m x).toFin = Fin.ofNat' (2 ^ m) (x.toNat >>> s) := by simp [extractLsb', toInt_ofNat] From 779193e19d4372a26afed26511519a50d9df5c6c Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Thu, 20 Feb 2025 18:47:56 +0000 Subject: [PATCH 5/9] chore: implicit args Co-authored-by: Siddharth --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 5dea38efe1fc..66fb2540fecc 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -785,7 +785,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) : (extractLsb' s m x).toFin = Fin.ofNat' (2 ^ m) (x.toNat >>> s) := by simp [extractLsb', toInt_ofNat] -@[simp] theorem extractLsb_toFin (hi lo : Nat) (x : BitVec n) : +@[simp] theorem extractLsb_toFin {hi lo : Nat} {x : BitVec n} : (extractLsb hi lo x).toFin = Fin.ofNat' (2 ^ (hi - lo + 1)) (x.toNat >>> lo) := by simp [extractLsb, toInt_ofNat] From 5b29b8c5a12783919139738bc55d3f6aa49d1100 Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Wed, 26 Feb 2025 22:21:48 +0000 Subject: [PATCH 6/9] chore: formatting --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 66fb2540fecc..23626bb0c7e3 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -773,7 +773,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) : @[simp] theorem extractLsb_toNat (hi lo : Nat) (x : BitVec n) : (extractLsb hi lo x).toNat = (x.toNat >>> lo) % 2^(hi-lo+1) := rfl -@[simp] theorem extractLsb'_toInt {s m : Nat} {x : BitVec n} : +@[simp] theorem toInt_extractLsb' {s m : Nat} {x : BitVec n} : (extractLsb' s m x).toInt = ((x.toNat >>> s) : Int).bmod (2 ^ m) := by simp [extractLsb', toInt_ofNat] From 1cc49a66509131d66acdc50a21e0800089a59a00 Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Wed, 26 Feb 2025 22:22:38 +0000 Subject: [PATCH 7/9] chore: formatting --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 23626bb0c7e3..32405ec821b1 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -777,7 +777,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) : (extractLsb' s m x).toInt = ((x.toNat >>> s) : Int).bmod (2 ^ m) := by simp [extractLsb', toInt_ofNat] -@[simp] theorem extractLsb_toInt {hi lo : Nat} {x : BitVec n} : +@[simp] theorem toInt_extractLsb {hi lo : Nat} {x : BitVec n} : (extractLsb hi lo x).toInt = ((x.toNat >>> lo) : Int).bmod (2 ^ (hi - lo + 1)) := by simp [extractLsb, toInt_ofNat] From eb650c117308eede0268b1ea6505d65ae6b9cd09 Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Wed, 26 Feb 2025 22:22:47 +0000 Subject: [PATCH 8/9] chore: formatting --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 32405ec821b1..b79f8ff7821d 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -781,7 +781,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) : (extractLsb hi lo x).toInt = ((x.toNat >>> lo) : Int).bmod (2 ^ (hi - lo + 1)) := by simp [extractLsb, toInt_ofNat] -@[simp] theorem extractLsb'_toFin {s m : Nat} {x : BitVec n} : +@[simp] theorem toFin_extractLsb' {s m : Nat} {x : BitVec n} : (extractLsb' s m x).toFin = Fin.ofNat' (2 ^ m) (x.toNat >>> s) := by simp [extractLsb', toInt_ofNat] From c3edb9a73a89fac8d0f677827513fc824a00c525 Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Wed, 26 Feb 2025 22:22:57 +0000 Subject: [PATCH 9/9] chore: formatting --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index b79f8ff7821d..3406e818aab4 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -785,7 +785,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) : (extractLsb' s m x).toFin = Fin.ofNat' (2 ^ m) (x.toNat >>> s) := by simp [extractLsb', toInt_ofNat] -@[simp] theorem extractLsb_toFin {hi lo : Nat} {x : BitVec n} : +@[simp] theorem toFin_extractLsb {hi lo : Nat} {x : BitVec n} : (extractLsb hi lo x).toFin = Fin.ofNat' (2 ^ (hi - lo + 1)) (x.toNat >>> lo) := by simp [extractLsb, toInt_ofNat]