---------------------------------------------------
             EXECUTING PROOFS AS COMPUTER PROGRAMS
      ---------------------------------------------------

                         Chuangjie Xu

          Monday 14-16, HS B 252, start 16th Oct 2017

          http://www.math.lmu.de/~xu/teaching/agda17/


The objective of this course is to encourage you to make use of proof
assistants in your study of mathematics.  In specific, I will use the
Agda proof assistant for demonstration.


--------------------------
    PLAN of the course
--------------------------

1. Introduction

   (1) Computer assisted formalisation of mathematics

   (2) Martin-Löf type theory & "Proofs as Programs"

   (3) Introduction to the Agda proof assistant

2. Continuity in type theory

   I will present some results about continuity from my PhD thesis to show

   (1) the subtle problem of expressing "existence" in type theory, and

   (2) how to make axioms computational.

3. The Fan theorem

   Dr. Josef Berger will be lecturing a course on the Fan theorem

       Wednesday 14-16, B040, start 18 October

   I plan to attend his course and formalise some results of the Fan
   theorem together with you.

4. Real numbers

   I also plan to develop a basic fragment of the theory of real numbers
   in Agda, following the method of Prof. Helmut Schwichtenberg in his
   previous course on constructive analysis.



------------------
    Literature
------------------

1. Agda and type theory

   (1) The Agda wiki:  http://wiki.portal.chalmers.se/agda/pmwiki.php

   (2) Dependently Typed Programming in Agda.  U. Norell and J. Chapman

   (3) Learn you an Agda  (if you already know e.g. "some" Haskell)

   (4) Chapter 1 of the HoTT book.  Available at

           https://homotopytypetheory.org/book/

2. Continuity and the Fan theorem

   (1) A continuous computational interpretation of type theories.
       Chuangjie Xu, PhD thesis, 2015.  Available at

           http://www.mathematik.uni-muenchen.de/~xu/

   (2) The webpage of Dr. Berger's course

           http://www.math.lmu.de/~jberger/fan.php

3. Analysis

   Constructive analysis with witnesses.  Helmut Schwichtenberg,
   lecture notes, wintersemester 2016/17, LMU.  Available at

      http://www.mathematik.uni-muenchen.de/~schwicht/seminars/semws16/index.php







------------------
    MOTIVATION
------------------

1. Correctness

   (1) To remove deep errors

       E.g. In 2013, Voevodsky discovered a fundamental error in an important
       and widely studied paper of him and Kapranov published in 1989.

   (2) To handle enormous proofs with large computer calculations
   
       E.g. The odd-order theorem was proved originally by Feit and
       Thompson in a 255-page-long paper.

       E.g. The four colour theorem: Appel and Haken’s proof took 139
       pages and depends on long computer calculations.

       E.g. The Kepler conjecture: The proof by Hales consisted of 250
       pages and 3 gigabytes of computer programs and data.

   (3) People trust machines more than human beings?
   
       In some areas of theoretical computer science, it has become a
       standard to publish papers together with computer-verified proofs.

2. Beyond correctness

   (1) Proof automation
   
       Some proof assistants can automatically search for new proofs
       (via various proof tactics), e.g. by testing a number of case
       distinctions.

   (2) Computation extraction
   
       Some proof assistants allow users to extract certified computer
       programs from proofs.

   (3) Other practical features

       User tactics, typeset documents generation, library management, ...

   (4) New mathematics
   
       Voevodsky’s univalent foundations and homotopy type theory

3. My personal experience

   Reviewers gave positive feedback to the Agda proofs for my published papers.
   
   My Agda implementation/formalisation of my PhD. thesis interested
   the examiners and convinced them all my proofs are correct.

   Formalising math is still difficult and time-consuming.

   Correctly formulating mathematics in e.g. type theory is not easy.



-------------------
    Examination
-------------------

Oral exam (+ simple proofs in Agda)



\begin{code}

Type = Set

\end{code}

------------------------------
    Martin-Löf type theory
------------------------------

MLTT is based on the well-known slogan "propositions as types". The
idea is that formulas in intuitionistic logic are interpreted as types
as follows

                Propositions  │  Types
           ───────────────────┼───────────────────
                           ⊥  │  𝟘
                           ⊤  │  𝟙
                       P → Q  │  P → Q
                       P ∧ Q  │  P × Q
                       P ∨ Q  │  P + Q
                 ∀(x:A).P(x)  │  Π(x:A).P(x)
                 ∃(x:A).P(x)  │  Σ(x:A).P(x)
            Leibniz equality  │  identity types
        inductive predicates  │  (dependent) W-types
      coinductive predicates  │  (dependent) M-types

