Keith Devlin writes: All the mathematical methods I l=
earned in my university math degree

becamse obsolete in my lifetim=
e.When I graduated with a bachelors degree in mathematics from one of=20 the most prestigious university mathematics programs in the world (Kings College London) in 1968, I had acquired a set of skills that guaranteed full employment, wherever I chose to go, for the then-foreseeable=20 future=E2=80=94a state of affairs that had been in existence ever since mod= ern=20 mathematics began some three thousand years earlier. By the turn of the=20 new Millennium, however, just over thirty years later, those skills were essentially worthless, having been very effectively outsourced to=20 machines that did it faster and more reliably, and were made widely=20 available with the onset of first desktop- and then cloud-computing. In a single lifetime, I experienced first-hand a dramatic change in the=20 nature of mathematics and how it played a role in society.

The shift began w=
ith the=20
introduction of the electronic calculator in the 1960s, which rendered=20
obsolete the need for humans to master the ancient art of mental=20
arithmetical calculation. Over the succeeding decades, the scope of=20
algorithms developed to perform mathematical procedures steadily=20
expanded, culminating in the creation of desktop packages such as *Mathe=
matica* and cloud-based systems such as *Wolfram Alpha*
that can execute pretty well any mathematical procedure,=20
solving=E2=80=94accurately and in a fraction of a second=E2=80=94any mathem=
atical=20
problem formulated with sufficient precision (a bar that allows in all=20
the exam questions I and any other math student faced throughout our=20
entire school and university careers).

So what, then, re=
mains in=20
mathematics that people need to master? The answer is, the set of skills
required to make effective use of those powerful new (procedural)=20
mathematical tools we can access from our smartphone. Whereas it used to
be the case that humans had to master the computational skills required
to *carry out* various mathematical procedures (adding and=20
multiplying numbers, inverting matrices, solving polynomial equations,=20
differentiating analytic functions, solving differential equations,=20
etc.), what is required today is a sufficiently deep *understanding*
of all those procedures, and the underlying concepts they are built on,
in order to know when, and how, to use those digitally-implemented=20
tools effectively, productively, and safely.

It looks like the probl=
em is related to GCL, not Axiom.

GCC changed behavior causing=
the GCL build to fail.

It might be fixed in GCL 13pre but I have =
not completed the port<= br>

https://sourceforge.net/projects/swaret/

As an alternaive you might consider using VirtualBox runnin=
g Ubuntu.

The game is to prove GCD in NonNe=
gativeInteger (NNI).

We would like to use the 'nat' th=
eorems from the existing libraryat build time.

=

theorem =3D (a, b : Type) : Boolean :=3D .....

signatures from the BasicType Category. The collection of all of

Unfortunately it =
appears the Coq and Lean will not take kindly to

removing the exis=
ting libraries and replacing them with a new versiontheorem ~=3D (a, b : Type) : Boolean :=3D ....

T=
hese theorems would be imported into NNI when it inherits the

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.

=

Axiom proofs would still depend on the external proof syste=
m but only

for the correctness engine, not the library struct=
ure. This will minimize

the struggle about Axiom's world =
view (e.g. handling excluded middle).

It will also organize t=
he logic library to more closely mirror abstract algebra.

<=
div>

<=
/div>

Dear Tim,

(eq : =CE=B1 =E2=86=92 =CE=B1 =E2=86=92 bool) (neq : =CE=B1 =E2=86=92 =
=CE=B1 =E2=86=92 bool)

=

<=
div>=C2=A0 check a ?=3D? b

I don't understand what y=
ou mean. For one thing, theorems in both Lean and Coq are marked as opaque,=
since you generally don't care about the contents. But even if we repl=
ace "theorem" by "definition," I don't know what yo=
u imagine going into the "...".

I think =
what you want to do is represent Axiom categories as structures. For exampl=
e, the declarations below declare a BasicType structure and notation for el=
ements of that structure. You can then prove theorems about arbitrary types=
=C2=A0=CE=B1 that have a BasicType structure. You can also extend the struc=
ture as needed.

(Presumably you will eventuall=
y want to add axioms to the structures that say things about what eq and ne=
q do. Otherwise, you are just reasoning about a type with two relations.)

Best wishes,

Jeremy

<=
div>class BasicType (=CE=B1 : Type) : Type :=3D

infix `?=3D?`:50 =C2=A0:=3D=
BasicType.eq

infix `?~=3D?`:50 :=3D BasicType.neq

=

section

=C2=A0 variables (=CE=B1 : Type) [BasicType =
=CE=B1]

=C2=A0 variables a b : =CE=B1=C2=A0

=C2=A0 check a ?~=3D? b

end<=
/div>

On Wed, Feb 8, 2017 at 9:29 AM=
, Tim Daly <axiomcas@gmail.com> wrote:

<= /font>theorems by changing external references from =3D to spad=3D ev= erywhere.Eventually there should be enough embedded logic to start coding Axi= omI= nitially this would make Axiom depend on the external library structure.the name of Axiom's algebra language).FoCaL but I suspect it has the same bootstrap problem.t= hat only contains a limited number of theorems. I'm not yet sure about<= br>remov= ing the existing libraries and replacing them with a new versionfor the logic system. So BasicTy= pe would containdefinitions of =3D and ~=3D so we cou= ld create a new library structureIn the ideal case we would decorate= BasicType with the existingbut extract those t= heorems automatically from Axiom sourcesThe game is to prov= e GCD in NonNegativeInteger (NNI).We would like to use the &#= 39;nat' theorems from the existing libraryat build time.is BasicType which contains two signatures:

<= /div>Axiom's NNI inherits from a dozen Category objects,= one of which

<= /div>=C2=A0?=3D?: (%,%) -> Boolean=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 ?= ~=3D?: (%,%) -> Booleantheorem =3D (a, b : Type) : Boolean :=3D= .....theorem ~=3D (a, b : Type) : Boolean :=3D ....

=These theorems would be imported into NNI when it inherits the <= br>signatures from the BasicType Category. The collection of all= ofthe theorems in NNI's Category structure would be use= d (hopefullyexclusively) to prove GCD. In this way, all of t= he theorems used toprove Axiom source code would be inheriti= ed from the Categorystructure.Unfor= tunately it appears the Coq and Lean will not take kindly to

Jeremy Avigad (Lean) made the suggestion to rename these theorems.

Thus, instead of =3D, the supporting theorem would be 'spad=3D' = (spad isAxiom proofs would still depend on the external= proof system but onlyfor the correctness engine, not the li= brary structure. This will minimizethe struggle about Axiom&= #39;s world view (e.g. handling excluded middle).It will als= o organize the logic library to more closely mirror abstract algebra.TimComments, suggestions?<= div>

Part of your =
struggle of understanding what I wrote is that I'm not yet fluent in th=
e

logic language and syntax. I'm learning as fast as I can so =
please be patient.=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

CATEGORY SIGNATURE vs DOMAIN SEM= ANTICS

> Presumably you will eventually want to add axioms to the= structures that say

> things about what eq and neq do

not in the Category (well...you can... s=
igh)

Each domain that inherits '=3D' from the Category= BasicType needs to specify the meaning

of that function for the Domain = you're implementing.. For a Polynomial domain with some

structural = data representation you have to define what it means for two polynomial obj= ects

to be =3D. such as a function to compare coefficients. Part of the= game would be to prove

that the coefficient-compare function=
is correct, always returns a Boolean, and terminates.

All a Category like BasicType does is specify that the Domain Polyno= mial should

implement an =3D operation with the given signature.=C2=A0 = That is, you have to implement

=C2=A0=C2=A0=C2=A0= =C2=A0 poly =3D poly

which returns a boolean. (Note that= there are other =3D functions in Polynomial such as one

that=
returns an equation object but that signature is inherited from a differen=
t Category).

It looks like your 'class' syntax im=
plements what I need. I will try this for the other

Categorie=
s used in NNI.

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

=
PROVING TERMINATION

=C2=A0=C2=A0 gcd(a:NNI,b:N= NI):NNI

=C2=A0=C2=A0=C2=A0 gcd(y rem x, x)

=

Every statement in the function is strongly type-checked.

can only be called with NNI argument=
s and is guaranteed to only return NNI results.

The langu= ages are very close in spirit if not in syntax.

Coq, i= n its version, will figure out that the recursion is on 'a' and tha= t it will terminate.

Part of the game is to provide the s= ame termination analysis on Spad code.

=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

ADDITIONAL CONSTRAINTS

It would be ideal to reject =
code that did not fulfill all of the requirements

such as spe=
cifying at the Category level definition of gcd that it not only

<=
div>has to have the correct signature, it also has to return the 'posit=
ive'divisor. For NNI this is trivially fulfilled.

So for some = domains we have:

of loops which I mentioned = in a previous email.)

