\documentclass[a4]{seminar}
\usepackage{advi}
\usepackage{color}
\usepackage{amssymb}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.4,0}
\definecolor{slidered}{rgb}{1,0,0}
\newpagestyle{fw}{}{\hfil\textcolor{slideblue}{\sf\thepage}\qquad\qquad}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{#1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\dashskip}{\strut\enskip{ }}

\begin{document}\sf
\renewcommand{\sliderightmargin}{0mm}
\renewcommand{\slideleftmargin}{20mm}
\renewcommand{\slidebottommargin}{6mm}

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large mapping HOL into Coq}

Freek Wiedijk\\
University of Nijmegen

TYPES 2002, Nijmegen\\
2002-04-28, 12:00

LRI, Paris\\
2002-06-28, 13:30
\end{slide}

\begin{slide}
\slidetitle{overview}

translating HOL proofs to Coq\\
\smallskip
\adviwait
\dashskip analogue of HOL to Nuprl translator by Naumov, Stehr and Mesequer
\adviwait

\dashskip I'll describe my attempt \advirecord{failed}{that failed}\\
\adviwait
\dashskip translation used axioms\adviwait\adviplay{failed}: inconsistent with Coq\\
\adviwait
\dashskip \textcolor{slidered}{can anyone help me do this properly?}
\medskip
\adviwait

translating \textbf{constructive} HOL proofs to Coq\\
\adviwait
\dashskip still a problem left with HOL type definitions
\vfill
\end{slide}

\begin{slide}
\slidetitle{from FTA to FTC?}

FTA project: 1999-2000\\
\dashskip Fundamental Theorem of Algebra:\\
\dashskip \dashskip \textcolor{slidegreen}{every complex polynomial has a root}\\
\adviwait
\dashskip also formalized in Mizar and HOL
\adviwait

next step?\\
\adviwait
\dashskip Fundamental Theorem of Calculus\\
\dashskip \dashskip \textcolor{slidegreen}{$\displaystyle{d\over dx}$ and $\displaystyle\int$ are inverse operations}
\adviwait

\dashskip already present in Mizar and HOL libraries!\\
\adviwait
\dashskip \textcolor{slidered}{import this into Coq?}
\adviwait

in the meantime:\\
\dashskip Lu\'\i s Cruz-Filipe has proved FTC in the FTA framework\\
\dashskip constructive proof from Bishop's book
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{translating mathematics: the de Bruijn criterion}

Coq\\
-- proofs checked by small kernel\adviwait: `proof object'\\
\adviwait
-- don't contain the traces of the calculations\\
\dashskip checking time can be much bigger than size of proof object
\adviwait

HOL\\
-- proofs checked by small kernel\\
\adviwait
\dashskip proofs not stored in memory: `ephemeral proof object'\\
\adviwait
-- do contain full traces of calculations\\
\dashskip $\beta$-reduction is proof step called \texttt{BETA}
\adviwait

\begin{tabular}{ll}
basic HOL library & 1.5 million proof steps\\
\noalign{\vspace{-\smallskipamount}}
HOL version of FTC & 2.5 million proof steps
\smallskip
\end{tabular}
\adviwait

\textbf{translation approach:}\\
generate a Coq definition for each HOL proof step
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Coq proof objects}

2 sort constructors:

\quad
\begin{tabular}{l}
\verb|Prop| ($=$ \verb|Prop|, \verb|Set|)\quad
\verb|Type|
\end{tabular}
\medskip

16 term constructors:

\quad
\begin{tabular}{l}
\texttt{Rel}\quad
\texttt{Var}\quad
\texttt{Meta}\quad
\texttt{Evar}\quad
\texttt{Sort}\quad
\texttt{Cast}\quad
\texttt{Prod}\quad
\texttt{Lambda}\quad
\texttt{LetIn}\\
\texttt{App}\quad
\texttt{Const}\quad
\texttt{Ind}\quad
\texttt{Construct}\quad
\texttt{Case}\quad
\texttt{Fix}\quad
\texttt{CoFix}
\end{tabular}
\vfill
\end{slide}

\begin{slide}
\slidetitle{HOL ephemeral proof objects}

2 type constructors:

\quad
\begin{tabular}{l}
\texttt{Tyvar}\quad
\texttt{Tyapp} (\texttt{bool}, \texttt{fun}, \texttt{ind})
\end{tabular}
\medskip

4 term constructors:

\quad
\begin{tabular}{l}
\texttt{Var}\quad
\texttt{Const} (\texttt{=}, \texttt{@})\quad
\texttt{Comb}\quad
\texttt{Abs}
\end{tabular}
\medskip

$\textsf{10}\advirecord{+3}{+\textsf{3}}$ thm constructors:

\quad
\begin{tabular}{l}
\texttt{REFL}\quad
\texttt{TRANS}\quad
\texttt{MK\_COMB}\quad
\texttt{ABS}\quad
\texttt{BETA}\quad
\texttt{ASSUME}\quad
\texttt{EQ\_MP}\\
\texttt{DEDUCT\_ANTISYM\_RULE}\quad
\texttt{INST}\quad
\texttt{INST\_TYPE}\\
\noalign{\medskip}
\adviwait
\adviplay{+3}%
\texttt{new\_axiom} \quad (\texttt{INFINITY\_AX}, \texttt{ETA\_AX}, \texttt{SELECT\_AX})\\
\noalign{\vspace{-\smallskipamount}}
\texttt{new\_basic\_definition}\\
\noalign{\vspace{-\smallskipamount}}
\texttt{new\_basic\_type\_definition}
\end{tabular}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{a naive translation scheme}

% HOL to Coq translation needs two parts:\\
% -- how to model the objects\\
% -- which classical axioms to add
% \adviwait

\textbf{translation scheme:}

\quad
\begin{tabular}{rcl}
\verb|hol_type| &$\to$& \verb|Set|\\
\noalign{\vspace{-\smallskipamount}}
\verb|fun| &$\to$& \verb|->|\\
\noalign{\vspace{-\smallskipamount}}
\verb|bool| &$\to$& \verb|bool|\\
\noalign{\vspace{-\smallskipamount}}
\verb|ind| &$\to$& \verb|nat|\\
\noalign{\vspace{-\smallskipamount}}
\verb|=| &$\to$& Leibniz equality
\end{tabular}
\medskip
\adviwait

\textbf{add two `classical axioms' to get classical mathematics:}
\adviwait

\begin{tabular}{ll}
extensionality &
\verb|(A,B:Set; f,g:A->B)((x:A)(f x)=(g x))->f=g|\\
\adviwait
choice &
\verb|(A:Set)~(is_empty A)->A|
\end{tabular}\\
\adviwait
\dashskip\dashskip \verb|is_empty| \verb|[A:Set]:Prop| \verb|:=| \verb|(a:A)False| \quad ($\equiv \forall a\in A.\,\bot$)
\medskip
\adviwait

choice is equivalent to excluded middle for \verb|Set|\\
\adviwait
choice implies excluded middle for \verb|Prop|: classical logic
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{impredicativity of \texttt{Set}}

\strut\rlap{in Coq:}\hfill
\begin{tabular}{c}
\dashskip \verb|Set->bool| \verb|:| \verb|Set|\\
\quad \verb|(A:Set)A->bool| \verb|:| \verb|Set|
\end{tabular}\hfill
\adviwait

\strut\rlap{in the $\lambda$-cube, $\lambda 2$:}\hfill
\adviwait
\begin{tabular}{c}
$2:* \,\vdash\, (\Pi A\!:\!*.\,2) : *$\\
$2:* \,\vdash\, (\Pi A\!:\!*.\,\Pi a\!:\!A.\,2) : *$
\end{tabular}\hfill
\adviwait

\strut\rlap{mathematically:}\hfill
\adviwait
\begin{tabular}{c}
${\cal P}({\sf Set}) \in {\sf Set}$\\
%(Russell paradox is ${\cal P}({\sf Set}) \subseteq {\sf Set}$)
$\prod_{A\in{\sf Set}} {\cal P}(A) \in {\sf Set}$
%(`product of all power sets is a set')
\end{tabular}\hfill
\medskip
\adviwait

in classical set theory this gives a paradox:
\adviwait

\dashskip define $U \equiv \prod_{A\in{\sf Set}} {\cal P}(A)$\\
\adviwait
\dashskip define $X \equiv \{ u\in U \,|\, u\not\in u_U \}
\adviwait
\in{\cal P}(U)$\\
\adviwait
\dashskip take any $x\in U$ with $x_U = X$\\
\adviwait
\dashskip $x\in x_U \adviwait \iff x\in X \adviwait \iff x\not\in x_U$ \adviwait\quad{\textcolor{slidered}{contradiction}}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Coq is incompatible with classical mathematics}

naive thought:\\
constructive mathematics is weaker than classical mathematics\\
\adviwait
\dashskip $\Rightarrow$ adding `classical' axioms to Coq is safe
\adviwait

doesn't work!\\
\dashskip excluded middle for \verb|Set| is inconsistent with the Coq logic!\\
\adviwait
\dashskip (excluded middle for \verb|Prop| is safe)
\adviwait

moving the two axioms from \verb|Set| to \verb|Type|: does it help?\\
\adviwait
\dashskip $\verb|Set| \subseteq \verb|Type|$\\
\dashskip $\Rightarrow$ a choice operator for \verb|Type| is also a choice operator for \verb|Set|
\medskip
\adviwait

\textcolor{slideblue}{wanted:
\textbf{classical axioms}\\
-- use Coq as a `super-HOL'\\
-- consistent with the Coq logic}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{Prop} $\leftrightarrow$ \texttt{bool}}

Coq: \verb|Prop| \quad type for propositions

