>(3) might be delicate
Hoare triples for loop pre-/post-conditions. I had a discussion about
potentially creating a 'while' tactic that might help loop proofs.
Axiom tends to use variables as 'named constants' in that, except for
loops, they tend to have a single assignment. Where that isn't true it
(should?) be easy to introduce a new constant instead of a reassignment.
Single assignment of local variables does not affect the purity of a function.
>(4) seems to be
>out of scope for the moment (that is let's trust it, as an axiom so to speak ).
Actually, this is 'in scope' also. I have automated the use of ACL2 for
proving the lisp code in the compiler and interpreter. I have proven one
lisp function so far (just to 'turn the crank') and more are in plan. The first
real step is developing signatures for all of the functions. In Volume 5,
the interpreter, you'll find a new appendix listing the signatures of functions.
I didn't mention it here because this group of people are working much
closer to the Spad level, not the Lisp level. I've had Lisp-level discussions
(offline so far) but I certainly plan to provide proofs of the interpreter/compiler
code base. Spad is, after all, just a domain specific language in lisp.
Implementing another, compatible Spad compiler would be much too
difficult. The compiler has to know about subtle things like 'the add chain'
and name overloading and many other issues. Besides, that would have
to be proven anyway. So instead of making progress on proofs we'd be
back to pre-compiler problems.
>
>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).
I'm perfectly willing to replace existing code with code that can be proven
correct that implements the same functionality. The need to do that is almost
a certainty. I expect that this effort will push the bounds of Axiom as well as
Coq/Lean/FoCaL and ACL2. But the time has come to require proofs of
computational mathematics.
>
>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.
Why do you say that (b) is not what we really want? I expect that the
proof effort will uncover a lot of problems in Spad code. The hope is
that it improves Axiom.
...clipped...
>
>
>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.
Indeed, neither am I but Jeremy's example is a starting point.
>
>>
>> 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.
This might allow us to restructure the Coq libraries to match the Axiom
Category type tower. If so, I can automate extracting the 'class'
information directly from the Category structure when proving a Domain
function.
>
>>
>> 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).
Thanks for the link... more to know.
>> 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.
I'm going to try to build the 'class' definitions for the Category hierarchy used
by NNI and automate their extraction, followed by proving gcd automatically.
Hopefully. Maybe. The idea is to 'turn the crank' for the first time and create
a prototype proof environment that runs during system builds.
>
>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).
Thanks. I'll look at it in detail.
Tim
>
>--------------242E01CAAAC57564FEDE2669
>Content-Type: text/plain; charset=UTF-8;
> name="field_mpl.v"
>Content-Transfer-Encoding: 7bit
>Content-Disposition: attachment;
> filename="field_mpl.v"
>
>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.
>*)