saw-script: Remove non-working command prove_by_bv_induction.

[brianhuffman]

Currently any non-trivial use of prove_by_induction fails with an internal SAWCore type error.

Instead of prove_by_bv_induction, tactic goal_apply should be used with a suitable induction rule.

Fixes #2770.

[brianhuffman]

I would probably be good to add a regression test that proves a goal using some kind of induction rule over a bit vector type. The strong induction principle that was formerly hard-coded into prove_by_bv_induction does not work well, because its universally-quantified inductive hypothesis is not supported by any of our prover backends, nor can our rewriter make use of it. Something with 0 and n+1 cases should work well.

[sauclovian-g]

Yeah, it would be good to have a test. We should probably have some kind of induction tactic that manages the proof state nicely... and I'm not sure we should close #2770 without one... but having a working example is an important step on the way there.

(I am, perhaps naively, assuming there's some complication such that it made sense to add prove_by_bv_induction in the first place; but maybe not...)

[brianhuffman]

I'm converting to "draft" status until I come up with a good induction rule and example proof that uses it.

[brianhuffman]

I added a regression test in 22a94af that defines a bit-vector induction principle in SAWCore and proves some non-trivial properties using it: I show that two different functions defined by primitive recursion are equivalent to closed-form non-recursive definitions.

I think this shows pretty convincingly that goal_apply is fit for purpose and that we don't need prove_by_bv_induction.

[sauclovian-g]

It seems unfortunate that this is necessary... but on review it also seems like it just belongs in Prelude.sawcore. Any reason not to move it there?

[brianhuffman]

Yes, we should probably figure out a minimal set of defining axioms for primitives like bvAdd and put those in the prelude.

An axiom like the following would let us prove bvNat_Succ and also the existing axioms bvAddZeroL and bvAddZeroR:

axiom bvNat_addNat:
  Eq (Vec n Bool)
  (bvNat n (addNat x y))
  (bvAdd.n (bvNat n x) (bvNat n y);

saw-script/saw-core/prelude/Prelude.sawcore

Lines 1821 to 1822 in 9bd84f0

	axiom bvAddZeroL : (n : Nat) -> (x : Vec n Bool) -> Eq (Vec n Bool) (bvAdd n (bvNat n 0) x) x;
	axiom bvAddZeroR : (n : Nat) -> (x : Vec n Bool) -> Eq (Vec n Bool) (bvAdd n x (bvNat n 0)) x;

So maybe I'll update Prelude.sawcore accordingly.

[brianhuffman]

Changing the set of axioms in the Prelude means figuring out how to map the new axioms into Rocq for the Rocq back-end, and that seems like a bit of mission creep for this PR. I'll open a ticket to remind us to move stuff into Prelude.sawcore later.

[brianhuffman]

I opened issue #3222 to track the SAWCore prelude updates.

[brianhuffman]

The only test failure is the infamous test_timeout, so I'm going to go ahead and merge anyway.