Coq: \verb|bool| \quad type for `decidable propositions'\\
\dashskip exactly two elements:\\
\dashskip \dashskip \verb|(b:bool) b = true \/ b = false|
\adviwait

HOL: \verb|bool| \quad classical logic\\
\dashskip also has exactly two elements:\\
\dashskip \dashskip \verb|!b:bool. (b = T) \/ (b = F)|
\smallskip
\adviwait

which of the two Coq types corresponds to the HOL \verb|bool|?
\vfill
\end{slide}

\begin{slide}
\slidetitle{the HOL Light architecture: LCF kernel + constructive core + rest}

HOL Light by John Harrison
\medskip
\adviwait

top level file \verb|hol.ml|, loads 35 subfiles:
\begin{center}
\begin{tabular}{ll}
\enskip 1 file with basic library functions & \verb|lib.ml|\\
\enskip 3 files with the `de Bruijn kernel' & \verb|type.ml| \verb|term.ml| \verb|thm.ml|\\
%LCF style proof kernel
13 files with constructive HOL & {\dots} \verb|num.ml| \dots\\
18 files with classical HOL & \verb|class.ml| \dots
\end{tabular}
\end{center}
\adviwait
\begin{flushright}
\textcolor{slidegreen}{`Extensional, classical reasoning with AC starts now!'}
\end{flushright}
\adviwait

axioms:\\
one `constructive axiom': infinity (\verb|INFINITY_AX|)\\
two `classical axioms': extensionality (\verb|ETA_AX|) and choice (\verb|SELECT_AX|)
\vfill
\end{slide}

\begin{slide}
\slidetitle{HOL definitions of logical operators}

basic notions: $\lambda$-calculus and $=$
\adviwait

HOL definitions of logical operators:
\begin{eqnarray*}
\top &\equiv& ((\lambda x.\, x) = (\lambda x.\, x))\\
(t_1 \land t_2) &\equiv& (\lambda f.\, f t_1 t_2) = (\lambda f.\, f \top \top)\\
(t_1 \to t_2) &\equiv& ((t_1 \land t_2) = t_1)\\
(\forall x.\, P x) &\equiv& (P = \lambda x.\, \top)\\
(\exists x.\, P x) &\equiv& (\forall Q.\, (\forall x.\, P x \to Q) \to Q)\\
(t_1 \lor t_2) &\equiv& (\forall t.\, (t_1 \to t) \to (t_2 \to t) \to t)\\
\bot &\equiv& (\forall t.\, t)
\end{eqnarray*}
\vfill
\end{slide}

\begin{slide}
\slidetitle{translating HOL types into Coq setoids}

\textbf{translation scheme:}

\quad
\begin{tabular}{rcl}
\verb|hol_type| &$\to$& `typoid': setoid in \verb|Type|\\
\verb|fun| &$\to$& `functionoid': function setoid\\
\verb|bool| &$\to$& `$\Omega$ setoid': \verb|Prop| with \verb|<->| as setoid equality\\
\verb|ind| &$\to$& \verb|nat| with \verb|==| as setoid equality\\
\verb|=| &$\to$& setoid equality
\end{tabular}
\adviwait

seems to work
\adviwait
(with no axioms needed for constructive HOL)\\
\adviwait
-- no `uniform' equality\\
\dashskip (\verb|hol_type| does not translate to a Coq type but to a Coq record)\\
\adviwait
-- extensionality (\verb|ETA_AX|) turns out to be valid\\
\adviwait
-- HOL \verb|bool| corresponds to Coq \verb|Prop|
\vfill
\end{slide}

\begin{slide}
\slidetitle{HOL type definitions are not constructive}

HOL type definitions: subtypes
\adviwait
\begin{center}
type $A$ + predicate $P$ on $A$ + object of type $A$ that satisfies $P$
\end{center}
\adviwait
-- new type $A'$\\
\adviwait
-- two functions $\verb|abs|:A\to A'$ and $\verb|rep|:A'\to A$\\
\adviwait
-- two thms that state that they are inverse to each other
\adviwait

\verb|abs| maps \textbf{all} objects of $A$ to $A'$\\
\adviwait
\dashskip not constructive!
\vfill
\end{slide}

\begin{slide}
\slidetitle{constructivizing HOL type definitions}

variant of HOL type definition scheme (John Harrison):
\adviwait
\begin{center}
$A$ + $P$ +
\adviwait
$\pi : A\to A$ that will correspond to $\verb|rep| \circ \verb|abs|$
\end{center}
\adviwait

\strut\rlap{thms to prove:}\\
\strut\hfill$\forall a.\, \pi(\pi a) = \pi a$\hfill\strut\\
\strut\hfill$\forall a.\, P a \leftrightarrow (\pi a = a)$\hfill
\adviwait

valid under the setoid interpretation\\
\adviwait
too weak: HOL definitions of ${\mathbb N}$ and $A\times B$ don't work anymore
\medskip
\adviwait

\textcolor{slideblue}{wanted:
\textbf{variant of HOL subtype definitions}\\
-- constructive\\
-- allows definition of ${\mathbb N}$ and $A\times B$ in the HOL style}
\vfill
\end{slide}

\end{document}