The Category definition should say something like

=
=C2=A0=C2=A0 gcd(%,%) -> %=C2=A0 and gcd >=3D 1$%

where=
1$% says to use the unit from the implementing Domain.So for some = domains we have:

=C2=A0 gcd(x,y) =3D=3D

=C2=A0=C2=
=A0=C2=A0 x :=3D unitCanonical x

=C2=A0=C2=A0=C2=A0 y :=3D un=
itCanonical y

=C2=A0=C2=A0=C2=A0 while not zero? y repeat

=

=

=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 (x,y) :=3D (y, x rem y)

=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 y :=3D unitCanonical y

=
=C2=A0=C2=A0=C2=A0 x

using unitCanonical to deal with things l=
ike signs. (This also adds the complication of loops which I mentioned = in a previous email.)

Not only the signature but the side=
-conditions would have to be checked.

=

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

ALTERNATE APPROACHES

=
Instead of a new library organization it might be possi=
ble to have a generator function

in Coq that translates Coq c=
ode to Spad code. Or a translator from Spad code to

Coq code.=

Unfortunately Coq and Lean do not seem to use function name overlo= ading

Unfortunately Coq and Lean do not seem to use function name overlo= ading

or inheritance (or do they?) which confuses the problem=
of name translation.

Axiom has 42 functions named '=
gcd', each living in a different Domain.

=

There is no such thing as a simple job. But this one promise=
s to be interesting.

In any case I'll push the implem=
entation forward. Thanks for your help.

Tim

On Wed, Feb 8, = 2017 at 5:52 PM, Jeremy Avigad <avigad@cmu.edu> wrote:

Dear Tim,

I don't understand what you mean. For one thing, theore=
ms in both Lean and Coq are marked as opaque, since you generally don't=
care about the contents. But even if we replace "theorem" by &qu=
ot;definition," I don't know what you imagine going into the "=
;...".

I think what you want to do is represe=
nt Axiom categories as structures. For example, the declarations below decl=
are a BasicType structure and notation for elements of that structure. You =
can then prove theorems about arbitrary types=C2=A0=CE=B1 that have a Basic=
Type structure. You can also extend the structure as needed.

=

(Presumably you will eventually want to add axioms to the st=
ructures that say things about what eq and neq do. Otherwise, you are just =
reasoning about a type with two relations.)

Best w=
ishes,

Jeremy

class =
BasicType (=CE=B1 : Type) : Type :=3D

(eq : =CE=B1 =E2=86=92 =CE=
=B1 =E2=86=92 bool) (neq : =CE=B1 =E2=86=92 =CE=B1 =E2=86=92 bool)

infix `?=3D?`:50 =C2=A0:=3D BasicType.eq

infix `=
?~=3D?`:50 :=3D BasicType.neq

section

=
=C2=A0 variables (=CE=B1 : Type) [BasicType =CE=B1]

=C2=A0 variab=
les a b : =CE=B1=C2=A0

=C2=A0 check a ?=3D? b

=C2=A0 check a ?~=3D? b

end

=

On Wed, F=
eb 8, 2017 at 9:29 AM, Tim Daly <axiomcas@gmail.com> wrote:=

Timtheorems by changing ex= ternal references from =3D to spad=3D everywhere.Eventually there should be e= nough embedded logic to start coding AxiomInitially this would make Axiom depe= nd on the external library structure.the name of Axiom= 's algebra language).Thus, instead of =3D, the suppor= ting theorem would be 'spad=3D' (spad isJeremy Avigad (Lean) made the sug= gestion to rename these theorems.FoCaL but I suspect it has= the same bootstrap problem.that only contains a limited number = of theorems. I'm not yet sure aboutremoving the existing libraries and repl= acing them with a new versionfor the logic system. So BasicType would contain=C2=A0?=3D?: (%,%) -> Boole= an=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 ?~=3D?: (%,%) -> Booleanis BasicType= which contains two signatures:but extract those theorems automatically from Axiom so= urcesThe game is to prove GCD in NonNegativeInteger (NNI).<= br>We would like to use the 'nat' theorems from the exist= ing libraryat build time.Axiom's NNI= inherits from a dozen Category objects, one of which

<= /div>In the ideal case we would decorate BasicType with the existing

definitions of =3D and ~=3D so we could create a new library structure= theorem =3D (a, b : Type) : Boolean :=3D .....theorem ~=3D (= a, b : Type) : Boolean :=3D ....These theorems would be = imported into NNI when it inherits thesignatures from the B= asicType Category. The collection of all ofthe theorems in N= NI's Category structure would be used (hopefullyexclusiv= ely) to prove GCD. In this way, all of the theorems used top= rove Axiom source code would be inheritied from the Category= structure.Unfortunately it appears the Coq and Lea= n will not take kindly toAxiom p= roofs would still depend on the external proof system but onlyfor the correctness engine, not the library structure. This will minimize= the struggle about Axiom's world view (e.g. handling exc= luded middle).It will also organize the logic library to mor= e closely mirror abstract algebra.Comments, sugges= tions?=

On Wed, Feb 8, 2017 at 9:23 PM, Tim Daly <axiomcas@gmail.com>=
wrote:

=Part of your struggl= e of understanding what I wrote is that I'm not yet fluent in theThe semantics of =3D is given in the Domain (= the current one being defined is called % in Spad)

logic language and syntax. I'm learning as fast as I can so please = be patient.

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

CATEGORY SIGNATURE vs DOMAIN SEM= ANTICS

> Presumably you will eventually wa= nt to add axioms to the structures that say

> things about what eq a= nd neq donot in the= Category (well...you can... sigh)

Each domain that inherits &= #39;=3D' from the Category BasicType needs to specify the meaning

of= that function for the Domain you're implementing..

In ou=
r language, we would say that every instance of the structure has all the n=
ecessary data. For example, every group (=3Dinstance of the group structure=
, or element of the type group =CE=B1) has a unit, a binary operation, and =
inverse operation, etc.

=C2=A0

For a = Polynomial domain with some=C2=A0

structural data representation you have to = define what it means for two polynomial objects

to be =3D. such as a fu= nction to compare coefficients. Part of the game would be to provethat the coefficient-compare function is correct, always returns a Bo= olean, and terminates.

All a Category like BasicTy= pe does is specify that the Domain Polynomial should

implement an =3D o= peration with the given signature.=C2=A0 That is, you have to implement

=

=C2=A0=C2=A0=C2=A0=C2=A0 poly =3D poly=

which returns a boolean. (Note that there are other =3D functions in Po= lynomial such as onethat returns an equation object but that= signature is inherited from a different Category).

Is there anything that =
requires that the operation you implement is reflexive, symmetric, and tran=
sitive?=C2=A0 Putting axioms on the structure specifies that that has to be=
the case. Without such axioms, you cannot prove anything about implementat=
ions in general. You can only prove things about individual implementations=
.

