Variable Macro For bv_decide

Stream: new members

[Oscar Bender-Stone]

I am trying to use bv_decide on a vector of variables, and it returns with a "potientially spurious counterexample":

import Mathlib.Data.BitVec
import Std.Tactic.BVDecide

/- The prover found a counterexample, consider the following assignment: -/
/- x = 0x3#2 -/
/- y = 0x3#2 -/
lemma test (x y : BitVec 2): x &&& ~~~x + y = 0 := by
  bv_decide

/- The prover found a potentially spurious counterexample: -/
/- - It abstracted the following unsupported expressions as opaque variables: [x[1], x[0]] -/
/- Consider the following assignment: -/
/- v[0] = 0x3#2 -/
/- v[1] = 0x3#2 -/
lemma vector_test (v : Vector (BitVec 2) 2): v[0] &&& ~~~v[0] + v[1] = 0 := by
  bv_decide

I understand from this GitHub issue [https://github.com/leanprover/lean4/issues/5326] that bv_decide doesn't always work with abstracted terms. In the case above, the counterexample is correct, but I want to use Array.foldl to generate new constraints (e.g., to check whether each component of the vector is 0). Is there a way that I could generate n variables (of the same type) in a theorem using a macro, or would I need to combine my variables into a single BitVec? I tried writing a macro to create two variables, and that didn't work:

macro "#vars" : command => `(variable (x y : Bool))

#vars

/- unknown identifier 'x' -/
/- unknown identifier 'y' -/
theorem macro_test: x && y = 0 := by bv_decide

[Henrik Böving]

I understand from this GitHub issue https://github.com/leanprover/lean4/issues/5326 that bv_decide doesn't always work with abstracted terms

Yes, the reason for this is that bv_decide only works on BitVec and Bool theory so when you have, in your case, a Vector term around there is nothing saying that you might not have additional hypotheses from the theorey that your BitVec atoms are coming from that would invalidate counter examples that bv_decide finds so it has to account for this.

Your macro doesn't work because of hygiene.

It's not quite clear to me what your desired end goal here is. Do you want to generate a theorem statements automatically? Do you want to automatically introduce additional hypotheses?

[Oscar Bender-Stone]

Oh I see - thank you for the clarification on bv_decide and hygiene.

I want to generate theorem statements automatically. For instance, I would like to write something like:

theorem (x1 ... xn : BitVec 2): x1 + ... + xn = 0

for, say, n = 3.

[Henrik Böving]

You can write a macro that does something like this in principle sure. Is there a particular reason you dislike the Vector based approach?

[Oscar Bender-Stone]

Henrik Böving said:

Is there a particular reason you dislike the Vector based approach? In my situation, I have several constraints like these:

Is there a way to make bv_decide work with Vector and Array.foldl?

def gt_one (vars : Vector (BitVec 10) 3) : Bool :=
  Array.foldl (fun acc v => v > 1 && acc) true vars.1

/- The prover found a potentially spurious counterexample: -/
/- - It abstracted the following unsupported expressions as opaque variables: [BitVec.ofBool (gt_one vars)] -/
/- Consider the following assignment: -/
/- BitVec.ofBool (gt_one vars) = 0x0#1 -/
theorem gt_one_test (vars : Vector (BitVec 10) 3) : gt_one vars := by bv_decide

I want to make sure bv_decide does return sat if the theorem is actually sat and not this error message. It would be great if I could also get the counter-example. Either way, I am not sure how to expand out Array.foldl to make this work.

[Henrik Böving]

Basically speaking bv_decide will only work on things that are within the basic BitVec theory of Lean so if you want to call it you need to first simplify your goal towards this. What you can do in this specific situation is run something like this:

import Std.Tactic.BVDecide

def gt_one (vars : Vector (BitVec 10) 3) : Bool :=
  Array.foldl (fun acc v => v > 1 && acc) true vars.1

theorem gt_one_test (vars : Vector (BitVec 10) 3) : gt_one vars := by
  simp [gt_one, Array.foldl, Array.foldlM, Array.foldlM.loop, Id.run]
  bv_decide

Which is of course a bit annoying but works out. If we had more simp API around this type of stuff this would certainly be more convenient to write.

[Oscar Bender-Stone]

Thank you, that works well! I appreciate your help! I didn't know about completely simplifying Array.foldl.

[Notification Bot]

Oscar Bender-Stone has marked this topic as resolved.

[Notification Bot]

Oscar Bender-Stone has marked this topic as unresolved.

[Notification Bot]

Oscar Bender-Stone has marked this topic as resolved.

[Notification Bot]

Oscar Bender-Stone has marked this topic as unresolved.

[Oscar Bender-Stone]

Could anyone provide some code to generate variables via a macro in a theorem? Currently, when I use BitVec, it sometimes assigns the same component of a vector two two different numbers. I think the main culprit is using .toNat in a few functions, so if there is a way to simplify .toNat methods instead, that would be even better.