Transcript coq - University of Virginia, Department of Computer Science

Proofs and Programs
Wei Hu
11/01/2007
Outline
Motivation
Theory





Lambda calculus
Curry-Howard Isomorphism
Dependent types
Practice


2
Coq
Wei Hu
Motivation - Why Learn Coq
Helps understand PL theory better


Good for CS615 (sadly, not quals)
Coq is becoming popular



People rethinking trusted software
Functional programming is gaining attention
Has been used to



Prove mathematical theorems
Specify hardware
Recently, papers being published for



3
Operating systems
Compilers
Wei Hu
Coq is an Interactive Theorem Prover
Two types of theorem provers


Automated TP


Simplify, CVC, …
Interactive TP (aka, Proof Assistants)

Coq, PVS, ACL2, HOL, Isabelle, Twelf, NuPRL, Agda
Coq’s highlights






4
Higher-order intuitionistic logic
Higher-order type theory
Embedded functional programming language
Goal transformation through tactics
Mainly works interactively, with limited support of automation
to discharge trivial propositions
Wei Hu
Coq as a Programming Language
ML-like

Fixpoint is_even (n:nat) : bool :=
match n with
| 0
=> true
| 1
=> false
| S (S n') => is_even n’
end.
Eval compute in is_even 3.
Let’s try it out!
Restrictions



5
No side effects
No non-terminating programs (to avoid inconsistency)
Wei Hu
Program Extraction
Fixpoint is_even (n:nat) : bool :=
match n with
| 0
=> true
| 1
=> false
| S (S n') => is_even n’
end.
Coq
let rec is_even = function
| O -> True
| S n0 -> (match n0 with
| O -> False
| S n' -> is_even n')
OCaml
is_even n =
case n of
O -> True
S n0 -> (case n0 of
O -> False
S n' -> is_even n')
Haskell
6
Wei Hu
Nothing Is Built-in!
Inductive bool : Set :=
| true : bool
| false : bool.
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
type bool =
| True
| False
Coq
(theories/Init/Datatypes.v)
OCaml
type nat =
| O
| S of nat
data Bool = True
| False
Haskell
data Nat = O
| S Nat
7
Wei Hu
Simply Typed Lambda Calculus
Type



Base types: nat, bool, …
Function types: nat->nat, nat->bool, …
Term




Variables: x, y, z
Abstractions: x: T1. t2
Applications: M N
Environment ()


8
Gives typing for variables
Wei Hu
Typing Rules
x:T
 |- x : T
(Var)
, x: T1 |- t2 : T2
 |- x: T1. t2 : T1 -> T2
 |- t1 : T11 -> T12
(Abs)
 |- t2 : T11
 |- t1 t2 : T12
The typing rules work equally well in logic!
9
Wei Hu
(App)
Curry-Howard Isomorphism




Propositions = Types
Proofs (inhabit Props) = Programs (inhabit Sets)
Proof tactics = Program constructs
So what?



Proof checking now becomes type checking
(can be undecidable if non-termination is allowed)
Programs and proofs are organically unified
Why is it hard to prove something?



10
Unlike general programming, we are doing type-level
programming
In other words, we are constructing programs for a given type
Tactics help with the construction
Wei Hu
C-H at Work
Section example1.
Hypothesis A B : Prop.
Hypothesis C : B -> A.
x:T
Lemma Var : B -> A.
exact C.
Qed.
Lemma Abs : A -> A.
intros.
exact H.
Qed.
 |- x : T
, x: T1 |- t2 : T2
 |- x: T1. t2 : T1 -> T2
Lemma App : A -> (A -> B) -> B.
intros.
 |- t1 :
apply H0.
function
exact H.
or implication?
Qed.
11
T11 -> T12  |- t2 : T11
 |- t1 t2 : T12
Wei Hu
Type-centric View


-> is primitive, others not
theories/Init/Logic.v
Inductive True : Prop := I : True.
Inductive False : Prop :=.
BHK Interpretation
(Brouwer-HeytingKolmogorov)
Definition not (A:Prop) := A -> False.
Inductive and (A B:Prop) : Prop :=
conj : A -> B -> A /\ B.
Inductive or (A B:Prop) : Prop :=
| or_introl : A -> A \/ B
| or_intror : B -> A \/ B.
12
Wei Hu
Intuitionistic (Constructive) Logic vs.
Classical Logic

A set of equivalent axioms missing in IL






Law of excluded middle: P ∨ ~P
Double negation rule: ~~P → P
Peirce’s Law: ((P→Q)→P)→P
The correspondence between call/cc and Pierce’s Law
See Coq FAQ #30 “What axioms can be safely added to Coq?”
CL takes a denotational view

Assigns to every variable a value (true or false)

Builds truth tables for primitive operations /\ ∨ ~

(P -> Q) ≡ (~P ∨ Q )
13
Wei Hu
Polymorphism and Universal Quantification

Parametric polymorphism


You have been using it all the time!
Polymorphic functions




Definition id := fun (X : Set) (x : X) => x.
Check id.
id : forall X : Set, X -> X.
Polymorphic data types (e.g., lists)
Universal quantification


Lemma refl : forall P : Prop, P -> P.
intros. apply H. Qed.
Print refl.
refl = fun (P : Prop) (H : P) => H
: forall P : Prop, P -> P
14
Wei Hu
Dependent Types


Type systems in ML-like languages are just not expressive
enough
We want to specify propositions like
∀ n:nat, n ≤ n
The result type (n ≤ n) depends on arguments (n)


We generalize arrows (A -> B, or λx:A. B) to
dependent products (∏x:A. B) where B is
dependent on x.
In Coq:


15
forall n:nat, n<=n
forall m n: nat, m + n = n + m
Wei Hu
Dependent Types

Compatibility with non-dependent product

The type of a function that builds a pair:
forall (A B:Set) (a:A) (b:B), A*B
forall A B : Set, A -> B -> A * B

Defining existential



∀ x, (P x -> ∃ x, P x)
Dependent sums
Dependent types in programming





16
Epigram (http://www.e-pig.org/)
Ynot (http://www.eecs.harvard.edu/~greg/ynot.html)
Concoqtion (http://www.metaocaml.org/concoqtion/)
Omega (http://web.cecs.pdx.edu/~sheard/)
ATS (http://www.cs.bu.edu/~hwxi/ATS/)
Wei Hu
Polymorphism vs. Dependent Types

Polymorphism


Dependent types


Terms can take types as arguments
Types can take terms as arguments
Inductive types and predicates


17
Generalization of conventional user-defined data types
We are talking about parameterized data types (e.g. vector n)
and propositions (e.g. m <= n)
Wei Hu
Conclusions

We talked about type theory



We did not cover common proof techniques


*
Curry-Howard correspondence is cool
*
Dependent types matter
Proof by induction
Use of tactics and tacticals
T. Altenkirch, C. McBride, and J. McKinna, “Why Dependent
Types Matter”
18
Wei Hu
How to Learn Coq?

Resources (for beginners)


Hardest parts (IMO)




http://www.cs.virginia.edu/~wh5a/coq.html
Design/Formalization
Combination of tactics
Tools are getting better,
but still hard
What’s the next breakthrough?
19
Wei Hu