with the same name and same arguments but differ= ent return types, for example).by the arguments but also by the return type (so there can be m= ultiple functionsEver= ything in Spad is strongly typed and function definitions are chosen not on= ly=C2=A0=C2=A0=C2=A0 gcd(y rem x, x)=C2=A0=C2=A0=C2=A0 zero= ? x =3D> y=C2=A0 gcd(x:NNI,y:NNI):NNI =3D=3Dand Axiom's definition is=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0 | S a' =3D> gcd (b mod (S a')) (S a')=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 | 0 =3D> b<= div>=C2=A0=C2=A0=C2=A0 match a withCoq provides gcd asa function that fulfills the signature ofIt looks like your 'class&#= 39; syntax implements what I need. I will try this for the other<= div>Categories used in NNI.

=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D==3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D PROVING TERMINATIONAs I under= stood from class, for an algorithm like gcd it should be sufficient to cons= truct

=C2= =A0=C2=A0 gcd(a:NNI,b:NNI):NNI

=C2=A0 Fixpoint gcd a b :=3D

=

=C2=A0=C2=A0=C2=A0 end.

Every statement in the function is stro= ngly type-checked.

Th=
at is what I referred to as a shallow embedding -- you are associating to e=
very axiom definition a Coq or Lean definition which has the same behavior.=

If you do that, you cannot model arbitrary while =
loops. You have to write functions in Coq or Lean in a way that, from the s=
tart, they are guaranteed to terminate. You can do this, for example, by sh=
owing the recursive calls are decreasing along a suitable measure, or givin=
g a priori bounds on a while loop. If you want to translate spad functions =
automatically, you'll have to write the former in such a way that the t=
ranslations have this property. You can't translate an arbitrary, a pri=
ori partial, function and then show after the fact that it terminates for e=
very input.

Other approaches are possible. You can=
, for example, translate spad functions to relations in Coq or Lean, and th=
en prove that the relations give rise to total functions.

Best wishes,

Jeremy

Thus we are guaranteed that the Spa= d version of gcd above (in the Domain NNI)can only be called= with NNI arguments and is guaranteed to only return NNI results.==

The languages are very close in spirit if not in syntax.What Axiom does not do, for example, is prove terminati= on.

Coq, in its version, will figure out that the recursion is on &= #39;a' and that it will terminate.

Part of the game i= s to provide the same termination analysis on Spad code.

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D ADDITIONAL CONSTRAINTSIt w= ould be ideal to reject code that did not fulfill all of the requirementssuch as specifying at the Category level definition of gcd tha= t it not onlyhas to have the correct signature, it also has = to return the 'positive'divisor. For NNI this is tri= vially fulfilled.The Category definition should say something= like=C2=A0=C2=A0 gcd(%,%) -> %=C2=A0 and gcd >=3D= 1$%where 1$% says to use the unit from the implementing Dom= ain.

So for some domains we have:=C2=A0 gcd(x,y) =3D=3D==C2=A0=C2=A0=C2=A0 x :=3D unitCanonical x=C2= =A0=C2=A0=C2=A0 y :=3D unitCanonical y=C2=A0=C2=A0=C2=A0 whi= le not zero? y repeat=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 (x,y) := =3D (y, x rem y)=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 y :=3D unitCa= nonical y=C2=A0=C2=A0=C2=A0 xusing unitCanonic= al to deal with things like signs. (This also adds the complication

of = loops which I mentioned in a previous email.)Not only th= e signature but the side-conditions would have to be checked.

=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D = ALTERNATE APPROACHESInstead of a new library = organization it might be possible to have a generator functionin Coq that translates Coq code to Spad code. Or a translator from Spad c= ode to

Coq code.

Unfortunately Coq and Lean do not se= em to use function name overloading

Unfortunately Coq and Lean do not se= em to use function name overloading

or inheritance (or do the=
y?) which confuses the problem of name translation.

Axio=
m has 42 functions named 'gcd', each living in a different Domain.<=
br>

There is no such thing as a si=
mple job. But this one promises to be interesting.

In any=
case I'll push the implementation forward. Thanks for your help.

Tim

<=
div><=
/div>

<=
div>

On Wed, Feb 8, 2017 at 5:52 PM, Jeremy Avigad <= span dir=3D"ltr"><av= igad@cmu.edu> wrote:

On Wed, Feb 8, 2017 at 5:52 PM, Jeremy Avigad <= span dir=3D"ltr"><av= igad@cmu.edu> wrote:

Dear Tim,I don't unde= rstand what you mean. For one thing, theorems in both Lean and Coq are mark= ed as opaque, since you generally don't care about the contents. But ev= en if we replace "theorem" by "definition," I don't= know what you imagine going into the "...".=I think what you want to do is represent Axiom categories as structure= s. For example, the declarations below declare a BasicType structure and no= tation for elements of that structure. You can then prove theorems about ar= bitrary types=C2=A0=CE=B1 that have a BasicType structure. You can also ext= end the structure as needed.(Presumably you w= ill eventually want to add axioms to the structures that say things about w= hat eq and neq do. Otherwise, you are just reasoning about a type with two = relations.)Best wishes,= Jeremyclass BasicType (=CE=B1 : Type) : Type= :=3D(eq : =CE=B1 =E2=86=92 =CE=B1 =E2=86=92 bool) (neq : =CE=B1= =E2=86=92 =CE=B1 =E2=86=92 bool)infix `?=3D?`:50= =C2=A0:=3D BasicType.eqinfix `?~=3D?`:50 :=3D BasicType.neqsection=C2=A0 variables (=CE=B1 : Type) [B= asicType =CE=B1]=C2=A0 variables a b : =CE=B1=C2=A0=C2=A0 check a ?=3D? b=C2=A0 check a ?~=3D? b=endOn Wed, Feb 8, 2017 at 9:29 AM, Tim Daly <axiomcas@gmail.com> wrote: theo= rems by changing external references from =3D to spad=3D everywhere.Eventuall= y there should be enough embedded logic to start coding AxiomInitially this wo= uld make Axiom depend on the external library structure.Thus, instead= of =3D, the supporting theorem would be 'spad=3D' (spad isJeremy Avigad = (Lean) made the suggestion to rename these theorems.FoCaL b= ut I suspect it has the same bootstrap problem.that only contain= s a limited number of theorems. I'm not yet sure aboutremoving the existing= libraries and replacing them with a new version=for the logic system. So BasicType would contain=definitions of =3D and ~=3D so we could create a new = library structureIn the ideal case we would decorate BasicType with = the existing=C2=A0?=3D?= : (%,%) -> Boolean=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 ?~=3D?: (%,%) -&g= t; Booleanbut extract those theorems automati= cally from Axiom sourcesThe game is to prove GCD in NonNega= tiveInteger (NNI).We would like to use the 'nat' theo= rems from the existing libraryat build time.is BasicType which contains two signatures:

Axiom's NNI inherits from a dozen Category objects, one of whichtheorem =3D (a, b : Type) : Boolean :=3D .....=theorem ~=3D (a, b : Type) : Boolean :=3D ....These= theorems would be imported into NNI when it inherits thesi= gnatures from the BasicType Category. The collection of all ofthe theorems in NNI's Category structure would be used (hopefully

=exclusively) to prove GCD. In this way, all of the theorems used= toprove Axiom source code would be inheritied from the Cate= gorystructure.Unfortunately it appe= ars the Coq and Lean will not take kindly to

the name of Axiom's algebra language).Axiom proofs would still depend on the external proof system bu= t onlyfor the correctness engine, not the library structure.= This will minimizethe struggle about Axiom's world view= (e.g. handling excluded middle).It will also organize the l= ogic library to more closely mirror abstract algebra.

Comments, suggestions?

Tim

--001a113f1e72c6f37c05480ff56c-- From MAILER-DAEMON Wed Feb 08 22:28:06 2017 Received: from list by lists.gnu.org with archive (Exim 4.71) id 1cbfOw-0001N2-BC for mharc-axiom-developer@gnu.org; Wed, 08 Feb 2017 22:28:06 -0500 Received: from eggs.gnu.org ([2001:4830:134:3::10]:53120) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from

To: axiom-developer@nongnu.org

From: Kurt Pag= ani <nilqed@gmail.com>

Dat= e: Thu, 9 Feb 2017 03:23:48 +0100

>> The game is to prove GCD = in NonNegativeInteger (NNI).

>

>We encounter numerous problems = when trying to prove gcd from EuclideanDomain:

>

>---

>gc= d(x, y) =3D=3D=C2=A0=C2=A0 --Euclidean Algorithm

>=C2=A0 x :=3D unitC= anonical x

>=C2=A0 y :=3D unitCanonical y

>=C2=A0 while not zer= o? y repeat

>=C2=A0=C2=A0=C2=A0 (x, y) :=3D (y, x rem y)

>=C2= =A0=C2=A0=C2=A0 y :=3D unitCanonical y=C2=A0=C2=A0=C2=A0=C2=A0 -- this does= n't affect the

>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 -- correctness of Euclid'= s algorithm,

>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 -- but

>=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 --= a) may improve performance

>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 -- b) ensures gcd(x,= y)=3Dgcd(y, x)

>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 --=C2=A0=C2=A0=C2=A0 if canonica= lUnitNormal

>=C2=A0 x

>

>---

>

>1. Define typ= e EuclideanDomain (tower of hierarchies)

>2. Define unitCanonical (de= pends on canonicalUnitNormal etc.)

>3. Imperative elements in spad

>4. Trust interpreter/compiler and lisp

>

>While (1= ,2) seems not so difficult,

Indeed, I'm trying to constru=
ct the Category tower for NNI. JeremyFrom: Kurt Pag= ani <nilqed@gmail.com>

Dat= e: Thu, 9 Feb 2017 03:23:48 +0100

>> The game is to prove GCD = in NonNegativeInteger (NNI).

>

>We encounter numerous problems = when trying to prove gcd from EuclideanDomain:

>

>---

