From 8011eac0c0cbf70a61d7dcf2ad55ede1f01a026c Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Thu, 24 Mar 2016 10:29:11 0400
Subject: [PATCH] books/bookvol13 Quote example Euclid proof using TLA+
Goal: Proving Axiom Correct

books/bookvol13.pamphlet  293 ++++++++++++++++++++++++++++++++++++++
changelog  2 +
patch  12 +
src/axiomwebsite/patches.html  2 +
4 files changed, 290 insertions(+), 19 deletions()
diff git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index a110c03..29aaa64 100644
 a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ 73,7 +73,7 @@ adaptability.}
\end{quote}
\begin{quote}
...constructive mathematics provides a way of viewing the language of
+{\bf ...constructive mathematics provides a way of viewing the language of
logical propositions as a {\sl specification} language for
programs. An ongoing thrust of work in computer science has been to
develop program specification languages and formalisms for
@@ 90,7 +90,7 @@ isomorphic to a type expression, and the proof of a proposition would
suggest precisely how to construct an inhabitant of the type, which
would be a term in a functional programming language. The term that
inhabits the type corresponding to a proposition is often referred to as
the {\sl computational content} of the proposition.
+the {\sl computational content} of the proposition.}
 Paul Bernard Jackson\cite{Jack95}
@@ 432,6 +432,12 @@ let rec gcd a b = if b = 0 then a else gcd b (a mod b)
val gcd : int > int > int =
\end{verbatim}
+\chapter{Temporal Logic of Actions (TLA) \cite{TLA16}}
+\begin{quote}
+{\bf Sloppiness is easier than precision and rigor}
+ Leslie Lamport\cite{Lamp14a}
+\end{quote}
+
Leslie Lamport\cite{Lamp14} on $21^{st}$ Century Proofs.
A method of writing proofs is described that makes it harder to prove
@@ 443,12 +449,283 @@ Lamport points out that proofs need rigor and precision.
Structure and Naming are important. Every step of the proof
names the facts it uses.
Temporal Logic of Actions (TLA)
\begin{quote}
{\bf Sloppiness is easier than precision and rigor}
 Leslie Lamport\cite{Lamp14a}
\end{quote}
+Quoting from \cite{TLA16}:
+
+Broadly speaking, a TLA+ proof is a collection of {\sl claims},
+arranged in a hierarchical structure which we describe below, where
+each claim has an {\sl assertion} tht is either {\sl unjustified} or
+justified by a collection of {\sl cited facts}. The purpose of TLAPS
+is to check the userprovided proofs of theorems, that is, to check
+that the hierarchy of claims indeed establishes the truth of the theorem
+if the claims were true, and then to check that the assertion of every
+justified claim indeed is implied {\sl by} its cited facts. If a TLA+
+theorem has a proof with no unjustified claims, then, as a result of
+checking the proof, TLAPS verifies the truth of the theorem.
+
+\section{The algorithm}
+
+The wellknown Euclidean algorithm can be written in the PlusCal
+language as follows:
+\begin{verbatim}
+algorithm Euclid {
+ variables x \in 1..M, y \in 1..N, x0 = x, y0 = y;
+ {
+ while (x # y) {
+ if (x < y) { y := y  x; }
+ else { x := xy; }
+ };
+ assert x = GCD(x0, y0) /\ y = GCD(x0, y0)
+ }
+\end{verbatim}
+
+The PlusCal translator translates this algorithm into a TLA+ specification
+that we could prove correct. However, in this tutorial, we shall write a
+somewhat simpler specification of Euclid's algorithm directly in TLA+.
+
+\subsection{Creating a new TLA+ module}
+
+In order to get the definitions of arithmetic operators ($+$, $$, etc.),
+we shall make this specification {\sl extend} the {\tt Integers}
+standard module.
+
+\begin{verbatim}
+ Module Euclid 
+EXTENDS Integers
+\end{verbatim}
+
+\subsection{Definitions}
+
+We shall then define the GCD of two integers. For that purpose, let us
+define the predicate ``p divides q'' as follows: p divides q iff there
+exists some integer d in the interval 1..q such that q is equal to p
+times d.
+
+\begin{verbatim}
+p  q == \E d \in 1..q : q = p * d
+\end{verbatim}
+
+We then define the set of divisors of an integer q as the sets of integers
+which both belong to the interval 1..q and divide q:
+\begin{verbatim}
+Divisors(q) == {d \in 1..q : d  q}
+\end{verbatim}
+
+We define the maximum of a set S as one of the elements of this set which
+is greater than or equal to all the other elements:
+\begin{verbatim}
+Maximum(S) == CHOOSE x \in S : \A y \in S : x >= y
+\end{verbatim}
+
+And finally, we define the GCD of two integers p and q to be the maximum
+of the intersection of Divisors(p) and Divisors(a):
+\begin{verbatim}
+GCD(p,q) == Maximum(Divisors(p) \cap Divisors(q))
+\end{verbatim}
+
+For convenience, we shall also define the set of all positive integers as:
+\begin{verbatim}
+Number = Nat \ {0}
+\end{verbatim}
+
+\subsection{Constants and variables}
+We then define the two constants and two variables needed to describe
+the Euclidean algorithm, where M and N are the values whose GCD is to
+be computed:
+\begin{verbatim}
+CONSTANTS M, N
+VARIABLES x, y
+\end{verbatim}
+
+\subsection{The specification}
+We define the initial state of the Euclidean algorithm as follows:
+\begin{verbatim}
+Init == (x = M) /\ (y = N)
+\end{verbatim}
+
+In the Euclidean algorithm, two actions can be performed:
+\begin{itemize}
+\item set the value of y to y  x if x $<$ y
+\item set the value of x to x  y if x $>$ y
+\end{itemize}
+
+These actions are again written as a definition of {\tt Next}, which
+specifies the nextstate relation. In TLA+, a primed variable refers
+to its value at the next state of the algorithm.
+\begin{verbatim}
+Next == \/ /\ x < y
+ /\ y' = y  x
+ /\ x' = x
+ \/ /\ y < x
+ /\ x' = xy
+ /\ y' = y
+\end{verbatim}
+
+The specification of the algorithm asserts that the variables have the
+correct initial values and, in each execution step, either a {\tt Next}
+action is performed or x and y keep the same values:
+\begin{verbatim}
+Spec == Init /\ [][Next]_<>
+\end{verbatim}
+
+(For reasons that are irrelevant to this algorithm, TLA specifications
+always allow {\sl stuttering steps} that leave all the variables
+unchanged.)
+We want to prove that the algorithm always satisfies the following
+property:
+\begin{verbatim}
+ResultCorrect == (x = y) => x = GCD(M, N)
+\end{verbatim}
+
+Hence we want to prove the following theorem named Correctness:
+\begin{verbatim}
+THEOREM Correctness == Spec => []ResultCorrect
+\end{verbatim}
+
+\subsection{Summary}
+
+\begin{verbatim}
+ Module Euclid 
+EXTENDS Integers
+
+p  q == \E d \in 1..q : q = p * d
+Divisors(q) == {d \in 1..q : d  q}
+Maximum(S) == CHOOSE x \in S : \A y \in S : x >= y
+GCD(p,q) == Maximum(Divisors(p) \cap Divisors(q))
+Number == Nat \ {0}
+
+CONSTANTS M, N
+VARIABLES x, y
+
+Init == (x = M) /\ (y = N)
+
+Next == \/ /\ x < y
+ /\ y' = y  x
+ /\ x' = x
+ \/ /\ y < x
+ /\ x' = xy
+ /\ y' = y
+
+Spec == Init /\ [][Next]_<>
+
+ResultCorrect == (x = y) => x = GCD(M,N)
+
+THEOREM Correctness == Spec => []ResultCorrect
+\end{verbatim}
+
+\section{A simple proof}
+\subsection{The invariant}
+
+Intuitively, the theorem Correctness holds because the implementation
+guarantees the following {\sl invariant}
+\begin{verbatim}
+InductiveInvariant == /\ x \in Number
+ /\ y \in Number
+ /\ GCD(x, y) = GCD(M, N)
+\end{verbatim}
+
+That is, {\tt InductiveInvariant} holds for the initial state (i.e.,
+the state specified by {\tt Init}) and is preserved by the
+nextstate relation {\tt [Next]\_}$<>$
+
+\subsection{Checking proofs}
+
+First we need to assume that constants M and N are not equal to zero
+\begin{verbatim}
+ASSUME NumberAssumption == M \in Number /\ N \in Number
+\end{verbatim}
+
+Let us then prove that {\tt InductiveInvariant} holds for the initial state.
+\begin{verbatim}
+THEOREM InitProperty == Init => InductiveInvariant
+\end{verbatim}
+
+To check whether TLAPS can prove that theorem by itself, we declare
+its proof obvious.
+\begin{verbatim}
+THEOREM InitProperty == Init => InductiveInvariant
+ OBVIOUS
+\end{verbatim}
+
+We now ask TLAPS to prove that theorem. But TLAPS does not know how to
+prove the proof obligation corresponding to that proof. It prints
+that obligation and reports failures to three backends, Zenon, Isabelle,
+and SMT. The default behavior of TLAPS is to send obligations first to
+an SMT solver (by default CVC3), then if that fails to the automatic
+prover Zenon, then if Zenon fails to Isabelle (with the tactic ``auto'').
+
+\subsection{Using facts and definitions}
+The obligation cannot be proved because TLAPS treats the symbols
+{\tt Init} and {\tt InductiveInvariant} as opaque identifiers unless
+it is explicitly instructed to expand their definitions using the
+directive {\tt DEF}. The main purpose of this treantment of definitions
+is to make proofchecking tractable, because expanding definitions can
+arbitrarily increase the size of expressions. Explicit use of definitions
+is also a good hint to the (human) reader to look only at the listed
+definitions to understand a proof step. In tha precise case, we can ask
+TLAPS to expand definitions of {\tt Init} and {\tt InductiveInvariant},
+by replacing the proof {\tt OBVIOUS} by the proof\\
+{\tt BY DEF Init, InductiveInvariant}. In the obligations sent to the
+backends, the definitions of {\tt Init} and {\tt InductiveInvariant}
+have been expanded.
+
+Unfortunately, none of the backends could prove that obligation. As with
+{\tt definitions}, we have to specify which facts are {\sl usable}. In this
+case, we have to make the fact {\tt NumberAssumption} usable by changing
+the proof to
+\begin{verbatim}
+THEOREM InitProperty == Init => InductiveInvariant
+ BY NumberAssumption DEF Init, InductiveInvariant
+\end{verbatim}
+
+The general form of a {\tt BY} proof is:
+\[ {\tt BY\ } e_1,\ldots,e_m {\tt \ DEF\ } d_1,\ldots,d_n\]
+which claims that the assertion follows by assuming $e_1,\ldots,e_m$
+and expanding the definitions $d_1,\ldots,d_n$. It is the job of TLAPS
+to then check this claim, and also to check that the cited facts
+$e_1,\ldots,e_m$ are indeed true.
+
+Finally, SMT succeeds in proving that obligation.
+\begin{verbatim}
+ Module Euclid 
+EXTENDS Integers
+
+p  q == \E d \in 1..q : q = p * d
+Divisors(q) == {d \in 1..q : d  q}
+Maximum(S) == CHOOSE x \in S : \A y \in S : x >= y
+GCD(p,q) == Maximum(Divisors(p) \cap Divisors(q))
+Number == Nat \ {0}
+
+CONSTANTS M, N
+VARIABLES x, y
+
+Init == (x = M) /\ (y = N)
+
+Next == \/ /\ x < y
+ /\ y' = y  x
+ /\ x' = x
+ \/ /\ y < x
+ /\ x' = xy
+ /\ y' = y
+
+Spec == Init /\ [][Next]_<>
+
+ResultCorrect == (x = y) => x = GCD(M,N)
+
+InductiveInvariant == /\ x \in Number
+ /\ y \in Number
+ /\ GCD(x, y) = GCD(M, N)
+
+ASSUME NumberAssumption == M \in Number /\ N \in Number
+
+THEOREM InitProperty == Init => InductiveInvariant
+ BY NumberAssumption DEF Init, InductiveInvariant
+
+THEOREM Correctness == Spec => []ResultCorrect
+\end{verbatim}
+
+
+\chapter{Other Ideas to Explore}
Computerising Mathematical Text\cite{Kama15} explores various ways of
capturing mathematical reasoning.
@@ 464,8 +741,6 @@ Pierce\cite{Pier15} has a Software Foundations course in COQ with
downloaded files in Pier15.tgz.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Bibliography}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\bibliographystyle{axiom}
\bibliography{axiom}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff git a/changelog b/changelog
index 3059404..51c7f16 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20160324 tpd src/axiomwebsite/patches.html 20160324.02.tpd.patch
+20160324 tpd books/bookvol13 Quote example Euclid proof using TLA+
20160324 tpd src/axiomwebsite/patches.html 20160324.01.tpd.patch
20160324 tpd books/bookvolbib Add TLA16, Euclid Algorithm Proof in TLA+
20160320 tpd src/axiomwebsite/patches.html 20160320.04.tpd.patch
diff git a/patch b/patch
index 1e14b2b..02acdbe 100644
 a/patch
+++ b/patch
@@ 1,11 +1,3 @@
books/bookvolbib Add TLA16, Euclid Algorithm Proof in TLA+
+books/bookvol13 Quote example Euclid proof using TLA+
Goal: Axiom Algebra

@misc{TLA16,
 author = "Lamport, Leslie",
 title = "TLA+ Proof System",
 year = "2016",
 url = "https://tla.msrinria.inria.fr/tlaps/content/Documentation/Tutorial/The_example.html",
 abstract = "Demonstration of Euclid Algorithm Proof in TLA+"
}
+Goal: Proving Axiom Correct
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 47bc446..46afe62 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5246,6 +5246,8 @@ books/bookvolbib Add Fern92 Accurate Singular Values
books/bookvolbib Add Brow01, the McCallum CAD projection
20160324.01.tpd.patch
books/bookvolbib Add TLA16, Euclid Algorithm Proof in TLA+
+20160324.02.tpd.patch
+books/bookvol13 Quote example Euclid proof using TLA+

1.7.5.4