Induction and first-order assertions

[robdockins]

This PR adds some new capabilities to SAW's proof engine.

The first is the ability to automatically generate and use induction principles on bitvector values to prove inductive properties, with a new prove_by_bv_induction command. The idea is that the user specifies both the property to prove and also a decreasing bitvector value. The system automatically constructs an appropriate induction schema by reduction to induction on the natural numbers and applies it to the term. For example:

prove_by_bv_induction tac {{ \(x:[64]) (y:[64]) -> ( x, x+y == y+x) }}; 

Indicates that the user is attempting to prove that 64-bit addition is commutative by induction on the (unsigned) value of x. Upon invoking this, the given tactic will need to prove a goal of the following form (which as been cleaned up a bit for readability):

let { x@1 = Vec 64 Bool
    }
 in (x : x@1)
-> (y : x@1)
-> ((i_x : x@1)
    -> (i_y : x@1)
    -> EqTrue (bvult 64 i_x x)
    -> EqTrue
         (ecEq x@1 (PEqWord 64) (bvAdd 64 i_x i_y) (bvAdd 64 i_y i_x)))
-> EqTrue (ecEq x@1 (PEqWord 64) (bvAdd 64 x y) (bvAdd 64 y x))

This provides the user with an induction hypothesis for all x_i values less than x.

Also in this PR is the ability to assert universally-quantified statements to solvers via the What4 backend. This is helpful for, e.g., actually invoking the induction hypotheses that arise as above, but also for general reasoning up to universal lemmas.

[robdockins]

Incorporated into #1689