>gc= d(x, y) =3D=3D=C2=A0=C2=A0 --Euclidean Algorithm

>=C2=A0 x :=3D unitC= anonical x

>=C2=A0 y :=3D unitCanonical y

>=C2=A0 while not zer= o? y repeat

>=C2=A0=C2=A0=C2=A0 (x, y) :=3D (y, x rem y)

>=C2= =A0=C2=A0=C2=A0 y :=3D unitCanonical y=C2=A0=C2=A0=C2=A0=C2=A0 -- this does= n't affect the

>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 -- correctness of Euclid'= s algorithm,

>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 -- but

>=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 --= a) may improve performance

>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 -- b) ensures gcd(x,= y)=3Dgcd(y, x)

>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 --=C2=A0=C2=A0=C2=A0 if canonica= lUnitNormal

>=C2=A0 x

>

>---

>

>1. Define typ= e EuclideanDomain (tower of hierarchies)

>2. Define unitCanonical (de= pends 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

Jeremy recommended the boo=
k 'Concrete Semantics (free PDF at

http://www.concrete-semantics.org/) that looks like it ad= dresses

http://www.concrete-semantics.org/) that looks like it ad= dresses

Hoare triples for loop pre-/post-conditions. I had a=
discussion about

potentially creating a 'while' tact=
ic that might help loop proofs.

Axiom tends to=
use variables as 'named constants' in that, except for

(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 sco=
pe' also. I have automated the use of ACL2 for

proving th=
e lisp code in the compiler and interpreter. I have proven one

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 di=
dn'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 pr=
ovide proofs of the interpreter/compiler

code base. Spad is, =
after all, just a domain specific language in lisp.

<= br>

>

>Basically, I see two methods:

>

= >a) Implement spad language, e.g. like the "Imp" example:

&= gt;https= ://www.seas.upenn.edu/~cis500/current/sf/Imp.html

>and prove the = statements.

>Basically, I see two methods:

>

= >a) Implement spad language, e.g. like the "Imp" example:

&= gt;https= ://www.seas.upenn.edu/~cis500/current/sf/Imp.html

>and prove the = statements.

Implementing another, compatible Spad compile=
r would be much too

difficult. The compiler has to know about=
subtle things like 'the add chain'

and name overload=
ing and many other issues. Besides, that would have

to be pro=
ven anyway. So instead of making progress on proofs we'd be

>

>= ;b) Prove the math (by reusing existing [abundant] math libraries) and extr= act

>the functions (Definitions in Coq) as spad code.

>This wou= ld actually mean to replace parts of current code by new one (purely

>= ;functional).

I'm perfectly willing to replace existi=
ng code with code that can be proven

correct that implements =
the same functionality. The need to do that is almost

a certa=
inty. 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 proof=
s 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 l= imits (e.g. conflicts with

>built-in keywords)(**). Moreover, method = (b) is admittedly not what we really

>want: namely proving existing A= xiom code correct.

Why do you say that (b) is not what we=
really want? I expect that the

proof effort will uncover a l=
ot of problems in Spad code. The hope is

that it improves Ax=
iom.

...clipped...

&=
gt;

>

>Parameter BasicType:Type.

>Parameter eq: BasicType= -> BasicType -> bool.

>Parameter neq: BasicType -> BasicTyp= e -> bool.

>Infix "=3D" :=3D eq.

>

>Paramete= r x y z:BasicType.

>Check (x=3Dy).

>

>There are several b= etter choices of course: Module Type or type classes,

>whereas I'= m not very used to the latter.

>

>Parameter BasicType:Type.

>Parameter eq: BasicType= -> BasicType -> bool.

>Parameter neq: BasicType -> BasicTyp= e -> bool.

>Infix "=3D" :=3D eq.

>

>Paramete= r x y z:BasicType.

>Check (x=3Dy).

>

>There are several b= etter choices of course: Module Type or type classes,

>whereas I'= m not very used to the latter.

Indeed, neither am I but J=
eremy's example is a starting point.

=
>

>>

>> Unfortunately it appears the Coq and Lean wil= l not take kindly to

>> removing the existing libraries and replac= ing 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 a= nything and even do a

>

>$ coqtop -noinit

>

>so tha= t even "nat" is unknown.

>

>Coq < Check nat.

&g= t;Toplevel input, characters 6-9:

>> Check nat.

>>=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 ^^^

>Error: The reference nat was not = found in the current environment.

>>

>> Unfortunately it appears the Coq and Lean wil= l not take kindly to

>> removing the existing libraries and replac= ing 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 a= nything and even do a

>

>$ coqtop -noinit

>

>so tha= t even "nat" is unknown.

>

>Coq < Check nat.

&g= t;Toplevel input, characters 6-9:

>> Check nat.

>>=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 ^^^

>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 typ=
e tower. If so, I can automate extracting the 'class'

function.

>

>= ;>

>> Jeremy Avigad (Lean) made the suggestion to rename these= theorems.

