\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{-5em}$}

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

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large program extraction}

\red{logical verification} \\
week 7 \\
2004 10 20

\end{slide}

\begin{slide}
\sectiontitle{why intuitionism?}
\slidetitle{foundational crisis}
\green{Russell}, start 20th century:
{\large $$\red{\{ x \mathrel{|} x \not\in x \} \in \{ x \mathrel{|} x \not\in x \}} \;?$$}
\vspace{0pt}

shows that \green{naive} set theory / type theory is inconsistent

\vfill
\end{slide}

\begin{slide}
\slidetitle{Brouwer}
three schools:
\begin{itemize}
\item[$\bullet$]
\textbf{formalism}

\begin{tabular}{ccl}
Hilbert && {\dots} leads eventually to \blue{ZFC set theory}
\end{tabular}

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

\begin{tabular}{ccl}
Russell && {\dots} early version of \blue{type theory}
\end{tabular}

\item[$\bullet$]
\textbf{\red{intuitionism}}

\begin{tabular}{ccl}
\green{Brouwer} && rejects excluded middle,
 proves \green{all functions continuous}\toolong \\
$\downarrow$ \\
\green{Heyting} && the \green{logic} of intuitionism \\
$\downarrow$ \\
\green{Bishop} && variant that is \green{strictly weaker} than classical mathematics\toolong
\end{tabular}

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

\begin{slide}
\slidetitle{constructivism}
\green{Brouwer-Heyting-Kolmogorov interpretation}

\begin{center}
\begin{tabular}{rcl}
proof of $\bot$ &$\dots$& doesn't exist \\
proof of $A \to B$ &$\leftrightarrow$& function that maps proofs of $A$ to proofs of $B$ \\
proof of $A \land B$ &$\leftrightarrow$& pair of a proof of $A$ and a proof of $B$ \\
proof of $A \lor B$ &$\leftrightarrow$& either a proof of $A$ or a proof of $B$ \\
proof of $\forall x.\, P(x)$ &$\leftrightarrow$& function that maps object $x$ to proof of $P(x)$ \\
\red{proof of $\exists x.\, P(x)$} &$\leftrightarrow$& \red{object $a$} together with proof of $P(a)$
\end{tabular}\toolong
\end{center}
\bigskip

proof of existence corresponds to \blue{constructing} an example

\vfill
\end{slide}

\begin{slide}
\slidetitle{proofs are programs}
\textbf{program extraction}
\begin{center}
\begin{tabular}{c}
intuitionistic \red{proof} \\
$\red{\updownarrow}$ \\
executable \red{algorithm}
\end{tabular}
\end{center}
\bigskip

\blue{intuitionism the natural logic for computer science?}
\bigskip
\medskip

\begin{center}
\green{\ `code-carrying proofs'}
\end{center}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{verified programs}
\slidetitle{two approaches}
\begin{itemize}
\item[$\bullet$]
\textbf{correctness proofs}
\begin{center}
\begin{tabular}{rcc}
program &\red{$\to$}& {\dots} $+$ proof
\end{tabular}
\end{center}
\bigskip
\item[$\bullet$]
\textbf{program extraction}
\begin{center}
\begin{tabular}{rcl}
\green{program} &\red{$\leftarrow$}& proof\phantom{ $+$ \dots}
\end{tabular}
\end{center}
\end{itemize}
%\bigskip
%\bigskip
%\green{`free programs'}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Hoare logic}

\begin{center}
\begin{tabular}{c}
imperative program \\
$\downarrow$ \\
\red{annotated} imperative program \\
\noalign{\vspace{-\smallskipamount}}
\green{formulas of predicate logic} \\
$\downarrow$ \\
\red{proof obligations}
\end{tabular}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{why \& caduceus}
Jean-Christophe Filli{\^a}tre
\begin{itemize}
\item[$\bullet$]
\textbf{why}

Hoare logic for small programming language \\
\green{union of imperative and functional programming language}

\end{itemize}

\red{programming language independent} \\
\red{proof assistant independent} \\
designed to be used with Coq
\medskip

\begin{itemize}
\item[$\bullet$]
\textbf{caduceus}

Hoare logic for \gray{almost} full \green{ANSI C} \\
built on top of why

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{example}
\begingroup
\small
\def\\{\char`\\}%
\def\{{\char`\{}%
\def\}{\char`\}}%
\begin{alltt}
\advirecord{a1}{/*@ requires \\valid_range(t,0,n-1)
  @ ensures 
  @   (0 <= \\result < n => t[\\result] == v) &&
  @   (\\result == n => \\forall int i; 0 <= i < n => t[i] != v) 
  @*/}
int index(int t[], int n, int v) \{
  int i = 0;
\advirecord{a2}{  /*@ invariant 0 <= i && \\forall int k; 0 <= k < i => t[k] != v
    @ variant n - i */}
  while (i < n) \{
    if (t[i] == v) break;
    i++;
  \}
  return i;
\}
\end{alltt}
\adviwait
\adviplay[slidered]{a1}
\adviplay[slidered]{a2}
\endgroup
\vspace{-10pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{program extraction}

\begin{center}
\begin{tabular}{c}
specification \\
$\downarrow$ \\
constructive \red{proof} of existence of solution to the specification \\
$\downarrow$ \\
automatically generated \red{functional program} \\
\noalign{\vspace{-\smallskipamount}}
\green{guaranteed correct with respect to the specification}
\end{tabular}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{extraction to functional programs}
$$
\xymatrix@C=0.1em@R=5em{
& \txt{\red{coq} proof}\ar[dl]\ar[dr]\ar@{.}[rrrrrr] & &&&&& \txt{\rlap{\green{type theory}}\phantom{functional languages}} \\
\txt{\red{ML} program}\ar@{.}[rr] && \txt{\red{haskell} program}\ar@{.}[rrrrr] &&&&& \txt{\green{functional languages}}
}
$$

\vfill
\end{slide}

\begin{slide}
\sectiontitle{example: mirroring trees}
\slidetitle{\texttt{bintree}}
\blue{inductive type}

\begin{alltt}
Inductive \green{bintree} : Set :=
  \red{leaf} : nat -> bintree
| \red{node} : bintree -> bintree -> bintree.
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{mirror}}
\blue{recursive function}

\begin{alltt}
Fixpoint \green{mirror} (t : bintree) : bintree :=
  match t with
    leaf n => \red{leaf n}
  | node t1 t2 => \red{node (mirror t2) (mirror t1)}
  end.
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{Mirrored}}
\blue{inductive predicate}

\begin{alltt}
Inductive \green{Mirrored} : bintree -> bintree -> Prop :=
  \red{Mirrored_leaf} :
    forall n : nat, Mirrored (leaf n) (leaf n)
| \red{Mirrored_node} :
    forall t1 t2 t1' t2' : bintree,
      Mirrored t1 t1' -> Mirrored t2 t2' ->
      Mirrored (node t1 t2) (node t2' t1').
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{correctness of \texttt{mirror}}
\begin{alltt}
Lemma \green{Mirrored_mirror} :
  \red{forall t : bintree, Mirrored t (mirror t)}.
\gray{induction t.
simpl.
apply Mirrored_leaf.
simpl.
apply Mirrored_node.
exact IHt1.
exact IHt2.}
Qed.
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{two kinds of existential statements}
\begin{itemize}
\item[]
$$\red{\exists x : A.\, P(x)}$$
\end{itemize}
\bigskip

\begin{itemize}
\item[$\bullet$]
existential \green{in \texttt{Prop}}
\begin{center}
\red{\texttt{exists x :\ A,\ P x}} \\
%\texttt{@\green{ex} A (fun x :\ A => P x)}
\end{center}
\bigskip

\item[$\bullet$]
existential \green{in \texttt{Set}}
\begin{center}
\red{\texttt{\char`\{x :\ A\ |\ P x\char`\}}} \\
%\texttt{@\green{sig} A (fun x :\ A => P x)}
\end{center}
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{definition of \texttt{ex}}
%\begin{center}
%\texttt{\strut\ \green{ex} :\ forall A : Set, (A -> Prop) -> \red{Prop}}
%\end{center}
%\bigskip
%\bigskip
%
\blue{inductive type}
\begin{alltt}
Inductive  \green{ex} (A : Set) (P : A -> Prop) : \red{Prop} :=
  ex_intro : forall \green{x : A}, \green{P x} -> \green{ex P}
\end{alltt}
\bigskip
\bigskip

in practice
\begin{center}
\red{\texttt{exists x :\ A.\ P x}}
\end{center}
is syntax for
\begin{center}
\texttt{\green{ex} A (fun x :\ A => P x)}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{definition of \texttt{sig}}
%\begin{center}
%\texttt{\green{sig} :\ forall A : Set, (A -> Prop) -> \red{Set}\ \strut}
%\end{center}
%\bigskip
%\bigskip
%
\blue{inductive type}
\begin{alltt}
Inductive \green{sig} (A : Set) (P : A -> Prop) : \red{Set}  :=
     exist : forall \green{x : A}, \green{P x} -> \green{sig P}
\end{alltt}
\bigskip
\bigskip

in practice
\begin{center}
\red{\texttt{\char`\{x :\ A\ |\ P x\char`\}}} \\
\end{center}
is syntax for
\begin{center}
\texttt{\green{sig} A (fun x :\ A => P x)}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{existence proof for specification}
\vbox to 0pt{%
\vspace{-\medskipamount}
\begingroup
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}
Lemma \green{Mirror} :
  \red{forall t : bintree, \{t' : bintree | Mirrored t t'\}}.
\gray{induction t.
exists (leaf n).
apply Mirrored_leaf.
elim IHt1.
intros t1' H1.
elim IHt2.
intros t2' H2.
exists (node t2' t1').
apply Mirrored_node.
exact H1.
exact H2.}
Qed.
\end{alltt}
\endgroup
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{extracting the program}
\begin{alltt}
Coq < \red{Extraction Mirror.}
\green{(** val mirror : bintree -> bintree sig0 **)}
\end{alltt}
\begin{alltt}
\green{let rec mirror = function
  | Leaf n -> Leaf n
  | Node (b0, b1) -> Node ((mirror b1), (mirror b0))}
\end{alltt}
\begin{alltt}
Coq < 
\end{alltt}
\bigskip
\medskip
\adviwait

\begingroup
\def\mbox#1{{\sf #1}}
\begin{alltt}
\blue{type 'a sig0 = 'a}
\end{alltt}
%  (* \mbox{singleton inductive, whose constructor was exist} *)
\endgroup

\vfill
\end{slide}

\begin{slide}
\slidetitle{summarizing}
\begin{itemize}
\item[$\bullet$]
\textbf{specification}

\texttt{Inductive \green{Mirrored} :\ bintree -> bintree -> Prop := }\dots
\bigskip

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

\texttt{Fixpoint \green{mirror} (t :\ bintree) :\ bintree := }\dots
\item[$\bullet$]
\textbf{correctness}

\texttt{\red{forall t :\ bintree, Mirrored t (mirror t)}}
\bigskip

\item[$\bullet$]
\textbf{program extracted from existence proof for specification}

\texttt{\red{forall t :\ bintree, \char`\{t' :\ bintree | Mirrored t t'\char`\}}}
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{the general pattern}
\slidetitle{$\Pi_2$ sentences}
program specification

$$\forall x : \blue{A}.\, \green{P(x)} \to \exists y : \blue{B}.\, \red{Q(x,y)}$$
\bigskip

\begin{tabular}{rl}
$\blue{A}$ & input type \\
$\blue{B}$ & output type \\
$\green{P(x)}$ & precondition \\
$\red{Q(x,y)}$ & input/output behavior
\end{tabular}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the proof term versus the extracted program}

\begin{center}
\begin{tabular}{rcl}
coq type theory &=& functional programming language \\
\red{coq proof term} &=& functional program \\
\noalign{\medskip}
ML language &=& functional programming language \\
\red{ML program} &=& functional program
\end{tabular}
\end{center}
\medskip

\green{program extraction is \textbf{almost} the identity function}
\medskip
\adviwait

\begin{itemize}
\item[$\bullet$]
differences in type system
\item[$\bullet$]
not all parts of coq terms are computationally relevant
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{Prop} versus \texttt{Set}}
not all coq terms are computationally relevant \\
\green{`Curry-Howard-de Bruijn' terms don't need to be calculated}
\bigskip

\begin{tabular}{lrl}
terms of type in \texttt{Prop} & \red{`non-informative'} & discarded \\
terms of type in \texttt{Set} & \red{`informative'} & kept
\end{tabular}

\vfill
\end{slide}

\begin{slide}
\slidetitle{`elimination of Prop over Set'}
\begingroup
\def\\{\char`\\}
\begin{alltt}
Inductive \green{or} (A : Prop) (B : Prop) : Prop :=
  \red{or_introl} : A -> \green{A \\/ B}
| \red{or_intror} : B -> \green{A \\/ B}.

Definition foo (A : Prop) (\green{H : A \\/ ~A}) : bool :=
  match \green{H} with
    \red{or_introl} _ => true
  | \red{or_intror} _ => false
  end.
\end{alltt}
\endgroup
\medskip

\blue{
Elimination of an inductive object of sort : `\texttt{Prop}' \\
is not allowed on a predicate in sort : `\texttt{Set}' \\
because non-informative objects may not construct informative ones.
}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{example: negation in the booleans}
\slidetitle{statement}
\vspace{0pt}

\begin{center}
\texttt{\red{forall b :\ bool, \char`\{b' :\ bool |\ \char`\~(b = b')\char`\}}}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{extracted program}
\begin{alltt}
(** val negation : bool -> bool sig0 **)
\end{alltt}
\begin{alltt}
let negation = \red{function
  | True -> False
  | False -> True}
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{proof term}
\begingroup
\footnotesize
\begin{alltt}
\red{fun b : bool =>
bool_rec} (fun b0 : bool => {b' : bool | b0 <> b'})
  \red{(}exist (fun b' : bool => true <> b') \red{false}
     (\green{fun H : true = false =>
      let H0 :=
        eq_ind true (fun ee : bool => if ee return Prop then True else False)\toolong
          I false H in
      False_ind False H0})\red{)}
  \red{(}exist (fun b' : bool => false <> b') \red{true}
     (\green{fun H : false = true =>
      let H0 :=
        eq_ind false
          (fun ee : bool => if ee return Prop then False else True) I true H in\toolong
      False_ind False H0})\red{)} \red{b}
\end{alltt}
\endgroup
\medskip

\begingroup
\small
\begin{alltt}
\red{bool_rec} :
\blue{forall P : bool -> Set, P true -> P false -> forall b : bool, P b}\toolong
\end{alltt}
\endgroup
\vspace{-10pt}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{example: the predecessor function}
\slidetitle{statement}
\vspace{0pt}

\begin{center}
\texttt{\red{forall n :\ nat,\ \green{\char`\~(n = O)} -> \char`\{m :\ nat |\ S m = n\char`\}}}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{extracted program}
\begin{alltt}
(** val pred : nat -> nat sig0 **)
\end{alltt}
\begin{alltt}
let rec pred = \red{function
  | O -> \green{assert false (* absurd case *)}
  | S n0 -> n0}
\end{alltt}
\bigskip
\bigskip
\adviwait

\blue{the \texttt{assert} corresponds in the proof term to \dots}

\begingroup
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}
\green{False_rec \{m : nat | S m = 0\} (H (refl_equal 0))}
     : \{m : nat | S m = 0\}
\end{alltt}
\endgroup

\blue{{\dots} recursion on a proof of \texttt{False}}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{extraction in the large}
\slidetitle{FTA project}
\red{coq formalization of non-trivial mathematical theorem}

Fundamental Theorem of Algebra \\
\green{every non-constant complex polynomial has a root}
\bigskip

finished in 2000 \\
Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg
\bigskip

\red{intuitionistic proof}

\vfill
\end{slide}

\begin{slide}
\slidetitle{extracting the Fundamental Theorem of Algebra}
complex polynomials

$$
\xymatrix@R=5em{
\forall p.\, \red{(p\mbox{ not constant})} \to \exists z.\, \red{p(z) = 0}\ar[d]^{\txt{program extraction}} \\
\txt{\green{program for calculating roots of polynomials}}
}
$$
\vspace{0pt}

\begin{center}
\green{
\begin{tabular}{rl}
\textbf{input} & complex polynomial \\
$\hspace{4em}$\textbf{output} & sequence converging to a root
\end{tabular}
}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{extracting the Intermediate Value Theorem}
real polynomials

$$\forall p.\, \red{(p(0) < 0 \land p(1) > 0)} \to \exists x.\, \red{(0 < x \land x < 1 \land p(x) = 0)}$$
\vspace{-1.5\bigskipamount}
$$
\xymatrix@R=5em{
\green{\mbox{take }p(x) = x^2 - 2}\ar[d]^{\txt{program extraction}} \\
\txt{\green{program for approximating $\sqrt{2}$}}
}
$$

\vfill
\end{slide}

\begin{slide}
\sectiontitle{example: sorting lists}
\slidetitle{\texttt{natlist}}
\blue{inductive type}

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

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{Sorted}}
\blue{inductive predicate}

\begin{alltt}
Inductive \green{Sorted} : natlist -> Prop :=
  \red{Sorted_nil} : Sorted nil
| \red{Sorted_one} : forall n : nat, Sorted (cons n nil)
| \red{Sorted_cons} :
    forall (n m : nat) (l : natlist),
    n <= m -> Sorted (cons m l) -> Sorted (cons n (cons m l)).\toolong
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{Inserted}}
\blue{inductive predicate}

\begin{alltt}
Inductive \green{Inserted} (n : nat) : natlist -> natlist -> Prop :=\toolong
  \red{Inserted_front} :
    forall l : natlist, Inserted n l (cons n l)
| \red{Inserted_cons} :
    forall (m : nat) (l l' : natlist),
    Inserted n l l' -> Inserted n (cons m l) (cons m l').
\end{alltt}
\bigskip
\medskip
\green{\texttt{Inserted }\red{4}\texttt{ }\black{[1,2,3]}\texttt{ }\black{[\red{4},1,2,3]}} \\
\green{\texttt{Inserted }\red{4}\texttt{ }\black{[1,2,3]}\texttt{ }\black{[1,\red{4},2,3]}} \\
\green{\texttt{Inserted }\red{4}\texttt{ }\black{[1,2,3]}\texttt{ }\black{[1,2,\red{4},3]}} \\
\green{\texttt{Inserted }\red{4}\texttt{ }\black{[1,2,3]}\texttt{ }\black{[1,2,3,\red{4}]}}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{Permutation}}
\blue{inductive predicate}

\begin{alltt}
Inductive \green{Permutation} : natlist -> natlist -> Prop :=
  \red{Permutation_nil} : Permutation nil nil
| \red{Permutation_cons} :
    forall (n : nat) (l l' l'' : natlist),
    Permutation l l' -> Inserted n l' l'' ->
    Permutation (cons n l) l''.
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{statement}
\vspace{0pt}

\begin{center}
\texttt{\red{forall l :\ natlist,}} \\
\texttt{\red{\ \ \char`\{l' :\ natlist | Permutation l l' /\char`\\\ Sorted l'\char`\}}}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{insert}}
\blue{recursive function}

\begingroup
\begin{alltt}
Fixpoint \green{insert} (n : nat) (l : natlist) {struct l} : natlist :=\toolong
  match l with
    nil => \red{cons n nil}
  | cons m k =>
      match le_lt_dec n m with
        left _ => \red{cons n (cons m k)}
      | right _ => \red{cons m (insert n k)}
      end
  end.
\end{alltt}
\endgroup

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{sort}}
\blue{recursive function}

\begingroup
\begin{alltt}
Fixpoint \green{sort} (l : natlist) : natlist :=
  match l with
    nil => \red{nil}
  | cons m k => \red{insert m (sort k)}
  end.
\end{alltt}
\endgroup

\vfill
\end{slide}

\end{document}