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

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large propositional logic}

\red{logical verification} \\
week 1 \\
2004 09 08

\end{slide}

\begin{slide}
%\sectiontitle{first hour}
\slidetitle{who}
\begin{center}
\begin{tabular}{cc}
\includegraphics[height=75pt]{/home/freek/talks/lv-2004/femke.eps} & \advirecord{a1}{\includegraphics[height=75pt]{/home/freek/talks/lv-2004/babum.eps}} \\
\noalign{\vspace{-.6em}}
Femke & 
\adviwait
\adviplay{a1}
\adviwait \\
\noalign{\vspace{.8em}}
\includegraphics[height=75pt]{/home/freek/talks/lv-2004/freek.eps} & \advirecord{a2}{\includegraphics[height=75pt]{/home/freek/talks/lv-2004/paulien.eps}} \\
\noalign{\vspace{-.6em}}
Freek &
\adviwait
\adviplay{a2}
Paulien
\end{tabular}
\vspace{-1em}
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{what}
\begin{itemize}
\item[$\bullet$]
13 lectures
\medskip
\item[$\bullet$]
practical work
\begin{itemize}
\item
Coq proofs \& paper proofs
\item
\red{9 out of 12}
\end{itemize}
\item[$\bullet$]
\medskip
\red{final test}
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{stuff}
\begin{itemize}
\item[$\bullet$]
\red{hand out}
\begin{itemize}
\item
course notes
\item
exercises
\end{itemize}
\item[$\bullet$]
\red{web page}
\begin{itemize}
\item
hand out
\item
files for the exercises
\item
solutions for the exercises
\item
slides
\item
old tests
\end{itemize}
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{where}
\begin{itemize}
\item[$\bullet$]
lectures: \red{S201} \\
Coq lab: \red{S345}

\item[]
\url{http://www.cs.vu.nl/~tcs/al/} \\
\red{\url{tcs@cs.vu.nl}}
\smallskip

\item[$\bullet$]
Freek:

tuesdays \& wednesdays: U333 \\
\url{freek@cs.ru.nl}
\end{itemize}

\vfill
\end{slide}


\begin{slide}
\slidetitle{topic}

computer science
\medskip
\adviwait

$\qquad$formal methods
\medskip
\adviwait

$\qquad\qquad$proof assistants
\medskip
\adviwait

$\qquad\qquad\qquad$\red{type theory}

\vfill
\end{slide}

\begin{slide}
\slidetitle{examples of applications of formal methods}

\begin{itemize}
\item[$\bullet$]
Intel bug
\item[$\bullet$]
driverless train
\item[$\bullet$]
spacecraft
\item[$\bullet$]
credit cards
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{proof assistants}
\begin{itemize}
\item[$\bullet$]
PVS
\item[$\bullet$]
\red{Coq}/NuPRL
\item[$\bullet$]
ACL2
\item[$\bullet$]
HOL/Isabelle
\item[$\bullet$]
Mizar
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{what we will do here}

\begin{center}
\begin{tabular}{rcccc}
&&& \hbox to 0pt{\hss\green{{\small Curry-Howard-de Bruijn\enskip}}\hss} \\
\noalign{\vspace{-\medskipamount}}
&&& \hbox to 0pt{\hss\green{{\small isomorphism\enskip}}\hss} \\
\noalign{\vspace{-\smallskipamount}}
&& $\quad$\textbf{logic}$\quad$ &$\quad\longleftrightarrow\qquad$& \textbf{lambda calculus} \\
\noalign{\vspace{-\smallskipamount}}
&& natural deduction && \blue{`type theory'} \\
\noalign{\medskip\smallskip}
on paper &$\quad$& \red{$\bullet$} && \red{$\bullet$} \\
\noalign{\bigskip}
in Coq && \red{$\bullet$} && \red{$\bullet$}
\end{tabular}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{logics}
\begin{itemize}
\item[$\bullet$]
\red{the systems in this course}
\smallskip

\begin{tabular}{rcl}
propositional logic &\gray{$\longleftrightarrow$}& calculus called $\;\lambda{\to}$ \\
predicate logic &\gray{$\longleftrightarrow$}& calculus called $\;\lambda P$ \\
2nd order propositional logic &\gray{$\longleftrightarrow$}& calculus called $\;\lambda 2$
\end{tabular}
\medskip
\end{itemize}
$$
\xymatrix@!@=.5em{
 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
   & & \green{\lambda C} \ar@{-}[dd]
\\
 \red{\lambda2} \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
\\
 & \lambda\underline\omega \ar@{-}'[r][rr]
 & & \lambda P\underline\omega
\\
 \red{\lambda{\to}} \ar@{-}[rr]\ar@{-}[ur]
 & & \red{\lambda P} \ar@{-}[ur]
}
\vspace{-2em}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{and also}

\begin{itemize}
\item[$\bullet$]
\red{inductive types}
\begin{itemize}
\item
built-in
\item
higher order encoding
\end{itemize}
\medskip
\item[$\bullet$]
\red{program extraction}
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{today}

\begin{itemize}
\item[]
\gray{\phantom{second order}\llap{first order}} \red{propositional logic}
\item[]
\gray{\phantom{second order}\llap{first order}} predicate logic
\item[]
second order \gray{propositional logic}
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{formulas}

\begin{quote}
$
\begin{array}{ccl}
A \to B \\
\bot \\
\top \\
\neg A &\qquad& \red{:= \quad A \to \bot} \\
A \land B \\
A \lor B
\end{array}
$
\end{quote}

\vfill
\end{slide}

\begin{slide}
\slidetitle{logical rules}

two kinds of rules

\begin{itemize}
\item[$\bullet$]
\red{introduction} rules
\item[$\bullet$]
\red{elimination} rules
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{rules for $\to$}
introduction rule
$$
{
\begin{array}{c}
[A^x] \rlap{\hspace{3.5cm} \green{assumption}}\\
\vdots \\
B
\end{array}
\over
\strut
\red{A \to B}
}
\enskip
\green{I[x]{\to}}
$$
\adviwait

elimination rule
$$
{
\begin{array}{c}
\vdots \\
A \to B
\end{array}
\qquad
\begin{array}{c}
\vdots \\
A
\end{array}
\over
\strut
\red{B}
}
\enskip
\green{E{\to}}
$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{example}

$$\red{A \to A}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{bigger example}

$$\red{((A \to B) \to (C \to D)) \to C \to B \to D}$$

\vfill
\end{slide}

\begin{slide}
\sectiontitle{second hour}
\slidetitle{rules for the other connectives}

$\bot$ elimination

$\top$ introduction

$\neg$ introduction \\
$\neg$ elimination \\
%\phantom{$\neg$ }%
\green{excluded middle} \hspace{4em} \green{${A \lor \neg A}$}

$\land$ introduction \\
$\land$ elimination, left rule \\
$\land$ elimination, right rule

$\lor$ introduction, left rule \\
$\lor$ introduction, right rule \\
$\lor$ elimination

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

\begin{slide}
\slidetitle{the rules for $\lor$}
$\lor$ introduction
$$
{
\begin{array}{c}
\vdots \\
A
\end{array}
\over
\strut
\red{A \lor B}
}
\enskip
\green{Il{\lor}}
\hspace{5em}
{
\begin{array}{c}
\vdots \\
B
\end{array}
\over
\strut
\red{A \lor B}
}
\enskip
\green{Ir{\lor}}
$$
\adviwait

$\lor$ elimination
$$
{
\begin{array}{c}
\vdots \\
A \lor B
\end{array}
\quad
\begin{array}{c}
\vdots \\
A \to C
\end{array}
\quad
\begin{array}{c}
\vdots \\
B \to C
\end{array}
\over
\strut
\red{C}
}
\enskip
\green{E{\lor}}
$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{example with $\lor$}

$$\red{(A \lor B) \to (B \lor A)}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{Coq}
\begin{itemize}
\item[$\bullet$]
\red{goals}

Coq tells you what is left to be proved
\medskip

\item[$\bullet$]
\red{tactics}

you tell Coq how to prove it
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Coq term syntax}

\begin{quote}
\begin{tabular}{c}
\verb|A -> B| \\
\verb|False| \\
\verb|True| \\
\verb|~A|\phantom{\texttt{\char`\~}} \\
\verb|A /\ B| \\
\verb|A \/ B|
\end{tabular}
\end{quote}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the Coq language}
\textbf{commands}

