\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{slidelightblue}{rgb}{.8,.8,1}
\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\lightblue#1{\textcolor{slidelightblue}{#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}{\large\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}$}

\def\tto{\to\hspace{-5pt}\!\!\to}
\def\{{\char`\{}
\def\}{\char`\}}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large inductive types}

\red{logical verification} \\
week 4 \\
2004 09 29

\end{slide}

\begin{slide}
\sectiontitle{outline}
\slidetitle{subject}
\medskip

\begin{center}
\textbf{type theory}
$=$
typed $\lambda$-calculus
$+$
\red{inductive types}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Curry-Howard-de Bruijn}

\begin{center}
\begin{tabular}{rcl}
\textbf{logic} &$\sim$& \textbf{type theory} \\
\noalign{\bigskip}
formula &$\sim$& type \\
proof &$\sim$& term \\
\green{detour elimination} &$\sim$& \green{$\beta$-reduction} \\
\noalign{\adviwait\bigskip}
minimal logic &$\sim$& simply typed $\lambda$-calculus \adviwait\\
intuitionistic logic &\advirecord{a3}{$\sim$}& \advirecord{a1}{simply typed $\lambda$-calculus $+$ \red{inductive types}}$\!\!\!\!$ \\
classical logic &\advirecord{a4}{$\sim$}& \advirecord{a2}{{{\dots} $+$ exceptions}}
\end{tabular}
\end{center}
\adviwait
\adviplay{a1}
\adviplay{a3}
%\adviwait
\adviplay{a2}
\adviplay{a4}
\vfill
\end{slide}

\begin{slide}
\slidetitle{examples of inductive types}
\begin{itemize}
\item[$\bullet$]
\red{booleans}
\item[$\bullet$]
\red{natural numbers}
\item[$\bullet$]
integers
\item[$\bullet$]
pairs
\item[$\bullet$]
\red{linear lists}
\item[$\bullet$]
binary trees
\medskip
\item[$\bullet$]
\green{logical operations}
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{inductive types}
\begin{itemize}
\item[$\bullet$]
\red{types}
%\adviwait
\item[$\bullet$]
\textbf{recursive functions}

\begin{itemize}
\item
\red{definition using pattern matching}
\item
\blue{$\iota$-reduction} \green{$=$ evaluation of recursive functions}
%\medskip
%\adviwait
%\item
%\red{recursion principle}
\end{itemize}

\item[$\bullet$]
proof by cases \\
proof by \textbf{induction}

\begin{itemize}
\item
\red{induction principle}
\end{itemize}
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{examples}
\slidetitle{booleans: type}

{Coq definition:}
\medskip

\begin{quote}
\begin{alltt}
Inductive \red{bool} : Set :=
  \green{true} : bool
| \green{false} : bool.
\end{alltt}
\end{quote}

\vfill
\end{slide}

\begin{slide}
\slidetitle{booleans: recursive function}

definition of negation:
\medskip

\begin{quote}
\begin{alltt}
Definition \red{neg} (b : bool) : bool :=
  \blue{match} b with
    \green{true} => false
  | \green{false} => true
  end.
\end{alltt}
\end{quote}
\adviwait
\bigskip

\blue{$\iota$-reduction}
$$\verb|neg true| \enskip\tto\enskip \verb|false|$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{booleans: proof by cases}
\vspace{-\medskipamount}

\begin{center}
\red{\texttt{forall b :\ bool, neg (neg b) = b}}
\end{center}
\bigskip

\textbf{tactics}
\begin{itemize}
%\item[$\bullet$]
%\verb|intro.|
%\begin{quote}
%\green{
%\texttt{A -> }\dots \\
%\texttt{forall x :\ A, }\dots
%}
%\end{quote}

\item[$\bullet$]
\verb|elim b.|
\item[$\bullet$]
\verb|simpl.|
\item[$\bullet$]
\verb|reflexivity.|
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{booleans: induction principle}
\vspace{-\medskipamount}

\begin{alltt}
  \red{bool_ind} :
    forall P : bool -> Prop,
      P true -> P false -> forall b : bool, P b
\end{alltt}
\bigskip
\medskip

\verb|  |\green{$\forall P\in (\mbox{bool}{\to}\mbox{Prop}).\;\; P(\mbox{true}) \Rightarrow P(\mbox{false}) \Rightarrow \;\forall b\in \mbox{bool}.\, P(b)$}
\vfill
\end{slide}

\begin{slide}
\slidetitle{natural numbers: type}

{Coq definition:}
\medskip

\begin{quote}
\begin{alltt}
Inductive \red{nat} : Set :=
  \green{O} : nat
