Commit 89f2e7cb authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

English version of seance3 and td3

parent dac30ec1
Functional Programming in Coq (session 3)
=========================================
**M2 LMFI**
## Advanced Inductive Types
#### Ordinals
We can encode in Coq (some) ordinals, via the following type :
```coq
Inductive ord :=
| zero : ord
| succ : ord -> ord
| lim : (nat->ord) -> ord.
```
Note that this inductive type does satisfy the strict positivity constraint: constructor `lim` has an argument of type `nat->ord`, where `ord` appears indeed on the right. Having instead `lim:(ord->nat)->ord` would be refused by Coq.
We can plunge in this type the usual natural numbers of type `nat`.
For instance via a mixte addition `add : ord -> nat -> ord` :
```coq
Fixpoint add a n :=
match n with
| 0 => a
| S n => succ (add a n)
end.
Definition nat2ord n := add zero n.
```
Now, we could use constructor `lim` and this `add` function to go beyond the usual numbers.
```coq
Definition omega := lim (add zero).
Definition deuxomega := lim (add omega).
Fixpoint nomega n :=
match n with
| 0 => zero
| S n => lim (add (nomega n))
end.
Definition omegadeux := lim nomega.
```
Be careful, the standard equality of Coq is not very meaningful on these ordinals, since it is purely syntactic. For instance `add zero` and `add (succ zero)` are two different sequences (numbers starting at 0 vs. numbers starting at 1). So Coq will allow proving that `lim (add zero) <> lim (add (succ zero))` (where `<>` is the negation of the logical equality `=`). But we usually consider the limits of these two sequences to be two possible descriptions of `omega`, the first infinite ordinal. We would then have to define and use a specific equality on `ord`, actually an equivalence relation (we also call that a *setoid equality*).
#### Trees of variable arity
Let's encode a type of trees made of nodes having a natural number on them, and then an arbitrary number of subtrees, not just two like last week's `tree`.
```coq
Inductive ntree :=
| Node : nat -> list ntree -> ntree.
```
Note that this inductive type need not have a "base" constructeur like `O` for `nat` or `leaf` for last week `tree`. Instead, we could use `Node n []` for representing a leaf.
An example of program over this type:
```coq
Require Import List.
Import ListNotations.
(* Addition of all elements of a list of natural numbers *)
Fixpoint sum (l:list nat) : nat :=
match l with
| [] => 0
| x::l => x + sum l
end.
(* List.map : iterating a function over all elements of a list *)
Check List.map.
(* How many nodes in a ntree ? *)
Fixpoint ntree_size t :=
match t with
| Node _ ts => 1 + sum (List.map ntree_size ts)
end.
```
Why is this function `ntree_size` accepted as strictly decreasing ? Indee `ts` is a subpart of `t`, but we are not launching the recursive call on `ts` itself. Fortunately, here Coq is clever enough to enter the code of `List.map` and see that `ntree_size` will be launched on subparts of `ts`, and hence transitively subparts of `t`. But that trick only works for a specific implementation of `List.map` (check with your own during the practical session).
## Internal recursive function : fix
Is the Ackermann function structurally decreasing ?
- `ack 0 m = m+1`
- `ack (n+1) 0 = ack n 1`
- `ack (n+1) (m+1) = ack n (ack (n+1) m)`
No if we consider only one argument, as Coq does. Indeed, neither `n` nor `m` (taken separately) ensures a strict decrease. But there is a trick (quite standard now) : we could separate this function into an external fixpoint (decreasing on `n`) and an internal fixpoint (decreasing on `m`), and hence emulate a lexicographic ordering on the arguments. The inner fixpoint uses the `fix` syntax :
```coq
Fixpoint ack n :=
match n with
| 0 => S
| S n =>
fix ack_Sn m :=
match m with
| 0 => ack n 1
| S m => ack n (ack_Sn m)
end
end.
Compute ack 3 5.
```
## Induction Principles
For each new inductive type declared by the user, Coq automatically generates particular functions named induction principles. Normally, for a type `foo`, we get in particular a function `foo_rect`. This function mimics the shape of the inductive type for providing an induction dedicated to this type. For instead for `nat` :
```coq
Check nat_rect.
Print nat_rect.
```
Deep inside this `nat_rect`, one finds a `fix` and a `match`, and this recursion and case analysis is just as generic as it could be for `nat` :
we could program on `nat` without any more `Fixpoint` nor `fix` nor `match`, just with `nat_rect`! For instance:
```coq
Definition pred n : nat := nat_rect _ 0 (fun n h => n) n.
Definition add n m : nat := nat_rect _ m (fun _ h => S h) n.
```
In these two cases, the "predicate" `P` needed by `nat_rect` (its first argument `_`) is actually `fun _ => nat`, meaning that we are using `nat_rect` in a non-dependent manner (more on that in a forthcoming session).
## Pseudo Induction Principles
Example of `Pos.peano_rect` and `N.peano_rect` (mentioned in the solution of TD2) : we could manually "hijack" the (binary) recursion on type `positive` for building a peano-like induction principle following (apparently) a unary recursion. Check in particular that `Pos.peano_rect` is indeed structurally decreasing.
```coq
Require Import PArith NArith.
Check Pos.peano_rect.
Check N.peano_rect.
Print Pos.peano_rect.
Print N.peano_rect.
```
Functional Programming in Coq : TD3
===================================
**M2 LMFI**
Remainder :
```coq
Require Import Bool Arith List.
Import ListNotations.
```
## Classical exercises on lists
Program the following functions, without using the corresponding functions from the Coq standard library :
- `length`
- concatenate (`app` in Coq, infixe notation `++`)
- `rev` (for reverse, a.k.a mirror)
- `map : forall {A B}, (A->B)-> list A -> list B`
- `filter : forall {A}, (A->bool) -> list A -> list A`
- at least one `fold` function, either `fold_right` or `fold_left`
- `seq : nat -> nat -> list nat`, such that `seq a n = [a; a+1; ... a+n-1]`
Why is it hard to program function like `head`, `last` or `nth` ? How can we do ?
## Some executable predicates on lists
- `forallb : forall {A}, (A->bool) -> list A -> bool`.
- `increasing` which tests whether a list of numbers is strictly increasing.
- `delta` which tests whether two successive numbers of the list are always apart by at least `k`.
## Mergesort
- Write a `split` function which dispatch the elements of a list into two lists of half the size (or almost). It is not important whether an element ends in the first or second list. In particular, concatenating the two final lists will not necessary produce back the initial one, just a permutation of it.
- Write a `merge` function which merges two sorted lists into a new sorted list containing all elements of the initial ones. This can be done with structural recursion thanks to a inner `fix` (see `ack` in the session 3 of the course).
- Write a `mergesort` function based on the former functions.
## Powerset
Write a `powerset` function which takes a list `l` and returns the list of all subsets of `l`.
For instance `powerset [1;2] = [[];[1];[2];[1;2]]`. The order of subsets in the produced list is not relevant.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment