bitadd is equivalent to BitVector addition #358
Conversation
Std/Data/BitVec/Bitblast.lean
Outdated
| · simp [mod_one, ofBits] | ||
| · simp [bitwise_add, Nat.mod_eq_of_lt ofBits_lt] | ||
|
|
||
| theorem BV_add {x y : BitVec w} : bitwise_add (x.toNat) y.toNat w = (x + y).toNat := by |
There was a problem hiding this comment.
| theorem BV_add {x y : BitVec w} : bitwise_add (x.toNat) y.toNat w = (x + y).toNat := by | |
| theorem bitwise_add_toNat {x y : BitVec w} : bitwise_add x.toNat y.toNat w = (x + y).toNat := by |
Std/Data/BitVec/Bitblast.lean
Outdated
| | i + 1 => (x.testBit i && y.testBit i) || ((x.testBit i ^^ y.testBit i) && bitwise_carry x y i) | ||
|
|
||
| /-- Bitwise addition implemented via a ripple carry adder. -/ | ||
| @[simp] def bitwise_add (x y i : Nat) := |
There was a problem hiding this comment.
Are you sure you want @[simp] here? Usually it is a bad idea to just let definitions fall apart anytime someone mentions simp nearby!
There was a problem hiding this comment.
I see, in every use case when I want to unfold the definition I want to go directly to unfolding ofBits too (i.e. the intermediate state isn't useful). Perhaps, there's another way to automatically unfold ofBits too whenever I want to unfold without doing simp only [bitadd, ofBits]?
| /-! ### Preliminaries -/ | ||
|
|
There was a problem hiding this comment.
Most of this section should be moved to earlier files.
Co-authored-by: Scott Morrison <[email protected]>
Co-authored-by: Scott Morrison <[email protected]>
Co-authored-by: Scott Morrison <[email protected]>
Co-authored-by: Scott Morrison <[email protected]>
| def ofBits (f : Nat → Bool) (z : Nat) : Nat → Nat | ||
| | 0 => z | ||
| | i + 1 => ofBits f (z.bit (f i)) i |
There was a problem hiding this comment.
This has undergone a fair amount of review in Mathlib, but it seems the review there has been discarded and we've reverted back to the original version. The suggestion there was to use
| def ofBits (f : Nat → Bool) (z : Nat) : Nat → Nat | |
| | 0 => z | |
| | i + 1 => ofBits f (z.bit (f i)) i | |
| def ofBits {z : Nat} (f : Fin z → Bool) : Nat := sorry |
mhk119
changed the title
leanprover-community-mathlib4-bot
added
the
merge-conflict
|
I'm going to close this. The author's work was appreciated and adapted into #366. |
In this PR, we prove a bit-blasting theorem for addition. This depends on #314. I copied the changes in #314 and pasted them manually, but once that gets merged, the number of changes will decrease. The only real additions happen in
Std.Data.BitVec.Bitblast.