feat: add BitVec.toFin_append

[tobiasgrosser]

This adds BitVec.[toInt|toFIn]_append.

An alternative way to state toFin_append is:

[simp] theorem toFin_append (x : BitVec m) (y : BitVec n)
    (h : x.toNat <<< n ||| y.toNat < 2 ^ (m + n) := toNat_append_lt x y) :
    (x ++ y).toFin = @Fin.mk (2^(m+n)) (x.toNat <<< n ||| y.toNat) h  := by

which avoids the toNat_append proof in the match. @bollu reported this is preferable for robustness, but we would appreciate feedback from lean experts.

[bollu]

I think it's more general to have h be a proof, I have had situations where lean fails to unify correctly with the proposition when we fix the proof to be a a particular proof, even if we have proof irrelevance.

[tobiasgrosser]

I added a proof template for:

@[simp] theorem toInt_append {x : BitVec n} {y : BitVec m} :
    (x ++ y).toInt = if n == 0 then y.toInt else x.toInt * (2 ^ m) + y.toNat := by

but got a bit stuck in the actual proof. On the other hand, I find the toInt statement actually pretty neat.