chore: prove that negation on bitstreams is the same as negation on bitvectors

[AtticusKuhn]

There are currently three sorries in SSA/Experimental/Bits/Fast/BitStream.Lean.

In this current PR, I only remove the sorry from "neg" to keep each PR small and atomic.

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[bollu]

Unfortunately, I don't believe lemma1. Proof of disbelief:

axiom lemma1 {w n : Nat} {x : BitVec w} :
  (-x).getLsb (n + 1 + 1) = (x.getLsb (n + 1 + 1) != (-x).getLsb (n + 1))

open BitVec in
theorem contra : (-(1#2)).getLsb 2 =
  ((1#2).getLsb 2 != (-(1#2)).getLsb 1) :=
  lemma1

theorem exploison : False := by
  have := contra
  simp at this

/-- info: 'exploison' depends on axioms: [propext, lemma1, Quot.sound, Classical.choice] -/
#guard_msgs in #print axioms exploison

[AtticusKuhn]

That is a good catch @bollu . I did not see that before. I have refined these three lemmas so that proving my goal can be reduced to proving:

lemma lemma1 (h : n + 1 < w) : (-x).getLsb (n + 1) = decide (x.getLsb (n + 1) = !(-x).getLsb n) := by
  sorry

lemma lemma2 (h : n + 1 < w) (c  : x.getLsb n) :  (-x).getLsb (n + 1) = !x.getLsb (n + 1) := by
  sorry

lemma lemma3 :   (2 ^ w - x.toNat) % 2 ^ w / 2 % 2 = 1 ↔ (x.toNat / 2 % 2 = 1 ↔ ¬x.toNat % 2 = 1) := by
  sorry

And this time, I have written a script to check all small examples on lemma1, so I am confident that there will at least not be any obvious counter-examples to lemma1.

[AtticusKuhn]

Actually, I have managed to make further simplifications, and now I am only required to prove

lemma lemma7 {w t : Nat} (a : 0 < w) (h : t < 2 ^ w) : (2 ^ w - 1 - t + 1) % 2 = 1 ↔ t % 2 = 1 := by
  sorry

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[bollu]

@AtticusKuhn here you go:

theorem lemma7 (w : Nat) (hw : w > 0) (t : Nat) (h : t < 2 ^ w) : (2 ^ w - 1 - t + 1) % 2 = 1 ↔ t % 2 = 1 := by
  rcases w with rfl | w
  · simp at hw
  · omega

[AtticusKuhn]

Thanks to the help froim Sid and Henrik, I have now removed one sorry (which was for neg).

[tobiasgrosser]

Is this something that can already pulled out and be reviewed separately? Let's try to keep our prs small.

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[AtticusKuhn]

Is this something that can already pulled out and be reviewed separately? Let's try to keep our prs small.

Got it. I will only solve the case of "neg" in this PR and solve the other two cases in another PR.

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[AtticusKuhn]

I have removed the sorry in the case of "neg". I now think this PR is ready for review.

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[alexkeizer]

@AtticusKuhn I took the liberty of renaming your PR: it's generally best to describe the actual result you've proven, instead of saying you've removed a sorry from a file. The former requires the reader to have remembered less context to understand what the PR does!

In the PR description, then, you can mention that this result closes one of the open sorries in that particular file

[AtticusKuhn]

Thank you Alex for your feedback.

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[AtticusKuhn]

Thank you for your feedback.

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[AtticusKuhn]

I have now made all the changes from Sid's, Alex's, and William's review. I think this PR is ready to be merged now. (I know there are some unrelated changes in the git diff, they were already merged in https://github.com/opencompl/lean-mlir/pull/533 but I don't know how to mkake these changes disappear from the git diff)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[AtticusKuhn]

Thanks for your feedback. I have changed some "simp only"s to "simp"s in the case where it is in the terminal position.

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[AtticusKuhn]

I now think this PR is ready to be merged.

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)