Re: [Axiom-developer] Call for help

[daly]

I'm taking Pierce's online course at the moment (Software Foundations
in Coq).

>and in Coq.ZArith.Zgcd_alt [2], whereby the latter (earlier version) is
>based on Euclid's algorithm which is more suitable for our purposes.

It is becoming clear that between an implmentation of an algorithm and
its proof there is a bit of a gap. I've tried a couple of them so far
with no progress but that just means there is more to learn.

>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.

It is clear that we can prove some mathematical facts. The game is
to prove the implementation, as you point out. Currently a gathering of
the category level implementations into a file (obj/ubuntu/proofs/coq.v)
will give an overview of the problem. The hope is to get a foothold on
one or a few of these implementations and learn how to do this generally.

COQ has proofs of some of them already (e.g. not) and it might be
reasonable to accept them as "ground truth". We don't want to waste
time proving what COQ already knows, especially about the integers.
So one of the tasks will be to discover and import the COQ definitions
related to the specific proof.

Another issue is that the category implementations assume, in many
cases, that they are parameterized by a specific domain. So we would
be forced to say

    forall domains $
      where $ has the axioms....
        then this categorical method applies

where we have to collect the axioms from the categories of domain $.
That's the motivation for the task of finding and annotating the
categories with their axioms. 

We might be forced to do the proofs in each specific domain rather
than at the category level.

In any case, it seems best to do something in the face of overwhelming
ignorance, if only for the educational value of the mistakes made while
doing it wrong. 

Thanks for the links. 

Tim