\documentclass[12pt]{article}
\usepackage{latexsym,color,listings}

\lstset{
  language=Lisp,
  basicstyle=\ttfamily,
  moredelim=[is][\itshape]{&}{&},
  keywordstyle={},
  commentstyle={},
  stringstyle={}}
\author{Juha Arpiainen}
\title{Bourbaki Proof Checker}

\begin{document}

\maketitle
\newpage

\tableofcontents
\newpage

\section{Introduction}

Bourbaki is a program for writing and verifying formal mathematical proofs.
It is inspired mainly by Norman Megill's \emph{Metamath} and the related
programs Ghilbert and Mmj2, but aims on providing
more powerful syntax and tools for automated proof writing.

Nicolas Bourbaki is the pseudonym of a group of mathematicians, who have
written a rigorous multi-volume treatise of Mathematics emphasizing structures.
My long-term goal with Bourbaki is an online hyperlinked, computer-verified
encyclopedia of Mathematics, perhaps in conjunction with the
Hyperreal Dictionary of Mathematics project.

Bourbaki is implemented as an embedded language on top of ANSI Common Lisp.
This means most of Lisp features are available for the user, in particular
it is possible to write Lisp functions that construct proofs (See section 9).

The code of Bourbaki is roughly divided in two levels. The \emph{symbol level}
code implements a simple proof system. The \emph{reference level} code
provides a hierarchical namespace system to organize the information.
The names refer to the principal data types used on the respective levels.
There are also I/O methods for converting between various data formats formats.
%Figure 1 shows the relationship with the components.

Sections 2 to 4 of this document describe the symbol level part of Bourbaki.
The reference level code is described in sections 5 to 7.  More advanced,
programmable features are described in sections 8 and 9. Finally, section
10 deals with the various methods of importing and exporting Bourbaki data
to and from other formats.

\subsection{Quick start}

\begin{lstlisting}
$ tar xvf bourbaki.tar.gz
$ cd bourbaki
 clisp
> (load "init")
> (in-package bourbaki-user)
> (verify !!prop)
> (print-theorem !/prop!id)
\end{lstlisting}

\subsection{Note on definitions}

We refer to the Common Lisp specification for definitions of
terms such as \emph{form} (anything that can be evaluated by Lisp) and
\emph{string}.

New terms will be defined in BNF syntax. For example,
\begin{lstlisting}
&strings& := &string& | ( &string&* )
\end{lstlisting}
defines \emph{strings} to be either a string or a list of strings.

\section{Symbols and Formulae}

Mathematical expressions are treated as trees of symbols in Bourbaki.
Thus the expression $2(a + b)$ is stored internally
as \lstinline[mathescape]!($*_s\ $ ($2_s$) ($+_s\ $ ($a_s$) ($b_s$)))!,
where the $*_s, 2_s, \ldots$ are
Lisp objects corresponding to the multiplication operator, the
number $2$, etc.

One usually calls the function \lstinline!symtree-parse! to create such
expressions. Such calls are abbreviated with the \lstinline![ ]! syntax:
evaluating the form \lstinline![* 2 + a b]! would construct the above expression.
In this document we will sometimes use the \lstinline![ ]! notation to denote the symtree
resulting from such a call, although this is technically incorrect.

Note that we are
using the so-called \emph{Polish prefix notation}, where parentheses can be omitted
if each operator takes a fixed number of arguments (which is usually the case
in Bourbaki).

\subsection{Symbol kinds}

Each expression in Bourbaki has a \emph{syntactic type} or \emph{kind}.
For example, expressions of first order logic are \emph{variables}, \emph{terms} or
\emph{well formed formulae} (\emph{wffs}).

Such types are declared with the macro \lstinline!symkind!, for example,
\lstinline!(symkind "wff")!.

A syntactic type may be declared a subtype of another type by giving the
\lstinline!:super! keyword to \lstinline!symkind!. For example, the
line \lstinline!(symkind "var"  :super term)! says that every variable is a term.

The function \lstinline!(bsubtypep x y)! returns true if \lstinline!x! and
\lstinline!y! are the same type or if \lstinline!x! is a subtype of \lstinline!y!.
An expression $e$ can be substituted for a variable $v$ if
\lstinline!(bsubtypep (&type of e&) (&type of v&))! is true. If this is the case
we say $e$ is of \emph{correct type} for $v$.

\subsection{Primitive symbols}

Primitive symbols are defined with macro \lstinline!prim!:

\begin{lstlisting}
&prim-form& := (prim &symkind& &name& &varspec& &body&)
&name&      := &string&
&varspec&   := ( { &symkind& &strings& }* )
&body&      := &form&*
\end{lstlisting}

For example, the definition

\begin{lstlisting}
(prim wff "=" (term "x" term "y"))
\end{lstlisting}

states that \lstinline![= x y]! is a wff for any two terms
\lstinline!x! and \lstinline!y!. Here \lstinline!x! and \lstinline!y! are the
\emph{variables} of the symbol \lstinline!=!. The number of variables is called
the \emph{arity} of the symbol.

Several variables of the same kind can be declared by putting their names in a list:
\begin{lstlisting}
(prim wff "=" (term ("x" "y")))
\end{lstlisting}
would have worked. Bourbaki defines a
reader macro for `\lstinline$![$' for abbreviating such lists:
\begin{lstlisting}
(prim wff "=" (term ![x y]))
\end{lstlisting}
is equivalent to both of the above definitions.

The names of symbols and their variables are case-sensitive. The symbols are stored
in a namespace separate from Lisp symbols. A reference to the symbol can be obtained
using the `\lstinline$!$' reader macro: \lstinline$!=$ returns a reference to the
equality symbol just defined. Inside brackets the use of '\lstinline$!$' is optional:
\lstinline$[= a b]$ or \lstinline$[!= !a !b]$.

It is possible to redefine a symbol: the new definition replaces the original. Symtrees
may continue to point to the original symbol, however. The old and the new definition
are never the same symbol (in the sense of \lstinline!eq!), even if they have the
same arity and variables of the same types.

\subsection{Symbol trees}

A \emph{symbol tree}, or \emph{symtree} for short, is a list
\lstinline[mathescape]!(&op& $arg_1\ $ $arg_2\ $ $\ldots\ $ $arg_n$)!
such that $op$ is a Bourbaki symbol and
each $arg_i$ is a symtree. $op$ is called the \emph{operator} of the tree and the
$arg_i$ are \emph{arguments}. The leaves of the tree are symbols with no arguments
($n = 0$ is allowed in the definition).

More generally, the $op$ may be any Bourbaki context
(see section 5), in particular a theorem. We also call such lists symtrees.

A \emph{symtree pattern} is defined similarly, but the arguments may also be
integers or Lisp symbols.

The \emph{type} of a symtree \lstinline[mathescape]!(&op& $arg_1\ $ $\ldots\ $ $arg_n$)!
is the symbol kind of $op$.
The tree is \emph{well formed} if the arity of $op$
is $n$ and each $arg_i$ is well formed and of correct type for the corresponding variable of $op$.
In this document the term \emph{wff} is used for any well-formed symtree.

\subsection{Symtree functions}

The well-formedness of a symtree can be tested with the function \lstinline!wffp!.

Two symtrees can be compared with \lstinline!wff-equal!.
\lstinline!(wff-equal x y)! returns true if \lstinline!x! and \lstinline!y! have
isomorphic tree structure and the corresponding symbols are \lstinline!eq!.

\lstinline!wff-type! returns the type of a symtree.

A common operation is to simultaneously substitute all occurrences of a number of symbols
in a symtree with some other symtrees. This operation is performed by \lstinline!replace-vars!,
a function taking the symtree and a list of pairs
\lstinline[mathescape]!($sym_i\ $ . $subst_i$)! called the \emph{substitution map}
or \emph{smap} in the code.

The result of substituting $sym_i$ with $subst_i$ in the symtree $tr$
is denoted by $tr(sym_1/subst_1,\ldots,sym_n/subst_n)$ or
$tr(subst_1,\ldots,subst_n)$ if the $sym_i$ are clear from context.

\lstinline!(print-symtree tree stream)! prints the tree using the bracket
notation. The default value of \lstinline!stream! is
\lstinline!*standard-output*!.

\section{Theorems and Proofs}

\emph{Theorems} and \emph{axioms} in Bourbaki have zero or more \emph{variables},
\emph{hypotheses} and \emph{assertions}. In addition a theorem must have a \emph{proof}.
The variables are Bourbaki symbols of arity zero; the hypotheses and assertions are
wffs, usually containing the variables. In the simple case the proof is a sequence of
theorem references justifying the assertions.

The theorem is treated as a transformation rule: when its hypotheses are satisfied
for some symtrees substituted for its variables, its (correspondingly substituted)
assertions can be used to prove other theorems.

Theorems are defined using the macros \lstinline!th!, \lstinline!hypo!,
\lstinline!ass!, and \lstinline!proof!:

\begin{lstlisting}
&theorem-form&    := (th &name& &varspec& &body&)
&hypothesis-form& := (hypo &symtree&*)
&assertion-form&  := (ass &symtree&*)
&proof-form&      := (proof &proof-line&*)
&proof-line&      := &symtree&
\end{lstlisting}

Axioms are defined like theorems, but using \lstinline!ax! instead of \lstinline!th!:

\begin{lstlisting}
&axiom-form& := (ax &name& &varspec& &body&)
\end{lstlisting}

An example from propositional calculus follows:

\begin{lstlisting}
;; the implication symbol
(prim wff "->" (wff ![x y]))

;; the axioms
(ax "ax1" (wff ![A B])
  (ass [-> A -> B A]))
(ax "ax2" (wff ![A B C])
  (ass [-> -> A -> B C -> -> A B -> A C]))

;; modus ponens
(ax "ax-mp" (wff ![A B])
  (hypo [A] [-> A B])
  (ass [B]))

;; identity law for '->'
;; see below for interpretation of the proof
(th "id" (wff "A")
  (ass [-> A A])
  (proof
    [ax1 A [-> A A]]
    [ax2 A [-> A A] A]
    [ax-mp [-> A -> -> A A A]
           [-> -> A -> A A -> A A]]
    [ax1 A A]
    [ax-mp [-> A -> A A] [-> A A]]))
\end{lstlisting}

As seen from this this example, the \lstinline!hypo! (and \lstinline!ass!)
lines are optional. Multiple hypothesis and assertions lines can be used:
\begin{lstlisting}
(hypo [A])
(hypo [-> A B])
\end{lstlisting}
works as well. In contrast, each \lstinline!proof! replaces the previous one.
Hypothesis and axiom lines can be freely mixed, and the order usually does not
matter (but see section 9). The proof should be after all hypotheses and assertions.
Bourbaki allows a \lstinline!proof! expression for an axiom, although such proof
won't be used anywhere.

Theorems and axioms live in the same namespace with symbols. The rules concerning
redefinition of symbols apply also to theorems. A theorem's variables, hypotheses,
assertions and proof can be printed with \lstinline!print-theorem!.

\subsection{Verifying proofs}

The function \lstinline!verify! checks the correctness of a theorem or axiom $thr$.
The (somewhat simplified) verification algorithm follows:

\begin{enumerate}
\item Check that the hypotheses and assertion of $thr$ are well-formed.
\item If $thr$ is an axiom, we are done. Otherwise
initialize list $L$ with the hypotheses of $thr$.
\item For each proof line \lstinline[mathescape]![&ref& $subst_1\ \ldots\ subst_n$]!,
\begin{itemize}
\item Verify $ref$ if it is not already verified.
\item Check that the number of variables of $ref$ is equal to the number $n$ of
substitutions, and that each $subst_i$ is well-formed and of correct type.
\item For each hypothesis $h$ of $ref$, check that\\
\lstinline[mathescape]!$h$($var_1/subst_1,\ldots,var_n/subst_n$)! is in $L$,\\
where $var_1, \ldots, var_n$ are the variables of $ref$.
\item For each assertion $a$ of $ref$, insert \\
\lstinline[mathescape]!$a$($subst_1,\ldots,subst_n$)! into $L$.
\end{itemize}
\item Check that each assertion of $thr$ is in $L$.
\end{enumerate}

The verifier detects \emph{vicious circles} (theorems referring to themselves or
cycles of theorem references).

\subsection{Distinct variables}

Sometimes the simple substitution rule of Bourbaki causes problems. Consider for
example the theorem $\forall x \exists y (x \ne y)$ of predicate calculus
(which is true assuming there are at least two objects).
Simple substitution of $y$ for $x$ would result in the incorrect formula $y \ne y$.

In the above theorem $x$ and $y$ should be marked \emph{distinct} using the
macro \lstinline!dist!:

\begin{lstlisting}[mathescape]
(th "exists2" (var ![x y])
  (dist (!x !y))
  (ass [$\forall$  x $\exists$  y $\ne$  x y])
  (proof ...))
\end{lstlisting}

When two variables \lstinline!x! and \lstinline!y! are marked distict in a theorem,
substitution of $a$ for \lstinline!x! and $b$ for \lstinline!y! is valid only if
\begin{itemize}
\item no variable occurs in both $a$ and $b$, and
\item each variable occurring in $a$ is marked distinct from each variable in $b$.
\end{itemize}

Lists of more than two variables can be given to \lstinline!dist!. All variables in
the list are made pairwise distinct. The general form of \lstinline!dist! is
\begin{lstlisting}
&distinct-form& := (dist &condition&*)
&condition&     := ( &variable&* )
\end{lstlisting}

The reason distinct variable conditions are necessary is that the variables of
Bourbaki are \emph{metavariables} rather than individual variables of the
object language; see the Metamath book for more information.

\subsection{Local variables}

Sometimes it is necessary to use additional variables in a proof, not occurring in
hypotheses or assertions. Such `dummy' or `local' variables can be defined
with macro \lstinline!loc!, for example \lstinline!(loc var "z")!.

Local variables are treated as distinct from each other and the `normal' variables.

%\subsection{Statistics}

%proof lines, dependence on axioms, definitions used, theorems referencing this

%collect-stats, show-stats

\section{Definitions}

Writing everything in terms of primitive symbols gets tedious quickly. New symbols
can be defined in terms of previous ones with the \lstinline!def! macro.

\begin{lstlisting}
&definition-form& := (def &def-name& &symkind& &sym-name&
                        &sym-vars& &other-vars& &rhs& &body&)
&def-name&        := &string&
&sym-name&        := &string&
&sym-vars&        := &varspec&
&other-vars&      := &varspec&
&rhs&             := &symtree&
\end{lstlisting}

This behaves as if a primitive symbol was defined with
\begin{lstlisting}
(prim &symkind& &sym-name& &sym-vars&)
\end{lstlisting}
together with an axiom
\begin{lstlisting}
(ax &def-name& (&sym-vars& &other-vars&)
  (ass [&eq& &sym-name& &sym-vars& &rhs&])) .
\end{lstlisting}
Here \lstinline!&eq&! is the \emph{equality operator} for the symbol kind
of the defined symbol. For example, the equality operator for wffs is
the biconditional `$\leftrightarrow$'. The equality operator can be set with
\begin{lstlisting}[mathescape]
(setf (symkind-eq-op wff) (mkcontext !$\leftrightarrow$)) .
\end{lstlisting}
Note that in this case the biconditional must be a primitive symbol,\newline
\lstinline[mathescape]/(prim wff "$\leftrightarrow$" (wff ![$\phi\ \psi$]))/,
it cannot be used to define itself.

\subsection{Soundness of definitions}

A definition is \emph{sound} if
\begin{itemize}
\item each formula containing the defined symbol can be proved (using the definition)
to be equivalent to a formula without the symbol, and
\item for each theorem whose hypotheses and assertions do not contain the defined symbol,
there is a proof that does not use the definition.
\end{itemize}
These conditions state that definition does not add anything new to the language:
it is just an abbreviation for a pattern of primitive symbols.

