BitVec lemmas

Stream: mathlib4

[Jakob von Raumer]

I agree with the sentiment behind keeping the lemmas about BitVec in mathlib at a minimum, but shouldn't we at least have the ring iso to ZMod (2 ^ m) in there as an off-bridge? Right now it seems it's a CommRing instance without any algebraic properties proven about it? /cc @Kim Morrison @Alex Keizer @Patrick Massot

[Eric Wieser]

That equivalence is not true when m=0

[Eric Wieser]

I'd expect the iso with Fin (2^m) though

[Eric Wieser]

If you want Zmod then I'd expect you to have to compose with another iso

[Jakob von Raumer]

Shouldn't all algebraic statements rather be about ZMod? I thought the ring structure on Fin is more or less only defined to then put it on ZMod

[Jakob von Raumer]

Hm, though I guess both have their applications in terms of what the zero case should be

[Eric Wieser]

The nice thing about the Fin spelling is that the simplification lemmas can reduce the iso to ofFin and toFin, without needing to introduce new ofZMod and toZMod

[Patrick Massot]

I have no opinion about BitVec except I know that having BitVec stuff in Mathlib is annoying to the FRO.

[Eric Wieser]

Given we have the Ring instance in mathlib, I think a PR to add the corresponding RingEquiv alongside it would be very reasonable

[Jakob von Raumer]

Will do!

[Jakob von Raumer]

#20322

[Anirudh Suresh]

I’m trying to prove a BitVec lemma in Mathlib and I’m stuck on the right lemmas / approach.

import Mathlib

lemma BitVec.ofInt_append_zeros_eqv (w n : ℕ) (z : ℤ) :
  (BitVec.ofInt w z ++ (0#n)) = BitVec.ofInt (w + n) (z * 2 ^ n) := by
  sorry

Intuitively: 'ofInt w z' stores 'z mod 2^w', and appending 'n' zero bits should shift left by 'n', matching 'z * 2^n' at width 'w+n'
What’s the cleanest way to prove theorems like this which involves conversion between BitVec and Int? Any pointers to the right lemmas would be hugely appreciated.

[Eric Wieser]

I would start by applying toInt_injective, assuming that exists

[Anirudh Suresh]

Thanks. I tried that, and it does seem like the right first step.
After apply BitVec.toInt_injectiveand then simp/unfolding, the goal quickly turns into an Int arithmetic statement about Int.bmod.
The part I’m stuck on is that Int.bmod is defined via % plus the half-range adjustment, so the proof becomes reasoning about the % remainder and those < (m+1)/2 conditions.
Is there a lemma that relates bmod to emod/% under these inequalities?

import Mathlib

lemma BitVec.ofInt_append_zeros_eqv (w n : ℕ) (z : ℤ) :
  (BitVec.ofInt w z ++ (0#n)) = BitVec.ofInt (w + n) (z * 2 ^ n) := by
  apply (BitVec.toInt_inj (x:=BitVec.ofInt w z ++ 0#n) (y:=BitVec.ofInt (w + n) (z * 2 ^ n)) ).mp
  rw[BitVec.toInt_append_zero]
  rw[BitVec.toInt_ofInt,BitVec.toInt_ofInt,pow_add,mul_comm]
  all_goals sorry

[Ruben Van de Velde]

@loogle Int.bmod, _ % _

[loogle]

:search: Int.bmod_emod, Int.bmod_def, and 15 more

[Ruben Van de Velde]

A few of those should be relevant

[Violeta Hernández]

Why do we have lemmas about a data structure in mathlib? Shouldn't this go in batteries?

[Eric Wieser]

Sometimes the lemmas are easier to prove in terms of Mathlib's alternative hierarchy, and so it's often easier to prove in mathlib and wait for someone who wants it in batteries to relocate it