MoreInd.lagda

\chapter{More on Induction}

In the last chapter we introduce more formally the idea of the \textit{Curry-Howard isomorphism}, in which
logical propositions correspond to type constructors. So, to what programming construct correspond mathematical 
induction principles? In this chapter, we will wee that induction corresponds to the notion of recursion 
in programming languages.

%if False
\begin{code}
module MoreInd where

open import Basics renaming (_*_ to _:*_;_+_ to _:+_)
open import Poly
open import Propositions
open import MorePropositions
open import Logic
open import ProofObjects
\end{code}
%endif

Unlike Coq, Agda does not generate an induction principle for each data type we define. Instead of using induction
or applying a generated induction principle, in Agda we just use recursive functions to express the property we want.
We can even express the induction principle generated by Coq using a simple Agda function.
\begin{code}
natInd : forall (P : Nat -> Set) -> P 0 -> (forall (n : Nat) -> P n -> P (suc n)) -> 
         forall (n : Nat) -> P n
natInd P p0 IH zero = p0
natInd P p0 IH (suc n) = natInd (\ z -> P (suc z)) (IH zero p0) (\ n1 -> IH (suc n1)) n
\end{code}
With |natInd| defined we can mimic Coq style proofs for natural numbers. Here is an example, were we proceed by induction on |n|:
\begin{spec}
multZeroR : forall (n : Nat) -> n :* 0 == 0
multZeroR n = natInd (HOLE GAP 0) (HOLE GAP 1) (HOLE GAP 2) n
\end{spec}
Since the property that we want to prove is that $\forall n. n * 0 \equiv 0$, |P| parameter corresponds to the property |n :* 0 == 0|,
resulting in:
\begin{spec}
multZeroR : forall (n : Nat) -> n :* 0 == 0
multZeroR n = natInd (\x -> x :* 0 == 0) (HOLE GAP 1) (HOLE GAP 2) n
\end{spec}
The last two holes correpond to the base case and the induction step for this proof, that are trivially solved by Agda's emacs mode auto solver.
The final proof is the following.
\begin{code}
multZeroR : forall (n : Nat) -> n :* 0 == 0
multZeroR n = natInd (\x -> x :* 0 == 0) refl (λ n1 z -> z) n
\end{code}
\begin{exe}[Induction on lists]
Let's remember the list data type definition:
\begin{spec}
  data List (A : Set) : Set where
    []   : List A
    _::_ : A -> List A -> List A
\end{spec}
Define the function |listInd|, the induction principle for lists and use it to prove the following theorem:
\begin{spec}
length-++' : forall (l l' : List A) -> length (l ++ l') == length l + length l'
length-++' = (HOLE GAP 0)
\end{spec}
\end{exe}
\begin{exe}[Induction on enumerated types]
Consider the following data type definition:
\begin{code}
data RGB : Set where
  red   : RGB
  blue  : RGB
  green : RGB
\end{code}
Define the function |rgbInd|, the induction principle for |RGB| type.
\end{exe}
\begin{exe}[Induction on propositions]
Consider the definition of the following inductive predicate over natural numbers:
\begin{spec}
data Beautiful : Nat -> Set where
   b0   : Beautiful 0
   b3   : Beautiful 3
   b5   : Beautiful 5
   bsum : forall {n m} -> Beautiful n -> Beautiful m -> Beautiful (n + m)
\end{spec}
Define the function |beautifulInd|, the induction principle on |Beautiful| and use it to prove that
it is equivalent to the following data type.
\begin{spec}
data Gorgeous : Nat -> Set where
  g0 : Gorgeous 0
  g3 : forall {n} -> Gorgeous n -> Gorgeous (3 :+ n)
  g5 : forall {n} -> Gorgeous n -> Gorgeous (5 :+ n)
\end{spec}
\end{exe}

\section{The Agda Trusted Computing Base}

One issue that arises with any automated proof assistant is ``why trust it?'': what if there is a bug 
in the implementation that renders all its reasoning suspect?

While it is impossible to allay such concerns completely, the fact that Agda is based on the Curry-Howard correspondence 
gives it a strong foundation. Because propositions are just types and proofs are just terms, checking that an alleged proof 
of a proposition is valid just amounts to type-checking the term. Type checkers are relatively small and straightforward 
programs, so the ``trusted computing base'' for Agda --- 
the part of the code that we have to believe is operating correctly --- is small too.

What must a typechecker do? Its primary job is to make sure that in each function application the expected and actual 
argument types match, that the arms of a match expression are constructor patterns belonging to the inductive type being 
matched over and all arms of the match return the same type, and so on.

There are a few additional wrinkles:

\begin{itemize}
  \item Since Agda types can themselves be expressions, the checker must normalize these (by using the computation rules) before comparing them.
  \item The checker must make sure that match expressions are exhaustive. That is, there must be an arm for every possible constructor. 
   To see why, consider the following alleged proof object:
   \begin{spec}
     orBugs : forall P Q -> P + Q -> P
     orBugs P Q (inl H) = H
   \end{spec}
   All the types here match correctly, but the match only considers one of the possible constructors for or. Agda's 
   exhaustiveness check will reject this definition.
   \item The checker must make sure that each fix expression terminates. It does this using a syntactic check to 
         make sure that each recursive call is on a subexpression of the original argument. To see why this is essential, 
         consider this alleged proof:
    \begin{spec}
      natEmpty : forall (n : Nat) -> Empty 
      natEmpty n = natEmpty n
    \end{spec}
     Again, this is perfectly well-typed, but (fortunately) Agda will reject it, highlighting it as brown in Agda emacs mode.
\end{itemize}

Note that the soundness of Agda depends only on the correctness of its typechecking engine.