Definitions of the form \lstinline[mathescape]![&eq& &sym& $var_1 \ldots var_n\ $ &rhs&]! are
provably sound if the equality operator is an \emph{equivalence relation} satisfying
the \emph{substitution laws}, that is, the following formulae are theorems:
\begin{itemize}
\item \lstinline![&eq& a a]! (Reflexivity)
\item \lstinline[mathescape]![$\to\ $ &eq&  a b &eq&  b a]! (Symmetry)
\item \lstinline[mathescape]![$\to\ \land\ $ &eq&  a b &eq&  b c &eq&  a c]! (Transitivity)
\item \lstinline[mathescape]![$\to\ $ &eq&  a b &eq'&  &$\phi$(a)&  &$\phi$(b)&]! for any
formula $\phi$. Here \lstinline!&eq'&! is the equality operator for the type of $\phi$;
\lstinline[mathescape]!$\phi$(a)! denotes the formula where \lstinline!a! is properly
substituted for \lstinline!x! in \lstinline[mathescape]!$\phi$(x)!.
\end{itemize}

Ensuring these conditions hold is a responsibility of the user.

\subsection{Bound Variables}

The right-hand-side of a definition may contain primitive symbols, already defined symbols,
variables of the defined symbol, and additional \emph{bound variables}, the
\lstinline!&other-vars&! of the definition. A symbol can be made to bind a variable
by giving an additional \lstinline!:bound! argument in the \lstinline!&varspec&!.
The universal quantifier should properly be specified
\begin{lstlisting}[mathescape]
(prim wff "$\forall$" ((:bound var) "x" wff "$\phi$")) .
\end{lstlisting}
The \lstinline!&other-vars&! of a definition are implicitly marked bound and
distinct from each other and the \lstinline!&sym-vars&!.

All occurrences of a variable \lstinline!x! in a symtree
\lstinline[mathescape]![&op& $subst_1 \ldots subst_n$]! are bound by \lstinline!&op&! if
\lstinline!x! occurs in a substitution $subst_i$ such that the corresponding variable
of \lstinline!&op&! is marked bound.

A definition \lstinline[mathescape]![&eq& &sym& $var_1 \ldots var_n\ $ &rhs&]! is valid
only if all potential occurrences of each variable \lstinline!x! marked bound are bound
in \lstinline!&rhs&!. The validity is verified by the function \lstinline!verify!,
otherwise definitions are treated like axioms by the verifier.

\subsection{Sample Definitions}

\begin{lstlisting}[mathescape]
;; Conjunction
(def "df-and" wff "$\land$" (wff ![$\phi\ \psi$]) ()
  [$\neg\ \to\ \phi\ \neg\ \psi$])

;; Existential quantification
(def "df-ex" wff "$\exists$" ((:bound var) "x" wff "$\phi$")
  [$\neg\ \forall\ x\ \neg\ \phi$])

;; Proper substitution. Theorem "sb7" in set.mm
;; [sb a x $\phi$] is the wff where a is properly
;; substituted for x in $\phi$.
(def "df-subst" wff "sb" (term "a" var "x" wff "$\phi$") (var "y")
  [$\exists\ y\ \land\ =\ y\ a$
     [$\exists\ x\ \land\ =\ x\ y\ \phi$]])
\end{lstlisting}

In the third example, \lstinline!x! cannot be marked bound: if the term substituted for
\lstinline!a! contains free occurrences of the variable substituted for \lstinline!x!,
those occurrences are free in the \lstinline!rhs!. This explains the term
\emph{potential occurrences} used above. If \lstinline!x! were distinct from \lstinline!a!,
the definition would be valid.

\section{The Context System}

For larger projects it gets inconvenient to have all theorems and symbols in the same namespace.
Bourbaki provides a hierarchy of namespaces, called \emph{contexts}, to place related symbols and
theorems in. At the top of the hierarchy there is a \emph{root context}, the value of
\lstinline!*root-context*!. Changing the value of \lstinline!*root-context*! allows several
(possibly unrelated) systems to be loaded at the same time. It is also possible to have
contexts outside any hierarchy.

Contexts are defined with macros \lstinline!module! and \lstinline!context!. \lstinline!module!
creates a \emph{top-level context}, that is, a context directly below the root of the hierarchy;
\lstinline!context! is used to create nested subcontexts.

A sample hierarchy follows. This will be referred to in following examples.
%For example, the following code creates the hierarchy of Figure NN.

\begin{lstlisting}[mathescape]
(module "logic"
  (context "propositional"
    (prim wff "$\to$" (wff ![$\phi\ \psi$])))
  (context "predicate")
    (prim wff "$\forall$" (var "x" wff "$\phi$")))
(module "set-theory"
  (context "zfc"
    (context "axioms"
      (ax "union" ...)
      (ax "choice" ...))))
\end{lstlisting}

At any time one of the contexts, the value of \lstinline!*current-context*!, is selected.
New symbols and theorems are inserted into \lstinline!*current-context*! by default.
Macros such as \lstinline!context! and \lstinline!module! bind \lstinline!*current-context*!
to the context being defined. The macro \lstinline!in-context! explicitly binds
\lstinline!*current-context*!.

Symbols and theorems are retrieved from the context hierarchy with the function
\lstinline!seek-sym!, usually abbreviated with the reader macro \lstinline$!$.
The following example illustrates the use of \lstinline!in-context! and
\lstinline!seek-sym!.

\begin{lstlisting}[mathescape]
;; !/ specifies an absolute reference,
;; with respect to *root-context*
;; Same as (print-theorem
;;           (seek-sym :abs "set-theory" "zfc"
;;                          "axioms" "choice"))
(print-theorem !/set-theory!zfc!axioms!choice)

(in-context !/set-theory!zfc
  ;; Single ! specifies a reference
  ;; relative to *current-context*
  ;; Same as (print-theorem (seek-sym :rel "axioms" "union"))
  (print-theorem !axioms!union)

  (in-context !axioms
    ;; Add an axiom
    (ax "pairing" ...))

  (th "foo" (wff "$\phi$")
    ;; ! can be used within []
    (ass [!/logic!propositional!$\to\ \phi\ \phi$])))
\end{lstlisting}

Symbols and theorems are actually contexts is Bourbaki, and may contain subcontexts.
For example, the variables of a theorem $th$ are symbols that are subcontexts of $th$.
The words \emph{symbol} and \emph{context} are used somewhat interchangeably in
this document.

\subsection{Meta information}

Each context contains a table of meta information indexed by Lisp symbols.
Some fields are to be filled by the user, others by Bourbaki or other programs.
Meta information can be accessed with \lstinline!(gethash &key& (context-meta &context&))!
The macro \lstinline!meta! sets meta fields of the current context:

\begin{lstlisting}
&meta-form& := (meta (&key& . &content&)*)
&key& := &symbol&
&content& := &form&
\end{lstlisting}

The following fields are used by the current version of Bourbaki. They are all symbols in the
\lstinline!keyword! package.

:assume,
:bound,
:comment,
:def,
:defs-used,
:depends-on,
:description,
:full-name,
:html-fn,
:html-proof-fn,
:html-sym,
:index,
:original,
:parent,
:proof-length,
:used-by

\subsection{Nested variables and hypotheses}

In mathematical theories it is common to have theorems with common variables and hypotheses.
For example, theorems in the theory of topological spaces would all have a variable
\lstinline!X! and a hypothesis \lstinline![topo-space X]!. Such common variables and
hypotheses can be moved to the parent context:

\begin{lstlisting}
(module "topology"
  (def wff "topo-space" (set "X") ...)
  
  (theory "topo" (set "X")
    (hypo [topo-space X])

    ;; closure of A in the topology of X
    (def set "closure" (set "A") ...)

    (th "some-theorem" (set "Y") ...)))
\end{lstlisting}

The macro \lstinline!theory! is just a version of \lstinline!context! that
allows specification of variables.
When used from outside \lstinline!topo! this behaves as the following:

\begin{lstlisting}
(in-context !/topology
  (context "topo"
    (def set "closure" (set "X" set "A") ...)
    (th "some-theorem" (set "X" set "Y")
      (hypo [topo-space X])
      ...)))
\end{lstlisting}

Within \lstinline!topo! the space \lstinline!X! is used by default:

\begin{lstlisting}[mathescape]
(in-context !/topology!topo
  (print-symtree [closure $\emptyset$]))
$\Rightarrow$[closure X $\emptyset$]
\end{lstlisting}

This is a case of \emph{importing} symbols, as defined in the next section.
When variables from multiple contexts are nested, the variables of the
innermost context are on the \emph{rightmost}.

\subsection{Context functions}

New contexts are created with function \lstinline!create-context!:
\begin{lstlisting}
(create-context :name &string& :parent &context&
                :type &symkind& :class &symbol&)
\end{lstlisting}

\lstinline!parent! defaults to \lstinline!*current-context*!,
a \lstinline!nil! parent creates a context outside the hierarchy.
\lstinline!class! should be one of the following symbols:

:axiom,
:definition,
:theorem,
:prim,
:sym,
:arg,
:loc,
:context,
:module

\lstinline!create-context! does not yet insert the new context
to parent's symbol table, see \lstinline!insert-sym! in the
next section.

\lstinline!mkrootcontext! creates a context without a parent, suitable
value for \lstinline!*root-context*!. \lstinline!flush! sets
\lstinline!*root-context*! to a new root context, usually sending the previous
hierarchy to the garbage collector.

%defcontext, copy-th

All symbols and theorems in Bourbaki are structures of type \lstinline!context!:

\begin{lstlisting}
(defstruct context
  name
  type
  class
  (meta (make-hash-table 'eq))
  
  vars
  hypo
  assert
  distinct
  proof
  
  (syms (make-hash-table 'equal))
  imports
  exports)
\end{lstlisting}

The \lstinline!syms!, \lstinline!imports! and \lstinline!exports! are
describend in the next section.

There is some redundancy. The \lstinline!proof!, for example, does not
make sense for a primitive symbol. Future versions of Bourbaki might
take a more object-orinted approach.

\section{Symbol References}

A \emph{symbol reference} or \emph{symref} is a function taking symtrees
as arguments and returning a symtree. They are used to represent argument
transformations. For example, the call
\lstinline$(in-context !/topology!topo !closure)$ returns a function taking
one argument. When applied to \lstinline!A! the function returns
\lstinline![closure X A]!.

\subsection{Terminology}

The symbol references are structures of type \lstinline!symref!:

\begin{lstlisting}
(defstruct symref
  target
  args-needed
  fn)
\end{lstlisting}

\lstinline!target! is the referred context, or \lstinline!nil! if the symref
doesn't refer to a specific context.
\lstinline!args-needed! is an integer $n$ describing the function \lstinline!fn!.

If $n \ge 0$, \lstinline!fn! is a function taking a \emph{fixed number} $m \ge n$
of arguments. The symref is \emph{exact} if $m = n$.

If $n < 0$, \lstinline!fn! is a function taking a \emph{variable number} of
arguments, at least $|n| - 1$. In the rest of this section we assume that $n \ge 0$,
symrefs with variable number of arguments are treated in section <Metasyms>.

A symref is \emph{composable} if \lstinline!args-needed! $\ge 0$ and the \lstinline!target!
is not \lstinline!nil!. The function \lstinline!(mkcontext x)! returns
\lstinline!x! itself if it is a context, and the target of \lstinline!x! if \lstinline!x!
is a composable symref. Many of the Bourbaki functions taking context arguments
also accept composable symrefs, calling \lstinline!mkcontext!.
\lstinline!verify! and \lstinline!print-theorem! are examples of these.

\subsection{Composing References}

The fundamental operation of symrefs is composition. Given an exact, composable
symref \lstinline!f! of $n$ arguments and a symref \lstinline!g! of $m$ arguments,
\lstinline!(compose-ref f g)! is an exact symref of $n + m$ arguments. It is
composable if and only if \lstinline!g! is.

When the function of \lstinline!(compose-ref f g)! is called with arguments\newline
$a_1, a_2, \ldots, a_n, b_1, b_2, \ldots, b_m$, the first $n$ arguments
are given to \lstinline!f!. \lstinline!f! should return a list
$c_1, c_2, \ldots, c_k$ of symtrees, where $m + k$ is the actual number of
arguments $g$ expects. The result of calling \lstinline!(compose-ref f g)!
is then the result of calling \lstinline!g! with $c_1, \ldots, c_k, b_1, \ldots, b_m$.
%This is illustrated in Figure <Fig>.

Corresponding to a theorem
\begin{lstlisting}
(th "example" (type1 "var1" ... typeN "varN")
    ...)
\end{lstlisting}
the \lstinline!syms! hashtable of the parent context contains a symref with
\lstinline!args-needed = N! under the key \lstinline!"example"!. The symref
function just passes on its arguments without modification. The same applies
also to contexts of other type.

A reference \lstinline$!/foo!bar!example$ composes these references while going
down the context hierarchy, resulting in a symref with \lstinline!example!'s
arity.

Actually the order of arguments is opposite to the one described here:
\lstinline!f! takes the \emph{last} $n$ arguments of \lstinline!(compose-ref f g)!.
This makes the code simpler and more efficient.

\subsection{The Parser}

The function \lstinline!symtree-parse! takes arguments of various types and
attempts to construct a symtree from them. If the first argument to
\lstinline!symtree-parse! is a list, it is assumed to be an already parsed
symtree and returned as is. If the first argument is an integer or a
Lisp symbol, a one-element list containing it is returned. This allows
\lstinline!symtree-parse! to be used to create symtree patterns.
Otherwise the first argument must be a symref or a context.

If the first argument $op$ is a context with $n$ variables,
\lstinline!symtree-parse! is called recursively to parse $n$
subexpressions. The symtree \lstinline[mathescape]![&op& $sub_1,\ldots,sub_n$]!
is then returned.

If $op$ is a symref with \lstinline!args-needed! $= n \ge 0$,
the function of $op$ is applied to the next $n$ subepressions
in \emph{reversed order} (see the note at the end of 6.2).
$op$ must therefore be an exact symref.

If $n < 0$, subepressions are parsed until all the arguments
are used up. $op$ is then applied to the subexpressions in
reversed order.

Interpretation of the function call depends on the \lstinline!target!
of $op$. If \lstinline!target! is \lstinline!nil!, the result is
assumed to be a valid symtree and is returned as is. Otherwise
the result is assumed to be a list of arguments to \lstinline!target!
in reversed order, and the symtree \lstinline!(&target&  . (reverse &result&))!
is returned.

The reader macro for `\lstinline![!' is an abbreviation for \lstinline!symtree-parse!.
Whitespace-separated tokens are read until a `\lstinline!]!' is seen.
Tokens beginning with one of the characters `\lstinline![!', `\lstinline$!$',
`\lstinline!"!', `\lstinline!(!', or `\lstinline!,!' receive a special treatment.
Otherwise the token is a string naming a symbol in \lstinline!*current-context*!.
Thus \lstinline![+ x y]! is an abbreviation for
\begin{lstlisting}
(symtree-parse (seek-sym :rel "+")
               (seek-sym :rel "x")
               (seek-sym :rel "y"))
\end{lstlisting}

The special characters are treated as follows:

\begin{itemize}
\item \lstinline![! begins a nested symtree. This is necessary when dealing with
symrefs taking variable number of arguments. It may be used to parenthesize the
expression for clarity.
\item \lstinline$!$ begins a call to \lstinline!seek-sym! read with the usual syntax of
\lstinline$!$.
\item \lstinline!"! begins a string read with the Lisp reader and given to
\lstinline!seek-sym!. It may be used to escape the special characters in a symbol's name,
for example, \lstinline![+ "[foo bar]"  3]!.
\item When a `\lstinline!,!' is encountered, the Lisp reader is used to read a form. The form
is then evaluated and given to \lstinline!symtree-parse!. This works like with backquote.
Example:
\begin{lstlisting}
(let ((x [+ a b]) (y [- a b]))
  [* ,x ,y])
\end{lstlisting}
produces the same symtree as \lstinline![* + a b - a b]!. \lstinline![-> ,1 ,2]! constructs
a symtree pattern.
\item \lstinline[mathescape]!($\ldots$! is simply an abbreviation for
\lstinline[mathescape]!,($\ldots$!.
\end{itemize}

\subsection{Importing and Exporting}

It gets tedious to write references such as
\lstinline[mathescape]|!/logic!propositional!$\to$| or
\lstinline|!/topology!topo!closure| all the time. Bourbaki allows the relevant contexts to be
\emph{imported}:

\begin{lstlisting}[mathescape]
(module "test"
  (import !/logic!propositional)
  (import !/topology!topo)

  (print-symtree [$\to$ x y])
  (print-symtree [closure A B]))

;; error: the import is only visible within "test"
(print-symtree [closure A B])
\end{lstlisting}

More generally, default values can be given to some of the variables of
the imported context by using \lstinline!import! with a symtree pattern:

\begin{lstlisting}[mathescape]
(theory "continous" (set ![X Y])
  ;; f: X -> Y is continuous
  (def "df-cont" wff "cont" (set "f") ...))

(context "calculus"
  ;; Specialize to continuous real-valued functions
  (import [!/continuous ,0 IR])

  (print-symtree [cont A f]))
$\Rightarrow$[cont A IR f]
\end{lstlisting}

Import only allows references to be abbreviated within a context.
To provide an everywhere accessible version of df.cont that defaults to IR
one must use \lstinline!export!:

\begin{lstlisting}[mathescape]
(context "test1"
  (export [!/continuous R R]))
(context "test2"
  (import [!/continuous R R]))

(print-symtree [!test1!cont f])
$\Rightarrow$[cont R R f]

(print-symtree [!test2!cont f])
$\Rightarrow$Error: symbol "cont" not found
\end{lstlisting}

The Bourbaki import and export are analoguous to the Lisp functions
with the same names; both deal with visibility of symbols.
There are differences, however: Bourbaki import and export deal with
whole contexts instead of individual symbols. The symbols and theorems
defined in a context are also exported by default.
The require and provide described in section 7 are something
closer to Ghilbert's import/export.

\subsection{Seeking symbols}

%function \lstinline!seek-sym!

%order of imports/exports

%reader macro `\lstinline$!$'

\subsection{Aliases}

Sometimes it is necessary to export only a few symbols instead of the whole
context. In such cases one can use \lstinline!alias! macro.

\lstinline!pattern! constructs such a symref without inserting it to current-context

\section{Modules and Files}

It is common to have theorems of similar form, but different symbols in
their assertions. For example, the inclusion relation $a \subseteq b$ and
the less-than-or-equal relation $\langle x,y\rangle \in \le$ of real numbers
are both partial orders (here the relation $\le$ is interpreted as a
set of ordered pairs of real numbers as usual).

Bourbaki allows writing ``templates'' for such theorems and re-using them in
different contexts. In the above situation we could write

\begin{lstlisting}[mathescape]
;;; File order-ax.lisp
;;; Axioms for partial orders

(module "order-ax"
  (import [!!logic-ax])
  (symkind "obj")
  (prim wff "$\le$" (obj ![a b]))

  ;; Define the associated strict order
  (def "df-less" wff "<" (obj ![a b])
    [$\land \le a b \not = a b$])

  ;; Antisymmetric law
  (ax "antisym" (obj ![a b])
    (ass [$\to \land \le a b \le b a = a b$]))

  ;; Transitive law
  (ax "tr" (obj ![a b c])
    (ass [$\to \land \le a b \le b c \le a c$])))

;;; File order.lisp
;;; Theorems for partial orders

(module "order"
  (import [!!logic])
  (import [!!order-ax])

  ;; Strict order is transitive
  (ax "less-tr" (obj ![a b c])
    (ass [$\to \land < a b < b c < a c$])
    (proof ...))
  ...)

set.lisp
calculus.lisp
\end{lstlisting}

Here the line \lstinline$(import [!!order-ax])$ tells Bourbaki to import the symbols from
the top-level context \lstinline!order-ax!, loading the file \lstinline!order-ax.lisp! if the context
was not found. The line \lstinline$(provide ... (export [!!order]))$ binds the name \lstinline!order-ax!
and the symbol kind \lstinline!obj! to \lstinline!provide-order-ax! and \lstinline!set!, respectively.
The file \lstinline!order.lisp! is
then loaded with these bindings and the resulting context is exported.

The end result is that \lstinline$!/set!less-tr$ is a theorem with assertion\newline
\lstinline[mathescape]![$\to\ \land\ \subset\ a\ b\ \subset\ b\ c\ \subset\ a\ c$]!
and \lstinline$!/calculus!less-tr$ one with\newline
\lstinline[mathescape]![$\to\ \land\ <\ a\ b\ <\ b\ c\ <\ a\ c$]!.

\subsection{Require and Provide}

\subsection{Guidelines for Re-usable Theories}

\section{Structured Proofs}

\subsection{Seeking}
\subsection{RPN}

\section{Metasymbols}

\section{Input and Output}

\end{document}