[Axiom-developer] Proving Axiom Correct

[daly]

ACL2 proof automation is already in place.

With this latest push every function in every category, domain, and
package has an attached signature. Every function is automatically
pushed through COQ, only as a comment form at the moment. Function
proofs can be automated by lifting them out of the comment section
which leads to an incremental strategy.

There appear to be about 14000+ algebra functions so this effort will
take a few weeks :-)

The next step is to choose functions to prove. 

Initially this seems like one of three choices:

  1 choose functions that are trivial (e.g. == false)
  2 choose functions that are covers for underlying lisp code
  3 choose a domain, e.g. List

Choice 1 seems easiest to prove and will likely be an initial step.

Choice 2 has the advantage that the underlying lisp code can be
proven in ACL2 and the algebra level by COQ. This demonstrates the
synergy between the two system when used in Axiom.

Choice 3 attacks a domain that seems well studied in the COQ literature.

In any case, the preparations are in place.

Tim