| \green{S} : \blue{nat} -> nat.
\end{alltt}
\end{quote}

\vfill
\end{slide}

\begin{slide}
\slidetitle{natural numbers: recursive function}

definition of plus:
\medskip

\begin{quote}
\begin{alltt}
\blue{Fixpoint} \red{plus} (n m : nat) \{struct n\} : nat :=
  match n with
    O => m
  | S p => S (\blue{plus} p m)
  end.
\end{alltt}
\end{quote}
\adviwait
\bigskip

\blue{$\iota$-reduction}
$$\verb|plus (S O) (S O)| \enskip\tto\enskip \verb|S (plus O (S O))| \enskip\tto\enskip \verb|S (S O)|$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{natural numbers: proof by induction}
\vspace{-\medskipamount}

\begin{center}
\red{\texttt{forall n :\ nat, plus n O = n}}
\end{center}
\bigskip

\textbf{tactics}
\begin{itemize}
\item[$\bullet$]
elim n.
\item[$\bullet$]
induction n.
\item[$\bullet$]
rewrite IHn.
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{natural numbers: induction principle}
\vspace{-\medskipamount}

\begin{alltt}
  \red{nat_ind} :
    forall P : nat -> Prop,
      P 0 -> (forall n : nat, P n -> P (S n)) ->
        forall n : nat, P n
\end{alltt}
\bigskip
\medskip

\verb|  |\green{$\forall P.\;\; P(0) \Rightarrow\; (\forall n\in{\mathbb N}.\; P(n) \Rightarrow P(n + 1)) \Rightarrow \;\forall n\in{\mathbb N}.\, P(n)$}
\vfill
\end{slide}

\begin{slide}
\slidetitle{lists: type}

{Coq definition:}
\medskip

\begin{quote}
\begin{alltt}
Inductive \red{natlist} : Set :=
  \green{nil} : natlist
| \green{cons} : nat -> natlist -> natlist
\end{alltt}
\end{quote}
\bigskip
\bigskip

\strut\phantom{the term}\llap{the list} $\;\red{1, 2, 3, 4}\;\,$ is encoded by \\
\phantom{the term}$\;$ \red{\texttt{cons} \texttt{1} \texttt{(cons} \texttt{2} \texttt{(cons} \texttt{3} \texttt{(cons 4 nil)))}}

\vfill
\end{slide}

\begin{slide}
\slidetitle{lists: recursive function}

definition of append:
\medskip

\begin{quote}
\begin{alltt}
Fixpoint \red{append} (l k : natlist) \{struct l\} : natlist :=\toolong
  match l with
    nil => k
  | cons n l' => cons n (append l' k)
  end.
\end{alltt}
\end{quote}
\adviwait
\bigskip

\blue{$\iota$-reduction}
$$\begin{array}{rcl} \verb|append (cons 0 nil) nil| &\enskip\tto\enskip& \verb|cons 0 (append nil nil)| \\ &\enskip\tto\enskip& \verb|cons 0 nil| \end{array}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{lists: induction principle}
\vspace{-\medskipamount}

\begin{alltt}
\red{natlist_ind} :
  forall P : natlist -> Prop, P nil ->
    (forall (n : nat) (l : natlist), P l -> P (cons n l)) ->\toolong
      forall l : natlist, P l
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{\gray{second hour}}
\slidetitle{truth: type}

{Coq definition:}
\medskip

\begin{quote}
\begin{alltt}
Inductive \red{True} : \blue{Prop} :=
  \green{I} : True.
\end{alltt}
\end{quote}
\vfill
\end{slide}

\begin{slide}
\slidetitle{falsity: type}

{Coq definition:}
\medskip

\begin{quote}
\begin{alltt}
Inductive \red{False} : Prop :=
  .
\end{alltt}
\end{quote}
\vfill
\end{slide}

\begin{slide}
\slidetitle{falsity: induction principle}
\vspace{-\medskipamount}

\begin{alltt}
  \red{False_ind} :
    forall P : Prop, False -> P
\end{alltt}
\adviwait
\bigskip
\medskip

$$
{
\begin{array}{c}
\vdots \\
\bot
\end{array}
\over
\strut P
}
\enskip
\red{E\bot}
\bigskip
$$

\vfill
\end{slide}

\begin{slide}
\sectiontitle{universes}
\slidetitle{\texttt{Prop} versus \texttt{Set}}

