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

\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}\footnote{http://www.metamath.org}
and the related programs Ghilbert\footnote{http://ghilbert.org} by Raph Levien and
Mmj2\footnote{http://planetx.cc.vt.edu/AsteroidMeta/mmj2} by Mel O'Cat, 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 the concept
of mathematical structures.\cite{bsets}
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.\footnote{http://planetx.cc.vt.edu/AsteroidMeta/HDM}

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

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 mathematical content.
These terms 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 \ref{s_syms} to \ref{s_def} of this document describe the symbol level part of Bourbaki.
The reference level code is described in sections \ref{s_ctx} to \ref{s_module}.  More advanced,
programmable features are described in sections \ref{s_proof} and \ref{s_meta}.% Finally, section
%\ref{s_io} deals with the various methods of importing and exporting Bourbaki data
%to and from other formats.

\subsection{Quick start}

\begin{lstlisting}
Extract the archive:
$ tar xzvf bourbaki.tar.gz
$ cd bourbaki

Start Lisp:
$ clisp

Load Bourbaki:
> (load "init")
> (in-package bourbaki-user)

Load and verify the propositional calculus module:
> (verify !!prop)
\end{lstlisting}

\subsection{Note on definitions}

We refer to the Common Lisp specification\cite{hyperspec} 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}
\label{s_syms}

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. Calls to \lstinline!symtree-parse! are abbreviated with the \lstinline![ ]! syntax:
evaluating the form \lstinline![* 2 + a b]! would construct the above tree, assuming
that the symbols have been properly declared before.
In this document we will sometimes use the \lstinline![ ]! notation to denote the resulting
symtree, 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}). Usually one type (the wff) is special
in that all \emph{propositions} of the system have this type. The definition
feature (section \ref{s_def}) implicitly assumes a wff type, otherwise the wff type
is not treated specially.

Syntactic types are declared with the macro \lstinline!symkind!, for example,
\begin{lstlisting}
(symkind "WFF")
\end{lstlisting}

A syntactic type may be declared a subtype of another type by giving the
\lstinline!:super! keyword to \lstinline!symkind!. For example, the line
\begin{lstlisting}
(symkind "VAR" :super term)
\end{lstlisting}
says that any variable is also a term. Note that the symkind names should
be in upper case due to the way Lisp treats symbol names.

The function \lstinline!(subkindp 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!(subkindp (^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 declared with macro \lstinline!prim!:

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

For example, the declaration
\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 as well. Bourbaki defines a
reader macro `\lstinline$![$' for abbreviating lists of strings:
\begin{lstlisting}
(prim wff "=" (term ![x y]))
\end{lstlisting}
is equivalent to both of the above declarations.

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 declaration replaces the original. References
to the old symbol are not updated automatically, however. The old and the new symbol
are never the same in the sense of \lstinline!eq! even if they have the
same arity and variables of the same types. This feature should be used only while `debugging'
proofs interactively. Identically named symbols would typically cause exportion to other proof systems
to fail.

\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).

\emph{Patterns} of symtrees are represented with symtree-like objects that have integers
or Lisp symbols in place of some of the subtrees, standing for unspecified symtrees. Note
that a lone integer or symbol is not a valid symtree pattern.

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.

Later on we will use "generalized" symtrees that have theorems or other Bourbaki objects
as operators (in place of Bourbaki symbols). Most of this section is valid for
the generalized symtrees also, and we will call them simply symtrees. The type
of a generalized symtree is \lstinline!nil! if the operator is not a Bourbaki symbol.

\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}
\label{s_thr}

\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 (see section \ref{s_proof} for the general case).

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}

Listing \ref{lst_prop} contains an example from propositional calculus.

\begin{lstlisting}[caption={Beginnings of propositional calculus},label=lst_prop]
;; File example1.lisp
(symkind "WFF")

;; 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
;; compare with id1 in set.mm
(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 for \lstinline!ax-mp!. 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 RPN proofs (section 9?)
The proof should be after the hypotheses and assertions.
Bourbaki allows a \lstinline!proof! expression for an axiom, although the 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}
\label{ss_verify0}

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

% TODO: update to structured proof format
\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 $z$ for both $x$ and $y$ would result in the incorrect formula
$\exists z (z \ne z)$.

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,
the 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}
(in case $a$ and $b$ are more complex expressions the name \emph{disjoint} variable
condition might be more appropriate).

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}

Distinct variable conditions are logically simpler than the concept of
a term being `free for' a variable in a wff.\cite{mendelson}
See the Metamath site \cite{mm-dist} for details and for an axiomatization
of predicate logic using distinct variable conditions.

%The reason distinct variable conditions are necessary is that the variables of
%Bourbaki correspond to \emph{metavariables} rather than the individual variables of
%the predicate calculus; see chapter CH of \cite{mm} for more information.

\subsection{Local variables}

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

\begin{lstlisting}
^local-form^ := (loc ^varspec^)
\end{lstlisting}

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

\subsection{Statistics}

The function \lstinline!collect-stats! walks through the proof of its argument
theorem $thr$ and calculates the following information for $thr$
and (recursively) the theorems referenced by $thr$:
\begin{itemize}
\item the axioms the theorem depends on
\item definitions (see below) used in the proof, either directly or by a referenced theorem
\item number of proof steps if the proof were expanded to axioms
\item list of theorems directly referencing this theorem.
\end{itemize}
The function \lstinline!show-stats! prints the collected information.

Example:
\begin{lstlisting}[caption=Statistics,label=lst_stats]
> (load "doc/example1.lisp")
> (collect-stats !id)
> (show-stats !id)
Depends on axioms: ax-mp ax2 ax1
Uses definitions:
Is used by 0 theorems:
Total proof length: 5
> (show-stats !ax1)
Depends on axioms:
Uses definitions:
Is used by 1 theorem: id
Total proof length: 0
\end{lstlisting}

\section{Definitions}
\label{s_def}

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}
^define-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 declared 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}

The right-hand-side may contain only primitive and already defined symbols,
variables of the defined symbol, and \emph{auxiliary variables}
(the \lstinline!^other-vars^!) that must be \emph{bound} (see section \ref{ss_bound}).

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 would in this case
be specified with
\begin{lstlisting}[mathescape]
(set-symkind-eq-op wff !$\leftrightarrow$)
\end{lstlisting}
Trying to define a symbol of a type for which no equality operator is
specified is an error.

The equality operator should be of the `wff' type and have exactly two variables.
Note that the equality operator of the wff type (the biconditional) cannot be
used to define itself; it must be a primitive symbol in Bourbaki.

\subsection{Soundness of definitions}
\label{ss_sound_def}

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 proved using the definition, if its 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 they satisfy certain bound variable conditions (see below) and
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$(x/a) $\phi$(x/b)]! for any
wff $\phi(x)$. Here \lstinline!^eq'^! is the equality operator for the type of $\phi$;
\lstinline[mathescape]!$\phi$(x/a)! denotes the formula where \lstinline!a! is properly
substituted for \lstinline!x! in \lstinline[mathescape]!$\phi$(x)!.
\end{itemize}

Ensuring that these conditions hold for \lstinline!^eq^! is a responsibility of the user.

\subsection{Bound Variables}
\label{ss_bound}

If the right-hand side of a definition uses auxiliary variables, they must be \emph{bound}
in the sense that the value of \lstinline!^rhs^! in the formal system does not depend on
what is substituted for the auxiliary variables. For example, $x$ is bound in
$\exists x (x > y)$ because $\exists x (x > y) \leftrightarrow \exists z (z > y)$ for
any variable $z$ distinct from $y$.

More formally, a symbol $s$ with variables $v_1, \ldots, v_n$ \emph{binds} $v_i$ if the
formula
\begin{lstlisting}[mathescape]
[^eq^ [^s^ $a_1$ $\ldots$ $a_{i-1}$ $v_i$ $a_{i+1}$ $\ldots$ $a_n$]
    [^s^ $a_1(v_i/a_i)$ $\ldots$ $a_{i-1}(v_i/a_i)$ $a_i$ $a_{i+1}(v_i/a_i)$ $\ldots$ $a_n(v_i/a_i)$]]
\end{lstlisting}
is provable for any substitutions $a_1, \ldots, a_n$ of correct type and $a_i$ distinct from the other $a_j$.
In this case we say all occurrences of $v_i$ within
\lstinline[mathescape]![^s^ $a_1$ $\ldots$ $a_{i-1}$ $v_i$ $a_{i+1}$ $\ldots$ $a_n$]!
are \emph{bound by} $s$.

To declare that a symbol binds some of its variables, one can give an additional \lstinline!:bound!
argument in the \lstinline!^varspec^! of that symbol. For example, the universal quantifier
should properly be declared as
\begin{lstlisting}[mathescape]
(prim wff "$\forall$" ((:bound var) "x" wff "$\phi$"))
\end{lstlisting}
The \lstinline!^other-vars^! of a definition are implicitly marked \lstinline!:bound! and
distinct from each other and the \lstinline!^sym-vars^!.

Like the substitution law in the previous section, Bourbaki cannot generally verify
the validity of a \lstinline!:bound! declaration for a primitive symbol. However, the following
check is possible for a defined symbol:

A definition \lstinline[mathescape]![^eq^ ^sym^ $var_1 \ldots var_n\ $ ^rhs^]! is valid
if for every $var_i$ marked \lstinline!:bound! (and all the auxiliary variables),
all the \emph{potential} occurrences of $var_i$ are bound in \lstinline!^rhs^!, that is,
$var_i$ must be distinct from all variables that occur free in the \lstinline!^rhs^!.

This condition is checked by \lstinline!verify!,
otherwise definitions are treated like axioms by the verifier.

\subsection{Sample Definitions}

\begin{lstlisting}[mathescape,caption=Definitions,label=lst_def]
;; 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 \lstinline!: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 example should explain the term
%\emph{potential occurrence} used above.
If \lstinline!x! were distinct from \lstinline!a!,
it could be marked \lstinline!:bound!.

\section{The Context System}
\label{s_ctx}

When writing mathematics, it is usual to omit information that is formally necessary, but
``clear from context''. For example, when speaking about closed sets in a Hilbert
space $H$, we mean closed with respect to \emph{the topology induced by the metric
induced by the norm induced by the inner product of $H$}.

A \emph{context} in Bourbaki contains among other things bindings for the parser that
make it possible to parse \lstinline![closed A]! as
\begin{lstlisting}
[closed A [topology-of metric-of norm-of inner-product H]],
\end{lstlisting}
for example.
These bindings are established by \emph{importing} and \emph{exporting} contexts
(section \ref{ss_impexp}).

In this section we describe the \emph{namespace hierarchy} provided by the contexts:
a context may contain symbols, theorems and subcontexts. At the top of the hierarchy
there is a \emph{root context}, the value of \lstinline!*root-context*!. New symbols and
theorems declared with \lstinline!prim!, \lstinline!th! and so on, are inserted into
the \emph{current context}, the value of \lstinline!*current-context*!. By default,
\lstinline!*current-context*! is the same as \lstinline!*root-context*!.

New contexts are created with macros \lstinline!module! and \lstinline!local!:
\begin{lstlisting}
^module-form^ := (module ^name^ ^body^)
^local-form^  := (local ^name^ ^body^)
^name^        := ^string^
\end{lstlisting}

\lstinline!local! creates a new subcontext of the current context and evaluates the \lstinline!^body^!
expressions in this new context. \lstinline!module! always creates a \emph{top-level} context,
one that is a subcontext of the root contetx.

A sample context hierarchy follows.
%Listing \ref{lst_ctx1} generates the hierarchy of Figure \ref{fig_ctx1}.
%Note that the symbols and theorems are technically contexts (with variables
%as subcontexts).
\begin{lstlisting}[mathescape,caption={Sample context hierarchy},label=lst_ctx1]
;; File example2.lisp
(module "logic"
  (local "propositional"
    (prim wff "$\to$" (wff ![$\phi\ \psi$])))
  (local "predicate")
    (prim wff "$\forall$" ((:bound var) "x" wff "$\phi$")))
(module "set-theory"
  (local "zfc"
    (prim wff "$\in$" (set ![x y]))
    (local "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$!$'.
References beginning with \lstinline|!/| are \emph{absolute} (with respect to
the root context), other references are relative to the current context.
In the sample hierarchy, \lstinline|!/set-theory!zfc!axioms!union| and
\lstinline|!axioms!union| refer to the same axiom if \lstinline|!/set-theory!zfc|
is the current context. The macro \lstinline!in-context! can be used to bind
\lstinline!*current-context*!:
\begin{lstlisting}
(in-context !/set-theory!zfc!axioms
  (ax "infinity" ...))
\end{lstlisting}
re-opens the \lstinline!axioms! context to insert a new axiom.

The symbols and theorems in Bourbaki are actually treated as contexts, and may themselves
have subcontexts. For example, lemmas can be conveniently placed as subcontexts of the
theorem they are used for:

\begin{lstlisting}
(th "sample" (wff "X")
  (th "lemma1" ...)
  (th "lemma2" ...)
  ...)
\end{lstlisting}

The words \emph{symbol} and \emph{context} are used somewhat interchangeably in
the rest of this document.

The \emph{full name} of a context is the list of names of the ancestors of that
context, for example, \lstinline!("union" "axioms" "zfc" "set-theory")! is the
full name of \lstinline|!/set-theory!zfc!axioms!union|.

\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}

Table \ref{t_meta} lists the fields reserved by the current version of Bourbaki. They are all symbols in the
\lstinline!keyword! package.

\begin{table}[htbp]
\begin{tabular}{l l l}
Key & Set by & Description (reference) \\
\hline
\lstinline!:bound!   & Symbol defining macros & the :bound status of a variable \\
\lstinline!:comment! & user                   & short description \\
\lstinline!:def!     & \lstinline!def!        & definition corresponding to a symbol \\
\lstinline!:defs-used!   & \lstinline!collect-stats!      & \\
\lstinline!:depends-on!  & \lstinline!collect-stats!      & axioms this theorem's proof depends on \\
\lstinline!:description! & user               & longer textual description \\
\lstinline!:full-name!   & \lstinline!create-context!  & the full name of this context \\
\lstinline!:parent!        & \lstinline!create-context! & parent context in the hierarchy \\
\lstinline!:proof-length!  & \lstinline!collect-stats!  & length of proof when expanded to axioms \\
\lstinline!:used-by!       & \lstinline!collect-stats!  & list of theorems using this one in a proof \\
\end{tabular}
\caption{Meta keys used by Bourbaki}
\label{t_meta}
\end{table}

\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]!. Common variables and
hypotheses can be moved to the parent context:

\begin{lstlisting}[caption=Topological spaces,label=lst_ref1]
(def wff "topo-space" (set "X") ...)

(theory "topology" (set "X")
  (hypo [topo-space X])

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

  ;; Theorem: closure is idempotent
  (th "clos-idem" (set "A")
    (ass [= [closure closure A] [closure A]])
    (proof ...)))
\end{lstlisting}

The macro \lstinline!theory! is just a version of \lstinline!local!
taking a \lstinline!^varspec^!.
When used from outside of \lstinline!topology! this behaves as the following were
written instead:
\begin{lstlisting}
(local "topology"
  (def set "closure" (set "X" set "A") ...)
  (th "clos-idem" (set "X" set "Y")
    (hypo [topo-space X])
    ...))
\end{lstlisting}

Within \lstinline!topology! the space \lstinline!X! is used by default when
referring to other theorems and definitions in \lstinline!topology!
\begin{lstlisting}[mathescape]
> (in-context !/topology
    (print-symtree [closure $\emptyset$]))
[closure X $\emptyset$]
\end{lstlisting}

This is a case of \emph{importing} symbols, as defined in section \ref{ss_impexp}.
When variables from multiple levels are nested, the variables of the
innermost context are the \emph{rightmost} ones.

Note that definitions, unlike axioms and theorems, do \emph{not} inherit hypotheses
from the parent context. This is to ensure the definition can always be
eliminated.

% TODO: technical detail: explain sharing structure of the variable, hypothesis lists

\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 symbols
\lstinline!:axiom!, \lstinline!:definition!, \lstinline!:theorem!,
\lstinline!:prim!, \lstinline!:sym!, \lstinline!:arg! (a variable),
\lstinline!:loc! (a dummy variable), \lstinline!:context!, or \lstinline!:module!.

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

Usually \lstinline!create-context! is not called directly, but context creating
macros such as \lstinline!th! and \lstinline!prim! are used instead.
\lstinline!defcontext! is the general form of these macros:
\begin{lstlisting}
^defcontext-form^ := (defcontext ^class^ ^name^ ( ^varspec^ ) ^body^)
\end{lstlisting}
Like \lstinline!create-context!, \lstinline!defcontext! does not insert to parent's
symbol table.

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

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
described in section \ref{s_symref}.

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}
\label{s_symref}

A \emph{symbol reference} or \emph{symref} is a function taking symtrees
as arguments and returning a symtree. Symrefs are used to represent argument
transformations. For example, in the hierarchy of listing \ref{lst_ref1} above, the call
\begin{lstlisting}
(in-context !/topology
  !closure)
\end{lstlisting}
returns a symref taking
one argument. When applied to a symtree \lstinline!A! this symref returns
\lstinline![closure X A]!.

\subsection{Terminology}

The symbol references are structures of type \lstinline!symref!:
\begin{lstlisting}
(defstruct symref
  target
  arity
  fn
  proof)
\end{lstlisting}
where \lstinline!target! is the referred context (or \lstinline!nil!, if the symref does not
refer to a specific context), and \lstinline!fn! is a Lisp function used to
construct arguments for the target context (\lstinline!fn! should return a list of symtrees with
length equal to \lstinline!target!'s arity).
\lstinline!arity! is an integer $n$ describing the function \lstinline!fn!.

If $n \ge 0$, \lstinline!fn! is a function taking some \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$. 

A symref is \emph{composable} if \lstinline[mathescape]!arity $\ge 0$! and the \lstinline!target!
is not \lstinline!nil!. In the rest of this section we assume all symrefs to be composable.
Symrefs with variable number of arguments and \lstinline!nil! target appear in section
\ref{s_meta}.

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! if necessary.
\lstinline!verify! and \lstinline!print-theorem! are examples of these.

Given an exact symref $r$ with \lstinline[mathescape]!arity = $n$! and some symtrees
$t_1, \ldots, t_n$ we can construct the symtree with $r$'s target as operator
and the results of \lstinline[mathescape]!(funcall (symref-fn $r$) $t_1\ldots t_n$)! as
arguments. The function \lstinline!apply-ref! performs this operation:
\begin{lstlisting}
(defun apply-ref (ref rest args)
  (cons (symref-target ref)
        (apply (symref-fn ref) args)))
\end{lstlisting}
When speaking about \emph{applying} a symref, we mean this operation.

\subsection{Composing References}

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

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>.

%TODO: Figure illustrating going down hierarchy

Corresponding to a theorem
\begin{lstlisting}[mathescape]
(th "example" ($type_1$ "$var_1$" $\ldots$ $type_N$ "$var_N$")
    ...)
\end{lstlisting}
the \lstinline!syms! hashtable of the parent context contains a symref with
\lstinline!arity = N! under the key \lstinline!"example"!. The symref
function in this case just returns its arguments unmodified. Contexts of other types
are inserted into the symbol table in the same way. Note that if an ancestor context of \lstinline!"example"!
has variables, the arity of \lstinline!"example"! is greater than $N$ and the symref is not exact
(the symref function should be called with all arguments for the target, not just the innermost ones).

A reference \lstinline$!/x!y!z!example$ composes these subcontext references while going
down the context hierarchy, resulting in an exact symref with \lstinline!"example"!'s
arity.

The composition of symrefs is an associative operation as long as all te compositions
are legal.

%Implementation detail:
%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 $op$ to
\lstinline!symtree-parse! is a symref with \lstinline!arity! $= n \ge 0$,
$op$ is applied to the next $n$ subtrees parsed recursively
($op$ must be an exact symref).
If $n < 0$, subtrees are parsed until all
the arguments are used up. $op$ is then applied to all of the parsed subexpressions.

If the first argument is of any other type, it is immediately returned. This allows
construction of symtree patterns that have integers or Lisp symbols in place of
subtrees.

\subsubsection{Examples}

\lstinline|(symtree-parse !* !+ !a !b !- !a !b)| finds that \lstinline|!*| is a symref
requiring two arguments.
It then parses the subtrees \lstinline|[+ a b]| and \lstinline|[- a b]| and finally applies
\lstinline|!*| to them, resulting in \lstinline|[* [+ a b] [- a b]]|.

\begin{lstlisting}
(symtree-parse !*
               (symtree-parse !+ !a !b)
               (symtree-parse !- !a !b))
\end{lstlisting}
returns the same symtree as the first example:
when getting arguments for \lstinline|!*|, \lstinline!symtree-parse! sees the two lists from the nested calls
and passes them to \lstinline|!*|.

\lstinline|(symtree-parse !* 0 1)| returns the symtree pattern \lstinline[mathescape]|($*_s$ 0 1)|.

%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.

\subsubsection{Bracket syntax}

The reader macro `\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 !+ !x !y)
\end{lstlisting}

The special characters are treated as follows:

\begin{itemize}
\item \lstinline![! begins a nested symtree. Using this construct is necessary to disambiguate
expressions with operators taking a variable number of arguments. It may be used at any time to
parenthesize the expression for clarity.
\item \lstinline$!$ begins a call to \lstinline!seek-sym! read with the usual syntax of
`\lstinline$!$'.
\item \lstinline!"! reads a symbol name using Lisp syntax for strings.
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 with integers.
%\item \lstinline[mathescape]!($\ldots$! is simply an abbreviation for
%\lstinline[mathescape]!,($\ldots$!.
\end{itemize}

\subsection{Importing and Exporting}
\label{ss_impexp}

We now return to the example of topology in Hilbert spaces mentioned in section \ref{s_ctx},
using topological closure as an example.
Begin from the theories of topological and metric spaces:
\begin{lstlisting}
(theory "Topo" (set "X")
  (hypo [topo-space X])
  
  ;; Define closure of A in the topology of X
  (def "df-clos" set "clos" (set "A") ...)

  ;; Sample theorem: closure is idempotent
  (th "clos-idem" (set "A")
    (ass [= clos clos A clos A])))

(theory "Metric" (set "d")
  (hypo [metric d])

  ;; Define the topology induced by d
  (def "df-metric-topo" set "topology-of" () ...))
\end{lstlisting}

Now, to make use of the topology theorems for metric spaces, \emph{import} the context Topo:
\begin{lstlisting}
(in-context !/Metric
  (import [Topo topology-of]))
\end{lstlisting}
This creates an exact symref $i$ of arity 0 with the function
\begin{lstlisting}
(lambda () (list [topology-of d]))
\end{lstlisting}

Now, when seek-sym tries to find a symbol named ``clos'' it looks not only at the
current context \lstinline:!/Metric:, but also the imported context \lstinline:!/Topo:. The 1-argument
symref \lstinline:!clos: is composed with $i$ resulting in an exact symref taking
an argument \lstinline!A! and returning the list \lstinline!([topology-of d] A)!.

Imported symbols are only visible from the importing context. It is not
possible to use \lstinline:!/Metric!clos: outside the context
\lstinline:!/Metric:. To achieve this, we should use \lstinline!export! instead of
\lstinline!import!:
\begin{lstlisting}
(in-context !/Metric
  (export [Topo topology-of]))
\end{lstlisting}
Now \lstinline:!/Metric!clos: can be used from everywhere as the closure
operator specialized to metric spaces: \lstinline:[!/Metric!clos d A]:
is the closure of \lstinline!A! in the topology induced by the metric \lstinline!d!.
The statement \lstinline!(export [Topo topology-of])! creates a symref $e$ with arity 0 and
function
\begin{lstlisting}
(lambda (x) [topology-of ,x])
\end{lstlisting}
(Note that $e$ is not an exact symref.)
When parsing \lstinline:[!/Metric!clos d A]:, the symref \lstinline:!Metric:
is composed with $e$ and \lstinline:!clos: yielding finally an exact symref
with arity 2 and function
\begin{lstlisting}
(lambda (x y) [!Topo!closure [topology-of ,x] ,y])
\end{lstlisting}

The intended use of \lstinline!export! is to provide specialized or extended versions of theories,
while \lstinline!import! is used  to abbreviate references within a context.
For example, most contexts will import propositional and predicate calculus for easy
use of the logic symbols.

We can now define the theories of normed and Hilbert spaces in the same way:
\begin{lstlisting}
(theory "Normed" (set "N")
  (hypo [Normed-space N])

  (def "df-metric" set "metric-of" () ...)
  (export [Metric metric-of]))

(theory "Hilbert" (set "H")
  (hypo [H-space H])

  (def "df-norm" set "norm-of" () ...)
  (export [Normed norm-of]))
\end{lstlisting}

Here the statement \lstinline!(export [Metric ...])! exports not only
\lstinline!Metric!, but also all contexts exported from \lstinline!Metric!
by composing the symrefs associated with the \lstinline!export! statements.
Thus \lstinline!Normed! will export all symbols from \lstinline!Topo! with
the symref
\begin{lstlisting}
(lambda (x) [topology-of metric-of ,x])
\end{lstlisting}
Likewise, \lstinline!Hilbert! will export symbols from
\lstinline!Topo!, \lstinline!Metric! and \lstinline!Normed!.

The Bourbaki \lstinline!import! and \lstinline!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 within a context are also exported by default.
%The require and provide described in section 7 are something
%closer to Ghilbert's import/export.

More generally, default values can be given to just some of the variables of
the imported context by using \lstinline!import! or \lstinline!export!
with a symtree pattern.
Take the theory of continuous functions, for example:

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

  ...)
\end{lstlisting}

We can specialize this to continuous real-valued functions with
\begin{lstlisting}[mathescape]
(local "real-valued"
  (import [Cont ,0 $\mathbb{R}$]))

(in-context !real-valued
  (print-symtree [continuous A f]))
$\Rightarrow$ [continuous A $\mathbb{R}$ f]
\end{lstlisting}
and to paths (continuous functions from the unit interval $I$)
with \lstinline[mathescape]!(import [Cont I ,0])!.

\subsection{Importing and exporting with proofs}
\label{ss_imp_prf}

In the account of previous section we have skipped over one detail:
\lstinline!Topo! has hypothesis \lstinline![topo-space X]! while \lstinline!Hilbert! has
\lstinline![H-space H]!. It would be nice if the proof fragment corresponding
to Hilbert $\Rightarrow$ Normed $\Rightarrow$ Metric $\Rightarrow$ Topology could be stored
with the exports and inserted automatically whenever a topology theorem is
used in a Hilbert space proof.

The optional \lstinline!:proof! argument of \lstinline!import! and \lstinline!export!
does just this, as illustrated in the following listing (see section \ref{s_proof} for
\lstinline!linear-subproof!):

\begin{lstlisting}
(theory "Metric" (set "d")
  (hypo [metric d])

  ;; Define the topology induced by d
  (def "df-metric-topo" set "topology-of" () ...)

  ;; A conversion theorem:
  ;; the induced topology is a topological space
  (th "Metric-to-Topo" ()
    (ass [topo-space topology-of])
    (proof ...))

  ;; Export !/Topo with a proof
  (export [!/Topo topology-of]
          :proof (linear-subproof ([metric d])
                                  ([topo-space topology-of])
                   [Metric-to-Topo])))
\end{lstlisting}

When multiple symrefs with proofs are composed, the resulting proof will be a 
concatenation of the original proof fragments. The proof is used whenever
a reference to an axiom, theorem or definition is made via the symref
within the proof of a theorem (or whenever the variable \lstinline!*current-proof*!
is set).

\subsection{Seeking symbols}

The function \lstinline!seek-sym! seeks a symbol by name from the context hierarchy,
returning a symref. The first argument to \lstinline!seek-sym! is either
\lstinline!:rel! or \lstinline!:abs! specifying search from the current context or
the root.

In a call \lstinline!(seek-sym :rel "name1" "name2" ... "nameN")! the first name is
searched from the \emph{imports} of \lstinline!*current-context*!. If a symbol $s_1$ is
found via an import $i$, \lstinline!"name2"! is searched from the \emph{exports} of
$s_1$. For each further name \lstinline!seek-sym! takes one step ``sideways''through
an export and one step ``down'' to find the next name. \lstinline!seek-sym! composes the
symrefs it follows returning finally a symref with target a symbol named \lstinline"nameN".
In an absolute reference the first name is searched from the imports of \lstinline!*root-context*!
instead.

The \emph{exports} of a context $K$ are searched in the following order:
\begin{enumerate}
\item $K$ always exports itself with an identity symref
\item If $K$ exports other contexts $C_1, \ldots, C_n$ in this order, seek from the export lists of
the $C_i$ in \emph{reverse order} (first $C_n$, then contexts exported by $C_n$,
then $C_{n-1}$, and so on).
\end{enumerate}

The \emph{imports} of a context $K$ are searched in the following order:
\begin{enumerate}
\item $K$ imports itself with a constant function returning the list of variables
of $K$.
\item If $K$ imports contexts $C_1, \ldots, C_n$, seek from the \emph{export} lists of
the $C_i$ in \emph{reverse order}.
\item Seek from the import list of the parent of $K$.
\end{enumerate}

Note that the list of exports is always a subset of the list of imports. A statement
\lstinline!(export [X])! adds \lstinline!X! to both lists.

The reader macro `\lstinline:!:' abbreviates calls to \lstinline!seek-sym!. After the initial
`\lstinline:!:' or `\lstinline:!/:' exclamation mark separated tokens are read until
whitespace is seen. Special characters in a token can be escaped by enclosing it in
double quotes.

\subsection{Aliases}

The imports and exports just described provide argument transformations for whole
contexts. Sometimes it is useful to abbreviate just a single symbol or pattern of
symbols in this way.

For example, binary relations are encoded as sets of ordered pairs in set theory.
Thus we would have to write $\langle x,y\rangle\in \le_{set}$ or
\lstinline[mathescape]:[$\in$ pair x y $\le_{set}$]: for the usual $x\le y$.

We could of course introduce a definition
\begin{lstlisting}[mathescape]
(def "df-less" wff "<=" (set ![x y]) ()
  [$\in$ [pair x y] $\le$])
\end{lstlisting}
but this has the inconvenience that `\lstinline!<=!' is a new primitive symbol
from the point of view of the verifier. Specialized versions of the general
properties of binary relations would have to be proved anew for every symbol
introduced in this way.

Instead we can introduce an \emph{alias} to the symbol table:
\begin{lstlisting}[mathescape]
(alias "<=" (set ![x y])
  [$\in$ [pair x y] $\le$])
\end{lstlisting}
The name '\lstinline!<=!' is now associated with a symref
\lstinline[mathescape]!(lambda (x y) [$\in$ [pair ,x ,y] $\le$])!. The
verifier never sees a symbol named `\lstinline!<=!'.

The macro \lstinline!pattern! constructs and returns
this symref without inserting it into the symbol table:
\begin{lstlisting}[mathescape]
(pattern (set ![x y])
  [$\in$ [pair x y] $\le$])
\end{lstlisting}

\section{Modules and Files}
\label{s_module}

It is common to have theorems of similar form, but different symbols in
their assertions. Taking the partial orders (actually lattices) $\le$ and
$\subseteq$ as an example, we have theorem pairs such as
`$x \le y \Leftrightarrow x = \min(x,y)$' and
`$x \subseteq y \Leftrightarrow x = x \cap y$'. The following listing exhibits
the characteristic properties of these relations using a generic ``object'' symkind.


%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

%%TODO fix symtrees in the following

\begin{lstlisting}[mathescape,caption=Partial orders,label=lst_poset1]
;;; File order.lisp

(module "order"
  (symkind "OBJ")

  (prim wff "$\le$" (obj ![a b]))

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

  (def "df-meet" obj "/\\" (obj ![a b]) ...)
  (def "df-join" obj "\/" (obj ![a b]) ...)

  ;;; Axioms for partial orders
  ;; 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]))

  ;;; Theorems for partial orders
  (th "meet-le" (obj ![a b])
    (ass [$\leftrightarrow$ [$\le$ a b] [= a /\ a b]]))

  ...)
