I'm trying to do a slightly odd thing with z3. I'm trying to see if I can use z3 to get something like an "apply" tactic from an interactive theorem prover. I have a theorem like ForAll([x], Implies(a(x),b(x))
, and a goal c
that is syntactically equal to b(x)
for the appropriate choice of x
. If I could instantiate x correctly, I can replace the goal c
with a(inst_x)
. Is there a way to use z3 the get the appropriate x? I can't use just a model, because c might contain free variables.
I've been trying seeing if I could find it in z3 proof terms for a query like Implies(ForAll([x],b(x)), c)
, or somehow use the E-matching pattern facilities, but I'm stumped.
z3 internally must have sophisticated matching and unification capabilities, but I don't see where they might be exposed in the python interface.
Suggestions? Thanks