How to use `BitVec.le_def`

Stream: new members

[Luisa Cicolini]

Hello :) I have a very newbie question:
I am trying to use BitVec.le_def to prove that x >= x - y, where x and y are logical expressions (e.g. a &&& b) and x and y are bitvectors, but the tactic rewrite fails and I can not understand why. I guess it might be because I am missing some guarantees on y, but have no idea how to add that either for BitVecs.
thanks :)

[Ruben Van de Velde]

Please provide a #mwe (follow the link for instructions)

[Luisa Cicolini]

thank you for the link!
this is the theorem (no imports needed):

theorem ex1 :
  BitVec.ule (x ||| y) ((x ||| y) - (x &&& y)) := by
  rw [BitVec.le_def]

and the specific error I am getting is:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ?x ≤ ?y
w✝ : Nat
x y : BitVec w✝
⊢ (x ||| y).ule ((x ||| y) - (x &&& y)) = true

[Ruben Van de Velde]

That makes sense, because your goal is about BitVec.ule, not ≤

[Ruben Van de Velde]

@loogle BitVec.ule, LE.le

[loogle]

:search: BitVec.ule.eq_1

[Ruben Van de Velde]

That should work

[Luisa Cicolini]

it did!! Thank you very much :)