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 _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer