From b041263927533c08938ea5b8fbcf08a3966c1b90 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Mon, 23 Jan 2017 14:23:52 -0500
Subject: [PATCH] books/bookvol13 More details of the GCD proof
Goal: Proving Axiom Correct
\begin{chunk}{axiom.bib}
@misc{WikiED,
author = "Wikipedia",
title = "Euclidean Domain"
year = "2017",
link = "\url{https://en.wikipedia.org/wiki/Euclidean\_domain}"
}
\end{chunk}
In axiom.sty We added theorem, lemma, proposition, corollary,
example, remark, definition, qed, axiom as environments for proofs.
---
books/axiom.sty | 25 +++++
books/bookvol13.pamphlet | 207 ++++++++++++++++++++++++++++++++++++++-
books/bookvolbib.pamphlet | 10 ++
changelog | 4 +
patch | 29 ++----
src/axiom-website/patches.html | 2 +
6 files changed, 253 insertions(+), 24 deletions(-)
diff --git a/books/axiom.sty b/books/axiom.sty
index 44f9823..6eae42f 100644
--- a/books/axiom.sty
+++ b/books/axiom.sty
@@ -42,6 +42,31 @@
\mathchardef\bigslash="232C
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% implement theorem, lemma, proposition, corollary, example, remark,
+%% definition, qed ... add axiom
+%% from www.maths.tcd.ie/~dwilkins/LaTeXPrimer/Theorems.html
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newtheorem{theorem}{Theorem}
+\newtheorem{lemma}[theorem]{Lemma}
+\newtheorem{proposition}[theorem]{Proposition}
+\newtheorem{corollary}[theorem]{Corollary}
+\newtheorem{axiom}[theorem]{Axiom}
+
+\newenvironment{proof}[1][Proof]{\begin{trivlist}
+\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
+\newenvironment{definition}[1][Definition]{\begin{trivlist}
+\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
+\newenvironment{example}[1][Example]{\begin{trivlist}
+\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
+\newenvironment{remark}[1][Remark]{\begin{trivlist}
+\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
+
+\newcommand{\qed}{\nobreak \ifvmode \relax \else
+ \ifdim\lastskip<1.5em \hskip-\lastskip
+ \hskip1.5em plus0em minus0.5em \fi \nobreak
+ \vrule height0.75em width0.5em depth0.25em\fi}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% implement the ceiling and floor functions
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\providecommand{\ceiling}[1]{\left\lceil #1\right\rceil}
diff --git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index 329afd5..050d713 100644
--- a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ -14,8 +14,7 @@ daunting task of its own.
The proof of a single Axiom algorithm is done with an eye toward
automating the process. Automated machine proofs are not possible
-in general but will certainly exist for known algorithms.
-Bressoud said:
+in general but will exist for known algorithms.
\begin{quote}
{\bf Writing is nature's way of letting you know how sloppy your
@@ -98,11 +97,85 @@ the {\sl computational content} of the proposition.}
\end{quote}
\chapter{Here is a problem}
+
+Proving programs correct involves working with a second programming
+language, the proof language, that is well-founded on some theory.
+Proofs (programs), can be reduced (compiled) in this new language
+to the primitive constructs (machine language).
+
+The ideal case would be that the programming language used, such as
+Spad, can be iosmorphic, or better yet, syntactically the same as
+the proof language. Unfortunately that is not (yet?) the case with Spad.
+
+The COQ system language, Gallina, is the closest match to Spad.
+
+\section{Setting up the problem}
+
+The GCD function will be our first example of a proof.
+
The goal is to prove that Axiom's implementation of
the Euclidean GCD algorithm is correct.
-From category EuclideanDomain (EUCDOM) we find the implementation of
-the Euclidean GCD algorithm:
+We need to be clear about what is to be proven. In this case, we
+need to show that, given GCD(a,b),
+\begin{enumerate}
+\item {\bf GCD} is a function from $a\times b \Rightarrow c$
+\item {\bf a} and {\bf b} are elements of the correct type
+\item {\bf c}, the resullt, is the correct type
+\item the meaning of {\bf divisor}
+\item the meaning of a {\bf common divisor}
+\item {\bf GCD} terminates
+\end{enumerate}
+
+We next need to set up the things we know in "the global environment",
+generally referred to as {\bf E} in Coq.
+
+Axiom's GCD is categorically defined to work over any Euclidean domain.
+This means that the axioms of a Euclidean domain are globally available.
+In fact, this is stronger than we need since
+\begin{itemize}
+\item commutative rings $\subset$ integral domains
+\item integral domains $\subset$ integrally closed domains
+\item integrally closed domains $\subset$ GCD domains
+\item GCD domains $\subset$ unique factorization domains
+\item unique factorization domains $\subset$ principlal ideal domains
+\item principlal ideal domains $\subset$ Euclidean domains
+\end{itemize}
+
+A Euclidean function on $R$ is a function $f$ from $\mathbb{R}\\\{0\}$
+to the non-negative integers satisfying the following fundamental
+division-with-remainder property\cite{WikiED}:
+
+$D(a,b)$ = set of common divisors of $a$ and $b$.
+
+$\gcd(a,b) = \max{D(a,b)}$
+
+
+\section{Axiom NNI GCD}
+
+NonNegativeInteger inherits {\tt gcd} from {\tt Integer} up the ``add chain''
+since it is a subtype of {\tt Integer}. {\tt Integer} has {\tt EuclideanDomain}
+as an ancestor\cite{Book103}:
+\begin{verbatim}
+(1) -> getAncestors "Integer"
+
+ (1)
+ {AbelianGroup, AbelianMonoid, AbelianSemiGroup, Algebra, BasicType,
+ BiModule, CancellationAbelianMonoid, CharacteristicZero, CoercibleTo,
+ CombinatorialFunctionCategory, CommutativeRing, ConvertibleTo,
+ DifferentialRing, EntireRing, EuclideanDomain, GcdDomain,
+ IntegerNumberSystem, IntegralDomain, LeftModule, LeftOreRing,
+ LinearlyExplicitRingOver, Module, Monoid, OpenMath, OrderedAbelianGroup,
+ OrderedAbelianMonoid, OrderedAbelianSemiGroup,
+ OrderedCancellationAbelianMonoid, OrderedIntegralDomain, OrderedRing,
+ OrderedSet, PatternMatchable, PrincipalIdealDomain, RealConstant,
+ RetractableTo, RightModule, Ring, Rng, SemiGroup, SetCategory, StepThrough,
+ UniqueFactorizationDomain}
+ Type: Set(Symbol)
+\end{verbatim}
+
+From category {\tt EuclideanDomain} (EUCDOM) we find the implementation of
+the Euclidean GCD algorithm\cite{Book102}:
\begin{verbatim}
gcd(x,y) == --Euclidean Algorithm
x:=unitCanonical x
@@ -117,8 +190,8 @@ the Euclidean GCD algorithm:
-- if canonicalUnitNormal
x
\end{verbatim}
-The unitCanonical function comes from the category IntegralDomain (INTDOM)
-where we find:
+The {\tt unitCanonical} function comes from the category
+{\tt IntegralDomain} (INTDOM) where we find:
\begin{verbatim}
unitNormal: % -> Record(unit:%,canonical:%,associate:%)
++ unitNormal(x) tries to choose a canonical element
@@ -150,6 +223,43 @@ implemented as
true
\end{verbatim}
+Coq proves the following GCD function:
+\begin{verbatim}
+ Fixpoint gcd a b :=
+ match a with
+ | 0 => b
+ | S a' => gcd (b mod (S a')) (S a')
+ end.
+\end{verbatim}
+
+This can be translated directly to working Spad code:
+\begin{verbatim}
+ GCD(x:NNI,y:NNI):NNI ==
+ zero? x => y
+ GCD(y rem x,x)
+\end{verbatim}
+with the test case results of:
+\begin{verbatim}
+(1) -> GCD(2415,945)
+ Compiling function mygcd2 with type (NonNegativeInteger,
+ NonNegativeInteger) -> NonNegativeInteger
+
+ (1) 105
+ Type: PositiveInteger
+(2) -> GCD(0,945)
+
+ (2) 945
+ Type: PositiveInteger
+(3) -> GCD(2415,0)
+
+ (3) 2415
+ Type: PositiveInteger
+(4) -> GCD(17,15)
+
+ (4) 1
+ Type: PositiveInteger
+\end{verbatim}
+
\section{Mathematics}
From Buchberger\cite{Buch97},
@@ -2091,6 +2201,91 @@ proof of the Euclidean algorithm using COQ.
Aczel\cite{Acze13} Homotopy Type Theory
+\appendix
+
+\chapter{The Global Environment}
+
+Let $S$ be a set. Let $\circ$ be a binary operation.
+Let $+$ be an additive operation. Let $*$ be a multiplicative operation.
+
+\begin{axiom}[Magma]
+A {\bf Magma} is the
+set $S$ with a {\bf closed binary operation}
+$S \circ S \rightarrow S$ such that
+\[\forall a,b \in S \Rightarrow a \circ b \in S\].
+\end{axiom}
+
+\begin{axiom}[Semigroup]
+A {\bf Semigroup} is a
+{\bf Magma} with the operation $\circ$ that is {\bf associative} such that
+\[\forall a,b,c \in S \Rightarrow (a \circ b) \circ c = a \circ (b \circ c)\]
+\end{axiom}
+
+\begin{axiom}[Abelian Semigroup]
+An {\bf Abelian Semigroup} is a {\bf Semigroup} with the operation
+$\circ$ that is {\bf commutative} such that
+\[\forall a,b \in S \Rightarrow a \circ b = b \circ a\]
+\end{axiom}
+
+\begin{axiom}[Monoid]
+A {\bf Monoid} is a
+{\bf Semigroup} with an {\bf identity element} $e \in S$ such that
+\[\forall a \in S \Rightarrow e \circ a = a \circ e = a\]
+\end{axiom}
+
+\begin{axiom}[Group]
+A {\bf Group} is a {\bf Monoid} with an {\bf inverse element} $b \in S$
+and an identity element $i \in S$
+such that
+\[\forall a \in S~\exists b \in S \Rightarrow a \circ b = b \circ a = i\]
+\end{axiom}
+
+\begin{axiom}[Group Unique Identity]
+A {\bf Group} has a {\bf unique identity element} $e \in S$ such that
+\[\exists e \land \forall a,b \in S \land a \ne e \land b \ne e \Rightarrow
+a \circ b \ne e\]
+\end{axiom}
+
+\begin{axiom}[Group Unique Inverse]
+A {\bf Group} has a {\bf unique inverse element} $i \in S$ such that
+\[\exists i \land \forall a,b \in S \land a \ne i \land b \ne i \Rightarrow
+a \circ b \ne i\]
+\end{axiom}
+
+\begin{axiom}[Group Right Quotient]
+A {\bf Group} has a {\bf Right Quotient} (right division) such that
+\[x \circ a = b \Rightarrow x \circ a \circ a^{-1} = b \circ a^{-1}
+\Rightarrow x = b \circ a^{-1}\]
+\end{axiom}
+
+\begin{axiom}[Group Left Quotient]
+A {\bf Group} has a {\bf Left Quotient} (left division) such that
+\[a \circ x = b \Rightarrow a^{-1} \circ a \circ x = a^{-1} \circ b
+\Rightarrow x = a^{-1} \circ b\]
+\end{axiom}
+
+\begin{axiom}[Abelian Group]
+An {\bf Abelian Group} is a {\bf Group} with the operation $\circ$ that is
+{\bf commutative} such that
+\[\forall a,b \in S \Rightarrow a \circ b = b \circ a\]
+\end{axiom}
+
+\begin{axiom}[Abelian Group Quotient]
+An {\bf Abelian Group} has a {\bf Quotient} (division) such that
+\[a^{-1} \circ a \circ x = a \circ a^{-1} \circ x\]
+\end{axiom}
+
+
+
+\begin{axiom}[Euclidean Domain]
+Let $R$ be an integral domain. Let $f$ be a function from
+$R\backslash \{0\}$ to the NonNegativeInteger domain.
+If $a$ and $b$ are in $R$ and $b$ is nonzero, then there are
+$q$ and $r$ in $R$ such that $a=bq+r$ and either $r=0$ or
+$f(r)
readme add Jeremy Avigad to credit list

20170122.01.tpd.patch
books/bookvolbib add Warner The Foundational Crisis of Mathematics

+20170123.01.tpd.patch
+books/bookvol13 More details of the GCD proof

--
1.7.5.4