\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}{-2}
\begin{slide}
\sectiontitle{newsflash}
\slidetitle{Simon$\,$! mice$\,$!}

\begin{center}
\includegraphics{/home/freek/talks/lv-2004/simon00l.eps}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\Large inductive predicates}

\red{logical verification} \\
week 5 \\
2004 10 06

\end{slide}

\begin{slide}
\sectiontitle{recap in abstracto}
\slidetitle{what is an inductive type?}
\vspace{0pt}

\begin{center}
`\red{minimal} set such that \textbf{constructors} exist'
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{`free'}
\vspace{0pt}

\begin{center}
all terms built with only constructors are \red{different}
\end{center}
\bigskip
\bigskip

inductive type $=$ \green{set of all `terms'}

\vfill
\end{slide}

\begin{slide}
\slidetitle{what do you get?}
\begin{itemize}
\item[$\bullet$]
a new type

\qquad \green{\texttt{nat}}

\item[$\bullet$]
constructor functions

\qquad \green{\texttt{O }}and\green{\texttt{ S}} 

\item[$\bullet$]
\verb|match| $\;+\;$ \red{$\iota$-reduction}

\qquad \green{\texttt{match }{\dots} \texttt{with O => }{\dots} \texttt{| S m => }{\dots} \texttt{end}}

\item[$\bullet$]
\red{induction principle}
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{universes}
$$
\xymatrix{
\txt{\blue{terms}}\ar@{-}[d] & \txt{\blue{types}}\ar@{-}[d] & \txt{\blue{kinds}}\ar@{-}[d] \\
\texttt{S O}\ar@{}[r]|-{\mbox{\large\textbf{:}}}\ar@{-}[dd] & \green{\texttt{nat}}\ar@{}[r]|-{\mbox{\large\textbf{:}}}\ar@{-}[dd] & \red{\texttt{Set}}\ar@{}[dr]|-{\mbox{\large\textbf{:}}}\ar@{-}[dd] \\
&&& \red{\texttt{Type}}\ar@{}[r]|-{\mbox{\large\textbf{:}}} & \red{\texttt{Type}}\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{-2.1em}
$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{inductive types can be defined in each universe}

\def\sfdots{\textsf{\dots}}

\begin{alltt}
Inductive {\sfdots} : \red{Set} :=
  {\sfdots}
\end{alltt}
\bigskip

\begin{alltt}
Inductive {\sfdots} : \red{Prop} :=
  {\sfdots}
\end{alltt}
\bigskip

\begin{alltt}
Inductive {\sfdots} : \red{Type} :=
  {\sfdots}
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{inductive types for datatypes}
\slidetitle{booleans}
\begin{alltt}
Inductive \red{bool} : Set :=
  | \green{true} : bool
  | \green{false} : bool.
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{enumeration types}
\begin{alltt}
Inductive \red{color} : Set :=
  | \green{black} : color
  | \green{white} : color
  | \green{red} : color
  | \green{yellow} : color
  | \green{green} : color
  | \green{blue} : color
  | \green{brown} : color
  | \green{orange} : color
  | \green{purple} : color
  | \green{pink} : color
  | \green{gray} : color.
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{singleton type}
\begin{alltt}
Inductive \red{unit} : Set :=
    \green{tt} : unit.
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{empty type}
\begin{alltt}
Inductive \red{Empty_set} : Set :=
    .
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{natural numbers}
\begin{alltt}
Inductive \red{nat} : Set :=
  | \green{O} : nat
  | \green{S} : nat -> nat.
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{linear lists of natural numbers}
\begin{alltt}
Inductive \red{natlist} : Set :=
  | \green{nil} : natlist
  | \green{cons} : nat -> natlist -> natlist.
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{polymorphic linear lists}
\begin{alltt}
Inductive \red{list} \blue{(A : Set)} : Set :=
  | \green{nil} : list A
  | \green{cons} : A -> list A -> list A.
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{unlabeled binary trees}
\begin{alltt}
Inductive \red{bintree} : Set :=
  | \green{leaf} : bintree
  | \green{node} : bintree -> bintree -> bintree.
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{polymorphic labeled binary trees}
\begin{alltt}
Inductive \red{bintree} \blue{(A B : Set)} : Set :=
  | \green{leaf} : B -> bintree A B
  | \green{node} : A -> bintree A B -> bintree A B -> bintree A B.
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{option type}
\begin{alltt}
Inductive \red{option} \blue{(A : Set)} : Set :=
  | \green{Some} : A -> option A
  | \green{None} : option A.
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{disjoint union of two types}
\begin{alltt}
Inductive \red{sum} \blue{(A B : Set)} : Set :=
  | \green{inl} : A -> sum A B
  | \green{inr} : B -> sum A B.
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{cartesian product of two types}
\begin{alltt}
Inductive \red{prod} \blue{(A B : Set)} : Set :=
    \green{pair} : A -> B -> prod A B.
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{inductive types for logic}
\slidetitle{Curry-Howard-de Bruijn isomorphism}
\vspace{0pt}

\begin{center}
proposition is \red{true} \\
$\Updownarrow$ \\
type is \red{inhabited}
\end{center}

\vfill
\end{slide}

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

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

\begin{slide}
\slidetitle{conjunction}
\begin{alltt}
Inductive \red{and} (A B : Prop) : Prop :=
    \green{conj} : A -> B -> and A B.
\end{alltt}
\adviwait
\bigskip

\def\back{\char`\\}
\begin{alltt}
\blue{Notation "A /{\back} B" := (and A B) : type_scope.}
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{disjunction}
\begin{alltt}
Inductive \red{or} (A B : Prop) : Prop :=
  | \green{or_introl} : A -> or A B
  | \green{or_intror} : B -> or A B 
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{datatypes in \texttt{Set} $\enskip\,\longleftrightarrow\,\enskip$ logic in \texttt{Prop}}
\vspace{0pt}

