chore: prove that subtraction on BitStreams corresponds to subtraction on BitVectors #559
Conversation
|
Alive Statistics: 64 / 93 (29 failed) |
|
Alive Statistics: 64 / 93 (29 failed) |
4 similar comments
|
Alive Statistics: 64 / 93 (29 failed) |
|
Alive Statistics: 64 / 93 (29 failed) |
|
Alive Statistics: 64 / 93 (29 failed) |
|
Alive Statistics: 64 / 93 (29 failed) |
|
@AtticusKuhn, what a success! 🎉 Turning my broken hack into such a beautiful proof. I left many comments, but this is one of the most polished PRs I started reviewing. In retrospect, the proof seems straightforward, which is remarkable given the complex proof states one can reach. You broke it down into a couple of well-structured semantic pieces. |
|
Alive Statistics: 64 / 93 (29 failed) |
|
Alive Statistics: 64 / 93 (29 failed) |
1 similar comment
|
Alive Statistics: 64 / 93 (29 failed) |
There was a problem hiding this comment.
I am done. This looks perfect to me. @alexkeizer @bollu, feedback would be appreciated.
|
Alive Statistics: 64 / 93 (29 failed) |
1 similar comment
|
Alive Statistics: 64 / 93 (29 failed) |
Thank you for your guidance. Your feedback is very helpful. |
tobiasgrosser
changed the title
tobiasgrosser
changed the title
|
Alive Statistics: 64 / 93 (29 failed) |
|
If no one objects, then I am going to merge this PR because there has been no activity on it for three days. |
|
Alive Statistics: 64 / 93 (29 failed) |
| let carry : Bool := match i with | ||
| | 0 => false | ||
| | i + 1 => a.subCarries? b i | ||
| (!a i && b i || !xor (a i) (b i) && carry) |
There was a problem hiding this comment.
I find it hard to follow operator precedence here, with the xor. Some more parens would be appreciated!
| theorem subAux_inductive_lemma (i : Nat) : | ||
| a.subAux b i = ⟨(a.addAux b.neg i).1, subCarries? a b i⟩ := by | ||
| induction' i with i ih |
There was a problem hiding this comment.
We generally prefer rather mechanical names, based on a theorems type, over names based on intended usage.
This could, e.g., be called subAux_eq_addAux_neg
| theorem ofBitVec_sub : ofBitVec (x - y) ≈ʷ (ofBitVec x) - (ofBitVec y) := by | ||
| calc | ||
| _ ≈ʷ ofBitVec (x + -y) := by rw [BitVec.sub_eq_add_neg] | ||
| _ ≈ʷ ofBitVec x + ofBitVec (-y) := ofBitVec_add | ||
| _ ≈ʷ ofBitVec x + -(ofBitVec y) := add_congr equal_up_to_refl ofBitVec_neg | ||
| _ ≈ʷ ofBitVec x - ofBitVec y := by rw [sub_eq_add_neg] | ||
|
|
| <;> simp | ||
|
|
||
| @[simp] | ||
| theorem not_eq_and {a b : Bool} : ((!b) == (a && b)) = (!a && b) := by |
There was a problem hiding this comment.
You've got an extra whitespace here, just before the :=!
…n on BitVectors (#559) This PR proves the key theorem ```lean theorem ofBitVec_sub : ofBitVec (x - y) ≈ʷ (ofBitVec x) - (ofBitVec y) := by calc _ ≈ʷ ofBitVec (x + - y) := by rw [BitVec.sub_add_neg] _ ≈ʷ ofBitVec x + ofBitVec (-y) := ofBitVec_add _ ≈ʷ ofBitVec x + - ofBitVec y := add_congr equal_up_to_refl ofBitVec_neg _ ≈ʷ ofBitVec x - ofBitVec y := by rw [sub_add_neg] ``` Which shows that subtraction on BitStreams corresponds to subtraction on BitVectors. In doing so, this PR removes the last "sorry" from the file BitStream.lean. Note that this PR is a continuation of PR #554 --------- Co-authored-by: Atticus Kuhn <atticusmkuhn@atticsmkuhn.com> Co-authored-by: Tobias Grosser <tobias@grosser.es>
This PR proves the key theorem
Which shows that subtraction on BitStreams corresponds to subtraction on BitVectors.
In doing so, this PR removes the last "sorry" from the file BitStream.lean.
Note that this PR is a continuation of PR
#554