and proofs as terms, known as the Curry-Howard interpretation.
                                  ̅̅̅̅̅̅̅̅̅̅̅̅̅̅̅̅̅̅̅̅̅̅

There are numerous versions and variants of MLTT. Here we study only
the intensional MLTT because of its computational features:
                                    ̅̅̅̅̅̅̅̅̅̅̅̅̅̅̅̅̅̅
 * Type-checking (or proof-checking) is decidable.

 * Any closed term (no free variables) has a canonical form.

 * Normalisation always terminate.

MLTT can be regarded as a dependently typed programming language.  The
design of a number of proof assistants and programming languages is
based on certain variants of MLTT, including Agda, Coq, Lean and Nuprl.


A type in type theory is usually given by rules of
                                          ̅̅̅̅
 ■ formation    - how a type is formed

 ■ introduction - constructors (also called the closure axiom)

 ■ elimination  - destructors (also called the least-fixed-point axiom)

 ■ computation  - how a term is reduced

Examples given by rules (on blackboard): Π-types, Σ-types.

Π-types are primitive in Agda, and Π(x:A).P(x) is written as (x : A) → P x.
̅̅̅̅̅̅
Σ-types are defined inductively, using e.g. data declaration.
̅̅̅̅̅̅
\begin{code}

infixr 5 _,_

data Σ {A : Type} (P : A  Type) : Type where
 _,_ : (a : A) (b : P a)  Σ \(x : A)  P x

pr₁ : {A : Type} {P : A  Type}
     (Σ \(x : A)  P x)  A
pr₁ (a , b) = a

pr₂ : {A : Type} {P : A  Type}
     (w : Σ P)  P (pr₁ w)
pr₂ (a , b) = b

\end{code}

Binary products are a special case of Σ-types.
̅̅̅̅̅̅̅̅̅̅̅̅̅̅̅
\begin{code}

infixr 10 _×_

_×_ : Type  Type  Type
A × B = Σ \(_ : A)  B

\end{code}

Coproducts can also be defined using data declaration.
̅̅̅̅̅̅̅̅̅̅
\begin{code}

data _+_ (A B : Type) : Type where
 inl : A  A + B
 inr : B  A + B

case : {A B C : Type}  (A  C)  (B  C)  A + B  C
case f g (inl a) = f a
case f g (inr b) = g b

\end{code}

Natural numbers
̅̅̅̅̅̅̅̅̅̅̅̅̅̅
\begin{code}

data  : Type where
 zero : 
 succ :   
{-# BUILTIN NATURAL  #-}

data _≤_ :     Type where
 ≤-zero : {n : }  0  n
 ≤-succ : {n m : }  n  m  succ n  succ m

\end{code}

Agda proofs are already executable programs.
                        ̅̅̅̅̅̅̅̅̅̅̅̅̅̅̅̅
For instance, once we prove that every list has a reversed list, we
can run the proof to reverse given lists.

\begin{code}

infixr 20 _::_
infixl 10 _++_

data List (A : Type) : Type where
 []   : List A
 _::_ : A  List A  List A

[_] : {A : Type}  A  List A
[ a ] = a :: []

_++_ : {A : Type}  List A  List A  List A
[] ++ v = v
(a :: u) ++ v = a :: (u ++ v)

data reversed {A : Type} : List A  List A  Type where
 r-nil  : reversed [] []
 r-cons : {u v : List A} {a : A}  reversed u v  reversed (a :: u) (v ++ [ a ])

Thm[ListRev] : {A : Type}
              (u : List A)  Σ \(v : List A)  reversed u v
Thm[ListRev] [] = [] , r-nil
Thm[ListRev] (a :: u) = v ++ [ a ] , r-cons p
 where
  v : List _
  v = pr₁ (Thm[ListRev] u)
  p : reversed u v
  p = pr₂ (Thm[ListRev] u)

exL : List 
exL = 0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: []

revL : List 
revL = pr₁ (Thm[ListRev] exL)
-- Evaluate it by typing "Ctrl-c Ctrl-n" and then entering "revL", and get
--
--   7 :: 6 :: 5 :: 4 :: 3 :: 2 :: 1 :: 0 :: []

\end{code}