The Coq system is a proof assistant. It is designed to build and verify mathematical proofs. The Coq system contains the functional programming language Gallina and is capable of proving properties about programs written in this language.
Coq is a dependently typed language. This means that the types of the language may depend on the values of variables. In this respect, it is similar to other related languages such as Agda, Idris, F*, Lean, and others. Via the Curry-Howard correspondence, programs, properties and proofs are formalized in the same language.
Coq is developed in OCaml and shares some syntactic and conceptual similarity with it. Coq is a language containing many fascinating but difficult topics. This tutorial will focus on the programming aspects of Coq, rather than the proving. It may be helpful, but not necessary to learn some OCaml first, especially if you are unfamiliar with functional programming. This tutorial is based upon its OCaml equivalent
The standard usage model of Coq is to write it with interactive tool assistance, which operates like a high powered REPL. Two common such editors are the CoqIDE and Proof General Emacs mode.
Inside Proof General Ctrl+C Ctrl+<Enter> will evaluate up to your cursor.
1(*** Comments ***)
2
3(* Comments are enclosed in (* and *). It's fine to nest comments. *)
4
5(* There are no single-line comments. *)
6
7(*** Variables and functions ***)
8
9(* The Coq proof assistant can be controlled and queried by a command
10 language called the vernacular. Vernacular keywords are capitalized and
11 the commands end with a period. Variable and function declarations are
12 formed with the Definition vernacular. *)
13
14Definition x := 10.
15
16(* Coq can sometimes infer the types of arguments, but it is common practice
17 to annotate with types. *)
18
19Definition inc_nat (x : nat) : nat := x + 1.
20
21(* There exists a large number of vernacular commands for querying
22 information. These can be very useful. *)
23
24Compute (1 + 1). (* 2 : nat *) (* Compute a result. *)
25
26Check tt. (* tt : unit *) (* Check the type of an expressions *)
27
28About plus. (* Prints information about an object *)
29
30(* Print information including the definition *)
31Print true. (* Inductive bool : Set := true : Bool | false : Bool *)
32
33Search nat. (* Returns a large list of nat related values *)
34Search "_ + _". (* You can also search on patterns *)
35Search (?a -> ?a -> bool). (* Patterns can have named parameters *)
36Search (?a * ?a).
37
38(* Locate tells you where notation is coming from. Very helpful when you
39 encounter new notation. *)
40
41Locate "+".
42
43(* Calling a function with insufficient number of arguments does not cause
44 an error, it produces a new function. *)
45Definition make_inc x y := x + y. (* make_inc is nat -> nat -> nat *)
46Definition inc_2 := make_inc 2. (* inc_2 is nat -> nat *)
47Compute inc_2 3. (* Evaluates to 5 *)
48
49
50(* Definitions can be chained with "let ... in" construct. This is roughly
51 the same to assigning values to multiple variables before using them in
52 expressions in imperative languages. *)
53
54Definition add_xy : nat := let x := 10 in
55 let y := 20 in
56 x + y.
57
58(* Pattern matching is somewhat similar to switch statement in imperative
59 languages, but offers a lot more expressive power. *)
60
61Definition is_zero (x : nat) :=
62 match x with
63 | 0 => true
64 | _ => false (* The "_" pattern means "anything else". *)
65 end.
66
67(* You can define recursive function definition using the Fixpoint
68 vernacular.*)
69
70Fixpoint factorial n := match n with
71 | 0 => 1
72 | (S n') => n * factorial n'
73 end.
74
75(* Function application usually doesn't need parentheses around arguments *)
76Compute factorial 5. (* 120 : nat *)
77
78(* ...unless the argument is an expression. *)
79Compute factorial (5-1). (* 24 : nat *)
80
81(* You can define mutually recursive functions using "with" *)
82Fixpoint is_even (n : nat) : bool := match n with
83 | 0 => true
84 | (S n) => is_odd n
85end with
86 is_odd n := match n with
87 | 0 => false
88 | (S n) => is_even n
89 end.
90
91(* As Coq is a total programming language, it will only accept programs when
92 it can understand they terminate. It can be most easily seen when the
93 recursive call is on a pattern matched out subpiece of the input, as then
94 the input is always decreasing in size. Getting Coq to understand that
95 functions terminate is not always easy. See the references at the end of
96 the article for more on this topic. *)
97
98(* Anonymous functions use the following syntax: *)
99
100Definition my_square : nat -> nat := fun x => x * x.
101
102Definition my_id (A : Type) (x : A) : A := x.
103Definition my_id2 : forall A : Type, A -> A := fun A x => x.
104Compute my_id nat 3. (* 3 : nat *)
105
106(* You can ask Coq to infer terms with an underscore *)
107Compute my_id _ 3.
108
109(* An implicit argument of a function is an argument which can be inferred
110 from contextual knowledge. Parameters enclosed in {} are implicit by
111 default *)
112
113Definition my_id3 {A : Type} (x : A) : A := x.
114Compute my_id3 3. (* 3 : nat *)
115
116(* Sometimes it may be necessary to turn this off. You can make all
117 arguments explicit again with @ *)
118
119Compute @my_id3 nat 3.
120
121(* Or give arguments by name *)
122Compute my_id3 (A:=nat) 3.
123
124(* Coq has the ability to extract code to OCaml, Haskell, and Scheme *)
125Require Extraction.
126Extraction Language OCaml.
127Extraction "factorial.ml" factorial.
128(* The above produces a file factorial.ml and factorial.mli that holds:
129
130type nat =
131| O
132| S of nat
133
134(** val add : nat -> nat -> nat **)
135
136let rec add n m =
137 match n with
138 | O -> m
139 | S p -> S (add p m)
140
141(** val mul : nat -> nat -> nat **)
142
143let rec mul n m =
144 match n with
145 | O -> O
146 | S p -> add m (mul p m)
147
148(** val factorial : nat -> nat **)
149
150let rec factorial n = match n with
151| O -> S O
152| S n' -> mul n (factorial n')
153*)
154
155
156(*** Notation ***)
157
158(* Coq has a very powerful Notation system that can be used to write
159 expressions in more natural forms. *)
160
161Compute Nat.add 3 4. (* 7 : nat *)
162Compute 3 + 4. (* 7 : nat *)
163
164(* Notation is a syntactic transformation applied to the text of the program
165 before being evaluated. Notation is organized into notation scopes. Using
166 different notation scopes allows for a weak notion of overloading. *)
167
168(* Imports the Zarith module holding definitions related to the integers Z *)
169
170Require Import ZArith.
171
172(* Notation scopes can be opened *)
173Open Scope Z_scope.
174
175(* Now numerals and addition are defined on the integers. *)
176Compute 1 + 7. (* 8 : Z *)
177
178(* Integer equality checking *)
179Compute 1 =? 2. (* false : bool *)
180
181(* Locate is useful for finding the origin and definition of notations *)
182Locate "_ =? _". (* Z.eqb x y : Z_scope *)
183Close Scope Z_scope.
184
185(* We're back to nat being the default interpretation of "+" *)
186Compute 1 + 7. (* 8 : nat *)
187
188(* Scopes can also be opened inline with the shorthand % *)
189Compute (3 * -7)%Z. (* -21%Z : Z *)
190
191(* Coq declares by default the following interpretation scopes: core_scope,
192 type_scope, function_scope, nat_scope, bool_scope, list_scope, int_scope,
193 uint_scope. You may also want the numerical scopes Z_scope (integers) and
194 Q_scope (fractions) held in the ZArith and QArith module respectively. *)
195
196(* You can print the contents of scopes *)
197Print Scope nat_scope.
198(*
199Scope nat_scope
200Delimiting key is nat
201Bound to classes nat Nat.t
202"x 'mod' y" := Nat.modulo x y
203"x ^ y" := Nat.pow x y
204"x ?= y" := Nat.compare x y
205"x >= y" := ge x y
206"x > y" := gt x y
207"x =? y" := Nat.eqb x y
208"x <? y" := Nat.ltb x y
209"x <=? y" := Nat.leb x y
210"x <= y <= z" := and (le x y) (le y z)
211"x <= y < z" := and (le x y) (lt y z)
212"n <= m" := le n m
213"x < y <= z" := and (lt x y) (le y z)
214"x < y < z" := and (lt x y) (lt y z)
215"x < y" := lt x y
216"x / y" := Nat.div x y
217"x - y" := Init.Nat.sub x y
218"x + y" := Init.Nat.add x y
219"x * y" := Init.Nat.mul x y
220*)
221
222(* Coq has exact fractions available as the type Q in the QArith module.
223 Floating point numbers and real numbers are also available but are a more
224 advanced topic, as proving properties about them is rather tricky. *)
225
226Require Import QArith.
227
228Open Scope Q_scope.
229Compute 1. (* 1 : Q *)
230
231(* Only 1 and 0 are interpreted as fractions by Q_scope *)
232Compute 2. (* 2 : nat *)
233Compute (2 # 3). (* The fraction 2/3 *)
234Compute (1 # 3) ?= (2 # 6). (* Eq : comparison *)
235Close Scope Q_scope.
236
237Compute ( (2 # 3) / (1 # 5) )%Q. (* 10 # 3 : Q *)
238
239
240(*** Common data structures ***)
241
242(* Many common data types are included in the standard library *)
243
244(* The unit type has exactly one value, tt *)
245Check tt. (* tt : unit *)
246
247(* The option type is useful for expressing computations that might fail *)
248Compute None. (* None : option ?A *)
249Check Some 3. (* Some 3 : option nat *)
250
251(* The type sum A B allows for values of either type A or type B *)
252Print sum.
253Check inl 3. (* inl 3 : nat + ?B *)
254Check inr true. (* inr true : ?A + bool *)
255Check sum bool nat. (* (bool + nat)%type : Set *)
256Check (bool + nat)%type. (* Notation for sum *)
257
258(* Tuples are (optionally) enclosed in parentheses, items are separated
259 by commas. *)
260Check (1, true). (* (1, true) : nat * bool *)
261Compute prod nat bool. (* (nat * bool)%type : Set *)
262
263Definition my_fst {A B : Type} (x : A * B) : A := match x with
264 | (a,b) => a
265 end.
266
267(* A destructuring let is available if a pattern match is irrefutable *)
268Definition my_fst2 {A B : Type} (x : A * B) : A := let (a,b) := x in
269 a.
270
271(*** Lists ***)
272
273(* Lists are built by using cons and nil or by using notation available in
274 list_scope. *)
275Compute cons 1 (cons 2 (cons 3 nil)). (* (1 :: 2 :: 3 :: nil)%list : list nat *)
276Compute (1 :: 2 :: 3 :: nil)%list.
277
278(* There is also list notation available in the ListNotations modules *)
279Require Import List.
280Import ListNotations.
281Compute [1 ; 2 ; 3]. (* [1; 2; 3] : list nat *)
282
283
284(* There is a large number of list manipulation functions available,
285 including:
286
287• length
288• head : first element (with default)
289• tail : all but first element
290• app : appending
291• rev : reverse
292• nth : accessing n-th element (with default)
293• map : applying a function
294• flat_map : applying a function returning lists
295• fold_left : iterator (from head to tail)
296• fold_right : iterator (from tail to head)
297
298 *)
299
300Definition my_list : list nat := [47; 18; 34].
301
302Compute List.length my_list. (* 3 : nat *)
303
304(* All functions in coq must be total, so indexing requires a default value *)
305Compute List.nth 1 my_list 0. (* 18 : nat *)
306Compute List.map (fun x => x * 2) my_list. (* [94; 36; 68] : list nat *)
307Compute List.filter (fun x => Nat.eqb (Nat.modulo x 2) 0) my_list.
308 (* [18; 34] : list nat *)
309Compute (my_list ++ my_list)%list. (* [47; 18; 34; 47; 18; 34] : list nat *)
310
311(*** Strings ***)
312
313Require Import Strings.String.
314
315(* Use double quotes for string literals. *)
316Compute "hi"%string.
317
318Open Scope string_scope.
319
320(* Strings can be concatenated with the "++" operator. *)
321Compute String.append "Hello " "World". (* "Hello World" : string *)
322Compute "Hello " ++ "World". (* "Hello World" : string *)
323
324(* Strings can be compared for equality *)
325Compute String.eqb "Coq is fun!" "Coq is fun!". (* true : bool *)
326Compute "no" =? "way". (* false : bool *)
327
328Close Scope string_scope.
329
330(*** Other Modules ***)
331
332(* Other Modules in the standard library that may be of interest:
333
334• Logic : Classical logic and dependent equality
335• Arith : Basic Peano arithmetic
336• PArith : Basic positive integer arithmetic
337• NArith : Basic binary natural number arithmetic
338• ZArith : Basic relative integer arithmetic
339
340• Numbers : Various approaches to natural, integer and cyclic numbers
341 (currently axiomatically and on top of 2^31 binary words)
342• Bool : Booleans (basic functions and results)
343
344• Lists : Monomorphic and polymorphic lists (basic functions and results),
345 Streams (infinite sequences defined with co-inductive types)
346• Sets : Sets (classical, constructive, finite, infinite, power set, etc.)
347• FSets : Specification and implementations of finite sets and finite maps
348 (by lists and by AVL trees)
349• Reals : Axiomatization of real numbers (classical, basic functions,
350 integer part, fractional part, limit, derivative, Cauchy series,
351 power series and results,...)
352• Relations : Relations (definitions and basic results)
353• Sorting : Sorted list (basic definitions and heapsort correctness)
354• Strings : 8-bit characters and strings
355• Wellfounded : Well-founded relations (basic results)
356 *)
357
358(*** User-defined data types ***)
359
360(* Because Coq is dependently typed, defining type aliases is no different
361 than defining an alias for a value. *)
362
363Definition my_three : nat := 3.
364Definition my_nat : Type := nat.
365
366(* More interesting types can be defined using the Inductive vernacular.
367 Simple enumeration can be defined like so *)
368
369Inductive ml := OCaml | StandardML | Coq.
370Definition lang := Coq. (* Has type "ml". *)
371
372(* For more complicated types, you will need to specify the types of the
373 constructors. *)
374
375(* Type constructors don't need to be empty. *)
376Inductive my_number := plus_infinity
377 | nat_value : nat -> my_number.
378Compute nat_value 3. (* nat_value 3 : my_number *)
379
380
381(* Record syntax is sugar for tuple-like types. It defines named accessor
382 functions for the components. Record types are defined with the notation
383 {...} *)
384
385Record Point2d (A : Set) := mkPoint2d { x2 : A ; y2 : A }.
386(* Record values are constructed with the notation {|...|} *)
387Definition mypoint : Point2d nat := {| x2 := 2 ; y2 := 3 |}.
388Compute x2 nat mypoint. (* 2 : nat *)
389Compute mypoint.(x2 nat). (* 2 : nat *)
390
391(* Types can be parameterized, like in this type for "list of lists of
392 anything". 'a can be substituted with any type. *)
393
394Definition list_of_lists a := list (list a).
395Definition list_list_nat := list_of_lists nat.
396
397(* Types can also be recursive. Like in this type analogous to
398 built-in list of naturals. *)
399
400Inductive my_nat_list :=
401 EmptyList | NatList : nat -> my_nat_list -> my_nat_list.
402
403Compute NatList 1 EmptyList. (* NatList 1 EmptyList : my_nat_list *)
404
405(** Matching type constructors **)
406
407Inductive animal := Dog : string -> animal | Cat : string -> animal.
408
409Definition say x :=
410 match x with
411 | Dog x => (x ++ " says woof")%string
412 | Cat x => (x ++ " says meow")%string
413 end.
414
415Compute say (Cat "Fluffy"). (* "Fluffy says meow". *)
416
417(** Traversing data structures with pattern matching **)
418
419(* Recursive types can be traversed with pattern matching easily.
420 Let's see how we can traverse a data structure of the built-in list type.
421 Even though the built-in cons ("::") looks like an infix operator,
422 it's actually a type constructor and can be matched like any other. *)
423Fixpoint sum_list l :=
424 match l with
425 | [] => 0
426 | head :: tail => head + (sum_list tail)
427 end.
428
429Compute sum_list [1; 2; 3]. (* Evaluates to 6 *)
430
431
432(*** A Taste of Proving ***)
433
434(* Explaining the proof language is out of scope for this tutorial, but here
435 is a taste to whet your appetite. Check the resources below for more. *)
436
437(* A fascinating feature of dependently type based theorem provers is that
438 the same primitive constructs underly the proof language as the
439 programming features. For example, we can write and prove the
440 proposition A and B implies A in raw Gallina *)
441
442Definition my_theorem : forall A B, A /\ B -> A :=
443 fun A B ab => match ab with
444 | (conj a b) => a
445 end.
446
447(* Or we can prove it using tactics. Tactics are a macro language to help
448 build proof terms in a more natural style and automate away some
449 drudgery. *)
450
451Theorem my_theorem2 : forall A B, A /\ B -> A.
452Proof.
453 intros A B ab. destruct ab as [ a b ]. apply a.
454Qed.
455
456(* We can easily prove simple polynomial equalities using the
457 automated tactic ring. *)
458
459Require Import Ring.
460Require Import Arith.
461Theorem simple_poly : forall (x : nat), (x + 1) * (x + 2) = x * x + 3 * x + 2.
462 Proof. intros. ring. Qed.
463
464(* Here we prove the closed form for the sum of all numbers 1 to n using
465 induction *)
466
467Fixpoint sumn (n : nat) : nat :=
468 match n with
469 | 0 => 0
470 | (S n') => n + (sumn n')
471 end.
472
473Theorem sum_formula : forall n, 2 * (sumn n) = (n + 1) * n.
474Proof. intros n. induction n.
475 - reflexivity. (* 0 = 0 base case *)
476 - simpl. ring [IHn]. (* induction step *)
477Qed.
With this we have only scratched the surface of Coq. It is a massive ecosystem with many interesting and peculiar topics leading all the way up to modern research.