td1-english.md 3.68 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
Functional Programming in Coq : TD1
===================================

**M2 LMFI**

## Launching Coq

There are several ways to use Coq:

 * via `coqide`, a graphical interface based on `gtk`
 * via `proofgeneral`, which is a plugin for `emacs`
 * directly in a browser via `jsCoq`, for instance https://jscoq.github.io/node_modules/jscoq/examples/scratchpad.html
   (see https://github.com/ejgallego/jscoq for usage instructions)
 * or perhaps via `coqtop`, a read-eval-print loop (repl) which is quite bare, similar to the `ocaml` interactive loop.

Each method has its advocates (even the last one...).

The coq source files are always named with `.v` as extension (for "vernacular"...).

After launch, both `coqide` and `proofgeneral` and `jsCoq` provide interfaces with a similar layout : the file being edited is in the left half of the screen, while proofs in progress are in right top and system messages are in right bottom (Coq answers, error messages, etc).
In the source file, colors are used to indicate which part of the file has already been processed by Coq, and this colored zone will grow when we send more phrases to Coq. Conversely the colored zone may also shrink if we "undo" and get Coq back to some earlier state.

Until January, we will mostly use the following commands:

 * `Definition` : binds some name with a (non-recursive) Coq term
 * `Fixpoint` : same, for a recursive definition
 * `Inductive` : creates a new inductive type and its constructors
 * `Check` : displays the type of a Coq term
 * `Print` : displays the body of a definition or the details of an inductive type
 * `Compute` : reduces a term (i.e. determines its normal form) and prints it.

A dot `.` is mandatory to end each Coq phrase.

## Functions and only that

#### Exercise 1 : function composition

Define a function `compose : forall A B C, (B->C)->(A->B)->(A->C)`. Test it with functions `S` and `pred` on natural numbers (type `nat`).

Pierre Letouzey's avatar
typos    
Pierre Letouzey committed
40
#### Exercise 2 : Boolean ersatz
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56

Define (without using `bool` nor any other inductive type):

 - a type `mybool : Type`
 - two constants `mytrue` and `myfalse` of type `mybool`
 - a function `myif : forall A, mybool -> A -> A -> A` such that `myif mytrue x y` computes to `x` and `myif myfalse x y` computes to `y`

#### Exercise 3 : Church numerals

Encode in Coq the Church numerals, for which the number `n` is represented by `λfλx.(f (f (... (f x))))` where `f` is applied `n` times.

More precisely, define (without using `nat` nor any other inductive type):

 - a type `church : Type`
 - two constant `zero` and `one` of type `church`
 - a function `succ` of type `church->church`
Pierre Letouzey's avatar
typos    
Pierre Letouzey committed
57
 - two functions `plus` and `mult` of type `church->church->church`
58
59
60
61
62
63
64
 - a function `power`
 - a test `iszero`

Also define two functions `nat2church : nat -> church` and `church2nat : church -> nat` 

## Base types

Pierre Letouzey's avatar
typos    
Pierre Letouzey committed
65
#### Exercise 4 : Booleans
66

Pierre Letouzey's avatar
typos    
Pierre Letouzey committed
67
  - Write a function `checktauto : (bool->bool)->bool` which tests whether a Boolean unary function always answers `true`.
68

Pierre Letouzey's avatar
typos    
Pierre Letouzey committed
69
  - Same for `checktauto2` and `checktauto3` for Boolean functions expecting 2, then 3 arguments. This can be done by enumerating all cases, but there is a clever way to proceed (for instance by re-using `checktauto`.
70

Pierre Letouzey's avatar
typos    
Pierre Letouzey committed
71
  - Check whether `fun a b c => a || b || c || negb (a && b) || negb (a && c)` is a tautology.
72
73
    Note : the command `Open Scope bool_scope.` activates notations `||` and `&&` (respectively for functions `orb` and `andb`).

Pierre Letouzey's avatar
typos    
Pierre Letouzey committed
74
  - Define some functions behaving like Coq standard functions `negb` and `orb` and `andb`.
75
76
77
78
79
80
81
82
83
84
85

#### Exercise 5 : usual functions on natural numbers.

Define the following functions on `nat` (without using the ones of Coq standard library):

  - addition
  - multiplication
  - subtraction
  - factorial
  - power
  - gcd