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
> Axiom-developer@nongnu.org
> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>
Module Field.
Parameter F : Set.
Parameter plus : F->F->F.
Parameter times : F->F->F.
Parameter null : F.
Parameter one : F.
Parameter neg : F->F.
Parameter inv : F->F.
Infix "+" := plus.
Infix "*" := times.
Notation "0" := null.
Notation "1" := one.
Notation "- 1":=(neg one).
Notation "- u" := (neg u).
Notation "1 / u" := (inv u)
(at level 75, right associativity).
Axiom F1: forall u v:F, exists w:F, w=u+v.
Axiom F2: forall u v:F, exists w:F, w=u*v.
Axiom F3: forall u v:F, u+v = v+u.
Axiom F4: forall u v:F, u*v = v*u.
Axiom F5: forall u v w:F, u+(v+w) = (u+v)+w.
Axiom F6: forall u v w:F, u*(v*w) = (u*v)*w.
Axiom F7: forall u v w:F, u*(v+w) = (u*v)+(u*w).
Axiom F8: forall u v w:F, (u+v)*w = (u*w)+(v*w).
Axiom F9: forall u:F, u+0 = u.
Axiom F10: forall u:F, u*1 = u.
Axiom F11: forall u:F, u+(-u) = 0.
Axiom F12: forall u:F, ~(u=0) -> u * (1/u) = 1.
Axiom F13: 1 <> 0.
Proposition null_unique: forall n:F, (forall u:F, u+n=u) -> n=0.
proof.
let n:F.
assume(forall u : F, u+n = u).
then (0 + n = 0).
then f1:(n+0 = 0) by F3.
then f2:(n+0 = n) by F9.
thus thesis by f1,f2.
end proof.
Qed.
Proposition one_unique: forall e:F, (forall u:F, u*e=u) -> e=1.
proof.
let e:F.
assume(forall u : F, u*e = u).
then (1*e = 1).
then f1:(e*1 = 1) by F4.
then f2:(e*1 = e) by F10.
thus thesis by f1,f2.
end proof.
Qed.
(*
Lemma neg_null: forall u:F, (u=neg u) -> u=null.
proof.
let u:F.
assume(u=neg u).
then (plus u u=plus u (neg u)).
then (plus u u=null) by F11.
end proof.
Qed.
*)
Proposition neg_unique: forall u:F, forall v:F, (u+v=0) -> v=-u.
proof.
let u:F, v:F.
assume(u+v = 0).
then ((-u)+(u+v)=(-u)+0).
then f1:((-u) + (u+v)=-u) by F9.
then ((-u) + (u+v)=((-u)+u)+v) by F5.
then ((-u) + (u+v)=(u + (-u)) + v) by F3.
then ((-u) + (u+v)=0+v) by F11.
then f2:((-u)+(u+v)=v) by F3,F9.
thus thesis by f1,f2.
end proof.
Qed.
Proposition inv_unique: forall u:F, forall v:F, (~(u=0)/\(u*v=1)) -> v=(1/u).
proof.
let u:F, v:F.
assume a:(u<>0 /\ u * v = 1).
then ((1/u)*(u*v)=((1/u)*1)).
then f1:((1/u)*(u*v)=(1/u)) by F10.
then ((1/u)*(u*v)=((1/u)*u)*v) by F6.
then ((1/u)*(u*v)=(u*(1/u))*v) by F4.
then ((1/u)*(u*v)=1*v) by a,F12.
then f2:((1/u)*(u*v)=v) by F4,F10.
thus thesis by f1,f2.
end proof.
Qed.
Proposition times_null: forall u:F, u*0 = 0.
proof.
let u:F.
then(u * (0+0) = (u*0) + (u*0)) by F7.
then(u*0 = (u*0) + (u*0)) by F9.
then(0 = ((u*0) + (u*0)) + (- (u*0))) by F11.
then(0 = (u*0) + ((u*0) + (- (u*0)))) by F5.
then(0 = (u*0) + 0) by F11.
then(0 = u * 0) by F9.
then f1:(u * 0 = 0) by F4.
take f1.
end proof.
Qed.
Proposition neg_is_neg_one_times: forall u:F, -u = (- 1) * u.
proof.
let u:F.
then(u + ( - 1 * u) = (u * 1) + (u * - 1)) by F4,F10.
then(u + ( - 1 * u)= u * (1 + - 1)) by F7.
then(u + ( - 1 * u)= u * 0) by F11.
then f1:(u + ( - 1 * u)= 0) by times_null.
thus thesis by f1,neg_unique.
end proof.
Qed.
Proposition neg_null_is_null: - 0 = 0.
proof.
have f1:(0+0 = 0) by F9.
thus thesis by f1, neg_unique.
end proof.
Qed.
Proposition inv_one_is_one: (1/1) = 1.
proof.
have f1:(1 * 1 = 1) by F10.
thus thesis by f1,F13,inv_unique.
end proof.
Qed.
Lemma neg_one_neq_null: not (- (1) = 0).
proof.
assume(- (1)= 0).
then f1:(1 + -1 = 1+0) by F11.
then f2:(1 + - 1 = 1) by F9.
then f3:(0 = 1) by f2,F11.
thus thesis by f3,F13.
end proof.
Qed.
Proposition inv_neg_one_is_neg_one : (1/ - 1 ) = - 1.
proof.
have (- 1 * (1/- 1 )= 1) by neg_one_neq_null,F12.
then f1:((1 + - 1) * (1/ - 1)= 0) by F11,F4,times_null.
then f2:( (1 + - 1) * (1/ - 1)= (1* (1/ - 1)) + (- 1 * (1/ - 1))) by F8.
then f3:((1+ - 1) * (1/- 1)= (1/ - 1) + 1) by F4,F10,F12, neg_one_neq_null.
then f4:(0 = (1/- 1) +1) by f1,f3.
then f5: (1+ (1/ - 1) = 0) by f4,F3.
thus thesis by neg_unique, f5.
end proof.
Qed.
Lemma neg_one_times_neg_one_is_one: -1 * -1 =1.
proof.
have f1:(-1*(1+ -1)=0) by F11, times_null.
then f2:(-1*(1+ -1)=-1*1 + -1*-1) by F7.
then f3:(-1*(1+ -1)=-1 + -1*-1) by f2,F10.
then f4:( 0=-1+ -1*-1) by f3,f1.
then (1+0 = 1 + (-1+ -1*-1) ) by f4.
then (1=(1+-1)+ (-1*-1)) by F5,F9.
then (1=0+(-1*-1)) by F11.
then f8:(1=(-1*-1)+0) by F3.
thus thesis by f8,F3,F9.
end proof.
Qed.
Proposition neg_times_neg_is_plus: forall u v:F, (-u)*(-v)=u*v.
proof.
let u:F, v:F.
have f1: ( -u = -1*u) by neg_is_neg_one_times.
have f2: ( -v = -1*v) by neg_is_neg_one_times.
then (-u * -v = (-1*u)*(-1*v)) by f1,f2.
then (-u * -v = ((-1*u)*-1)*v) by F6.
then (-u * -v = (-1*(-1*u))*v) by F4.
then (-u * -v = ((-1*-1)*u)*v) by F6.
then (-u * -v = (1*u)*v) by neg_one_times_neg_one_is_one.
then f3:(-u * -v = u*v) by F4,F10.
thus thesis by f3.
end proof.
Qed.
Lemma not_null_then_inv_not_null: forall u:F, u<>0 -> (1/u)<>0.
proof.
let u:F.
assume f1:(u<>0).
assume f2:( (1/u)=0).
then f3:(u*(1/u)=1) by f1,F12.
then (u*(1/u)=u*0) by f1,f2.
then f4:(1=u*0) by f3.
thus thesis by f4,times_null, F13.
end proof.
Qed.
Proposition inv_inv_is_id: forall u:F, ~(u=0) -> (1 / (1 / u)) = u.
proof.
let u:F.
assume h1:(u<>0).
have(u* (1/u)=1) by h1,F12.
then f1:( (1/u)*u=1) by F4.
then f2:((1/u)*(1 / (1/u))=1) by h1,not_null_then_inv_not_null, F12.
then ( (1/u)*(1 / (1/u)) = (1/u)*u ) by f1,f2.
then ( (1 / 1/u)*( (1/u)*(1 / (1/u))) = (1 / 1/u) * ( (1/u)*u )).
then ( ((1 / 1/u)* (1/u)) * (1 / (1/u)) = ((1 / 1/u) * (1/u))*u ) by F6.
then ( ( (1/u)*(1 / 1/u)) * (1 / (1/u)) = ( (1/u)*(1 / 1/u))*u ) by F4.
then f3:( 1* (1 / (1/u)) = 1*u) by f2.
thus thesis by f3,F4, F10.
end proof.
Qed.
Lemma prod_not_null: forall u v:F, ((u<>0)/\ (v<>0)) -> (u*v<>0).
proof.
let u:F, v:F.
assume h1:(u <> 0 /\ v <> 0).
then f1:(u<>0) by h1.
then f2:(v<>0) by h1.
assume h2:(u*v=0).
then (u*v=u*0) by times_null.
then ( (1/u)*(u*v) = (1/u)*(u*0)) by f1,F12.
then ( (u*(1/u))*v=(u*(1/u))*0) by F6,F4.
then f3:(v=0) by f1,F4,F12,F10.
thus thesis by f2,f3.
end proof.
Qed.
Proposition inv_prod_is_prod_inv: forall u v:F, ((u<>0)/\ (v<>0)) ->
((1/(u*v)) = (1/u)*(1/v)).
proof.
let u :F, v:F.
assume h1:(u <> 0 /\ v <> 0).
then f1:(u<>0) by h1.
then f2:(v<>0) by h1.
then f3:((u*v)<>0) by f1,f2,prod_not_null.
then ( (u*v)* ((1/u)*(1/v)) = (u*v)* ((1/v)*(1/u))) by F4.
then ( (u*v)* ((1/u)*(1/v)) = ((u*v)* (1/v))*(1/u)) by F6.
then ( (u*v)* ((1/u)*(1/v)) = (u*(v* (1/v))*(1/u))) by F6.
then ( (u*v)* ((1/u)*(1/v)) = (u*1)*(1/u)) by f2,F12.
then ( (u*v)* ((1/u)*(1/v)) = (u*(1/u))) by F10.
then ((u*v)* ((1/u)*(1/v)) = 1) by f1,F12.
then f4:((1/u)*(1/v)=(1 / u * v) ) by f3,inv_unique.
thus thesis by f4.
end proof.
Qed.
End Field.
Let S:=Field.F.
Notation "x + y":=(Field.plus x y).
Notation "x * y":=(Field.times x y).
Lemma comm: forall x y:S,x+y=y+x.
proof.
intros.
thus thesis by Field.F3.
end proof.
Qed.
Definition addAndSquare(a b:S):S:=(a+b)*(a+b).
Definition sq(a:S):S:=a*a.
Check addAndSquare Field.one Field.one.
Compute addAndSquare Field.one Field.null.
Proposition P1:forall a b:S, addAndSquare a b =
(sq a) + (sq b)+a*b+b*a.
proof.
let u:S.
let v:S.
compute.
thus thesis by Field.F7,Field.F8,Field.F3,Field.F5.
end proof.
Qed.
(*
have f1:((u+v)*(u+v) =u*(u+v)+v*(u+v)) by Field.F8.
then f2:((u+v)*(u+v) = u*u+u*v+v*(u+v)) by f1,Field.F7.
then f3:((u+v)*(u+v)= u*u+u*v+v*u+v*v) by f2, Field.F7,Field.F3,Field.F5.
thus thesis by f3, Field.F3,Field.F5.
end proof.
Qed.
*)
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
https://lists.nongnu.org/mailman/listinfo/axiom-developer
