Re: [Axiom-developer] [Proving Axiom Correct] Bootstrapping a library

[Kurt Pagani]

Am 08.02.2017 um 15:29 schrieb Tim Daly:
> The game is to prove GCD in NonNegativeInteger (NNI).

We encounter numerous problems when trying to prove gcd from EuclideanDomain:

---
gcd(x, y) ==   --Euclidean Algorithm
  x := unitCanonical x
  y := unitCanonical y
  while not zero? y repeat
    (x, y) := (y, x rem y)
    y := unitCanonical y     -- this doesn't affect the
                             -- correctness of Euclid's algorithm,
                             -- but
                             -- a) may improve performance
                             -- b) ensures gcd(x, y)=gcd(y, x)
                             --    if canonicalUnitNormal
  x

---

1. Define type EuclideanDomain (tower of hierarchies)
2. Define unitCanonical (depends on canonicalUnitNormal etc.)
3. Imperative elements in spad
4. Trust interpreter/compiler and lisp

While (1,2) seems not so difficult, (3) might be delicate and (4) seems to be
out of scope for the moment (that is let's trust it, as an axiom so to speak ).

Basically, I see two methods:

a) Implement spad language, e.g. like the "Imp" example:
https://www.seas.upenn.edu/~cis500/current/sf/Imp.html
and prove the statements.

b) Prove the math (by reusing existing [abundant] math libraries) and extract
the functions (Definitions in Coq) as spad code.
This would actually mean to replace parts of current code by new one (purely
functional).

Clearly, both methods will require a definition of spad's key
functions/operators. I believe that (a) is more laborious than (b). Moreover,
Coq's notation mechanism (Notation) has it's limits (e.g. conflicts with
built-in keywords)(**). Moreover, method (b) is admittedly not what we really
want: namely proving existing Axiom code correct.

(**) a parser might be a better solution
https://www.seas.upenn.edu/~cis500/current/sf/ImpParser.html

> 
> We would like to use the 'nat' theorems from the existing library
> but extract those theorems automatically from Axiom sources
> at build time.
> 
> Axiom's NNI inherits from a dozen Category objects, one of which
> is BasicType which contains two signatures:
> 
>  ?=?: (%,%) -> Boolean       ?~=?: (%,%) -> Boolean
> 
> In the ideal case we would decorate BasicType with the existing
> definitions of = and ~= so we could create a new library structure
> for the logic system. So BasicType would contain
> 
> theorem = (a, b : Type) : Boolean := .....
> theorem ~= (a, b : Type) : Boolean := ....
> 
> These theorems would be imported into NNI when it inherits the
> signatures from the BasicType Category. The collection of all of
> the theorems in NNI's Category structure would be used (hopefully
> exclusively) to prove GCD. In this way, all of the theorems used to
> prove Axiom source code would be inheritied from the Category
> structure.


Parameter BasicType:Type.
Parameter eq: BasicType -> BasicType -> bool.
Parameter neq: BasicType -> BasicType -> bool.
Infix "=" := eq.

Parameter x y z:BasicType.
Check (x=y).

There are several better choices of course: Module Type or type classes,
whereas I'm not very used to the latter.

> 
> Unfortunately it appears the Coq and Lean will not take kindly to
> removing the existing libraries and replacing them with a new version
> that only contains a limited number of theorems. I'm not yet sure about
> FoCaL but I suspect it has the same bootstrap problem.

I think you can overwrite anything and even do a

$ coqtop -noinit

so that even "nat" is unknown.

Coq < Check nat.
Toplevel input, characters 6-9:
> Check nat.
>       ^^^
Error: The reference nat was not found in the current environment.

> 
> Jeremy Avigad (Lean) made the suggestion to rename these theorems.
> Thus, instead of =, the supporting theorem would be 'spad=' (spad is
> the name of Axiom's algebra language).
> 
> Initially this would make Axiom depend on the external library structure.
> Eventually there should be enough embedded logic to start coding Axiom
> theorems by changing external references from = to spad= everywhere.
> 
> Axiom proofs would still depend on the external proof system but only
> for the correctness engine, not the library structure. This will minimize
> the struggle about Axiom's world view (e.g. handling excluded middle).
> It will also organize the logic library to more closely mirror abstract 
> algebra.

Indeed, this is an important point when dealing with dependent types. Type
classes
(http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf)
presumably could serve best to map the spad categories while reasoning in CoC
(whilst "exlcuded middle" may be introduced as needed).

> 
> Comments, suggestions?

I believe that some more research will be necessary to find the most suitable
approach before building a prototype. I should dig into the "type classes"
subject before making any suggestions.

BTW I have recently written "field_mpl.v" (attached) for a talk about MPL where
you can see how tedious it can be to prove simple facts from scratch, whereas
the last prop (P1) goes with ease owing to solid preparations (it's educational
only of course).
> 
> Tim
> 
> 
> 
> 
> _______________________________________________
> Axiom-developer mailing list
> address@hidden
> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>

field_mpl.v
Description: Text document