\end{lstlisting}

We would now like to \emph{interpret} \lstinline:!/order: in the language
of set theory to get versions of the theorems with $x \subseteq y$ and $\langle x,y\rangle\in\le$
where \lstinline:!/order: has \lstinline[mathescape]![$\le$ x y]!.

The solution is to load \lstinline!order.lisp! in such a way that Bourbaki sees \emph{aliases}
for the relevant symbols instead of the declarations in \lstinline!order.lisp!.
We now describe the functions \lstinline!require! and \lstinline!providing! that are
used to set up this interpretation.

%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}

The function \lstinline!(require ^name^  ^module^)! looks for a top-level context
\lstinline!^name^!. If such a context exists, a reference to it is returned
as if \lstinline:!/^name^: was used. Otherwise the file \lstinline:^module^.lisp:
is loaded (from the directory \lstinline!*bourbaki-db-path*! whose default value
is the \lstinline!"lib"! subdirectory). The file should define a top-level
context with the same name \lstinline!^module^!.

Before loading the file, \lstinline!require! sets \lstinline!*root-context*!
to a newly created context. This new root context is made to import the
previous one.
\lstinline!^module^.lisp! is thus free to define any additional top-level
contexts without cluttering the namespace of the module requiring it. This is similar
to Java, where a \lstinline!.java! file can contain one public class
with the same name, and additionally any number of private classes.

After the file is loaded, \lstinline!require! inserts the symref
to \lstinline!^module^! to the previous root context's symbol
table under the key \lstinline!^name^! and also returns this symref.

Usually \lstinline!require! is called with both arguments the same.
The reader macro \lstinline:!!^module^: is an abbreviation for
\lstinline:(require ^module^  ^module^):. This leads to the idiomatic
expression \lstinline:(import [!!^module^]): where the module is
loaded and imported at the same time.

A case where the \lstinline!^name^! argument is needed would be second order
logic, where we have predicate calculus for two kinds of variables ranging
over objects and collections. There we would use something like
\begin{lstlisting}
(require "obj" "predicate")
(require "coll" "predicate")
\end{lstlisting}

Returning to the example of partial orderds, we now move the axioms and definitions
to their own file:
\begin{lstlisting}[mathescape]
;;; File order-ax.lisp

(module "order-ax"
  (symkind "OBJ")

  (prim wff "$\le$" (obj ![a b]))

  ;; other primitive symbols, axioms and definitions as before
  )
\end{lstlisting}

\lstinline!order.lisp! will then \lstinline!require! the axiom file:
\begin{lstlisting}[mathescape]
;;; File order.lisp

(module "order"
  (symkind "OBJ")
  (export [!!order-ax])

  ;;; Theorems for partial orders
  (th "meet-le" (obj ![a b])
    (ass [$\leftrightarrow$ [$\le$ a b] [= a /\ a b]]))

  ;; other theorems as before

  )
\end{lstlisting}

Note that symbol kinds are stored in the symbol table of each
root context. Both files need to declare \lstinline!(symkind "OBJ")!
to ensure they use compatible types. The declaration in
\lstinline!order-ax.lisp! sees that a symkind with the same name
is already visible (through the import of \lstinline!order.lisp!'s root context)
and does not try to redefine the type. If the declaration was omitted, 
\lstinline!order-ax.lisp! could not be verified standalone.
If the declaration in \lstinline!order.lisp! was omitted, the \lstinline!OBJ!
from \lstinline!order-ax.lisp! would \emph{not} be copied into the root
context of \lstinline!order.lisp! and the theorems would not parse.

The only thing remaining to interpret the theory of partial orders is
to set \lstinline!order-ax! and \lstinline!OBJ! properly before using
\lstinline!(require "order")!.

\subsection{Providing}

The macro \lstinline!providing! evaluates its body within a temporary
root context that has a specified set of top-level bindings:
\begin{lstlisting}
^provide-form^ := (providing ( ^binding^* ) ^body^)
^binding^ := (^name^ ^symref^)
\end{lstlisting}

Now the set theory file can make use of \lstinline!order.lisp!:
\begin{lstlisting}[mathescape]
;;; file set.lisp

(module "set"
  (symkind "SET")

  ;; ...

  ;; properties of the subset relation
  (local "sub"

    (th "subset-antisym" (set ![A B])
        (ass [$\to$ $\land$ $\subseteq$ A B $\subseteq$ B A = A B])
        (proof ...))

    ;; ...

    (let ((prov (defcontext :context "provide-order-ax" ()
                  (alias "$\le$" (set ![a b])
                    [$\subseteq$ a b])
                  (alias "antisym" (set ![a b])
                    [subset-antisym a b])
                  ;; other symbols and axioms in the same way
                  )))
      (providing (("order-ax" prov)
                  ("OBJ" !/SET))
        (export [!!order])))))
\end{lstlisting}

Theorems for partial orders specialized to the subset relation are now
available as \lstinline:!/set!sub!meet-le: and so on. Similarly
a calculus filed could \lstinline!require! \lstinline!order! with aliases
\lstinline[mathescape]:(alias "$\le$" (set ![x y]) [$\in$ pair x y $\le$]):.
Bourbaki does not currently check that the provided aliases match with
the symbols in \lstinline!order-ax.lisp! (that the alias `$\le$' points
to a symbol with arity two and so on). The parser and the verifier must
be relied on to catch any mismatches.

Note that the temporary root context created by \lstinline!providing!
does not import the previous \lstinline!*root-context*! and the entries
in its symbol table are not copied to the root context of \lstinline!set.lisp!.
After the \lstinline!providing! form finishes, the only way to access the
\lstinline!order! theorems is through the \lstinline!export! in \lstinline:!/set!sub:.


In summary, the \lstinline!require! function is used in two ways:
\begin{itemize}
\item Within a \lstinline!providing! form to interpret an existing theory
\item At top level to state what axioms or parameters are needed and what are
their default values
\end{itemize}

\subsection{Writing re-usable modules}
\label{ss_reuse}

Making a module interpretable in many different contexts puts some constraints on it.

\begin{itemize}
\item The module should not depend on the exact properties of the symbols in the required
modules. The `$\le$' in \lstinline!order-ax.lisp! might be an alias expanding to a complex
expression rather than being a primitive symbol. This implies that symtrees should not be
constructed manually, \lstinline!symtree-parse! must always be used.
\item The module should not try to redefine or add symbols to the required contexts.
\item Top-level contexts other than those explicitly required may be visible when the file is
being loaded. New ``private'' modules may always be defined without fearing name clashes, however.
\item The module could be loaded multiple times within the same session.
If the file defines any global functions or variables, these
will be redefined each time the file is loaded. Global references to the Bourbaki context
system should not be put outside the system.
\end{itemize}

\section{Structured Proofs}
\label{s_proof}

The stricktly linear proofs used so far fails to separate the trivial manipulations
necessary in a formal proof from the ``interesting'' proof steps.
Bourbaki actually uses a structured proof format like the one described in \cite{lamport}.

A \emph{structured proof} consists of hypotheses, assertions and \emph{justification}.
The justification is either a theorem reference
(that is, a symtree whose operator is a theorem) or a sequence of (structured) subproofs.
We call these \emph{type 1} and \emph{type 2} proofs, respectively.
The proof of a theorem has the same hypotheses and assertions as the theorem.
Structured proofs are objects of type \lstinline!subproof!:
\begin{lstlisting}
(defstruct subproof
  hypo
  assert
  ref ; for type 1 proofs
  sub ; for type 2 proofs
  )
\end{lstlisting}

%Strictly speaking, a subproof should be \emph{self-contained}, that is, it should
%only rely its own stated hypotheses. Like \cite{lamport}, we follow a more relaxed
%definition: a subproof can freely use results proved at \emph{upper} levels of
%the structured proof. The hypotheses can thus be omitted, they are only used to
%convey information to humans and programs reading the proof.

\subsection{Verifying structured proofs}
\label{ss_verify1}

To check the validity of a structured proof, we maintain lists of wffs proved
at each level of the proof. The first list is initialized with the hypotheses of the
theorem being proved.

The algorithm for a type 2 proof $P$ goes as follows:
\begin{enumerate}
\item create a new empty list $L$.
\item for each subproof $S$,
\begin{itemize}
\item check the validity of $S$
\item add the assertions of $S$ to $L$.
\end{itemize}
\item check that each assertion of $P$ is in $L$ or one of the upper level
lists
\item discard the list $L$. Following steps may use only the stated assertions
of $P$, not any intermediate results.
\end{enumerate}

For a type 1 proof $P$,
\begin{enumerate}
\item check that the substituted expressions are well-formed and satisfy
the distinct variable conditions of the referred theorem
\item check that the (substituted) hypotheses of the theorem are found in the
upper-level lists of proven expressions
\item check that the assertions of $P$ are among the substituted
assertions of the theorem.
\end{enumerate}

Note that the hypotheses of a subproof are ignored; they are only hints
for humans and programs manipulating the proof.

Any structured proof can be ``flattened'' and the result will be valid
according to the algorithm of section \ref{ss_verify0}. The converse is not true:
if a structured proof step depends on some intermediate results of a type 2 subproof,
the flattened version will be valid even though the original proof is not.

\subsection{Parsing proofs}

There are several ways to create proof objects in Bourbaki.

The function \lstinline!parse-subproof! handles several kinds of arguments:
\begin{itemize}
\item A theorem reference is wrapped in a type 1 subproof with the obvious
hypotheses and assertions.
\item An argument of the \lstinline!subproof! type is returned without modification
\item When given an ordinary wff, \lstinline!parse-subproof! seeks for a theorem
proving this wff (see section \ref{ss_seek_prf}).
\item When given a symref pointing to a theorem, \lstinline!parse-subproof!
unifies hypotheses of the theorem against the previously proved wffs as
in a Metamath-style RPN proof.
(Not implemented yet; this requires maintaining the proof stack separately.)
\end{itemize}

When \lstinline!symtree-parse! is used within a structured proof to construct
a reference to an imported theorem, and the import has an associated proof
fragment (section \ref{ss_imp_prf}), a type 2 subproof consisting of the fragment
and the intended theorem reference is returned instead.

The most general macro to create type 2 proofs is \lstinline!subproof!:
\begin{lstlisting}
^subproof-form^ := (subproof (:hypo ^form^ :assert ^form^) ^body^)
\end{lstlisting}
The \lstinline!:hypo! and \lstinline!:assert! forms should be lists of wffs.
Within the \lstinline!^body^!, the macros \lstinline!hypo!, \lstinline!ass!
and \lstinline!line! are locally defined to add hypotheses, assertions and
subproofs to the proof being created. \lstinline!line! calls \lstinline!parse-subproof!
on its argument.

Within the body of a \lstinline!subproof! form the variable \lstinline!*current-proof*!
points to the list of assertions proved at earlier steps (including upper levels
of the proof). Membership on this list can be tested with \lstinline!(provenp ^wff^)!.

The case where the body of a \lstinline!subproof! form is just a sequence of
\lstinline!line! forms is abbreviated with the macro \lstinline!linear-subproof!:
\begin{lstlisting}
^linear-form^ := (linear-subproof ( ^hypo^* ) ( ^assertion^* ) ^line^* )
^hypo^      := ^symtree^
^assertion^ := ^symtree^
^line^      := ^theorem-reference^ | ^symtree^ | ^subproof^
\end{lstlisting}
Each \lstinline!^line^! is parsed by \lstinline!parse-subproof!. The macro
\lstinline!proof! is a version of \lstinline!linear-subproof! that uses
the hypotheses and assertions of \lstinline!*current-context*! by default
and sets the resulting proof object into the \lstinline!proof! slot of
\lstinline!*current-context*!.

%Linear proofs, such as those in section \ref{ss_verify0} are most easily created
%with the macro \lstinline!linear-subproof!:
%\begin{lstlisting}
%&linear-proof-form& := (linear-subproof ( &hypo&* ) ( &assertion&*) &line&* )
%&hypo&      := &symtree&
%&assertion& := &symtree&
%&line&      := &theorem-reference&
%\end{lstlisting}
%Each \lstinline!&line&! of the subproof is parsed with \lstinline!parse-subproof!

%Macro \lstinline!subproof! is the most general version
%\begin{lstlisting}
%(subproof (:hypo &form& :assert &form&) &body&)
%\end{lstlisting}
%\lstinline!subproof! defines the macros \lstinline!hypo!, \lstinline!ass! and
%\lstinline!line! locally to add hypotheses, assertions and subproofs to the
%proof being constructed. The \lstinline!&body&! may contain any Lisp code using
%these macros.

\subsection{Seeking theorems}
\label{ss_seek_prf}

The function \lstinline!parse-subproof! accepts not only theorem references.
When given a wff, it tries to find a theorem proving that wff. For this to be
practical references to theorems are stored to a search tree indexed by
symbols in the assertions of the theorem. This means
that a wff \lstinline![-> [\/ x y] [/\ u v]]! needs only be tested
against theorems of the forms \lstinline![-> a b]! (with \lstinline![\/ x y]!
substituted for \lstinline!a! and \lstinline![/\ u v]! for \lstinline!b!),
\lstinline![-> [\/ a b] c]!, and \lstinline![-> [\/ a b] [/\ c d]]!.
Each candidate theorem is tested with the same method that \lstinline!verify!
uses so that hypotheses and distinct variable conditions are correctly
checked.

Seeking currently works only for theorems whose assertion contains all the variables
of the theorem. This excludes inference rules such as modus ponens.
To apply modus ponens when proving a wff $\phi$ we would have to find a wff
of the form \lstinline[mathescape]![$\to$ $\psi$ $\phi$]! among the already
proved wffs such that $\psi$ has also been proved. The complexity for
finding substitutions for these ``extra'' variables explodes combinatorically
as the number of variables and hypotheses increases.

A theorem must be registered with the function \lstinline!th-pattern! to make
\lstinline!parse-proof! consider it for seeking.

% Explain pattern trees.
%Theorems are stored in nested hash tables indexed by symbols in the assertion.
%When seeking a proof for \lstinline![-> [\/ x y] [/\ u v]]! we only have to
%try theorems of the forms [-> a b] (with [\/ x y] substituted for "a" and
%[/\ u v] for "b"), [-> [\/ a b] c], and [-> [\/ a b] [/\ c d]]. For each
%matching theorem, \lstinline!parse-subproof! tests if its hypotheses are
%among already proved wffs and that its distinct variable conditions are
%satisfied.

%Note that seeking is restricted to theorems whose assertion contains all
%the variables of the theorem. This excludes inferences such as modus
%ponens. To apply modus ponens when proving a wff $\phi$ we would have
%to find a wff of the form "$\to \psi \phi$" among the proved wffs such
%that $\psi$ has also been proved. The complexity of
%finding substitutions for the "extra" variables not occurring in the assertion
%goes up quickly when the number of variables and hypotheses increases.

%Seeking could be extended to cover the case where each extra variable
%occurs in only one hypothesis (when the extra variables occur only bound,
%this can always be arranged by renaming). One could hope this extended
%seek procedure to cover most "interesting" theorems.

%Another interesting extension is multi-level seek. If restricted to theorems
%whose assertion is longer than any of the hypotheses, the seek is guaranteed
%to terminate. One possible application is proving properties of formulas
%(such as the property of a variable $x$ being bound in $\phi$)
%"by induction with respect to complexity of the formula".

%\subsection{RPN}

\subsection{Pattern trees}

TODO: insert here a description of the trees of wff patterns indexed by symbols;
these are used by \lstinline!parse-subproof! for seeking theorems and \lstinline!provenp!
for testing if a wff has been proved. Several functions in \lstinline!pattern.lisp!
for adding wffs to trees and checking membership. Note that removing wffs from pattern
trees is not yet possible.

\section{Metasymbols}
\label{s_meta}

What we have so far done with symrefs amounts to substitution of variables in symtrees.
Why not put more general Lisp functions in the \lstinline!fn! slot of a symref?
For example, we could want a summation operator $\Sigma$ taking variable number of arguments so that
\begin{itemize}
\item \lstinline[mathescape]![$\Sigma$ x]! is parsed to \lstinline![x]!,
\item \lstinline[mathescape]![$\Sigma$ a b ... n]! is parsed to \lstinline![+ a [+ b [+ ... n]]]!,
\item \lstinline[mathescape]![$\Sigma$]! is parsed to \lstinline![0]!.
\end{itemize}

As a Lisp function we would write
\begin{lstlisting}
(defun sum (&rest terms)
  (case (length terms)
    (0 [0])
    (1 (car terms))
    (otherwise [+ ,(car terms) ,(apply #'sum (cdr terms))])))
\end{lstlisting}

The macro \lstinline!metath! can be used to place our function in the context system:
\begin{lstlisting}[mathescape]
(metath "$\Sigma$" (&rest terms)
  (labels ((sum (terms)
             (case (length terms)
               (0 [0])
               (1 (car terms))
               (otherwise [+ ,(car terms)
                             ,(funcall #'sum (cdr terms))]))))
    (funcall #'sum terms)))
\end{lstlisting}
and \lstinline[mathescape]![$\Sigma$ x y z ...]! now works as advertised. The name
\lstinline!metath! refers of course to \emph{metatheorems}, but as in the current case,
it can be used to define \emph{metasymbols} of any type.

%more general Lisp functions? Take number theory for example. We have a binary operator "+" and
%a constant "0". We would like to define generalized addition operator "++" so that
%- [++ a b ... n] is parsed to [+ a [+ b [+ ... n]]]
%- [++ a] is parsed to [a]
%- [++] is parsed to [0].
%Or, as a Lisp function,
%\begin{lstlisting}
%(defun ++ (&rest terms)
%  (case (length terms)
%    (0 [0])
%    (1 (car terms))
%    (t [+ ,(car terms) ,(apply #'++ (cdr terms))])))
%\end{lstlisting}

%The macro \lstinline!metath! can be used to place our function in the context system:
%\begin{lstlisting}
%(metath "++" (&rest terms)
%  (labels ((++ (&rest terms)
%             (case (length terms)
%               (0 [0])
%               (1 (car terms))
%               (t [+ ,(car terms) ,(apply #'++ (cdr terms))]))))
%    (apply #'++ terms)))
%\end{lstlisting}

The call \lstinline!(metath ^name^  (^vars^) ^body^)! places a symref with the function
\lstinline!(lambda (^vars^) ^body^)! into the symbol table of the current context under the
key \lstinline!^name^!. The symref has \lstinline!nil! \lstinline!target! and arity $-1$. When
\lstinline!symtree-parse! encounters a symref with negative arity, it parses
subexpressions until it runs out of arguments. The symref function is then applied to all the
subexpressions. Unlike ordinary symrefs, the function must return a complete symtree
rather than the list of arguments for the \lstinline!target!. Because of these differences,
symrefs created with \lstinline!metath! cannot be used as the first argument to \lstinline!compose-ref!.

\subsection{Resolving name clashes}

Our `$\Sigma$' has a potential problem: the values of \lstinline![0]! and 
\lstinline![+ a b]! depend on the symbols visible from \lstinline!*current-context*!
at the time the \lstinline[mathescape]![$\Sigma$ ...]! expression is parsed.
The results may be unexpected should the user redefine `$+$'. (Sometimes having `$\Sigma$' automatically
use the currently visible `$+$' is just the right thing, however).

When the metasymbol function is called, the variable \lstinline!*meta-context*! is bound
to the value of \lstinline!*current-context*! at the time the metasymbol was being defined.
An unambiguous version of `$\Sigma$' would be
\begin{lstlisting}[mathescape]
(metath "$\Sigma$" (&rest terms)
  (in-context *meta-context*
    (labels ((sum (&rest terms)
               ;; the rest as before
      )))))
\end{lstlisting}

\subsection{Working with proofs}

Metasymbols constructing proofs or theorems are called \emph{metatheorems}.
The following listing illustrates some of the tools Bourbaki provides for
writing metatheorems. ``\lstinline!infer!'' converts a proof of
$\phi \to \psi$ or $\phi \leftrightarrow \psi$ to a proof of $\psi$ under the
hypothesis $\phi$ (or possibly vice versa in the case of a biconditional).

\begin{lstlisting}
(metath "infer" (line)
  ;; treat argument as a subproof
  (let ((prf (parse-subproof line)))
    (in-context *meta-context*
      ;; This works only for proofs with one assertion
      (match-case (car (subproof-assert prf))
        ([-> ,'?x ,'?y]
          (linear-subproof (?x) (?y)
            prf
            [ax-mp ,?x ,?y]))
        ([<-> ,'?x ,'?y]
           (if (provenp ?x)
             (linear-subproof (?x) (?y)
               prf
               ;; convert <-> to ->
               [bi> ,?x ,?y]
               [ax-mp ,?x ,?y])
             (if (provenp ?y)
               (linear-subproof (?y) (?x)
                 prf
                 ;; convert <-> to <-
                 [bi< ,?x ,?y]
                 [ax-mp ,?y ,?x]))))))))
\end{lstlisting}

This uses the pattern matching version of \lstinline!case!, a similar macro \lstinline!if-match! is
also defined. Note that in the case of a biconditional the metatheorem
tests which direction is intended by using the list \lstinline!*current-proof*! of
proven assertions.

The \lstinline!"infer"! metatheorems saves the user from invoking modus ponens explicitly.
It would be used like \lstinline![infer ax2 X Y Z]!. Compare this with the Metamath convention
of naming ``inference'' versions of theorems: \lstinline![ax2i X Y Z]!.

\subsection{Virtual namespaces}

Sometimes it is necessary to create completely new theorem objects.
For example, the deduction theorem converts a proof of $\psi$ under the hypothesis
$\phi$ to a proof of $\phi \to \psi$.
To do this, it needs to recursively create deduction versions of theorems referenced
by the proof.

There is a special macro \lstinline!virtual-metath! for writing theorem-creating
functions. A metatheorem created with \lstinline!virtual-metath! should take
exactly one argument that is a context, and also return a context. The results
are memoized to avoid wasting space and time computing the same theorems again
and again.

In addition to the standard way \lstinline![theorem ,argument]! of invoking
metatheorems Bourbaki experimentally supports \emph{virtual namespaces}.
When a theorem reference \lstinline:!/virtual!x!y!z: is parsed where
\lstinline:!/virtual: is created with \lstinline!virtual-metath!,
the remaining part \lstinline:!x!y!z: is taken as a full name
of a context. This context is given to \lstinline:!/virtual: and
the returned context is used instead of \lstinline!z!. This way
references can be printed to the theorems created on fly.

%\section{Input and Output}
%\label{s_io}

\begin{thebibliography}{99}
\bibitem{bsets} Bourbaki: Elements of Mathematics. Theory of Sets, Chapter IV
\bibitem{hyperspec} The Common Lisp HyperSpec, http://www.lisp.org/HyperSpec/FrontMatter/
\bibitem{mm} Megill: Metamath. Available at http://us.metamath.org/\#book
\bibitem{mendelson} Mendelson: Introduction to Mathematical Logic, third edition, p. 44
\bibitem{mm-dist} Megill: http://us.metamath.org/mpegif/mmset.html\#distinct
\bibitem{lamport} Lamport: How to Write a Proof, http://research.microsoft.com/users/lamport/
pubs/pubs.html\#lamport-how-to-write
\end{thebibliography}

\end{document}