From 9e28e3088df0063fc2102d5daa68da163de52eea Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 29 Nov 2023 13:34:43 +0000 Subject: [PATCH 01/28] feat: show that `BitVec` is a commutative ring --- Mathlib/Data/BitVec/Lemmas.lean | 40 +++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 97f2353f1d29f..f057a4a10411d 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -105,4 +105,44 @@ theorem ofFin_toFin {n} (v : BitVec n) : ofFin (toFin v) = v := by rfl #align bitvec.of_fin_to_fin Std.BitVec.ofFin_toFin +/-! + ## Distributivity of ofFin + We add simp-lemmas that show how `ofFin` distributes over various bitvector operations, showing + that bitvector operations are equivalent to `Fin` operations +-/ +@[simp] lemma neg_ofFin (x : Fin (2^w)) : -(ofFin x) = ofFin (-x) := by + rw [neg_eq_zero_sub]; rfl + +@[simp] lemma ofFin_and_ofFin (x y : Fin (2^w)) : ofFin x &&& ofFin y = ofFin (x &&& y) := rfl +@[simp] lemma ofFin_or_ofFin (x y : Fin (2^w)) : ofFin x ||| ofFin y = ofFin (x ||| y) := rfl +@[simp] lemma ofFin_xor_ofFin (x y : Fin (2^w)) : ofFin x ^^^ ofFin y = ofFin (x ^^^ y) := rfl +@[simp] lemma ofFin_add_ofFin (x y : Fin (2^w)) : ofFin x + ofFin y = ofFin (x + y) := rfl +@[simp] lemma ofFin_sub_ofFin (x y : Fin (2^w)) : ofFin x - ofFin y = ofFin (x - y) := rfl +@[simp] lemma ofFin_mul_ofFin (x y : Fin (2^w)) : ofFin x * ofFin y = ofFin (x * y) := rfl + +/-! +## Ring +-/ + +lemma zero_eq_ofFin_zero : 0#w = ofFin 0 := rfl +lemma one_eq_ofFin_one : 1#w = ofFin 1 := rfl + +/-! Now we can define an instance of `CommRing (BitVector w)` straightforwardly in terms of the + existing instance `CommRing (Fin (2^w))` -/ +instance : CommRing (BitVec w) where + add_assoc := by intro ⟨_⟩ ⟨_⟩ ⟨_⟩; simp [add_assoc] + zero_add := by intro ⟨_⟩; simp [zero_eq_ofFin_zero] + add_zero := by intro ⟨_⟩; simp [zero_eq_ofFin_zero] + sub_eq_add_neg := by intro ⟨_⟩ ⟨_⟩; simp [sub_eq_add_neg] + add_comm := by intro ⟨_⟩ ⟨_⟩; simp [add_comm] + left_distrib := by intro ⟨_⟩ ⟨_⟩ ⟨_⟩; simp [left_distrib] + right_distrib := by intro ⟨_⟩ ⟨_⟩ ⟨_⟩; simp [right_distrib] + zero_mul := by intro ⟨_⟩; simp [zero_eq_ofFin_zero] + mul_zero := by intro ⟨_⟩; simp [zero_eq_ofFin_zero] + mul_assoc := by intro ⟨_⟩ ⟨_⟩ ⟨_⟩; simp [mul_assoc] + mul_comm := by intro ⟨_⟩ ⟨_⟩; simp [mul_comm] + one_mul := by intro ⟨_⟩; simp [one_eq_ofFin_one] + mul_one := by intro ⟨_⟩; simp [one_eq_ofFin_one] + add_left_neg := by intro ⟨_⟩; simp [zero_eq_ofFin_zero] + end Std.BitVec From 333b40433dd3ec2285fe5c248100abce891dc6da Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 29 Nov 2023 16:32:05 +0000 Subject: [PATCH 02/28] add toFin_injective --- Mathlib/Data/BitVec/Lemmas.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index f057a4a10411d..de906651e3c39 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -27,6 +27,12 @@ theorem toNat_injective {n : Nat} : Function.Injective (@Std.BitVec.toNat n) theorem toNat_inj {x y : BitVec w} : x.toNat = y.toNat ↔ x = y := toNat_injective.eq_iff +theorem toFin_injective {n : Nat} : Function.Injective (@Std.BitVec.toFin n) + | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl + +theorem toFin_inj {x y : BitVec w} : x.toFin = y.toFin ↔ x = y := + toFin_injective.eq_iff + /-- `x < y` as natural numbers if and only if `x < y` as `BitVec w`. -/ theorem toNat_lt_toNat {x y : BitVec w} : x.toNat < y.toNat ↔ x < y := Iff.rfl From 70fe10c265580b1439797026c9320dbed390654c Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 29 Nov 2023 16:33:59 +0000 Subject: [PATCH 03/28] reverse direction of `ofFin_foo_ofFin` --- Mathlib/Data/BitVec/Lemmas.lean | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index de906651e3c39..48e71f653a036 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -116,15 +116,16 @@ theorem ofFin_toFin {n} (v : BitVec n) : ofFin (toFin v) = v := by We add simp-lemmas that show how `ofFin` distributes over various bitvector operations, showing that bitvector operations are equivalent to `Fin` operations -/ -@[simp] lemma neg_ofFin (x : Fin (2^w)) : -(ofFin x) = ofFin (-x) := by +@[simp] lemma neg_ofFin (x : Fin (2^w)) : ofFin (-x) = -(ofFin x) := by rw [neg_eq_zero_sub]; rfl -@[simp] lemma ofFin_and_ofFin (x y : Fin (2^w)) : ofFin x &&& ofFin y = ofFin (x &&& y) := rfl -@[simp] lemma ofFin_or_ofFin (x y : Fin (2^w)) : ofFin x ||| ofFin y = ofFin (x ||| y) := rfl -@[simp] lemma ofFin_xor_ofFin (x y : Fin (2^w)) : ofFin x ^^^ ofFin y = ofFin (x ^^^ y) := rfl -@[simp] lemma ofFin_add_ofFin (x y : Fin (2^w)) : ofFin x + ofFin y = ofFin (x + y) := rfl -@[simp] lemma ofFin_sub_ofFin (x y : Fin (2^w)) : ofFin x - ofFin y = ofFin (x - y) := rfl -@[simp] lemma ofFin_mul_ofFin (x y : Fin (2^w)) : ofFin x * ofFin y = ofFin (x * y) := rfl +@[simp] lemma ofFin_and_ofFin (x y : Fin (2^w)) : ofFin (x &&& y) = ofFin x &&& ofFin y := rfl +@[simp] lemma ofFin_or_ofFin (x y : Fin (2^w)) : ofFin (x ||| y) = ofFin x ||| ofFin y := rfl +@[simp] lemma ofFin_xor_ofFin (x y : Fin (2^w)) : ofFin (x ^^^ y) = ofFin x ^^^ ofFin y := rfl +@[simp] lemma ofFin_add_ofFin (x y : Fin (2^w)) : ofFin (x + y) = ofFin x + ofFin y := rfl +@[simp] lemma ofFin_sub_ofFin (x y : Fin (2^w)) : ofFin (x - y) = ofFin x - ofFin y := rfl +@[simp] lemma ofFin_mul_ofFin (x y : Fin (2^w)) : ofFin (x * y) = ofFin x * ofFin y := rfl + /-! ## Ring From d0f31eef5dc0c6bceda82afc0f7cd91d669c955b Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 29 Nov 2023 16:34:28 +0000 Subject: [PATCH 04/28] WIP --- Mathlib/Data/BitVec/Lemmas.lean | 50 +++++++++++++++++++++++---------- 1 file changed, 35 insertions(+), 15 deletions(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 48e71f653a036..c93e7ac8677dd 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -126,6 +126,11 @@ theorem ofFin_toFin {n} (v : BitVec n) : ofFin (toFin v) = v := by @[simp] lemma ofFin_sub_ofFin (x y : Fin (2^w)) : ofFin (x - y) = ofFin x - ofFin y := rfl @[simp] lemma ofFin_mul_ofFin (x y : Fin (2^w)) : ofFin (x * y) = ofFin x * ofFin y := rfl +/-! + ## Distributivity of toFin +-/ +@[simp] lemma toFin_neg (x : BitVec w) : (-x).toFin = -(x.toFin) := by + rw [neg_eq_zero_sub]; rfl /-! ## Ring @@ -134,22 +139,37 @@ theorem ofFin_toFin {n} (v : BitVec n) : ofFin (toFin v) = v := by lemma zero_eq_ofFin_zero : 0#w = ofFin 0 := rfl lemma one_eq_ofFin_one : 1#w = ofFin 1 := rfl +@[reducible] +instance : SMul ℕ (BitVec w) where + smul x y := x#w * y + +@[reducible] +instance : SMul ℤ (BitVec w) where + smul x y := (BitVec.ofInt w x) * y + +@[reducible] +instance : Pow (BitVec w) ℕ where + pow := + let rec pow x n := + match n with + | 0 => 1 + | n+1 => x * (pow x n) + pow + +instance : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩ +instance : IntCast (BitVec w) := ⟨BitVec.ofInt w⟩ + +-- lemma toFin_nsmul (n : ℕ) (x : BitVec w) : +-- (n • x).toFin = n + /-! Now we can define an instance of `CommRing (BitVector w)` straightforwardly in terms of the existing instance `CommRing (Fin (2^w))` -/ -instance : CommRing (BitVec w) where - add_assoc := by intro ⟨_⟩ ⟨_⟩ ⟨_⟩; simp [add_assoc] - zero_add := by intro ⟨_⟩; simp [zero_eq_ofFin_zero] - add_zero := by intro ⟨_⟩; simp [zero_eq_ofFin_zero] - sub_eq_add_neg := by intro ⟨_⟩ ⟨_⟩; simp [sub_eq_add_neg] - add_comm := by intro ⟨_⟩ ⟨_⟩; simp [add_comm] - left_distrib := by intro ⟨_⟩ ⟨_⟩ ⟨_⟩; simp [left_distrib] - right_distrib := by intro ⟨_⟩ ⟨_⟩ ⟨_⟩; simp [right_distrib] - zero_mul := by intro ⟨_⟩; simp [zero_eq_ofFin_zero] - mul_zero := by intro ⟨_⟩; simp [zero_eq_ofFin_zero] - mul_assoc := by intro ⟨_⟩ ⟨_⟩ ⟨_⟩; simp [mul_assoc] - mul_comm := by intro ⟨_⟩ ⟨_⟩; simp [mul_comm] - one_mul := by intro ⟨_⟩; simp [one_eq_ofFin_one] - mul_one := by intro ⟨_⟩; simp [one_eq_ofFin_one] - add_left_neg := by intro ⟨_⟩; simp [zero_eq_ofFin_zero] +instance : CommRing (BitVec w) := by + apply Function.Injective.commRing _ toFin_injective <;> (intros; try rfl) + · apply toFin_neg + · sorry + · sorry + · sorry + · sorry end Std.BitVec From 37480219b3939e7e62eccfd4dfd3668a8a08b463 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 29 Nov 2023 17:55:12 +0000 Subject: [PATCH 05/28] rename lemma to reflect to changed order --- Mathlib/Data/BitVec/Lemmas.lean | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index c93e7ac8677dd..47d09de624838 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -116,15 +116,16 @@ theorem ofFin_toFin {n} (v : BitVec n) : ofFin (toFin v) = v := by We add simp-lemmas that show how `ofFin` distributes over various bitvector operations, showing that bitvector operations are equivalent to `Fin` operations -/ -@[simp] lemma neg_ofFin (x : Fin (2^w)) : ofFin (-x) = -(ofFin x) := by +@[simp] lemma ofFin_neg (x : Fin (2^w)) : ofFin (-x) = -(ofFin x) := by rw [neg_eq_zero_sub]; rfl -@[simp] lemma ofFin_and_ofFin (x y : Fin (2^w)) : ofFin (x &&& y) = ofFin x &&& ofFin y := rfl -@[simp] lemma ofFin_or_ofFin (x y : Fin (2^w)) : ofFin (x ||| y) = ofFin x ||| ofFin y := rfl -@[simp] lemma ofFin_xor_ofFin (x y : Fin (2^w)) : ofFin (x ^^^ y) = ofFin x ^^^ ofFin y := rfl -@[simp] lemma ofFin_add_ofFin (x y : Fin (2^w)) : ofFin (x + y) = ofFin x + ofFin y := rfl -@[simp] lemma ofFin_sub_ofFin (x y : Fin (2^w)) : ofFin (x - y) = ofFin x - ofFin y := rfl -@[simp] lemma ofFin_mul_ofFin (x y : Fin (2^w)) : ofFin (x * y) = ofFin x * ofFin y := rfl +@[simp] lemma ofFin_and (x y : Fin (2^w)) : ofFin (x &&& y) = ofFin x &&& ofFin y := rfl +@[simp] lemma ofFin_or (x y : Fin (2^w)) : ofFin (x ||| y) = ofFin x ||| ofFin y := rfl +@[simp] lemma ofFin_xor (x y : Fin (2^w)) : ofFin (x ^^^ y) = ofFin x ^^^ ofFin y := rfl +@[simp] lemma ofFin_add (x y : Fin (2^w)) : ofFin (x + y) = ofFin x + ofFin y := rfl +@[simp] lemma ofFin_sub (x y : Fin (2^w)) : ofFin (x - y) = ofFin x - ofFin y := rfl +@[simp] lemma ofFin_mul (x y : Fin (2^w)) : ofFin (x * y) = ofFin x * ofFin y := rfl + /-! ## Distributivity of toFin From 10bf420f8bdfce022fbda585cf17ec9709712a11 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 29 Nov 2023 19:02:13 +0000 Subject: [PATCH 06/28] reorder Injectivivity proofs --- Mathlib/Data/BitVec/Lemmas.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 47d09de624838..73c71896fe348 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -21,18 +21,18 @@ open Nat variable {w v : Nat} -theorem toNat_injective {n : Nat} : Function.Injective (@Std.BitVec.toNat n) - | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl - -theorem toNat_inj {x y : BitVec w} : x.toNat = y.toNat ↔ x = y := - toNat_injective.eq_iff - theorem toFin_injective {n : Nat} : Function.Injective (@Std.BitVec.toFin n) | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl theorem toFin_inj {x y : BitVec w} : x.toFin = y.toFin ↔ x = y := toFin_injective.eq_iff +theorem toNat_injective {n : Nat} : Function.Injective (@Std.BitVec.toNat n) := + Function.Injective.comp Fin.val_injective toFin_injective + +theorem toNat_inj {x y : BitVec w} : x.toNat = y.toNat ↔ x = y := + toNat_injective.eq_iff + /-- `x < y` as natural numbers if and only if `x < y` as `BitVec w`. -/ theorem toNat_lt_toNat {x y : BitVec w} : x.toNat < y.toNat ↔ x < y := Iff.rfl From bbc3adc97c3eaf5a4ee35c9b5eebfe62970945e4 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 29 Nov 2023 19:05:45 +0000 Subject: [PATCH 07/28] refactor distributivity lemmas --- Mathlib/Data/BitVec/Lemmas.lean | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 73c71896fe348..9c449bd39d72c 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -112,10 +112,11 @@ theorem ofFin_toFin {n} (v : BitVec n) : ofFin (toFin v) = v := by #align bitvec.of_fin_to_fin Std.BitVec.ofFin_toFin /-! - ## Distributivity of ofFin - We add simp-lemmas that show how `ofFin` distributes over various bitvector operations, showing - that bitvector operations are equivalent to `Fin` operations +### Distributivity of `Std.BitVec.ofFin` -/ +section +variable (x y : Fin (2^w)) + @[simp] lemma ofFin_neg (x : Fin (2^w)) : ofFin (-x) = -(ofFin x) := by rw [neg_eq_zero_sub]; rfl @@ -126,13 +127,26 @@ theorem ofFin_toFin {n} (v : BitVec n) : ofFin (toFin v) = v := by @[simp] lemma ofFin_sub (x y : Fin (2^w)) : ofFin (x - y) = ofFin x - ofFin y := rfl @[simp] lemma ofFin_mul (x y : Fin (2^w)) : ofFin (x * y) = ofFin x * ofFin y := rfl +end /-! - ## Distributivity of toFin +### Distributivity of `Std.BitVec.toFin` -/ -@[simp] lemma toFin_neg (x : BitVec w) : (-x).toFin = -(x.toFin) := by +section +variable (x y : BitVec w) + +@[simp] lemma toFin_neg : toFin (-x) = -(toFin x) := by rw [neg_eq_zero_sub]; rfl +@[simp] lemma toFin_and : toFin (x &&& y) = toFin x &&& toFin y := rfl +@[simp] lemma toFin_or : toFin (x ||| y) = toFin x ||| toFin y := rfl +@[simp] lemma toFin_xor : toFin (x ^^^ y) = toFin x ^^^ toFin y := rfl +@[simp] lemma toFin_add : toFin (x + y) = toFin x + toFin y := rfl +@[simp] lemma toFin_sub : toFin (x - y) = toFin x - toFin y := rfl +@[simp] lemma toFin_mul : toFin (x * y) = toFin x * toFin y := rfl + +end + /-! ## Ring -/ From 86003cdfbb4aedebadf9e18c66833ef2d6a609b6 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 29 Nov 2023 19:06:40 +0000 Subject: [PATCH 08/28] remove extraneous arguments --- Mathlib/Data/BitVec/Lemmas.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 9c449bd39d72c..ff2f641b4f287 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -117,15 +117,15 @@ theorem ofFin_toFin {n} (v : BitVec n) : ofFin (toFin v) = v := by section variable (x y : Fin (2^w)) -@[simp] lemma ofFin_neg (x : Fin (2^w)) : ofFin (-x) = -(ofFin x) := by +@[simp] lemma ofFin_neg : ofFin (-x) = -(ofFin x) := by rw [neg_eq_zero_sub]; rfl -@[simp] lemma ofFin_and (x y : Fin (2^w)) : ofFin (x &&& y) = ofFin x &&& ofFin y := rfl -@[simp] lemma ofFin_or (x y : Fin (2^w)) : ofFin (x ||| y) = ofFin x ||| ofFin y := rfl -@[simp] lemma ofFin_xor (x y : Fin (2^w)) : ofFin (x ^^^ y) = ofFin x ^^^ ofFin y := rfl -@[simp] lemma ofFin_add (x y : Fin (2^w)) : ofFin (x + y) = ofFin x + ofFin y := rfl -@[simp] lemma ofFin_sub (x y : Fin (2^w)) : ofFin (x - y) = ofFin x - ofFin y := rfl -@[simp] lemma ofFin_mul (x y : Fin (2^w)) : ofFin (x * y) = ofFin x * ofFin y := rfl +@[simp] lemma ofFin_and : ofFin (x &&& y) = ofFin x &&& ofFin y := rfl +@[simp] lemma ofFin_or : ofFin (x ||| y) = ofFin x ||| ofFin y := rfl +@[simp] lemma ofFin_xor : ofFin (x ^^^ y) = ofFin x ^^^ ofFin y := rfl +@[simp] lemma ofFin_add : ofFin (x + y) = ofFin x + ofFin y := rfl +@[simp] lemma ofFin_sub : ofFin (x - y) = ofFin x - ofFin y := rfl +@[simp] lemma ofFin_mul : ofFin (x * y) = ofFin x * ofFin y := rfl end From d815ab7ef56356b1fcdfc62b6fd2a1a47edc5541 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 29 Nov 2023 19:08:40 +0000 Subject: [PATCH 09/28] add `ofFin_zero`/`_one` --- Mathlib/Data/BitVec/Lemmas.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index ff2f641b4f287..8cb951b60b9b7 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -127,6 +127,9 @@ variable (x y : Fin (2^w)) @[simp] lemma ofFin_sub : ofFin (x - y) = ofFin x - ofFin y := rfl @[simp] lemma ofFin_mul : ofFin (x * y) = ofFin x * ofFin y := rfl +@[simp] lemma ofFin_zero : @ofFin w 0 = 0 := rfl +@[simp] lemma ofFin_one : @ofFin w 1 = 1 := rfl + end /-! From e7b44adee35f7d7aa0ccbfebba051c359325792f Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 29 Nov 2023 19:12:43 +0000 Subject: [PATCH 10/28] add `toFin_zero`/`_one` --- Mathlib/Data/BitVec/Lemmas.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 8cb951b60b9b7..e876c59911cf9 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -148,6 +148,9 @@ variable (x y : BitVec w) @[simp] lemma toFin_sub : toFin (x - y) = toFin x - toFin y := rfl @[simp] lemma toFin_mul : toFin (x * y) = toFin x * toFin y := rfl +@[simp] lemma toFin_zero : @toFin w 0 = 0 := rfl +@[simp] lemma toFin_one : @toFin w 1 = 1 := rfl + end /-! From 365b86a941f70d696cc7fcd6f01783f2fadb7d57 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 29 Nov 2023 19:16:15 +0000 Subject: [PATCH 11/28] refactor `SMul`, `Pow` and `Cast` instances --- Mathlib/Data/BitVec/Lemmas.lean | 32 +++++++++----------------------- 1 file changed, 9 insertions(+), 23 deletions(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index e876c59911cf9..27ae4d30088be 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -157,31 +157,17 @@ end ## Ring -/ -lemma zero_eq_ofFin_zero : 0#w = ofFin 0 := rfl -lemma one_eq_ofFin_one : 1#w = ofFin 1 := rfl - -@[reducible] -instance : SMul ℕ (BitVec w) where - smul x y := x#w * y - -@[reducible] -instance : SMul ℤ (BitVec w) where - smul x y := (BitVec.ofInt w x) * y - -@[reducible] -instance : Pow (BitVec w) ℕ where - pow := - let rec pow x n := - match n with - | 0 => 1 - | n+1 => x * (pow x n) - pow - +instance : SMul ℕ (BitVec w) := ⟨fun x y => ofFin <| x • y.toFin⟩ +instance : SMul ℤ (BitVec w) := ⟨fun x y => ofFin <| x • y.toFin⟩ +instance : Pow (BitVec w) ℕ := ⟨fun x n => ofFin <| x.toFin ^ n⟩ instance : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩ -instance : IntCast (BitVec w) := ⟨BitVec.ofInt w⟩ --- lemma toFin_nsmul (n : ℕ) (x : BitVec w) : --- (n • x).toFin = n +/-- The obvious instance would be to define `IntCast` in terms of `Std.BitVec.ofInt`. -/ +instance : IntCast (BitVec w) := ⟨fun x => ofFin x⟩ + +@[simp] lemma natCast (x w : Nat) : (x : BitVec w) = BitVec.ofNat w x := rfl + +proof_wanted intCast (x : Int) (w : Nat) : (x : BitVec w) = BitVec.ofInt w x /-! Now we can define an instance of `CommRing (BitVector w)` straightforwardly in terms of the existing instance `CommRing (Fin (2^w))` -/ From f21956035d62fc7e8c5d0d209b646076bcd6a62b Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 29 Nov 2023 19:22:49 +0000 Subject: [PATCH 12/28] move instances to Defs file, use theorems by name --- Mathlib/Data/BitVec/Defs.lean | 8 +++++++ Mathlib/Data/BitVec/Lemmas.lean | 41 ++++++++++++++++----------------- 2 files changed, 28 insertions(+), 21 deletions(-) diff --git a/Mathlib/Data/BitVec/Defs.lean b/Mathlib/Data/BitVec/Defs.lean index d42b5be99a64e..3f32799256e6c 100644 --- a/Mathlib/Data/BitVec/Defs.lean +++ b/Mathlib/Data/BitVec/Defs.lean @@ -140,4 +140,12 @@ def toLEList (x : BitVec w) : List Bool := def toBEList (x : BitVec w) : List Bool := List.ofFn x.getMsb' +instance : SMul ℕ (BitVec w) := ⟨fun x y => ofFin <| x • y.toFin⟩ +instance : SMul ℤ (BitVec w) := ⟨fun x y => ofFin <| x • y.toFin⟩ +instance : Pow (BitVec w) ℕ := ⟨fun x n => ofFin <| x.toFin ^ n⟩ +instance : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩ + +/-- The obvious instance would be to define `IntCast` in terms of `Std.BitVec.ofInt`. -/ +instance : IntCast (BitVec w) := ⟨fun x => ofFin x⟩ + end Std.BitVec diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 27ae4d30088be..363bd75d58b56 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -151,32 +151,31 @@ variable (x y : BitVec w) @[simp] lemma toFin_zero : @toFin w 0 = 0 := rfl @[simp] lemma toFin_one : @toFin w 1 = 1 := rfl +variable (n : Nat) (z : Int) + +@[simp] lemma toFin_nsmul : toFin (n • x) = n • x.toFin := rfl +@[simp] lemma toFin_zsmul : toFin (z • x) = z • x.toFin := rfl +@[simp] lemma toFin_pow : toFin (x ^ n) = x.toFin ^ n := rfl +@[simp] lemma toFin_natCast : @toFin w n = n := rfl +@[simp] lemma toFin_intCast : @toFin w z = z := rfl + end /-! ## Ring -/ -instance : SMul ℕ (BitVec w) := ⟨fun x y => ofFin <| x • y.toFin⟩ -instance : SMul ℤ (BitVec w) := ⟨fun x y => ofFin <| x • y.toFin⟩ -instance : Pow (BitVec w) ℕ := ⟨fun x n => ofFin <| x.toFin ^ n⟩ -instance : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩ - -/-- The obvious instance would be to define `IntCast` in terms of `Std.BitVec.ofInt`. -/ -instance : IntCast (BitVec w) := ⟨fun x => ofFin x⟩ - -@[simp] lemma natCast (x w : Nat) : (x : BitVec w) = BitVec.ofNat w x := rfl - -proof_wanted intCast (x : Int) (w : Nat) : (x : BitVec w) = BitVec.ofInt w x - -/-! Now we can define an instance of `CommRing (BitVector w)` straightforwardly in terms of the - existing instance `CommRing (Fin (2^w))` -/ -instance : CommRing (BitVec w) := by - apply Function.Injective.commRing _ toFin_injective <;> (intros; try rfl) - · apply toFin_neg - · sorry - · sorry - · sorry - · sorry +instance : CommRing (BitVec w) := Function.Injective.commRing _ toFin_injective + toFin_zero + toFin_one + toFin_add + toFin_mul + toFin_neg + toFin_sub + toFin_nsmul + toFin_zsmul + toFin_pow + toFin_natCast + toFin_intCast end Std.BitVec From 2a760f479ecb25f44448f739456b6060862aa844 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Thu, 30 Nov 2023 04:27:37 +0000 Subject: [PATCH 13/28] Remove some simp lemmas --- Mathlib/Data/BitVec/Lemmas.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 363bd75d58b56..f25b5b872b0cf 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -148,13 +148,14 @@ variable (x y : BitVec w) @[simp] lemma toFin_sub : toFin (x - y) = toFin x - toFin y := rfl @[simp] lemma toFin_mul : toFin (x * y) = toFin x * toFin y := rfl -@[simp] lemma toFin_zero : @toFin w 0 = 0 := rfl -@[simp] lemma toFin_one : @toFin w 1 = 1 := rfl +-- These should be simp, but Std's simp-lemmas do not allow this yet. +lemma toFin_zero : toFin (0 : BitVec w) = 0 := rfl +lemma toFin_one : toFin (1 : BitVec w) = 1 := rfl variable (n : Nat) (z : Int) -@[simp] lemma toFin_nsmul : toFin (n • x) = n • x.toFin := rfl -@[simp] lemma toFin_zsmul : toFin (z • x) = z • x.toFin := rfl +lemma toFin_nsmul : toFin (n • x) = n • x.toFin := rfl +lemma toFin_zsmul : toFin (z • x) = z • x.toFin := rfl @[simp] lemma toFin_pow : toFin (x ^ n) = x.toFin ^ n := rfl @[simp] lemma toFin_natCast : @toFin w n = n := rfl @[simp] lemma toFin_intCast : @toFin w z = z := rfl From 9b53ed9e4ca7f1f3ab4437567e77b4f10b3f6de0 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Thu, 30 Nov 2023 10:04:04 +0000 Subject: [PATCH 14/28] Update Mathlib/Data/Bitvec/Lemmas.lean Co-authored-by: Eric Wieser --- Mathlib/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index f25b5b872b0cf..0e47cd9760c17 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -157,7 +157,7 @@ variable (n : Nat) (z : Int) lemma toFin_nsmul : toFin (n • x) = n • x.toFin := rfl lemma toFin_zsmul : toFin (z • x) = z • x.toFin := rfl @[simp] lemma toFin_pow : toFin (x ^ n) = x.toFin ^ n := rfl -@[simp] lemma toFin_natCast : @toFin w n = n := rfl +@[simp] lemma toFin_natCast : toFin (n : BitVector w) = n := rfl @[simp] lemma toFin_intCast : @toFin w z = z := rfl end From 4db1611c4bb7d023a7a8a0dabc28eb91a11a9d19 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 30 Nov 2023 12:09:33 +0000 Subject: [PATCH 15/28] tidy --- Mathlib/Data/BitVec/Lemmas.lean | 53 +++++++++++++++++---------------- 1 file changed, 28 insertions(+), 25 deletions(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 0e47cd9760c17..5aef119172fc1 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -21,14 +21,14 @@ open Nat variable {w v : Nat} -theorem toFin_injective {n : Nat} : Function.Injective (@Std.BitVec.toFin n) +theorem toFin_injective {n : Nat} : Function.Injective (toFin : BitVec n → _) | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl theorem toFin_inj {x y : BitVec w} : x.toFin = y.toFin ↔ x = y := toFin_injective.eq_iff -theorem toNat_injective {n : Nat} : Function.Injective (@Std.BitVec.toNat n) := - Function.Injective.comp Fin.val_injective toFin_injective +theorem toNat_injective {n : Nat} : Function.Injective (BitVec.toNat : BitVec n → _) := + Fin.val_injective.comp toFin_injective theorem toNat_inj {x y : BitVec w} : x.toNat = y.toNat ↔ x = y := toNat_injective.eq_iff @@ -127,9 +127,18 @@ variable (x y : Fin (2^w)) @[simp] lemma ofFin_sub : ofFin (x - y) = ofFin x - ofFin y := rfl @[simp] lemma ofFin_mul : ofFin (x * y) = ofFin x * ofFin y := rfl -@[simp] lemma ofFin_zero : @ofFin w 0 = 0 := rfl -@[simp] lemma ofFin_one : @ofFin w 1 = 1 := rfl +@[simp] lemma ofFin_zero : ofFin (0 : Fin (2^w)) = 0 := rfl +@[simp] lemma ofFin_one : ofFin (1 : Fin (2^w)) = 1 := rfl +lemma ofFin_nsmul (n : ℕ) (x : Fin (2^w)) : ofFin (n • x) = n • ofFin x := rfl +lemma ofFin_zsmul (z : ℤ) (x : Fin (2^w)) : ofFin (z • x) = z • ofFin x := rfl +@[simp] lemma ofFin_pow (n : ℕ) : ofFin (x ^ n) = ofFin x ^ n := rfl +@[simp] lemma ofFin_natCast (n : ℕ) : ofFin (n : Fin (2^w)) = n := rfl +@[simp] lemma ofFin_intCast (z : ℤ) : ofFin (z : Fin (2^w)) = z := rfl + +-- See Note [no_index around OfNat.ofNat] +@[simp] lemma ofFin_ofNat (n : ℕ) : + ofFin (no_index (OfNat.ofNat n : Fin (2^w))) = OfNat.ofNat n := rfl end /-! @@ -149,16 +158,18 @@ variable (x y : BitVec w) @[simp] lemma toFin_mul : toFin (x * y) = toFin x * toFin y := rfl -- These should be simp, but Std's simp-lemmas do not allow this yet. -lemma toFin_zero : toFin (0 : BitVec w) = 0 := rfl -lemma toFin_one : toFin (1 : BitVec w) = 1 := rfl +lemma toFin_zero : toFin (0 : BitVec w) = 0 := rfl +lemma toFin_one : toFin (1 : BitVec w) = 1 := rfl -variable (n : Nat) (z : Int) +lemma toFin_nsmul (n : ℕ) (x : BitVec w) : toFin (n • x) = n • x.toFin := rfl +lemma toFin_zsmul (z : ℤ) (x : BitVec w) : toFin (z • x) = z • x.toFin := rfl +@[simp] lemma toFin_pow (n : ℕ) : toFin (x ^ n) = x.toFin ^ n := rfl +@[simp] lemma toFin_natCast (n : ℕ) : toFin (n : BitVec w) = n := rfl +@[simp] lemma toFin_intCast (z : ℤ) : toFin (z : BitVec w) = z := rfl -lemma toFin_nsmul : toFin (n • x) = n • x.toFin := rfl -lemma toFin_zsmul : toFin (z • x) = z • x.toFin := rfl -@[simp] lemma toFin_pow : toFin (x ^ n) = x.toFin ^ n := rfl -@[simp] lemma toFin_natCast : toFin (n : BitVector w) = n := rfl -@[simp] lemma toFin_intCast : @toFin w z = z := rfl +-- See Note [no_index around OfNat.ofNat] +lemma toFin_ofNat (n : ℕ) : + toFin (no_index (OfNat.ofNat n : BitVec w)) = OfNat.ofNat n := rfl end @@ -166,17 +177,9 @@ end ## Ring -/ -instance : CommRing (BitVec w) := Function.Injective.commRing _ toFin_injective - toFin_zero - toFin_one - toFin_add - toFin_mul - toFin_neg - toFin_sub - toFin_nsmul - toFin_zsmul - toFin_pow - toFin_natCast - toFin_intCast +instance : CommRing (BitVec w) := + toFin_injective.commRing _ + toFin_zero toFin_one toFin_add toFin_mul toFin_neg toFin_sub + (Function.swap toFin_nsmul) (Function.swap toFin_zsmul) toFin_pow toFin_natCast toFin_intCast end Std.BitVec From 698608ed69679d69a4af8852d3051a25dcd95de1 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Fri, 1 Dec 2023 01:28:01 +0000 Subject: [PATCH 16/28] Fix proofs --- Mathlib/Data/BitVec/Lemmas.lean | 43 +++++++++++++++++++++++++-------- 1 file changed, 33 insertions(+), 10 deletions(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 5aef119172fc1..697ea34bbd6c0 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -120,25 +120,42 @@ variable (x y : Fin (2^w)) @[simp] lemma ofFin_neg : ofFin (-x) = -(ofFin x) := by rw [neg_eq_zero_sub]; rfl -@[simp] lemma ofFin_and : ofFin (x &&& y) = ofFin x &&& ofFin y := rfl -@[simp] lemma ofFin_or : ofFin (x ||| y) = ofFin x ||| ofFin y := rfl -@[simp] lemma ofFin_xor : ofFin (x ^^^ y) = ofFin x ^^^ ofFin y := rfl +@[simp] lemma ofFin_and : ofFin (x &&& y) = ofFin x &&& ofFin y := by + simp only [HAnd.hAnd, AndOp.and, Fin.land, BitVec.and, toNat_ofFin, ofFin.injEq, Fin.mk.injEq] + exact mod_eq_of_lt (Nat.and_lt_two_pow _ y.prop) + +@[simp] lemma ofFin_or : ofFin (x ||| y) = ofFin x ||| ofFin y := by + simp only [HOr.hOr, OrOp.or, Fin.lor, BitVec.or, toNat_ofFin, ofFin.injEq, Fin.mk.injEq] + exact mod_eq_of_lt (Nat.or_lt_two_pow x.prop y.prop) + +@[simp] lemma ofFin_xor : ofFin (x ^^^ y) = ofFin x ^^^ ofFin y := by + simp only [HXor.hXor, Xor.xor, Fin.xor, BitVec.xor, toNat_ofFin, ofFin.injEq, Fin.mk.injEq] + exact mod_eq_of_lt (Nat.xor_lt_two_pow x.prop y.prop) + @[simp] lemma ofFin_add : ofFin (x + y) = ofFin x + ofFin y := rfl @[simp] lemma ofFin_sub : ofFin (x - y) = ofFin x - ofFin y := rfl @[simp] lemma ofFin_mul : ofFin (x * y) = ofFin x * ofFin y := rfl -@[simp] lemma ofFin_zero : ofFin (0 : Fin (2^w)) = 0 := rfl -@[simp] lemma ofFin_one : ofFin (1 : Fin (2^w)) = 1 := rfl +-- These should be simp, but Std's simp-lemmas do not allow this yet. +lemma ofFin_zero : ofFin (0 : Fin (2^w)) = 0 := rfl +lemma ofFin_one : ofFin (1 : Fin (2^w)) = 1 := by + simp only [OfNat.ofNat, BitVec.ofNat, and_pow_two_is_mod] + rfl lemma ofFin_nsmul (n : ℕ) (x : Fin (2^w)) : ofFin (n • x) = n • ofFin x := rfl lemma ofFin_zsmul (z : ℤ) (x : Fin (2^w)) : ofFin (z • x) = z • ofFin x := rfl @[simp] lemma ofFin_pow (n : ℕ) : ofFin (x ^ n) = ofFin x ^ n := rfl -@[simp] lemma ofFin_natCast (n : ℕ) : ofFin (n : Fin (2^w)) = n := rfl + +@[simp] lemma ofFin_natCast (n : ℕ) : ofFin (n : Fin (2^w)) = n := by + simp only [Nat.cast, NatCast.natCast, OfNat.ofNat, BitVec.ofNat, and_pow_two_is_mod] + rfl + @[simp] lemma ofFin_intCast (z : ℤ) : ofFin (z : Fin (2^w)) = z := rfl -- See Note [no_index around OfNat.ofNat] @[simp] lemma ofFin_ofNat (n : ℕ) : - ofFin (no_index (OfNat.ofNat n : Fin (2^w))) = OfNat.ofNat n := rfl + ofFin (no_index (OfNat.ofNat n : Fin (2^w))) = OfNat.ofNat n := by + sorry end /-! @@ -150,9 +167,15 @@ variable (x y : BitVec w) @[simp] lemma toFin_neg : toFin (-x) = -(toFin x) := by rw [neg_eq_zero_sub]; rfl -@[simp] lemma toFin_and : toFin (x &&& y) = toFin x &&& toFin y := rfl -@[simp] lemma toFin_or : toFin (x ||| y) = toFin x ||| toFin y := rfl -@[simp] lemma toFin_xor : toFin (x ^^^ y) = toFin x ^^^ toFin y := rfl +@[simp] lemma toFin_and : toFin (x &&& y) = toFin x &&& toFin y := by + apply toFin_inj.mpr; simp only [ofFin_and] + +@[simp] lemma toFin_or : toFin (x ||| y) = toFin x ||| toFin y := by + apply toFin_inj.mpr; simp only [ofFin_or] + +@[simp] lemma toFin_xor : toFin (x ^^^ y) = toFin x ^^^ toFin y := by + apply toFin_inj.mpr; simp only [ofFin_xor] + @[simp] lemma toFin_add : toFin (x + y) = toFin x + toFin y := rfl @[simp] lemma toFin_sub : toFin (x - y) = toFin x - toFin y := rfl @[simp] lemma toFin_mul : toFin (x * y) = toFin x * toFin y := rfl From 772eba5a61503bd9d64f91308bab98bff3a6e6c3 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Fri, 1 Dec 2023 01:39:24 +0000 Subject: [PATCH 17/28] Fix more proofs --- Mathlib/Data/BitVec/Lemmas.lean | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 697ea34bbd6c0..0f882414a454e 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -155,7 +155,8 @@ lemma ofFin_zsmul (z : ℤ) (x : Fin (2^w)) : ofFin (z • x) = z • ofFin x := -- See Note [no_index around OfNat.ofNat] @[simp] lemma ofFin_ofNat (n : ℕ) : ofFin (no_index (OfNat.ofNat n : Fin (2^w))) = OfNat.ofNat n := by - sorry + simp only [OfNat.ofNat, Fin.ofNat', BitVec.ofNat, and_pow_two_is_mod] + end /-! @@ -182,17 +183,22 @@ variable (x y : BitVec w) -- These should be simp, but Std's simp-lemmas do not allow this yet. lemma toFin_zero : toFin (0 : BitVec w) = 0 := rfl -lemma toFin_one : toFin (1 : BitVec w) = 1 := rfl +lemma toFin_one : toFin (1 : BitVec w) = 1 := by + apply toFin_inj.mpr; simp only [ofNat_eq_ofNat, ofFin_ofNat] lemma toFin_nsmul (n : ℕ) (x : BitVec w) : toFin (n • x) = n • x.toFin := rfl lemma toFin_zsmul (z : ℤ) (x : BitVec w) : toFin (z • x) = z • x.toFin := rfl @[simp] lemma toFin_pow (n : ℕ) : toFin (x ^ n) = x.toFin ^ n := rfl -@[simp] lemma toFin_natCast (n : ℕ) : toFin (n : BitVec w) = n := rfl + +@[simp] lemma toFin_natCast (n : ℕ) : toFin (n : BitVec w) = n := by + apply toFin_inj.mpr; simp only [ofFin_natCast] + @[simp] lemma toFin_intCast (z : ℤ) : toFin (z : BitVec w) = z := rfl -- See Note [no_index around OfNat.ofNat] lemma toFin_ofNat (n : ℕ) : - toFin (no_index (OfNat.ofNat n : BitVec w)) = OfNat.ofNat n := rfl + toFin (no_index (OfNat.ofNat n : BitVec w)) = OfNat.ofNat n := by + simp only [OfNat.ofNat, BitVec.ofNat, and_pow_two_is_mod, Fin.ofNat'] end From ee150e9268478583b665fdced4df2387ad72acfa Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Fri, 1 Dec 2023 02:55:39 +0000 Subject: [PATCH 18/28] WIP: use `ofInt` as `IntCast` instance --- Mathlib/Data/BitVec/Defs.lean | 4 +--- Mathlib/Data/BitVec/Lemmas.lean | 31 ++++++++++++++++++++++++++++++- 2 files changed, 31 insertions(+), 4 deletions(-) diff --git a/Mathlib/Data/BitVec/Defs.lean b/Mathlib/Data/BitVec/Defs.lean index 3f32799256e6c..bf86fd5faedfa 100644 --- a/Mathlib/Data/BitVec/Defs.lean +++ b/Mathlib/Data/BitVec/Defs.lean @@ -144,8 +144,6 @@ instance : SMul ℕ (BitVec w) := ⟨fun x y => ofFin <| x • y.toFin⟩ instance : SMul ℤ (BitVec w) := ⟨fun x y => ofFin <| x • y.toFin⟩ instance : Pow (BitVec w) ℕ := ⟨fun x n => ofFin <| x.toFin ^ n⟩ instance : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩ - -/-- The obvious instance would be to define `IntCast` in terms of `Std.BitVec.ofInt`. -/ -instance : IntCast (BitVec w) := ⟨fun x => ofFin x⟩ +instance : IntCast (BitVec w) := ⟨BitVec.ofInt w⟩ end Std.BitVec diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 0f882414a454e..bfd551780dfba 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -5,6 +5,7 @@ Authors: Simon Hudon, Harun Khan -/ import Mathlib.Data.BitVec.Defs +import Mathlib.Tactic.Linarith /-! # Basic Theorems About Bitvectors @@ -150,7 +151,35 @@ lemma ofFin_zsmul (z : ℤ) (x : Fin (2^w)) : ofFin (z • x) = z • ofFin x := simp only [Nat.cast, NatCast.natCast, OfNat.ofNat, BitVec.ofNat, and_pow_two_is_mod] rfl -@[simp] lemma ofFin_intCast (z : ℤ) : ofFin (z : Fin (2^w)) = z := rfl +@[simp] lemma ofFin_intCast (z : ℤ) : ofFin (z : Fin (2^w)) = z := by + simp only [Int.cast, IntCast.intCast, BitVec.ofInt, ge_iff_le, tsub_le_iff_right] + cases' z with z z + <;> rw [Int.castDef] + <;> simp only [Nat.cast, NatCast.natCast, Fin.ofNat_eq_val, ofFin_neg, ofFin_natCast, ge_iff_le, + tsub_le_iff_right] + · simp only [Neg.neg, BitVec.neg, BitVec.sub, HSub.hSub, Sub.sub, Fin.sub, Nat.sub_eq, + and_pow_two_is_mod, zero_mod, zero_add, BitVec.ofNat, ofFin.injEq, Fin.mk.injEq] + induction' z using Nat.strongInductionOn with z ih + by_cases h : z + 1 < 2 ^ w + · rw [Nat.mod_eq_of_lt h, Nat.mod_eq_of_lt (lt_of_succ_lt h), Nat.sub_succ', Nat.sub_right_comm] + · by_cases h' : z + 1 = 2 ^ w + · simp only [h', mod_self, ge_iff_le, nonpos_iff_eq_zero, pow_eq_zero_iff', + OfNat.ofNat_ne_zero, ne_eq, false_and, tsub_zero, tsub_le_iff_right] + obtain rfl : z = 2 ^ w - 1 := by + apply Nat.succ_injective + show z + 1 = _ + 1 + rw [h', Nat.sub_add_cancel (one_le_two_pow _)] + have h_lt : 2 ^ w - 1 < 2 ^ w := by + sorry + simp only [ge_iff_le, Nat.mod_eq_of_lt h_lt, le_refl, tsub_eq_zero_of_le, zero_mod] + · have hz : z ≥ 2 ^ w := + sorry + rw [ + Nat.mod_eq_sub_mod (Nat.ge_of_not_lt h), + Nat.mod_eq_sub_mod hz, + Nat.succ_sub hz + ] + apply ih _ (Nat.sub_lt (lt_of_lt_of_le (two_pow_pos w) hz) (two_pow_pos w)) -- See Note [no_index around OfNat.ofNat] @[simp] lemma ofFin_ofNat (n : ℕ) : From 57a52e153a44476d5f24e93f6a0a52965f7c50df Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Fri, 1 Dec 2023 13:59:51 +0000 Subject: [PATCH 19/28] finish `ofFin_intCast` proof --- Mathlib/Data/BitVec/Lemmas.lean | 25 +++---------------------- Mathlib/Data/Nat/Order/Lemmas.lean | 25 +++++++++++++++++++++++++ 2 files changed, 28 insertions(+), 22 deletions(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index bfd551780dfba..dda82065e8984 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -159,27 +159,7 @@ lemma ofFin_zsmul (z : ℤ) (x : Fin (2^w)) : ofFin (z • x) = z • ofFin x := tsub_le_iff_right] · simp only [Neg.neg, BitVec.neg, BitVec.sub, HSub.hSub, Sub.sub, Fin.sub, Nat.sub_eq, and_pow_two_is_mod, zero_mod, zero_add, BitVec.ofNat, ofFin.injEq, Fin.mk.injEq] - induction' z using Nat.strongInductionOn with z ih - by_cases h : z + 1 < 2 ^ w - · rw [Nat.mod_eq_of_lt h, Nat.mod_eq_of_lt (lt_of_succ_lt h), Nat.sub_succ', Nat.sub_right_comm] - · by_cases h' : z + 1 = 2 ^ w - · simp only [h', mod_self, ge_iff_le, nonpos_iff_eq_zero, pow_eq_zero_iff', - OfNat.ofNat_ne_zero, ne_eq, false_and, tsub_zero, tsub_le_iff_right] - obtain rfl : z = 2 ^ w - 1 := by - apply Nat.succ_injective - show z + 1 = _ + 1 - rw [h', Nat.sub_add_cancel (one_le_two_pow _)] - have h_lt : 2 ^ w - 1 < 2 ^ w := by - sorry - simp only [ge_iff_le, Nat.mod_eq_of_lt h_lt, le_refl, tsub_eq_zero_of_le, zero_mod] - · have hz : z ≥ 2 ^ w := - sorry - rw [ - Nat.mod_eq_sub_mod (Nat.ge_of_not_lt h), - Nat.mod_eq_sub_mod hz, - Nat.succ_sub hz - ] - apply ih _ (Nat.sub_lt (lt_of_lt_of_le (two_pow_pos w) hz) (two_pow_pos w)) + rw [sub_succ_mod (two_pow_pos w)] -- See Note [no_index around OfNat.ofNat] @[simp] lemma ofFin_ofNat (n : ℕ) : @@ -222,7 +202,8 @@ lemma toFin_zsmul (z : ℤ) (x : BitVec w) : toFin (z • x) = z • x.toFin := @[simp] lemma toFin_natCast (n : ℕ) : toFin (n : BitVec w) = n := by apply toFin_inj.mpr; simp only [ofFin_natCast] -@[simp] lemma toFin_intCast (z : ℤ) : toFin (z : BitVec w) = z := rfl +@[simp] lemma toFin_intCast (z : ℤ) : toFin (z : BitVec w) = z := by + apply toFin_inj.mpr; simp only [ofFin_intCast] -- See Note [no_index around OfNat.ofNat] lemma toFin_ofNat (n : ℕ) : diff --git a/Mathlib/Data/Nat/Order/Lemmas.lean b/Mathlib/Data/Nat/Order/Lemmas.lean index 53533ef5aaddf..963622396d544 100644 --- a/Mathlib/Data/Nat/Order/Lemmas.lean +++ b/Mathlib/Data/Nat/Order/Lemmas.lean @@ -254,4 +254,29 @@ theorem div_lt_div_of_lt_of_dvd {a b d : ℕ} (hdb : d ∣ b) (h : a < b) : a / exact lt_of_le_of_lt (mul_div_le a d) h #align nat.div_lt_div_of_lt_of_dvd Nat.div_lt_div_of_lt_of_dvd +theorem sub_succ_mod {m : ℕ} (m_pos : m > 0) (y : ℕ) : + (m - (y + 1) % m) % m = (m - 1 - y % m) % m := by + induction' y using Nat.strongInductionOn with y ih + by_cases h : y + 1 < m + · rw [Nat.mod_eq_of_lt h, Nat.mod_eq_of_lt (lt_of_succ_lt h), Nat.sub_succ', Nat.sub_right_comm] + · by_cases h' : y + 1 = m + · simp only [h', mod_self, ge_iff_le, nonpos_iff_eq_zero, tsub_zero, tsub_le_iff_right] + obtain rfl : y = m - 1 := by + apply Nat.succ_injective + show y + 1 = _ + 1 + rw [h', Nat.sub_add_cancel m_pos] + have m_pred_lt : m - 1 < m := Nat.sub_one_lt_of_le m_pos Nat.le.refl + simp only [ge_iff_le, Nat.mod_eq_of_lt m_pred_lt, le_refl, tsub_eq_zero_of_le, zero_mod] + · have y_ge : y ≥ m := by + simp only [not_lt] at h + cases h + · contradiction + · assumption + rw [ + Nat.mod_eq_sub_mod (Nat.ge_of_not_lt h), + Nat.mod_eq_sub_mod y_ge, + Nat.succ_sub y_ge + ] + apply ih _ (Nat.sub_lt (lt_of_lt_of_le m_pos y_ge) m_pos) + end Nat From ee862420750839a5a0272052e206eee047159bcc Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Mon, 11 Dec 2023 22:21:49 +0000 Subject: [PATCH 20/28] WIP: fix `ofFin_intCast` Std changed the definition of `BitVec.ofInt`, breaking `ofFin_intCast`. This commit is a first step towards fixing this proof --- Mathlib/Data/BitVec/Lemmas.lean | 81 +++++++++++++++++++++++++++------ 1 file changed, 68 insertions(+), 13 deletions(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index dda82065e8984..3d2c34f8564fa 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -151,16 +151,6 @@ lemma ofFin_zsmul (z : ℤ) (x : Fin (2^w)) : ofFin (z • x) = z • ofFin x := simp only [Nat.cast, NatCast.natCast, OfNat.ofNat, BitVec.ofNat, and_pow_two_is_mod] rfl -@[simp] lemma ofFin_intCast (z : ℤ) : ofFin (z : Fin (2^w)) = z := by - simp only [Int.cast, IntCast.intCast, BitVec.ofInt, ge_iff_le, tsub_le_iff_right] - cases' z with z z - <;> rw [Int.castDef] - <;> simp only [Nat.cast, NatCast.natCast, Fin.ofNat_eq_val, ofFin_neg, ofFin_natCast, ge_iff_le, - tsub_le_iff_right] - · simp only [Neg.neg, BitVec.neg, BitVec.sub, HSub.hSub, Sub.sub, Fin.sub, Nat.sub_eq, - and_pow_two_is_mod, zero_mod, zero_add, BitVec.ofNat, ofFin.injEq, Fin.mk.injEq] - rw [sub_succ_mod (two_pow_pos w)] - -- See Note [no_index around OfNat.ofNat] @[simp] lemma ofFin_ofNat (n : ℕ) : ofFin (no_index (OfNat.ofNat n : Fin (2^w))) = OfNat.ofNat n := by @@ -202,9 +192,6 @@ lemma toFin_zsmul (z : ℤ) (x : BitVec w) : toFin (z • x) = z • x.toFin := @[simp] lemma toFin_natCast (n : ℕ) : toFin (n : BitVec w) = n := by apply toFin_inj.mpr; simp only [ofFin_natCast] -@[simp] lemma toFin_intCast (z : ℤ) : toFin (z : BitVec w) = z := by - apply toFin_inj.mpr; simp only [ofFin_intCast] - -- See Note [no_index around OfNat.ofNat] lemma toFin_ofNat (n : ℕ) : toFin (no_index (OfNat.ofNat n : BitVec w)) = OfNat.ofNat n := by @@ -212,6 +199,74 @@ lemma toFin_ofNat (n : ℕ) : end +/-! +### `IntCast` +-/ + +@[simp] +theorem Nat.bit_sub_bit (x y : ℕ) (a b : Bool) : + Nat.bit a x - Nat.bit b y = Nat.bit (a && !b) (x - y - (!a && b).toNat) := by + sorry + +@[simp] +theorem Nat.testBit_bit_succ (a : Bool) (x i : ℕ) : + testBit (bit a x) (i + 1) = testBit x i := by + sorry + +/-- If every bit of `y` is also set in `x`, then subtraction coincides with XOR -/ +theorem Nat.sub_eq_xor_of (x y : ℕ) (h : ∀ i, (y.testBit i = true) → (x.testBit i = true)) : + x - y = x ^^^ y := by + induction' x using Nat.binaryRec with x₀ x ih generalizing y + · simp only [zero_testBit, imp_false, Bool.not_eq_true] at h + rw [zero_of_testBit_eq_false h] + rfl + · cases' y using Nat.binaryRec with y₀ y + · simp only [tsub_zero, xor_zero] + · specialize ih y <| by intro i; simpa using h (i + 1) + have : y₀ = true → x₀ = true := by + simpa only [testBit_zero] using h 0 + cases y₀ + case false => + simp [-bit_false, ih] + case true => + obtain rfl : x₀ = true := this rfl + simp [-bit_true, -bit_false, ih] + +@[simp] lemma ofFin_intCast (z : ℤ) : ofFin (z : Fin (2^w)) = z := by + simp only [Int.cast, IntCast.intCast, BitVec.ofInt, ge_iff_le, tsub_le_iff_right] + cases' z with z z + <;> rw [Int.castDef] + <;> simp only [Nat.cast, NatCast.natCast, Fin.ofNat_eq_val, ofFin_neg, ofFin_natCast, ge_iff_le, + tsub_le_iff_right] + · simp only [Neg.neg, BitVec.neg, BitVec.sub, HSub.hSub, Sub.sub, Fin.sub, Nat.sub_eq, + and_pow_two_is_mod, zero_mod, zero_add, Complement.complement, BitVec.not, HXor.hXor, Xor.xor, + BitVec.xor, toNat_ofFin, BitVec.ofNat, ofFin.injEq, Fin.mk.injEq, Nat.shiftLeft_eq_mul_pow, + one_mul] + rw [ + sub_succ_mod (two_pow_pos w), + Nat.sub_sub, + Nat.mod_eq_of_lt <| Nat.sub_lt (two_pow_pos w) (Fin.size_pos'), + ←Nat.sub_sub + ] + show _ = (_ - 1) ^^^ _ + apply Nat.sub_eq_xor_of + intro i hz + rw [testBit_two_pow_sub_one, decide_eq_true_eq] + rw [testBit_to_div_mod, decide_eq_true_eq] at hz + induction' w with w ih generalizing i z + · exfalso + simp only [Nat.zero_eq, _root_.pow_zero, mod_one, Nat.zero_div, zero_mod, ne_eq, + not_true_eq_false] at hz + · cases' i with i + · exact succ_pos w + · apply succ_lt_succ + apply ih (z / 2) + simpa only [Nat.pow_succ, Nat.mul_comm, ← Nat.div_div_eq_div_mul, + ← Nat.div_mod_eq_mod_mul_div] using hz + +@[simp] lemma toFin_intCast (z : ℤ) : toFin (z : BitVec w) = z := by + apply toFin_inj.mpr; simp only [ofFin_intCast] + /-! ## Ring -/ From 8367843c194263351bd3c3e59dea25610c050b4c Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Mon, 11 Dec 2023 23:08:10 +0000 Subject: [PATCH 21/28] Update Mathlib/Data/BitVec/Lemmas.lean Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com> --- Mathlib/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 3d2c34f8564fa..7c7b091f71a77 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -246,7 +246,7 @@ theorem Nat.sub_eq_xor_of (x y : ℕ) (h : ∀ i, (y.testBit i = true) → (x.te sub_succ_mod (two_pow_pos w), Nat.sub_sub, Nat.mod_eq_of_lt <| Nat.sub_lt (two_pow_pos w) (Fin.size_pos'), - ←Nat.sub_sub + ← Nat.sub_sub ] show _ = (_ - 1) ^^^ _ apply Nat.sub_eq_xor_of From 61c9b26ab2e0929a7b6b92f80d98ee018d82e7b3 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Fri, 15 Dec 2023 14:34:15 +0000 Subject: [PATCH 22/28] Reduce PR to CommSemiring --- Mathlib/Data/BitVec/Lemmas.lean | 74 ++++----------------------------- 1 file changed, 8 insertions(+), 66 deletions(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 7c7b091f71a77..71ed1e3dbb6dd 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -203,77 +203,19 @@ end ### `IntCast` -/ -@[simp] -theorem Nat.bit_sub_bit (x y : ℕ) (a b : Bool) : - Nat.bit a x - Nat.bit b y = Nat.bit (a && !b) (x - y - (!a && b).toNat) := by - sorry +proof_wanted ofFin_intCast (z : ℤ) : + ofFin (z : Fin (2^w)) = z -@[simp] -theorem Nat.testBit_bit_succ (a : Bool) (x i : ℕ) : - testBit (bit a x) (i + 1) = testBit x i := by - sorry - -/-- If every bit of `y` is also set in `x`, then subtraction coincides with XOR -/ -theorem Nat.sub_eq_xor_of (x y : ℕ) (h : ∀ i, (y.testBit i = true) → (x.testBit i = true)) : - x - y = x ^^^ y := by - induction' x using Nat.binaryRec with x₀ x ih generalizing y - · simp only [zero_testBit, imp_false, Bool.not_eq_true] at h - rw [zero_of_testBit_eq_false h] - rfl - · cases' y using Nat.binaryRec with y₀ y - · simp only [tsub_zero, xor_zero] - · specialize ih y <| by intro i; simpa using h (i + 1) - have : y₀ = true → x₀ = true := by - simpa only [testBit_zero] using h 0 - cases y₀ - case false => - simp [-bit_false, ih] - case true => - obtain rfl : x₀ = true := this rfl - simp [-bit_true, -bit_false, ih] - -@[simp] lemma ofFin_intCast (z : ℤ) : ofFin (z : Fin (2^w)) = z := by - simp only [Int.cast, IntCast.intCast, BitVec.ofInt, ge_iff_le, tsub_le_iff_right] - cases' z with z z - <;> rw [Int.castDef] - <;> simp only [Nat.cast, NatCast.natCast, Fin.ofNat_eq_val, ofFin_neg, ofFin_natCast, ge_iff_le, - tsub_le_iff_right] - · simp only [Neg.neg, BitVec.neg, BitVec.sub, HSub.hSub, Sub.sub, Fin.sub, Nat.sub_eq, - and_pow_two_is_mod, zero_mod, zero_add, Complement.complement, BitVec.not, HXor.hXor, Xor.xor, - BitVec.xor, toNat_ofFin, BitVec.ofNat, ofFin.injEq, Fin.mk.injEq, Nat.shiftLeft_eq_mul_pow, - one_mul] - rw [ - sub_succ_mod (two_pow_pos w), - Nat.sub_sub, - Nat.mod_eq_of_lt <| Nat.sub_lt (two_pow_pos w) (Fin.size_pos'), - ← Nat.sub_sub - ] - show _ = (_ - 1) ^^^ _ - apply Nat.sub_eq_xor_of - intro i hz - rw [testBit_two_pow_sub_one, decide_eq_true_eq] - rw [testBit_to_div_mod, decide_eq_true_eq] at hz - induction' w with w ih generalizing i z - · exfalso - simp only [Nat.zero_eq, _root_.pow_zero, mod_one, Nat.zero_div, zero_mod, ne_eq, - not_true_eq_false] at hz - · cases' i with i - · exact succ_pos w - · apply succ_lt_succ - apply ih (z / 2) - simpa only [Nat.pow_succ, Nat.mul_comm, ← Nat.div_div_eq_div_mul, - ← Nat.div_mod_eq_mod_mul_div] using hz - -@[simp] lemma toFin_intCast (z : ℤ) : toFin (z : BitVec w) = z := by - apply toFin_inj.mpr; simp only [ofFin_intCast] +proof_wanted toFin_intCast (z : ℤ) : toFin (z : BitVec w) = z /-! ## Ring -/ -instance : CommRing (BitVec w) := - toFin_injective.commRing _ - toFin_zero toFin_one toFin_add toFin_mul toFin_neg toFin_sub - (Function.swap toFin_nsmul) (Function.swap toFin_zsmul) toFin_pow toFin_natCast toFin_intCast +-- TODO: generalize to `CommRing` after `ofFin_intCast` is proven +instance : CommSemiring (BitVec w) := + toFin_injective.commSemiring _ + toFin_zero toFin_one toFin_add toFin_mul (Function.swap toFin_nsmul) + toFin_pow toFin_natCast end Std.BitVec From 58717790f4af9f154986f004503dcbeb1ef1a1e7 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Fri, 15 Dec 2023 14:36:53 +0000 Subject: [PATCH 23/28] Formatting --- Mathlib/Data/BitVec/Lemmas.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 71ed1e3dbb6dd..908cae10472bc 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -203,8 +203,7 @@ end ### `IntCast` -/ -proof_wanted ofFin_intCast (z : ℤ) : - ofFin (z : Fin (2^w)) = z +proof_wanted ofFin_intCast (z : ℤ) : ofFin (z : Fin (2^w)) = z proof_wanted toFin_intCast (z : ℤ) : toFin (z : BitVec w) = z From 4e381cf70fa63b38011ef38ba2f80d9b6f29aafe Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 15 Dec 2023 16:15:51 +0100 Subject: [PATCH 24/28] Update Mathlib/Data/BitVec/Lemmas.lean Co-authored-by: Eric Wieser --- Mathlib/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 908cae10472bc..e0a4d5fd28c50 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -211,7 +211,7 @@ proof_wanted toFin_intCast (z : ℤ) : toFin (z : BitVec w) = z ## Ring -/ --- TODO: generalize to `CommRing` after `ofFin_intCast` is proven +-- TODO: generalize to `CommRing` after `ofFin_intCast` is proven instance : CommSemiring (BitVec w) := toFin_injective.commSemiring _ toFin_zero toFin_one toFin_add toFin_mul (Function.swap toFin_nsmul) From 98a9e96147022b93df64722a71f615fa11ae1588 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 15 Dec 2023 16:20:28 +0100 Subject: [PATCH 25/28] Add comment --- Mathlib/Data/BitVec/Lemmas.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index e0a4d5fd28c50..1f4677fab6da1 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -203,6 +203,8 @@ end ### `IntCast` -/ +-- Either of these follows trivially fromt he other. Which one to +-- prove is not yet clear. proof_wanted ofFin_intCast (z : ℤ) : ofFin (z : Fin (2^w)) = z proof_wanted toFin_intCast (z : ℤ) : toFin (z : BitVec w) = z From b8c92cb5e6853edaf24502b75ef7fd0205c546da Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 15 Dec 2023 16:21:36 +0100 Subject: [PATCH 26/28] Drop unused lemma --- Mathlib/Data/Nat/Order/Lemmas.lean | 25 ------------------------- 1 file changed, 25 deletions(-) diff --git a/Mathlib/Data/Nat/Order/Lemmas.lean b/Mathlib/Data/Nat/Order/Lemmas.lean index 963622396d544..53533ef5aaddf 100644 --- a/Mathlib/Data/Nat/Order/Lemmas.lean +++ b/Mathlib/Data/Nat/Order/Lemmas.lean @@ -254,29 +254,4 @@ theorem div_lt_div_of_lt_of_dvd {a b d : ℕ} (hdb : d ∣ b) (h : a < b) : a / exact lt_of_le_of_lt (mul_div_le a d) h #align nat.div_lt_div_of_lt_of_dvd Nat.div_lt_div_of_lt_of_dvd -theorem sub_succ_mod {m : ℕ} (m_pos : m > 0) (y : ℕ) : - (m - (y + 1) % m) % m = (m - 1 - y % m) % m := by - induction' y using Nat.strongInductionOn with y ih - by_cases h : y + 1 < m - · rw [Nat.mod_eq_of_lt h, Nat.mod_eq_of_lt (lt_of_succ_lt h), Nat.sub_succ', Nat.sub_right_comm] - · by_cases h' : y + 1 = m - · simp only [h', mod_self, ge_iff_le, nonpos_iff_eq_zero, tsub_zero, tsub_le_iff_right] - obtain rfl : y = m - 1 := by - apply Nat.succ_injective - show y + 1 = _ + 1 - rw [h', Nat.sub_add_cancel m_pos] - have m_pred_lt : m - 1 < m := Nat.sub_one_lt_of_le m_pos Nat.le.refl - simp only [ge_iff_le, Nat.mod_eq_of_lt m_pred_lt, le_refl, tsub_eq_zero_of_le, zero_mod] - · have y_ge : y ≥ m := by - simp only [not_lt] at h - cases h - · contradiction - · assumption - rw [ - Nat.mod_eq_sub_mod (Nat.ge_of_not_lt h), - Nat.mod_eq_sub_mod y_ge, - Nat.succ_sub y_ge - ] - apply ih _ (Nat.sub_lt (lt_of_lt_of_le m_pos y_ge) m_pos) - end Nat From affc6d45a4aa2fd277699473a105fc06b7e6e1e2 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Fri, 15 Dec 2023 15:25:19 +0000 Subject: [PATCH 27/28] Update Mathlib/Data/BitVec/Lemmas.lean Co-authored-by: Eric Wieser --- Mathlib/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index 1f4677fab6da1..ca4ace38f5269 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -203,7 +203,7 @@ end ### `IntCast` -/ --- Either of these follows trivially fromt he other. Which one to +-- Either of these follows trivially from the other. Which one to -- prove is not yet clear. proof_wanted ofFin_intCast (z : ℤ) : ofFin (z : Fin (2^w)) = z From a09afb8aa29036234c3e993dc2ef29fc61e3659f Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 15 Dec 2023 17:09:36 +0100 Subject: [PATCH 28/28] linarith --- Mathlib/Data/BitVec/Lemmas.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Data/BitVec/Lemmas.lean b/Mathlib/Data/BitVec/Lemmas.lean index ca4ace38f5269..6000cfe2541c2 100644 --- a/Mathlib/Data/BitVec/Lemmas.lean +++ b/Mathlib/Data/BitVec/Lemmas.lean @@ -5,7 +5,6 @@ Authors: Simon Hudon, Harun Khan -/ import Mathlib.Data.BitVec.Defs -import Mathlib.Tactic.Linarith /-! # Basic Theorems About Bitvectors