BitVector decide and networks

Stream: new members

[Michael Bucko]

Got inspired by lehmer_correct and Bitblast in the Lean4 repo.

Wrote two examples- one (Fin 10000) gives me (kernel) deep recursion detected, the other one (Fin 1000) works smoothly.

example : ∀ (bv : Fin 10000 → BitVec 64),
  (∑ i, bv i &&& bv ((i + 1) % 10000)) +
  (∑ i, bv i ^^^ bv ((i + 1) % 10000)) =
  (∑ i, bv i ||| bv ((i + 1) % 10000)) := by
  intros
  bv_decide

example : ∀ (bv : Fin 1000 → BitVec 64),
  (∑ i, bv i &&& bv ((i + 1) % 1000)) +
  (∑ i, bv i ^^^ bv ((i + 1) % 1000)) =
  (∑ i, bv i ||| bv ((i + 1) % 1000)) := by
  intros
  bv_decide

[Eric Wieser]

Note that (i + 1) % 10000 means the same thing as i + 1 there, as (10000 : Fin 10000) = 0 and fortunately x % 0 = x