$$
\xymatrix{
\texttt{S O}\ar@{}[r]|-{\mbox{\large\textbf{:}}} & \green{\texttt{nat}}\ar@{}[r]|-{\mbox{\large\textbf{:}}} & \red{\texttt{Set}}\ar@{}[dr]|-{\mbox{\large\textbf{:}}} \\
&&& \red{\texttt{Type}\advirecord{b1}{\,_0}}\ar@{}[r]|-{\mbox{\large\textbf{:}}} & \red{\texttt{Type}\advirecord{b2}{\,_1}}\ar@{}[r]|-{\mbox{\large\textbf{:}}} & \strut\red{\dots} \\
\texttt{fun x:A => x}\ar@{}[r]|-{\mbox{\large\textbf{:}}} & \green{\texttt{A -> A}}\ar@{}[r]|-{\mbox{\large\textbf{:}}} & \red{\texttt{Prop}}\ar@{}[ur]|-{\mbox{\large\textbf{:}}}
}\hspace{-3.3em}
\adviwait
\adviplay{b1}
\adviplay{b2}
$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{types}
\vspace{-\medskipamount}

\begin{center}
\texttt{fun x :\ \green{A} => }\dots$\,$\texttt{\ \ }

\texttt{forall x :\ \green{A}$\,$, }\dots\texttt{\ \ \ \ \ \ \ \ }
\end{center}
\bigskip

\begin{center}
\texttt{\ \ \ \ \ \ \ \ \ \green{A} :\ \red{Prop}}\phantom{\dots}$\,$

\texttt{\ \ \ \ \ \ \ \ \green{A} :\ \red{Set}}\phantom{\dots}$\,$

\texttt{\ \ \ \ \ \ \ \ \ \green{A} :\ \red{Type}}\phantom{\dots}$\,$
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{Prop} versus \texttt{bool}}

\begin{center}
\texttt{\ \ \ \ \ \blue{I} \ :\ \ \red{True} \ :\ \ \green{Prop}}
\medskip

\texttt{\red{true} \ :\ \ \green{bool} \ :\ \ Set\ }
\end{center}
\bigskip
\medskip

inductive types: \texttt{\red{True}} and \texttt{\green{bool}}
\bigskip

\red{true} is not a type at all:

Curry-Howard-de Bruijn only for \texttt{\red{True}} and \texttt{\green{Prop}}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{datatypes in $\lambda$-calculus}
\slidetitle{church natural numbers}
encoding of natural numbers in untyped $\lambda$-calculus
\begin{eqnarray*}
\noalign{\medskip}
0\, &=& \lambda f.\, \lambda x.\, x \\
1\, &=& \lambda f.\, \lambda x.\, f\, x \\
2\, &=& \lambda f.\, \lambda x.\, f\, (f\, x) \\
\vdots\, && \\
\noalign{\bigskip}
S &=& \lambda n.\, \lambda f.\, \lambda x.\, f\, (n\, f\, x) \\
%S &=& \lambda n.\, \lambda f.\, \lambda x.\, n\, f\, (f\, x) \\
\end{eqnarray*}

\vfill
\end{slide}

\begin{slide}
\slidetitle{church natural numbers can be typed}
type \green{$A$}
\begin{eqnarray*}
\noalign{\medskip}
0\, &=& \lambda f \green{\;: A \to A}.\; \lambda x \green{\;: A}.\; x \quad\red{\textbf{:}\quad (A \to A) \to (A \to A)} \\
S &=& \lambda n \red{\;: (A \to A) \to (A \to A)}.\; \lambda f \green{\;: A \to A}.\; \lambda x \green{\;: A}.\; f\, (n\, f\, x)
\end{eqnarray*}
\vspace{-\bigskipamount}
\medskip

\red{type of church natural numbers}
$$\red{(A \to A) \to (A \to A)}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{inductive natural numbers}
\vspace{-\medskipamount}

\begin{quote}
\begin{alltt}
Inductive \red{nat} : Set :=
  \green{O} : nat
| \green{S} : nat -> nat.
\end{alltt}
\end{quote}

\vfill
\end{slide}

\begin{slide}
\slidetitle{why inductive types built-in if we can define them?}
\begin{itemize}
\item[$\bullet$]
more efficient

\item[$\bullet$]
\red{different reduction behavior}

\end{itemize}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{a more involved coq proof}
\slidetitle{another function on lists: reverse}
\vspace{-\medskipamount}

\begin{quote}
\begin{alltt}
Fixpoint \red{reverse} (l : natlist) : natlist :=
  match l with
    nil => nil
  | cons n l' => \green{append} (\red{reverse} l') (cons n nil)
  end.
\end{alltt}
\end{quote}

\vfill
\end{slide}

\begin{slide}
\slidetitle{reverse is an involution}
\vspace{-\medskipamount}

\begin{center}
\red{\texttt{forall l :\ natlist, reverse (reverse l) = l}}
\end{center}

\vfill
\end{slide}

\end{document}