\documentclass[a4]{seminar}
\usepackage{advi}
\usepackage{advi-graphicx}
\usepackage{color}
\usepackage{amssymb}
%\usepackage[all]{xypic}
\usepackage{alltt}
\usepackage{url}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.6,.6,.6}
\definecolor{slidelightgray}{rgb}{.8,.92,.8}
\def\black#1{\textcolor{black}{#1}}
\def\white#1{\textcolor{white}{#1}}
\def\blue#1{\textcolor{slideblue}{#1}}
\def\green#1{\textcolor{slidegreen}{#1}}
\def\red#1{\textcolor{slidered}{#1}}
\def\gray#1{\textcolor{slidegray}{#1}}
\def\lightgray#1{\textcolor{slidelightgray}{#1}}
\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}{\strut #1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\quadskip}{{\tiny\strut}\quad}
\newcommand{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\enskipp}{{\tiny\strut}\enskip}
\newcommand{\exclspace}{\hspace{.45pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}
\newcommand{\toolong}{$\hspace{-3em}$}

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

\setcounter{slide}{-1}
\begin{slide}
%\slidetitle{\Large simple type theory with undefinedness in impredicative type theory\smallskip}
\slidetitle{\Large STTwU in Coq}

\green{Freek Wiedijk} \\
Radboud Universiteit, Nijmegen \\
Free University, Amsterdam
\smallskip

TYPES 2004 \\
%Campus Tal\`es \\
%Jouy-en-Josas, near Paris \\
2004 12 15, 15:10
\end{slide}

\begin{slide}
\sectiontitle{overview}
\slidetitle{the three points of this talk}
\begin{itemize}
\item[$\bullet$]
advertisement for Farmer's \red{STTwU} system
\adviwait

\item[$\bullet$]
report on a small \red{Coq formalization}
\adviwait

\item[$\bullet$]
\blue{how to map classical mathematics into constructive mathematics}
\bigskip
\adviwait

\green{isn't that \textbf{just} the double negation translation?}
\vspace{.5\smallskipamount}
\adviwait

{no:}
\begin{itemize}
\vspace{-.5\smallskipamount}
\item[]
\green{extensionality of equality?}
\item[]
\green{choice?}
\end{itemize}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
%\sectiontitle{simple type theory with undefinedness}
\sectiontitle{classical higher order logic in Coq}
\slidetitle{HOL}
%\adviwait
%{HOL}\quad
{simply typed lambda calculus + ML-style polymorphism} %\adviwait

\strut\quad {\rlap{type}\phantom{term} constants:}\quad
\texttt{bool}, \texttt{ind}, $\to$ \\
%booleans, individuals, function types \\
\strut\quad {term constants:}\quad
${=}\,$, $\advirecord{a6}{\varepsilon}\adviplay{a6}$ %(Hilbert's choice operator)
%\adviwait
$${\root n\of x \;:=\; \red{\varepsilon}\adviplay[slidered]{a6} y.\, (y^n = x \,\land (0 < x \Rightarrow 0 < y))}\adviwait$$

\blue{importing into Coq:}
\advirecord{a1}{\rlap{three axioms needed}}\advirecord{a2}{{two} axioms \advirecord{a5}{needed}\adviplay{a5}}\adviplay{a1}
\begin{center}
\begin{tabular}{rl}
\advirecord{a3b}{classical logic}\adviplay[slidegreen]{a3b} & \advirecord{a3}{\texttt{\small forall A:Prop, not (not A) -> A}} \\
\advirecord{a}{choice operator}\adviplay[slidegreen]{a} & \advirecord{a7}{\texttt{\small forall A:Set, not (notT A) -> A}} \\
\advirecord{a4}{extensionality}\adviplay[slidegreen]{a4} & \advirecord{a8}{\texttt{\small forall (A B:Set) (f g:A -> B),}} \\
\noalign{\vspace{-.8\medskipamount}}
& \advirecord{a8a}{\texttt{\small\ (forall x:A, f x = g x) -> f = g}}
\adviwait
\adviplay{a3}
\adviwait
\adviplay{a7}
\adviwait
\adviplay{a8}
\adviplay{a8a}
\adviwait
\adviplay[white]{a1}
\adviplay{a2}
\adviplay[slidegray]{a3}
%\adviplay[slidegray]{a3a}
\adviplay[slidegray]{a3b}
\adviwait
\adviplay[slidered]{a5}
\adviplay{a3b}
\adviplay[slidered]{a}
\adviplay{a4}
\end{tabular}
\end{center}

\vspace{-11pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{STTwU}
Bill Farmer\quad
\blue{IMPS} system $\to$ \blue{LUTINS} logic

\blue{L}ogic of \blue{U}ndefined \blue{T}erms for \blue{I}nference in a \blue{N}atural \blue{S}tyle
\bigskip
\adviwait

%didactic version: \\
\red{\blue{S}imple \blue{T}ype \blue{T}heory \blue{w}ith \blue{U}ndefinedness}
%\medskip
%\adviwait

simply typed lambda calculus + undefined terms

\strut\quad {\rlap{type}\phantom{term} constants:}\quad
\texttt{bool}, \texttt{ind}, $\to$ \\
%booleans, individuals, function types \\
\strut\quad {term constants:}\quad
${=}\,$, $\iota$ %(Church's choice operator)
\medskip
\adviwait

\green{choice operator becomes {partial}}
$$(\iota x.\, P x)\red{\downarrow} \;\Leftrightarrow\; \exists! x .\, P x\smallskip\adviwait$$
\green{\texttt{bool} is special:} {all} terms of type \texttt{bool} are defined %\\
%\strut\quad logic is strict \\
%\strut\quad if a \texttt{bool} term `should be undefined' it is $\bot$ instead

\vfill
\end{slide}

\begin{slide}
\slidetitle{the STTwU system as an LF context}
\vbox to 0pt{
\vspace{-\bigskipamount}
\begingroup
\let\green=\blue
\small
\def\etc{\smallskip\gray{\textsf{etcetera}}}
\begin{alltt}
Parameter \red{_type} : \green{Type}.
Parameter \red{_expr} : \green{_type -> Type}.
\end{alltt}
\begin{alltt}
Parameter \red{_bool} : \green{_type}.
Parameter \red{_ind} : \green{_type}.
Parameter \red{_fun} : \green{_type -> _type -> _type}.
\end{alltt}
\begin{alltt}
Parameter \red{_infer} : \blue{_expr _bool -> Type}.
\end{alltt}
\begin{alltt}
Parameter \red{_app} : \green{forall alpha beta:_type,
  _expr (_fun alpha beta) -> (_expr alpha -> _expr beta)}.
Parameter \red{_lambda} : \green{forall alpha beta:_type,
  (_expr alpha -> _expr beta) -> _expr (_fun alpha beta)}.
\end{alltt}
\begin{alltt}
Parameter \red{_eq} : \green{forall alpha:_type,
  _expr alpha -> (_expr alpha -> _expr _bool)}.
Parameter \red{_iota} : \green{forall alpha:_type,
  (_expr alpha -> _expr _bool) -> _expr alpha}.
\etc
\end{alltt}
\endgroup
\vss
}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{Coq formalization}
\slidetitle{a constructive model for STTwU in Coq}
\begin{center}
\begin{tabular}{rl}
classical logic & \green{double negation translation} \\
\adviwait
extensionality & \textbf{setoids} \\
\adviwait
partial logic & \textbf{partial} setoids \\
\adviwait
choice operator & \green{\textbf{dual} of partial setoid} \\
\end{tabular}
\end{center}
\bigskip
\adviwait

\red{no axioms needed!}

\vfill
\end{slide}

\def\_{\char`\_}

\begin{slide}
\slidetitle{a way to do the double negation translation}
\textbf{{classical propositions}} $\;=\;$ {copy of the \textbf{constructive propositions}}%$\,${\dots}
\begingroup
\small
\begin{alltt}
\red{Definition __bool := Prop.}
\end{alltt}
\endgroup
\medskip
\adviwait

{\dots} but interpreted \textbf{negatively}
\begingroup
\small
\begin{alltt}
Definition __true : __bool := False.
Definition __false : __bool := True.
\end{alltt}
\adviwait
\begin{alltt}
Definition __implies (A B : __bool) : __bool := ~(B -> A).
\end{alltt}
\adviwait
\begin{alltt}
\red{Definition _infer (A : __bool) : Type := ~A.}
\end{alltt}
\endgroup
\medskip
%\adviwait

\begingroup
\small
\begin{alltt}
Definition __not (A : __bool) : __bool := __implies A __false.
\end{alltt}
\begin{alltt}
\green{Lemma __notnot_elim:
  forall A : __bool, _infer (__not (__not A)) -> _infer A.}
\end{alltt}
\endgroup

\if 0
\vbox to 0pt{
\vspace{-\bigskipamount}
\begingroup
\small
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}
Record \red{__bool} : Type := \{\green{__neg} : \blue{Prop}\}.\adviwait
Definition \green{_neg} := Build___bool.
\advirecord{b}{Definition _infer (A:__bool) : Type := not (__neg A).}
\end{alltt}

$$\xymatrix{
*+\txt{\texttt{\blue{Prop}}}
%\ar@(ul,dl)[]_{\txt{\texttt{not}}}
\ar@/^1pc/[rr]^{\txt{\texttt{\green{\_neg}}}}
&&
*+\txt{\texttt{\red{\_\_bool}}}
\ar@/^1pc/[ll]^{\txt{\texttt{\green{\_\_neg}}}}
%\ar@(dr,ur)[]_{\txt{\texttt{\_\_not}}}
}\bigskip\adviwait\adviplay{b}\adviwait$$

\begin{alltt}
Definition \red{__false} : __bool := _neg True.
Definition \red{__implies} (A B : __bool) : __bool :=
  _neg (not (__neg B -> __neg A)).\adviwait
\end{alltt}
\begin{alltt}
Definition \red{__not} (A : __bool) : __bool :=
  __implies A __false.
Definition \red{__true} : __bool := __not __false.
\end{alltt}
\endgroup
\vss
}
\fi

\vfill
\end{slide}

\begin{slide}
\slidetitle{the dual of a partial setoid}
\vbox to 0pt{
\vspace{-\bigskipamount}
\begin{itemize}
%\item[$\bullet$]
%\textbf{setoid}
%
%$(A, \sim)$\quad where $\sim$ is a relation on $A$
%\adviwait

\item[$\bullet$]
\strut\advirecord{c1}{\rlap{\textbf{setoid}}}\advirecord{c2}{\textbf{partial} setoid}

$(\green{A}, \sim)$\quad where $\sim$ is \advirecord{c3}{\rlap{an equivalence relation on $A$}}\advirecord{c4}{a \textbf{partial} equivalence relation on $A$}
\adviplay{c1}\adviplay{c3}
\adviwait
\adviplay[white]{c1}\adviplay[white]{c3}
\adviplay{c2}\adviplay{c4}
\adviwait

\green{$a$ is `proper element' when $a \sim a$}
\adviwait

\item[$\bullet$]
\textbf{dual}

partial setoid of functions $\red{f} : \green{A} \to \blue{\texttt{\_\_bool}}$
\adviwait
\begin{center}
\vspace{-\bigskipamount}
%\vspace{-\smallskipamount}
\begin{picture}(220,90)(-10,0)
%\put(-10,0){\gray{\framebox(230,90){}}}

\put(20,10){\makebox(0,0)[lb]{\lightgray{\rule{25\unitlength}{10\unitlength}}}}
\put(50,10){\makebox(0,0)[lb]{\lightgray{\rule{25\unitlength}{10\unitlength}}}}
\put(80,10){\makebox(0,0)[lb]{\lightgray{\rule{25\unitlength}{10\unitlength}}}}
\put(110,10){\makebox(0,0)[lb]{\lightgray{\rule{25\unitlength}{10\unitlength}}}}
\put(140,10){\makebox(0,0)[lb]{\lightgray{\rule{25\unitlength}{10\unitlength}}}}
%\put(20,10){\framebox(25,10){}}
\put(50,10){\framebox(25,10){}}
\put(80,10){\framebox(25,10){}}
\put(110,10){\framebox(25,10){}}
%\put(140,10){\framebox(25,10){}}
\put(180,15){\makebox(0,0){\green{$A$}}}
\adviwait

\textcolor{red}
{
\put(18,35){\line(1,0){60}}
\put(78,35){\line(0,1){20}}
\put(78,55){\line(1,0){29}}
\put(107,55){\line(0,-1){20}}
\put(107,35){\line(1,0){60}}
}
\put(190,36){\makebox(0,0){\small\blue{\texttt{\_\_false}}}}
\put(190,56){\makebox(0,0){\small\blue{\texttt{\_\_true\ }}}}
\put(110,55){\gray{\line(1,0){57}}}
\put(18,55){\gray{\line(1,0){57}}}
\put(80,35){\gray{\line(1,0){25}}}

\put(8,30){\vector(0,1){30}}
\put(8,68){\makebox(0,0){\textcolor{red}{$f$}}}
\adviwait
\end{picture}
%\vspace{-\smallskipamount}
\end{center}
$\begin{array}{rcl}
f \sim g &\!\!\Leftrightarrow\!\!&
\exists \hspace{.4pt} a.\, f(a) \land (\forall b.\, f(b) \Leftrightarrow a \sim b) \land (\forall b.\, g(b) \Leftrightarrow a \sim b) \adviwait\\
\red{\iota f.\, P(f)} &\red{\!\!=\!\!}&
\red{\lambda a.\, (\exists f.\, P(f)) \land (\forall f.\, P(f) \Rightarrow (\forall b.\, f(b) \Leftrightarrow a \sim b))}
\end{array}$

\end{itemize}
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{{\dots} and can you really not do better than this?}
\red{Coq formalization heavily uses impredicativity of \texttt{Prop}}
\medskip

\textbf{questions:}
\begin{itemize}
\item[$\bullet$]
is it possible to do the same in a predicative system?

\green{Agda \\ NuPRL}
\medskip
\adviwait

\item[$\bullet$]
is it possible to do this for another Farmer system: \blue{STMM}

\green{\blue{S}et \blue{T}heory for \blue{M}echanized \blue{M}athematics}
\medskip
\adviwait

{axiom \green{NBG31} = the axiom of choice$\;\,$?}
\adviwait

maybe work in: \red{G\"odel's constructible universe $L$}

\end{itemize}

\vfill
\end{slide}

\end{document}