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