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`).
#### Exercise 2 : Boolean ersatz
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`
- two functions `plus` and `mult` of type `church->church->church`
- a function `power`
- a test `iszero`
Also define two functions `nat2church : nat -> church` and `church2nat : church -> nat`
## Base types
#### Exercise 4 : Booleans
- Write a function `checktauto : (bool->bool)->bool` which tests whether a Boolean unary function always answers `true`.
- 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`.
- Check whether `fun a b c => a || b || c || negb (a && b) || negb (a && c)` is a tautology.
Note : the command `Open Scope bool_scope.` activates notations `||` and `&&` (respectively for functions `orb` and `andb`).
- Define some functions behaving like Coq standard functions `negb` and `orb` and `andb`.
#### 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