\begin{tabular}{l}
$\bullet$\enskip \verb|Parameter| \\
$\bullet$\enskip \verb|Lemma| \\
$\bullet$\enskip \verb|Qed|
\end{tabular}

\medskip
\textbf{tactics}

\begin{tabular}{lcl}
$\bullet$\enskip \verb|intro| &$\hspace{4em}$& \green{$I[x]{\to}$} \\%\enskip \green{$I[x]\neg$}\\
$\bullet$\enskip \verb|apply| && \green{$E{\to}$} \\%\enskip \green{$E\neg$} \\
$\bullet$\enskip \verb|elim| && \green{$E\bot$}\enskip \green{$El\land$}\enskip \green{$Er\land$}\enskip \green{$E\lor$} \\
$\bullet$\enskip \verb|exact| && \textsl{assumption} \\
$\bullet$\enskip \verb|split| && \green{$I\land$} \\
$\bullet$\enskip \verb|left|\enskip \verb|right| && \green{$Il\lor$}\enskip \green{$Ir\lor$}
\end{tabular}

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

\begin{slide}
\slidetitle{interfaces}
\begin{itemize}
\item[$\bullet$]
\verb|coqtop| $+$ \verb|coqc|

`command line'
\medskip

\item[$\bullet$]
\verb|xemacs| + \red{Proof General}
\item[$\bullet$]
\verb|coqide|
\item[$\bullet$]
\verb|pcoq|
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{example}
\smallskip
\begin{center}
\red{\texttt{A -> A}}
\end{center}

\bigskip
\bigskip
\begin{itemize}
\item[$\bullet$]
with \verb|coqtop|
\adviwait
\bigskip
\item[$\bullet$]
with Proof General
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the second example}
\smallskip
\begin{center}
\red{\texttt{((A -> B) -> (C -> D)) -> C -> B -> D}}
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{and the third example}
\smallskip
\begin{center}
\red{\texttt{(A \char`\\/ B) -> (B \char`\\/ A)}}
\end{center}
\vfill
\vfill
\end{slide}

\begin{slide}
\slidetitle{summary}
\begin{itemize}
\item[$\bullet$]
formal methods
\item[$\bullet$]
\red{type theory}

the Curry-Howard-de Bruijn isomorphism
\item[$\bullet$]
\green{propositional logic}
\item[$\bullet$]
\green{Coq}
\end{itemize}
\vfill
\end{slide}

\end{document}