\begin{center}
\begin{tabular}{rcl}
\texttt{unit} &$\red{\longleftrightarrow}$& \texttt{True} \\
\texttt{Empty\char`\_set} &$\red{\longleftrightarrow}$& \texttt{False} \\
\texttt{prod} &$\red{\longleftrightarrow}$& \texttt{and} \\
\texttt{sum} &$\red{\longleftrightarrow}$& \texttt{or}
\end{tabular}
\end{center}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{inductive predicates}
\slidetitle{Curry-Howard-de Bruijn isomorphism}
\vspace{0pt}

\begin{center}
predicate is \red{true} \\
$\Updownarrow$ \\
inductive type is \red{inhabited}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{even natural numbers}
\begin{alltt}
Inductive \red{even} : nat -> Prop :=
  | \green{even_O} : even O
  | \green{even_S_S} : forall n, even n -> even (S (S n)).
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{even and odd natural numbers}
\begin{alltt}
Inductive \red{even} : nat -> Prop :=
  | \green{even_O} : even O
  | \green{even_S} : forall n, odd n -> even (S n)
with \red{odd} : nat -> Prop :=
    \green{odd_S} : forall n, even n -> odd (S n).
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{$n \le m$}
\begin{alltt}
Inductive \red{le} (n:nat) : nat -> Prop :=
  | \green{le_n} : le n n
  | \green{le_S} : forall m:nat, le n m -> le n (S m).
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{sorted lists of natural numbers}
\begin{alltt}
Inductive \red{Sorted} : natlist -> Prop :=
  | \green{Sorted_nil} : Sorted nil
  | \green{Sorted_one} : forall n : nat, Sorted (cons n nil)
  | \green{Sorted_cons} :
      forall (l : natlist) (n m : nat),
        Sorted (cons m l) -> le n m ->
          Sorted (cons n (cons m l)). 
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Leibniz equality}
\begin{alltt}
Inductive \red{eq} (A : Set) (x : A) : A -> Prop :=
    \green{refl_equal} : eq A x x.
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{coq tactics}
\slidetitle{applying the induction principle}
\begin{itemize}
\item[$\bullet$]
\texttt{elim}
\item[$\bullet$]
\texttt{\red{induction}}
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{inversion}
\begin{center}
\green{\texttt{Lemma not\char`\_even\char`\_1 :\ \char`\~(even 1).}}
\end{center}
\bigskip

\begin{itemize}
\item[$\bullet$]
\texttt{\red{inversion}}
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{what does inversion do?} % \rlap{\gray{\qquad (Christine Paulin)}}\qquad}
\slidetitle{abstract explanation}
elimination proves universally quantified properties
$$\green{\forall x_1,\dots,x_l.\,\red{\texttt{I}}(x_1,\dots,x_l) \Rightarrow P(x_1,\dots,x_l)}$$
\begin{itemize}
\item[$\bullet$]
what to do with $\green{\red{\texttt{I}}(t_1,\dots,t_l) \Rightarrow P(t_1,\dots,t_l)}$ when $\green{t_i}$ are not variables?
\adviwait
\item[$\bullet$]
generalize to $\green{\forall x_1,\dots,x_l.\,\red{\texttt{I}}(x_1,\dots,x_l) \Rightarrow P(x_1,\dots,x_l)}$
\adviwait
\item[$\bullet$]
what to do if the generalization does not hold?
\adviwait
\item[$\bullet$]
find another one which works:
%\adviwait
$$\hspace{-1em}\green{\forall x_1,\dots,x_l.\,\red{\texttt{I}}(x_1,\dots,x_l) \Rightarrow \underbrace{(x_1,\dots,x_l) = (t_1,\dots,t_l) \Rightarrow P(t_1,\dots,t_l)}}\hspace{-1em}$$
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{example}
constructors
$$\green{\mbox{{\texttt{even\char`\_O}}} \,:\, \texttt{even}\,(0) \qquad
\mbox{{\texttt{even\char`\_S\char`\_S}}} \,:\, \forall n.\, \texttt{even}\,(n) \Rightarrow \texttt{even}\,(n + 2)}$$
induction principe
$$\green{
P(0)
\qquad
\forall n.\,\texttt{even}\,(n) \Rightarrow P(n) \Rightarrow P(n + 2)
\over
\forall n.\, \texttt{even}\,(n) \Rightarrow P(n)
}\medskip$$
$$\red{\texttt{even}\,(1) \Rightarrow \bot\rlap{\qquad\mbox{\black{?}}}}\leqno{\mbox{how to prove}}$$
$$\green{P(n) = \red{n = 1 \Rightarrow \bot}}\leqno{\mbox{take:}}$$

\vfill
\end{slide}

\end{document}