>> Thus, instead of =3D, the supporting theorem would b= e 'spad=3D' (spad is

>> the name of Axiom's algebra la= nguage).

>>

>> Initially this would make Axiom depend on= the external library structure.

>> Eventually there should be eno= ugh embedded logic to start coding Axiom

>> theorems by changing e= xternal references from =3D to spad=3D everywhere.

>>

>>= Axiom proofs would still depend on the external proof system but only

&= gt;> for the correctness engine, not the library structure. This will mi= nimize

>> the struggle about Axiom's world view (e.g. handling= excluded middle).

>> It will also organize the logic library to m= ore closely mirror abstract algebra.

>

>Indeed, this is an impo= rtant point when dealing with dependent types. Type

>classes

>(= http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typec= lassestut.pdf)

>presumably could serve best to map the spad categ= ories while reasoning in CoC

>(whilst "exlcuded middle" may= be introduced as needed).

>= ;>

>> Jeremy Avigad (Lean) made the suggestion to rename these= theorems.

>> Thus, instead of =3D, the supporting theorem would b= e 'spad=3D' (spad is

>> the name of Axiom's algebra la= nguage).

>>

>> Initially this would make Axiom depend on= the external library structure.

>> Eventually there should be eno= ugh embedded logic to start coding Axiom

>> theorems by changing e= xternal references from =3D to spad=3D everywhere.

>>

>>= Axiom proofs would still depend on the external proof system but only

&= gt;> for the correctness engine, not the library structure. This will mi= nimize

>> the struggle about Axiom's world view (e.g. handling= excluded middle).

>> It will also organize the logic library to m= ore closely mirror abstract algebra.

>

>Indeed, this is an impo= rtant point when dealing with dependent types. Type

>classes

>(= http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typec= lassestut.pdf)

>presumably could serve best to map the spad categ= ories 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 fin= d the most suitable

>approach before building a prototype. I should d= ig into the "type classes"

>subject before making any sugge= stions.

I'm going to try to build the 'class'=
definitions for the Category hierarchy used

by NNI and autom=
ate their extraction, followed by proving gcd automatically.

=
Hopefully. Maybe. The idea is to 'turn the crank' for the first tim=
e and create

a prototype proof environment that runs during s=
ystem builds.

>

>BTW I have recently= written "field_mpl.v" (attached) for a talk about MPL where

&= gt;you can see how tedious it can be to prove simple facts from scratch, wh= ereas

>the last prop (P1) goes with ease owing to solid preparations = (it's educational

>only of course).

Thanks. I&#=
39;ll look at it in detail.

Tim

>

>--------------242E01CAAAC57564FEDE2669

>Content-Typ= e: text/plain; charset=3DUTF-8;

> name=3D"field_mpl.v"

&= gt;Content-Transfer-Encoding: 7bit

>Content-Disposition: attachment;<= br>> filename=3D"field_mpl.v"

>

>Module Field.

= >

>Parameter F : Set.

>Parameter plus : F->F->F.

&g= t;Parameter times : F->F->F.

>Parameter null : F.

>Parame= ter one : F.

>Parameter neg : F->F.

>Parameter inv : F->F= .

>

>Infix "+" :=3D plus.

>Infix "*" = :=3D times.

>Notation "0" :=3D null.

>Notation "= 1" :=3D one.

>Notation "- 1":=3D(neg one).

>Nota= tion "- u" :=3D (neg u).

>Notation "1 / u" :=3D (= inv u)

> (at level 75, right associativity).

>

>Axiom F1= : forall u v:F, exists w:F, w=3Du+v.

>Axiom F2: forall u v:F, exists = w:F, w=3Du*v.

>Axiom F3: forall u v:F, u+v =3D v+u.

>Axiom F4: = forall u v:F, u*v =3D v*u.

>Axiom F5: forall u v w:F, u+(v+w) =3D (u+= v)+w.

>Axiom F6: forall u v w:F, u*(v*w) =3D (u*v)*w.

>Axiom F7= : forall u v w:F, u*(v+w) =3D (u*v)+(u*w).

>Axiom F8: forall u v w:F,= (u+v)*w =3D (u*w)+(v*w).

>Axiom F9: forall u:F, u+0 =3D u.

>Ax= iom F10: forall u:F, u*1 =3D u.

>Axiom F11: forall u:F, u+(-u) =3D 0.=

>Axiom F12: forall u:F, ~(u=3D0) -> u * (1/u) =3D 1.

>Axiom= F13: 1 <> 0.

>

>

>Proposition null_unique: forall = n:F, (forall u:F, u+n=3Du) -> n=3D0.

>proof.

>let n:F.

&g= t;assume(forall u : F, u+n =3D u).

>then (0 + n =3D 0).

>then f= 1:(n+0 =3D 0) by F3.

>then f2:(n+0 =3D n) by F9.

>thus thesis b= y f1,f2.

>end proof.

>Qed.

>

>Proposition one_uniqu= e: forall e:F, (forall u:F, u*e=3Du) -> e=3D1.

>proof.

>let = e:F.

>assume(forall u : F, u*e =3D u).

>then (1*e =3D 1).

&g= t;then f1:(e*1 =3D 1) by F4.

>then f2:(e*1 =3D e) by F10.

>thus= thesis by f1,f2.

>end proof.

>Qed.

>

>(*

>Le= mma neg_null: forall u:F, (u=3Dneg u) -> u=3Dnull.

>proof.

>= let u:F.

>assume(u=3Dneg u).

>then (plus u u=3Dplus u (neg u)).=

>then (plus u u=3Dnull) by F11.

>end proof.

>Qed.

>= ;*)

>

>Proposition neg_unique: forall u:F, forall v:F, (u+v=3D0= ) -> v=3D-u.

>proof.

>let u:F, v:F.

>assume(u+v =3D 0)= .

>then ((-u)+(u+v)=3D(-u)+0).

>then f1:((-u) + (u+v)=3D-u) by = F9.

>then ((-u) + (u+v)=3D((-u)+u)+v) by F5.

>then ((-u) + (u+v= )=3D(u + (-u)) + v) by F3.

>then ((-u) + (u+v)=3D0+v) by F11.

>= then=C2=A0 f2:((-u)+(u+v)=3Dv) by F3,F9.

>thus thesis by f1,f2.

&g= t;end proof.

>Qed.

>

>

>Proposition inv_unique: for= all u:F, forall v:F, (~(u=3D0)/\(u*v=3D1)) -> v=3D(1/u).

>proof.**>let u:F, v:F.**

>assume a:(u<>0 /\ u * v =3D 1).

>the= n ((1/u)*(u*v)=3D((1/u)*1)).

>then f1:((1/u)*(u*v)=3D(1/u)) by F10.**>then ((1/u)*(u*v)=3D((1/u)*u)*v) by F6.**

>then ((1/u)*(u*v)=3D(u= *(1/u))*v) by F4.

>then ((1/u)*(u*v)=3D1*v) by a,F12.

>then f2:= ((1/u)*(u*v)=3Dv) by F4,F10.

>thus thesis by f1,f2.

>end proof.=

>Qed.

>

>Proposition times_null: forall u:F, u*0 =3D 0.<= br>>proof.

>let u:F.

>then(u * (0+0) =3D (u*0) + (u*0)) by F= 7.

>then(u*0 =3D (u*0) + (u*0)) by F9.

>then(0 =3D ((u*0) + (u*= 0)) + (- (u*0))) by F11.

>then(0 =3D (u*0) + ((u*0) + (- (u*0)))) by = F5.

>then(0 =3D (u*0) + 0) by F11.

>then(0 =3D u * 0) by F9.

>then f1:(u * 0 =3D 0)=C2=A0 by F4.

>take f1.

>end proof.**>Qed.**

>

>Proposition neg_is_neg_one_times: forall u:F, -u = =3D=C2=A0 (- 1) * u.

>proof.

>let u:F.

>then(u + ( - 1 * = u) =3D (u * 1) + (u * - 1)) by F4,F10.

>then(u + ( - 1 * u)=3D u * (1= + - 1)) by F7.

>then(u + ( - 1 * u)=3D u * 0) by F11.

>then f1= :(u + ( - 1 * u)=3D 0) by times_null.

>thus thesis by f1,neg_unique.<= br>>end proof.

>Qed.

>

>Proposition neg_null_is_null: = - 0 =3D 0.

>proof.

>have f1:(0+0 =3D 0) by F9.

>thus thes= is by f1, neg_unique.

>end proof.

>Qed.

>

>Proposit= ion inv_one_is_one: (1/1) =3D 1.

>proof.

>have f1:(1 * 1 =3D 1)= by F10.

>thus thesis by f1,F13,inv_unique.

>end proof.

>= Qed.

>

>Lemma neg_one_neq_null: not (- (1) =3D 0).

>proof= .

>assume(- (1)=3D 0).

>then f1:(1 +=C2=A0 -1 =3D 1+0) by F11.<= br>>then f2:(1 + - 1 =3D 1) by F9.

>then f3:(0 =3D 1) by f2,F11.**>thus thesis by f3,F13.**

>end proof.

>Qed.

>

><= br>>Proposition inv_neg_one_is_neg_one : (1/ - 1 ) =3D - 1.

>proof= .

>have (- 1 * (1/- 1 )=3D 1)=C2=A0 by neg_one_neq_null,F12.

>t= hen f1:((1 + - 1) * (1/ - 1)=3D 0) by F11,F4,times_null.

>then f2:( (= 1 + - 1) * (1/ - 1)=3D (1* (1/ - 1)) + (- 1 * (1/ - 1))) by F8.

>then= f3:((1+ - 1) * (1/- 1)=3D (1/ - 1) + 1)=C2=A0 by F4,F10,F12, neg_one_neq_n= ull.

>then f4:(0 =3D=C2=A0 (1/- 1) +1) by f1,f3.

>then f5: (1+ = (1/ - 1) =3D 0) by f4,F3.

>thus thesis by neg_unique, f5.

>end = proof.

>Qed.

>=C2=A0

>

>Lemma neg_one_times_neg_on= e_is_one: -1 * -1 =3D1.

>proof.

>have f1:(-1*(1+ -1)=3D0) by F1= 1, times_null.

>then f2:(-1*(1+ -1)=3D-1*1 + -1*-1) by F7.

>the= n f3:(-1*(1+ -1)=3D-1 + -1*-1) by f2,F10.

>then f4:( 0=3D-1+ -1*-1) b= y f3,f1.

>then (1+0 =3D 1 + (-1+ -1*-1) ) by f4.

>then (1=3D(1+= -1)+ (-1*-1)) by F5,F9.

>then (1=3D0+(-1*-1)) by F11.

>then f8:= (1=3D(-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)=3Du*v.

>proof.

>let u:F, v:F.

>have f1: = ( -u =3D -1*u) by neg_is_neg_one_times.

>have f2: ( -v =3D -1*v) by n= eg_is_neg_one_times.

>then (-u * -v =3D (-1*u)*(-1*v)) by f1,f2.

&= gt;then (-u * -v =3D ((-1*u)*-1)*v) by F6.

>then (-u * -v =3D (-1*(-1= *u))*v) by F4.

>then=C2=A0 (-u * -v =3D ((-1*-1)*u)*v) by F6.

>= then=C2=A0 (-u * -v =3D (1*u)*v) by neg_one_times_neg_one_is_one.

>th= en f3:(-u * -v =3D u*v) by F4,F10.

>thus thesis by f3.

>end pro= of.

>Qed.

>

>Lemma not_null_then_inv_not_null: forall u:F= , u<>0 -> (1/u)<>0.

>proof.

>let u:F.

>ass= ume f1:(u<>0).

>assume f2:( (1/u)=3D0).

>then f3:(u*(1/u)= =3D1) by f1,F12.

>then (u*(1/u)=3Du*0) by f1,f2.

>then f4:(1=3D= u*0) by f3.

>thus thesis by f4,times_null, F13.

>end proof.

= >Qed.

>

>Proposition inv_inv_is_id: forall u:F, ~(u=3D0) -&g= t; (1 / (1 / u)) =3D u.

>proof.

>let u:F.

>assume h1:(u&l= t;>0).

>have(u* (1/u)=3D1) by h1,F12.

>then f1:( (1/u)*u=3D1= ) by F4.

>then f2:((1/u)*(1 / (1/u))=3D1) by h1,not_null_then_inv_not= _null, F12.

>then ( (1/u)*(1 / (1/u)) =3D (1/u)*u ) by f1,f2.

>= then (=C2=A0 (1 / 1/u)*( (1/u)*(1 / (1/u))) =3D (1 / 1/u) * ( (1/u)*u )).**>then (=C2=A0 ((1 / 1/u)* (1/u)) * (1 / (1/u)) =3D=C2=A0 ((1 / 1/u) *=
=C2=A0 (1/u))*u ) by F6.**

>then (=C2=A0 ( (1/u)*(1 / 1/u)) * (1 / (1/u= )) =3D=C2=A0 ( (1/u)*(1 / 1/u))*u ) by F4.

>then f3:( 1* (1 / (1/u)) = =3D 1*u) by f2.

>thus thesis by f3,F4, F10.

>end proof.

>= Qed.

>

>Lemma prod_not_null: forall u v:F, ((u<>0)/\ (v&l= t;>0)) -> (u*v<>0).

>proof.

>let u:F, v:F.

>a= ssume h1:(u <> 0 /\ v <> 0).

>then f1:(u<>0) by h1.=

>then f2:(v<>0) by h1.

>assume h2:(u*v=3D0).

>then= (u*v=3Du*0) by times_null.

>then ( (1/u)*(u*v) =3D (1/u)*(u*0)) by f= 1,F12.

>then ( (u*(1/u))*v=3D(u*(1/u))*0) by F6,F4.

>then f3:(v= =3D0) by f1,F4,F12,F10.

>thus thesis by f2,f3.

>end proof.

&= gt;Qed.

>

>

>Proposition inv_prod_is_prod_inv: forall u v= :F, ((u<>0)/\ (v<>0)) ->

>=C2=A0 ((1/(u*v)) =3D (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.

&g= t;then ( (u*v)* ((1/u)*(1/v)) =3D (u*v)* ((1/v)*(1/u))) by F4.

>then = ( (u*v)* ((1/u)*(1/v)) =3D ((u*v)* (1/v))*(1/u)) by F6.

>then ( (u*v)= * ((1/u)*(1/v)) =3D (u*(v* (1/v))*(1/u))) by F6.

>then ( (u*v)* ((1/u= )*(1/v)) =3D (u*1)*(1/u)) by f2,F12.

>then ( (u*v)* ((1/u)*(1/v)) =3D= (u*(1/u))) by F10.

>then ((u*v)* ((1/u)*(1/v)) =3D 1) by f1,F12.

= >then f4:((1/u)*(1/v)=3D(1 / u * v) ) by f3,inv_unique.

>thus thes= is by f4.

>end proof.

>Qed.

>

>

>End Field.**>**

>

>Let S:=3DField.F.

>Notation "x + y":= =3D(Field.plus x y).

>Notation "x * y":=3D(Field.times x y)= .

>Lemma comm: forall x y:S,x+y=3Dy+x.

>proof.

>intros.<= br>>thus thesis by Field.F3.

>end proof.

>Qed.

>

&g= t;Definition addAndSquare(a b:S):S:=3D(a+b)*(a+b).

>Definition sq(a:S= ):S:=3Da*a.

>

>Check addAndSquare Field.one Field.one.

>C= ompute addAndSquare Field.one Field.null.

>

>Proposition P1:for= all a b:S, addAndSquare a b =3D

>=C2=A0 (sq a) + (sq b)+a*b+b*a.

&= gt;proof.

>let u:S.

>let v:S.

>compute.

>thus thesi= s by Field.F7,Field.F8,Field.F3,Field.F5.

>end proof.

>Qed.

= >

>(*

>have f1:((u+v)*(u+v) =3Du*(u+v)+v*(u+v)) by Field.F8.=

>then f2:((u+v)*(u+v) =3D u*u+u*v+v*(u+v)) by f1,Field.F7.

>th= en f3:((u+v)*(u+v)=3D 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.**>*)**

>

>--------------242E01CAAAC57564FEDE2669

>Content-Typ= e: text/plain; charset=3DUTF-8;

> name=3D"field_mpl.v"

&= gt;Content-Transfer-Encoding: 7bit

>Content-Disposition: attachment;<= br>> filename=3D"field_mpl.v"

>

>Module Field.

= >

>Parameter F : Set.

>Parameter plus : F->F->F.

&g= t;Parameter times : F->F->F.

>Parameter null : F.

>Parame= ter one : F.

>Parameter neg : F->F.

>Parameter inv : F->F= .

>

>Infix "+" :=3D plus.

>Infix "*" = :=3D times.

>Notation "0" :=3D null.

>Notation "= 1" :=3D one.

>Notation "- 1":=3D(neg one).

>Nota= tion "- u" :=3D (neg u).

>Notation "1 / u" :=3D (= inv u)

> (at level 75, right associativity).

>

>Axiom F1= : forall u v:F, exists w:F, w=3Du+v.

>Axiom F2: forall u v:F, exists = w:F, w=3Du*v.

>Axiom F3: forall u v:F, u+v =3D v+u.

>Axiom F4: = forall u v:F, u*v =3D v*u.

>Axiom F5: forall u v w:F, u+(v+w) =3D (u+= v)+w.

>Axiom F6: forall u v w:F, u*(v*w) =3D (u*v)*w.

>Axiom F7= : forall u v w:F, u*(v+w) =3D (u*v)+(u*w).

>Axiom F8: forall u v w:F,= (u+v)*w =3D (u*w)+(v*w).

>Axiom F9: forall u:F, u+0 =3D u.

>Ax= iom F10: forall u:F, u*1 =3D u.

>Axiom F11: forall u:F, u+(-u) =3D 0.=

>Axiom F12: forall u:F, ~(u=3D0) -> u * (1/u) =3D 1.

>Axiom= F13: 1 <> 0.

>

>

>Proposition null_unique: forall = n:F, (forall u:F, u+n=3Du) -> n=3D0.

>proof.

>let n:F.

&g= t;assume(forall u : F, u+n =3D u).

>then (0 + n =3D 0).

>then f= 1:(n+0 =3D 0) by F3.

>then f2:(n+0 =3D n) by F9.

>thus thesis b= y f1,f2.

>end proof.

>Qed.

>

>Proposition one_uniqu= e: forall e:F, (forall u:F, u*e=3Du) -> e=3D1.

>proof.

>let = e:F.

>assume(forall u : F, u*e =3D u).

>then (1*e =3D 1).

&g= t;then f1:(e*1 =3D 1) by F4.

>then f2:(e*1 =3D e) by F10.

>thus= thesis by f1,f2.

>end proof.

>Qed.

>

>(*

>Le= mma neg_null: forall u:F, (u=3Dneg u) -> u=3Dnull.

>proof.

>= let u:F.

>assume(u=3Dneg u).

>then (plus u u=3Dplus u (neg u)).=

>then (plus u u=3Dnull) by F11.

>end proof.

>Qed.

>= ;*)

>

>Proposition neg_unique: forall u:F, forall v:F, (u+v=3D0= ) -> v=3D-u.

>proof.

>let u:F, v:F.

>assume(u+v =3D 0)= .

>then ((-u)+(u+v)=3D(-u)+0).

>then f1:((-u) + (u+v)=3D-u) by = F9.

>then ((-u) + (u+v)=3D((-u)+u)+v) by F5.

>then ((-u) + (u+v= )=3D(u + (-u)) + v) by F3.

>then ((-u) + (u+v)=3D0+v) by F11.

>= then=C2=A0 f2:((-u)+(u+v)=3Dv) by F3,F9.

>thus thesis by f1,f2.

&g= t;end proof.

>Qed.

>

>

>Proposition inv_unique: for= all u:F, forall v:F, (~(u=3D0)/\(u*v=3D1)) -> v=3D(1/u).

>proof.

>assume a:(u<>0 /\ u * v =3D 1).

>the= n ((1/u)*(u*v)=3D((1/u)*1)).

>then f1:((1/u)*(u*v)=3D(1/u)) by F10.

>then ((1/u)*(u*v)=3D(u= *(1/u))*v) by F4.

>then ((1/u)*(u*v)=3D1*v) by a,F12.

>then f2:= ((1/u)*(u*v)=3Dv) by F4,F10.

>thus thesis by f1,f2.

>end proof.=

>Qed.

>

>Proposition times_null: forall u:F, u*0 =3D 0.<= br>>proof.

>let u:F.

>then(u * (0+0) =3D (u*0) + (u*0)) by F= 7.

>then(u*0 =3D (u*0) + (u*0)) by F9.

>then(0 =3D ((u*0) + (u*= 0)) + (- (u*0))) by F11.

>then(0 =3D (u*0) + ((u*0) + (- (u*0)))) by = F5.

>then(0 =3D (u*0) + 0) by F11.

>then(0 =3D u * 0) by F9.

>then f1:(u * 0 =3D 0)=C2=A0 by F4.

>take f1.

>end proof.

>

>Proposition neg_is_neg_one_times: forall u:F, -u = =3D=C2=A0 (- 1) * u.

>proof.

>let u:F.

>then(u + ( - 1 * = u) =3D (u * 1) + (u * - 1)) by F4,F10.

>then(u + ( - 1 * u)=3D u * (1= + - 1)) by F7.

>then(u + ( - 1 * u)=3D u * 0) by F11.

>then f1= :(u + ( - 1 * u)=3D 0) by times_null.

>thus thesis by f1,neg_unique.<= br>>end proof.

>Qed.

>

>Proposition neg_null_is_null: = - 0 =3D 0.

>proof.

>have f1:(0+0 =3D 0) by F9.

>thus thes= is by f1, neg_unique.

>end proof.

>Qed.

>

>Proposit= ion inv_one_is_one: (1/1) =3D 1.

>proof.

>have f1:(1 * 1 =3D 1)= by F10.

>thus thesis by f1,F13,inv_unique.

>end proof.

>= Qed.

>

>Lemma neg_one_neq_null: not (- (1) =3D 0).

>proof= .

>assume(- (1)=3D 0).

>then f1:(1 +=C2=A0 -1 =3D 1+0) by F11.<= br>>then f2:(1 + - 1 =3D 1) by F9.

>then f3:(0 =3D 1) by f2,F11.

>end proof.

>Qed.

>

><= br>>Proposition inv_neg_one_is_neg_one : (1/ - 1 ) =3D - 1.

>proof= .

>have (- 1 * (1/- 1 )=3D 1)=C2=A0 by neg_one_neq_null,F12.

>t= hen f1:((1 + - 1) * (1/ - 1)=3D 0) by F11,F4,times_null.

>then f2:( (= 1 + - 1) * (1/ - 1)=3D (1* (1/ - 1)) + (- 1 * (1/ - 1))) by F8.

>then= f3:((1+ - 1) * (1/- 1)=3D (1/ - 1) + 1)=C2=A0 by F4,F10,F12, neg_one_neq_n= ull.

>then f4:(0 =3D=C2=A0 (1/- 1) +1) by f1,f3.

>then f5: (1+ = (1/ - 1) =3D 0) by f4,F3.

>thus thesis by neg_unique, f5.

>end = proof.

>Qed.

>=C2=A0

>

>Lemma neg_one_times_neg_on= e_is_one: -1 * -1 =3D1.

>proof.

>have f1:(-1*(1+ -1)=3D0) by F1= 1, times_null.

>then f2:(-1*(1+ -1)=3D-1*1 + -1*-1) by F7.

>the= n f3:(-1*(1+ -1)=3D-1 + -1*-1) by f2,F10.

>then f4:( 0=3D-1+ -1*-1) b= y f3,f1.

>then (1+0 =3D 1 + (-1+ -1*-1) ) by f4.

>then (1=3D(1+= -1)+ (-1*-1)) by F5,F9.

>then (1=3D0+(-1*-1)) by F11.

>then f8:= (1=3D(-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)=3Du*v.

>proof.

>let u:F, v:F.

>have f1: = ( -u =3D -1*u) by neg_is_neg_one_times.

>have f2: ( -v =3D -1*v) by n= eg_is_neg_one_times.

>then (-u * -v =3D (-1*u)*(-1*v)) by f1,f2.

&= gt;then (-u * -v =3D ((-1*u)*-1)*v) by F6.

>then (-u * -v =3D (-1*(-1= *u))*v) by F4.

>then=C2=A0 (-u * -v =3D ((-1*-1)*u)*v) by F6.

>= then=C2=A0 (-u * -v =3D (1*u)*v) by neg_one_times_neg_one_is_one.

>th= en f3:(-u * -v =3D u*v) by F4,F10.

>thus thesis by f3.

>end pro= of.

>Qed.

>

>Lemma not_null_then_inv_not_null: forall u:F= , u<>0 -> (1/u)<>0.

>proof.

>let u:F.

>ass= ume f1:(u<>0).

>assume f2:( (1/u)=3D0).

>then f3:(u*(1/u)= =3D1) by f1,F12.

>then (u*(1/u)=3Du*0) by f1,f2.

>then f4:(1=3D= u*0) by f3.

>thus thesis by f4,times_null, F13.

>end proof.

= >Qed.

>

>Proposition inv_inv_is_id: forall u:F, ~(u=3D0) -&g= t; (1 / (1 / u)) =3D u.

>proof.

>let u:F.

>assume h1:(u&l= t;>0).

>have(u* (1/u)=3D1) by h1,F12.

>then f1:( (1/u)*u=3D1= ) by F4.

>then f2:((1/u)*(1 / (1/u))=3D1) by h1,not_null_then_inv_not= _null, F12.

>then ( (1/u)*(1 / (1/u)) =3D (1/u)*u ) by f1,f2.

>= then (=C2=A0 (1 / 1/u)*( (1/u)*(1 / (1/u))) =3D (1 / 1/u) * ( (1/u)*u )).

>then (=C2=A0 ( (1/u)*(1 / 1/u)) * (1 / (1/u= )) =3D=C2=A0 ( (1/u)*(1 / 1/u))*u ) by F4.

>then f3:( 1* (1 / (1/u)) = =3D 1*u) by f2.

>thus thesis by f3,F4, F10.

>end proof.

>= Qed.

>

>Lemma prod_not_null: forall u v:F, ((u<>0)/\ (v&l= t;>0)) -> (u*v<>0).

>proof.

>let u:F, v:F.

>a= ssume h1:(u <> 0 /\ v <> 0).

>then f1:(u<>0) by h1.=

>then f2:(v<>0) by h1.

>assume h2:(u*v=3D0).

>then= (u*v=3Du*0) by times_null.

>then ( (1/u)*(u*v) =3D (1/u)*(u*0)) by f= 1,F12.

>then ( (u*(1/u))*v=3D(u*(1/u))*0) by F6,F4.

>then f3:(v= =3D0) by f1,F4,F12,F10.

>thus thesis by f2,f3.

>end proof.

&= gt;Qed.

>

>

>Proposition inv_prod_is_prod_inv: forall u v= :F, ((u<>0)/\ (v<>0)) ->

>=C2=A0 ((1/(u*v)) =3D (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.

&g= t;then ( (u*v)* ((1/u)*(1/v)) =3D (u*v)* ((1/v)*(1/u))) by F4.

>then = ( (u*v)* ((1/u)*(1/v)) =3D ((u*v)* (1/v))*(1/u)) by F6.

>then ( (u*v)= * ((1/u)*(1/v)) =3D (u*(v* (1/v))*(1/u))) by F6.

>then ( (u*v)* ((1/u= )*(1/v)) =3D (u*1)*(1/u)) by f2,F12.

>then ( (u*v)* ((1/u)*(1/v)) =3D= (u*(1/u))) by F10.

>then ((u*v)* ((1/u)*(1/v)) =3D 1) by f1,F12.

= >then f4:((1/u)*(1/v)=3D(1 / u * v) ) by f3,inv_unique.

>thus thes= is by f4.

>end proof.

>Qed.

>

>

>End Field.

>

>Let S:=3DField.F.

>Notation "x + y":= =3D(Field.plus x y).

>Notation "x * y":=3D(Field.times x y)= .

>Lemma comm: forall x y:S,x+y=3Dy+x.

>proof.

>intros.<= br>>thus thesis by Field.F3.

>end proof.

>Qed.

>

&g= t;Definition addAndSquare(a b:S):S:=3D(a+b)*(a+b).

>Definition sq(a:S= ):S:=3Da*a.

>

>Check addAndSquare Field.one Field.one.

>C= ompute addAndSquare Field.one Field.null.

>

>Proposition P1:for= all a b:S, addAndSquare a b =3D

>=C2=A0 (sq a) + (sq b)+a*b+b*a.

&= gt;proof.

>let u:S.

>let v:S.

>compute.

>thus thesi= s by Field.F7,Field.F8,Field.F3,Field.F5.

>end proof.

>Qed.

= >

>(*

>have f1:((u+v)*(u+v) =3Du*(u+v)+v*(u+v)) by Field.F8.=

>then f2:((u+v)*(u+v) =3D u*u+u*v+v*(u+v)) by f1,Field.F7.

>th= en f3:((u+v)*(u+v)=3D u*u+u*v+v*u+v*v) by f2, Field.F7,Field.F3,Field.F5.

>end proof.

>Qed.

>Is there anything that requires th=
at the operation you implement is=20

>reflexive, symmetric, and transitive?=C2=A0 Putting axioms on the s= tructure=20

>specifies that that has to be the case. Without such axioms, you**>cannot=20
prove anything about implementations in general. You can **

>only prove= =20 things about individual implementations.

Yes. Such properties =
are required by the Category hierarchy. There is,>reflexive, symmetric, and transitive?=C2=A0 Putting axioms on the s= tructure=20

>specifies that that has to be the case. Without such axioms, you

>only prove= =20 things about individual implementations.

On Wed, Feb 8, 2017 at 9:44 PM, Jeremy Avigad <=
;avigad@cmu.edu>=
wrote:

On We= d, Feb 8, 2017 at 9:23 PM, Tim Daly <axiomcas@gmail.com> wr= ote:==The semantics of =3D is given in the= Domain (the current one being defined is called % in Spad)Part of your struggle of under= standing what I wrote is that I'm not yet fluent in thelogic = language and syntax. I'm learning as fast as I can so please be patient= .

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D

CATEGORY SIGNATURE vs DOMAIN SEMANTICS

> Presumably you will even= tually want to add axioms to the structures that say

> things about = what eq and neq don= ot in the Category (well...you can... sigh)

Each domain that i= nherits '=3D' from the Category BasicType needs to specify the mean= ing

of that function for the Domain you're implementing..<= /span>In our language, we would say that every instance of the structu= re has all the necessary data. For example, every group (=3Dinstance of the= group structure, or element of the type group =CE=B1) has a unit, a binary= operation, and inverse operation, etc.=C2=A0=C2= =A0For a Polynomial domain with some

structural= data representation you have to define what it means for two polynomial ob= jects

to be =3D. such as a function to compare coefficients. Part of th= e game would be to provethat the coefficient-compare functio= n is correct, always returns a Boolean, and terminates.

All a Category like BasicType does is specify that the Domain Polyno= mial should

implement an =3D operation with the given signature.=C2=A0 = That is, you have to implement

=C2=A0=C2=A0=C2=A0= =C2=A0 poly =3D poly

which returns a boolean. (Note that= there are other =3D functions in Polynomial such as onethat= returns an equation object but that signature is inherited from a differen= t Category).

Is there anything that requires that the operation you =
implement is reflexive, symmetric, and transitive?=C2=A0 Putting axioms on =
the structure specifies that that has to be the case. Without such axioms, =
you cannot prove anything about implementations in general. You can only pr=
ove things about individual implementations.

<= div>with the same name and same arguments but different return type= s, for example).by = the arguments but also by the return type (so there can be multiple functio= nsEverything in Spad = is strongly typed and function definitions are chosen not only=C2=A0=C2=A0=C2=A0 gcd(y rem x, x)=C2=A0=C2=A0=C2=A0 zero? x =3D> y=C2=A0 = gcd(x:NNI,y:NNI):NNI =3D=3Dand Axiom's definition is=C2=A0=C2=A0= =C2=A0 end.=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= | S a' =3D> gcd (b mod (S a')) (S a')=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0 | 0 =3D> b=C2=A0=C2=A0=C2=A0 match a with=C2=A0 Fixpoint= gcd a b :=3D<= div>Coq provides gcd asIt looks like your 'class' syntax impl= ements what I need. I will try this for the otherCategories = used in NNI.= a function that fulfills the signature of

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D PROVING TERMINATIONAs I understood from clas= s, for an algorithm like gcd it should be sufficient to construct

=C2=A0=C2=A0 gcd(a:N= NI,b:NNI):NNI

Every statement in the function is strongly type-check= ed.

That is wh=
at I referred to as a shallow embedding -- you are associating to every axi=
om definition a Coq or Lean definition which has the same behavior.

If you do that, you cannot model arbitrary while loops. Y=
ou have to write functions in Coq or Lean in a way that, from the start, th=
ey are guaranteed to terminate. You can do this, for example, by showing th=
e recursive calls are decreasing along a suitable measure, or giving a prio=
ri bounds on a while loop. If you want to translate spad functions automati=
cally, you'll have to write the former in such a way that the translati=
ons have this property. You can't translate an arbitrary, a priori part=
ial, function and then show after the fact that it terminates for every inp=
ut.

Other approaches are possible. You can, for ex=
ample, translate spad functions to relations in Coq or Lean, and then prove=
that the relations give rise to total functions.

=
Best wishes,

Jeremy

=C2=A0

Thus we are guaranteed= that the Spad version of gcd above (in the Domain NNI)can o= nly be called with NNI arguments and is guaranteed to only return NNI resul= ts.

The languages are very close in spirit if not in synt= ax.What Axiom does not do, for example, is pr= ove termination.

Coq, in its version, will figure out that the recu= rsion is on 'a' and that it will terminate.

Part = of the game is to provide the same termination analysis on Spad code.

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D ADDITIONAL CONSTRAINTSIt would be ideal to reject code that did not fulfill all of the re= quirementssuch as specifying at the Category level definitio= n of gcd that it not onlyhas to have the correct signature, = it also has to return the 'positive'divisor. For NNI= this is trivially fulfilled.The Category definition should s= ay something like=C2=A0=C2=A0 gcd(%,%) -> %=C2=A0 and= gcd >=3D 1$%where 1$% says to use the unit from the impl= ementing Domain.

So for some domains we have:=C2=A0 gcd= (x,y) =3D=3D=C2=A0=C2=A0=C2=A0 x :=3D unitCanonical x=C2=A0=C2=A0=C2=A0 y :=3D unitCanonical y=C2=A0=C2= =A0=C2=A0 while not zero? y repeat=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0 (x,y) :=3D (y, x rem y)=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= y :=3D unitCanonical y=C2=A0=C2=A0=C2=A0 xusi= ng unitCanonical to deal with things like signs. (This also adds the compli= cation

of loops which I mentioned in a previous email.)Not only the signature but the side-conditions would have to be checked.=

=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D<= br> ALTERNATE APPROACHESInstead of = a new library organization it might be possible to have a generator functio= nin Coq that translates Coq code to Spad code. Or a translat= or from Spad code toCoq code.

Unfortunately Coq and = Lean do not seem to use function name overloadingor inherita= nce (or do they?) which confuses the problem of name translation.

<= /div>Axiom has 42 functions named 'gcd', each living in a diff= erent Domain.There is no such= thing as a simple job. But this one promises to be interesting.In any case I'll push the implementation forward. Thanks for yo= ur help.Tim<= /span>

On Wed, Feb 8, 2017 at 5:52 PM, Jeremy Avigad= <= avigad@cmu.edu> wrote:Dear Tim,I don't un= derstand what you mean. For one thing, theorems in both Lean and Coq are ma= rked as opaque, since you generally don't care about the contents. But = even if we replace "theorem" by "definition," I don'= ;t know what you imagine going into the "...".I think what you want to do is represent Axiom categories as structu= res. For example, the declarations below declare a BasicType structure and = notation for elements of that structure. You can then prove theorems about = arbitrary types=C2=A0=CE=B1 that have a BasicType structure. You can also e= xtend the structure as needed.(Presumably you= will eventually want to add axioms to the structures that say things about= what eq and neq do. Otherwise, you are just reasoning about a type with tw= o relations.)Best wishes,Jeremy <= div class=3D"m_-395149912675556144gmail-m_7070670209948040027gmail-HOEnZb">=class BasicType (=CE=B1 : Type) : Ty= pe :=3D(eq : =CE=B1 =E2=86=92 =CE=B1 =E2=86=92 bool) (neq : =CE= =B1 =E2=86=92 =CE=B1 =E2=86=92 bool)infix `?=3D?`= :50 =C2=A0:=3D BasicType.eqinfix `?~=3D?`:50 :=3D BasicType.neq<= /div>section=C2=A0 variables (=CE=B1 : Type)= [BasicType =CE=B1]=C2=A0 variables a b : =CE=B1=C2=A0=C2=A0 check a ?=3D? b=C2=A0 check a ?~=3D? bend