Implement a `bvify by` tactic

[sonmarcho]

trafficstars

It often happens that bvify gets stuck because it is non trivial to discharge some precondition. When this happens one has to write by hand the target expression, and prove that it is a correct lifting by going the other way around (with for instance, natify; simp_scalar).

For this purpose, it would be good to introduce a bvify (at ident)? by tactic tactic, which would lift an assumption (or the goal) to something expressed using bit-vectors without any proof, and would let the user prove that the new proposition is equivalent to the old one.

For instance:

example (byte : U8) : byte.val >>> 4 < 16 := by
  bvify by
     /- The goal becomes:
          byte.val >>> 4 < 16 <-> byte.bv >> 4 < 16#8 -/
    natify; simp
  -- Now the goal is: byte.bv >>> 4 < 16#8
  bv_decide