Re: [Axiom-developer] Call for help

[Kurt Pagani]

A look at the definition of "gcd" in catdef.spad shows that the tricky
bit is how to deal with imperative constructs like while ... repeat etc.
In Coq's standard libraries we find "gcd" in Coq.ZArith.Znumtheory [1]
and in Coq.ZArith.Zgcd_alt [2], whereby the latter (earlier version) is
based on Euclid's algorithm which is more suitbale for our purposes.
Formally we only need to prove:

Theorem spad_gcd_ok: forall a,b : NNI, spad_gcd(a,b) = Zgcd_alt(a,b).

where "spad_gcd" means a suitable specification of "gcd" (preferably
1:1). However, this is not as simple as it might look at first sight.
There are various methods to do this as described in the links
(verficiation) below. It is certainly feasible to implement some
automatism (see the "tools" links further below), however, it might be
worthwile to do some thinking first.


[1] https://coq.inria.fr/library/Coq.ZArith.Znumtheory.html
[2] https://coq.inria.fr/library/Coq.ZArith.Zgcd_alt.html



catdef.spad (line 500 ff.)
====================================================================
import from NonNegativeInteger

-- declarations
x, y, z : %

...

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

====================================================================




---Verification
[Software Foundations]
http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
(esp. http://www.cis.upenn.edu/~bcpierce/sf/current/Imp.html)

[Proving sorted lists correct using the Coq proof assistant]
http://www.randomhacks.net/2015/07/19/proving-sorted-lists-correct-using-coq-proof-assistent/

[Software Validation and Verification], P. Cabalar
http://www.dc.fi.udc.es/~cabalar/vv/
(slides!)

[Introduction to the Coq proof-assistant for
practical software verication] by Christine Paulin-Mohring
https://www.lri.fr/~paulin/LASER/course-notes.pdf


--- Tools
Several tools are being built on top of Coq, for software verification
purposes:

[Ott]
http://www.cl.cam.ac.uk/~pes20/ott/

[Why3]
http://why3.lri.fr/

[Ynot]
http://ynot.cs.harvard.edu/

[Bedrock]
http://plv.csail.mit.edu/bedrock/


--- Math
[Implementation of Bourbaki's Elements of Mathematics in Coq]
http://www-sop.inria.fr/members/Jose.Grimm/coq.pdf
http://www-sop.inria.fr/marelle/gaia/

[Coq Math Projects]
https://coq.inria.fr/cocorico/List%20of%20Coq%20Math%20Projects


Kurt


Am 25.07.2015 um 13:38 schrieb address@hidden:
> Axiom has moved into a new phase. The goal is to prove Axiom correct.
> 
> There are several tools and several levels of proof. I've added
> the machinery to run proofs in COQ (for algebra) and ACL2 (for
> the interpreter and compiler).
> 
> One of the first steps for the algebra proofs involves decorating
> the categories with their mathematical axioms. That's where I am
> asking for your help.
> 
> There are 241 categories, such as Monoid, which need to be annotated.
> I've listed them below, sorted in the order by which they inherit
> from prior categories, so that the complexity increases. The file
> http://axiom-developer.org/axiom-website/endpaper.pdf
> has a graph of the categories from the Jenks book which could be
> a great help.
> 
> Please look at the categories and find or create the axioms.
> If you have a particularly good reference page on the web or
> a particularly good book that lists them, please let me know.
> 
> The axioms have to be in a certain form so they can be used in
> the calculus of inductive constructions (the theory behind COQ).
> 
> The plan is to decorate the categories, then provide proofs for
> category-default code. Unfortunately, Axiom is circular so some
> of the domains are going to require proofs also. 
> 
> This task should be at least as hard as it was to get Axiom to
> build stand-alone in the first place which took about a year.
> The best case will be that the implementations are proven correct.
> The bad case will be corner cases where the implementation cannot
> be proven.
> 
> In any case, your help will make this first step easier. Drag out
> your favorite reference book and decorate LeftModule :-).
> 
> Thanks,
> Tim
>