Chore: Prove that subtraction on BitVectors is the same as subtraction on BitStreams

[AtticusKuhn]

If this PR is successful, it will remove the last sorry from "BitStream.lean".

There is one difficulty, however, and that is that I am not sure how to prove that "a - b = a + (-b)" on bitstreams. For this reason, I am making this a draft PR until I figure out how to prove that. My only idea is to come up with some auxiliary function "f" such that

/--
g is some unknown auxiliary function that will be useful in proving sub_add_neg
-/
def g (a b : BitStream) (i : Nat) : Bool := sorry

theorem g_zero {a b : BitStream} :
    (!a 0 && b 0) = a.g b 0 := by
  sorry

theorem g_succ_left {a b : BitStream} (i : ℕ) :
    xor (b (i + 1)) (a.g b i) = ((!b (i + 1)) != ((b.negAux i).2 != (a.addAux (fun n => (b.negAux n).1) i).2)) := by
  sorry

theorem g_succ_right {a b : BitStream} (i : ℕ)  :
    (!a (i + 1) && b (i + 1) || !xor (a (i + 1)) (b (i + 1)) && a.g b i) = a.g b (i + 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)

[tobiasgrosser]

I just looked at this again. I feel the proof you are trying to proof here is indeed a bit complicated. Can you proof theorem neg_neg {a b : BitStream} : - - a ≈ʷ a? The proof strategy should in parts be similar, but this seems to have a lot less moving parts.

[AtticusKuhn]

I just looked at this again. I feel the proof you are trying to proof here is indeed a bit complicated. Can you proof theorem neg_neg {a b : BitStream} : - - a ≈ʷ a? The proof strategy should in parts be similar, but this seems to have a lot less moving parts.

@tobiasgrosser

Done, here it is:

theorem xor_lemma {a b : Bool}:  xor (!xor (a) b) b = !a := by
  cases a
  <;> cases b
  <;> simp

theorem and_lemma {a b : Bool}:  (!xor a b && b) = (a && b) := by
  cases a
  <;> cases b
  <;> simp

theorem neg_neg : a = - - a := by
  ext n
  have neg_lemma  (i : Nat):
    (a.neg).negAux i = ⟨a i , (a.negAux i).2 ⟩ := by
    induction' i with i ih
    · simp [neg, negAux]
    · simp [neg, negAux, ih,xor_lemma,and_lemma]
  simp [Neg.neg,neg,negAux,neg_lemma]

although I'm not sure how this will help me.

[tobiasgrosser]

Can you PR this? It helps me (and maybe others to get a good understanding of the problem).

[tobiasgrosser]

We can ask @alexkeizer and @bollu for input tomorrow. Meanwhile, maybe look back into the LLVM parsing work if you feel blocked.

[AtticusKuhn]

Can you PR this? It helps me (and maybe others to get a good understanding of the problem).

Sure, I can PR this. Would you like it in this PR or in a new PR?

[tobiasgrosser]

New one. Than we can already merge this.

[AtticusKuhn]

New one. Than we can already merge this.

@tobiasgrosser Done. See https://github.com/opencompl/lean-mlir/pull/558

[tobiasgrosser]

I oked the other PR. If you could rebase this on the other one, after this is merged, this is super helpful. Let's then see if @alexkeizer and @bollu to can take a look at this PR later today.

[AtticusKuhn]

Got it. Will do.

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[tobiasgrosser]

@AtticusKuhn, I made some progress. Can you see if this helps you over the hump?

[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)

[alexkeizer]

@AtticusKuhn I can't quite follow what's going on in the PR description. Could you try to format it a little, using codeblocks (i.e., ``` code ```), to make it a tad more readable?

That said, I would try to prove x - y = x + (-y) using a bisimulation. Roughly, that would go as follows

1. Reduce both operations to BitStream.corec (this operation exists), so that the goal becomes corec ?f = corec ?g, for some f and g
2. Then, prove a corec_eq_of_bisim lemma (I don't think it exists yet), akin to Stream'.eq_of_bisim in Mathlib. Our BitStreams are just Stream' Nats, so you should be able to reuse most of the Mathlib proof (since both us and Mathlib are Apache licensed, it's fine to copy/paste the proof!)
3. Using the lemma we just proved, our original goal reduces to showing that ?f and ?g are in bisimulation with eachother, which hopefully should be doable, given that bisimulation is a local (i.e., bit-by-bit) property

[AtticusKuhn]

I'm closing this PR because I think it is getting a bit long.

I proved the desired statement in PR https://github.com/opencompl/lean-mlir/pull/559