search

opencompl / lean-mlir

A minimal development of SSA theory
Other
88 stars 10 forks source link

chore: prove that subtraction on BitStreams corresponds to subtraction on BitVectors #559

Closed AtticusKuhn closed 2 months ago

AtticusKuhn commented 2 months ago

This PR proves the key theorem

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 https://github.com/opencompl/lean-mlir/pull/554

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

tobiasgrosser commented 2 months ago

@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.

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

AtticusKuhn commented 2 months ago

CC: @bollu @alexkeizer

I think this PR is in pretty good shape. I would appreciate if you would review it.

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

AtticusKuhn commented 2 months ago

I am done.

Thank you for your guidance. Your feedback is very helpful.

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

AtticusKuhn commented 2 months ago

If no one objects, then I am going to merge this PR because there has been no activity on it for three days.

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)