Commit 5d3f730e authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

td3

parent 4f1909fe
TD3 : Proofs on Coq lists
=========================
M2 LMFI
Pierre Letouzey (from A. Miquel)
## Revision : the Coq definition of lists ##
In Coq, the following commands load the standard definition of lists and their notations and some usual functions and their properties:
```coq
Require Import List.
Import ListNotations.
```
In the Coq standard library, these *polymorphic lists* are defined via this inductive definition (do not add it in your file):
```coq
Inductive list (A : Type) : Type :=
| nil : list A
| cons : A -> list A -> list A.
```
This definition adds in the current environment a type constructor `list : Type->Type`. For each type `A:Type`, it returns the associated type `(list A) : Type` of lists whose elements are in `A`.
This definition also provides two constructors:
```coq
nil : forall A : Type, list A
cons : forall A : Type, A -> list A -> list
```
and a induction principle `list_ind` allowing to reason inductively on lists (via the `induction` tactic). Try to guess the type of this induction principle (and for the adventurous its implementation), and check your answer via `Check list_ind` (resp. `Print list_ind`).
*Nota*: in Coq, the universal quantification `forall x : T, U(x)` provides a *functional type* which generalizes the arrow type `T -> U`. We call it the *dependant product*.
#### Revision : implicit arguments ####
Normally, the types of the form `forall A : Type,...` for
`nil` and `cons` implies that these constructors expect a first argument of type `A`. For instance, we would normally have to write
`(cons nat 3 (nil nat)) : list nat` for a list of numbers.
Fortunately, it is possible to make some arguments be *implicit*, and only write here `cons 3 nil`, while letting Coq *infer* internally these unwritten arguments. The Coq standard library provides `nil` et `cons` which are already in implicit mode, and similarly for the standard functions on lists.
For you own definitions, you could activate this implicit mode via the
following command (to be put in the file header):
```
Set Implicit Arguments.
```
Otherwise, you could also use the syntax `{A:Type}` instead of `(A:Type)`
for the function arguments that we wish to turn implicit (see for instance the `app` function below).
#### Revision : Notations ####
In addition to implicits, Coq also provides a notation system for lightening the syntax. For lists, some notations are available that mimic the ones from OCaml (cf. the command `Import ListNotations`):
* `[]` for `nil`
* `x :: l` for `cons x l`
* `[x;y;z]` for `x :: y :: z :: nil`, which is itself
`cons x (cons y (cons z nil))`
## List concatenation ##
The (polymorphic) concatenation operation is defined in Coq via:
```coq
Fixpoint app {A:Type} (l1 l2 : list A) : list A :=
match l1 with
| [] => l2
| x :: tl => x :: (app tl l2)
end.
```
Once again, do not redefine this definition, but rather use the predefined version, and its notation `l1 ++ l2` for `app l1 l2`.
1. What is the type of `app` ?
2. Show that for all lists `l`, we have `nil ++ l = l` and
`l ++ nil = l`.
Which of these two propositions corresponds to a definitional equality?
3. Show that the concatenation is associative.
## Length ##
1. Define a function `length : forall {A:Type}, list A -> nat`
such that `length l` returns the length of the list `l`.
Check that your definition is indeed the same than the standard definition of Coq.
2. Show that `length (l1 ++ l2) = length l1 + length l2`
for all listes `l1` and `l2`.
## Reversing a list ##
1. Define a function `rev : forall {A}, list A -> list A`
reversing the list it receives. For that, you can introduce an
auxiliary function `rev_append : forall {A}, list A -> list A -> list A`
which reverse the first list and catenate it to the second one.
2. Show that `length (rev l) = length l`.
3. Show that `rev (l1 ++ l2) = (rev l2) ++ (rev l1)`.
*Note*: you may need some intermediate statements!
## Splitting lists ##
Here is two ways to dispatch elements of a list in two sub-lists of approximatively the same length. For instance `split [1;2;3;4] = ([1;3],[2;4])`.
```coq
Fixpoint split {A} (l:list A) :=
match l with
| [] => ([],[])
| a::l => let (l1,l2) := split l in (a::l2,l1)
end.
Fixpoint splitbis {A} (l:list A) :=
match l with
| [] => ([],[])
| [a] => ([a],[])
| a::b::l => let (l1,l2) := splitbis l in (a::l1,b::l2)
end.
```
Show that `split` and `splitbis` always produce the same result. The following intermediate result may help:
```coq
Lemma split_equiv_aux {A} (l:list A) :
split l = splitbis l /\ forall x, split (x::l) = splitbis (x::l).
```
Show that `split` indeed dispatch the elements in the two final lists. For instance:
```coq
Lemma split_contains {A} (l:list A) :
let (l1,l2) := split1 l in
forall x, In x l <-> In x l1 \/ In x l2.
```
Show that the two lists produced by `split` have indeed (almost) the same length. For instance:
```coq
Lemma split_length {A} (l:list A) :
let (l1,l2) := split1 l in
length l1 = length l2 \/ length l1 = S (length l2).
```
......@@ -113,3 +113,46 @@ notation `l1 ++ l2` pour `app l1 l2`.
*Remarque*: Pour résoudre ces questions, il est utile d'énoncer
des lemmes intermédiaires!
## Découpe de listes ##
Voici deux manières de répartir les éléments d'une liste en deux sous-listes de tailles proches. Par exemple `split [1;2;3;4] = ([1;3],[2;4])`.
```coq
Fixpoint split {A} (l:list A) :=
match l with
| [] => ([],[])
| a::l => let (l1,l2) := split l in (a::l2,l1)
end.
Fixpoint splitbis {A} (l:list A) :=
match l with
| [] => ([],[])
| [a] => ([a],[])
| a::b::l => let (l1,l2) := splitbis l in (a::l1,b::l2)
end.
```
Montrer que `split` et `splitbis` produisent toujours le même résultat. On pourra montrer tout d'abord le résultat intermédiaire suivant:
```coq
Lemma split_equiv_aux {A} (l:list A) :
split l = splitbis l /\ forall x, split (x::l) = splitbis (x::l).
```
Montrer que `split` répartit bien les éléments de la liste d'origine dans les deux listes produites. Par exemple:
```coq
Lemma split_contains {A} (l:list A) :
let (l1,l2) := split1 l in
forall x, In x l <-> In x l1 \/ In x l2.
```
Montrer que les deux listes produites par `split` sont de tailles proches. Par exemple:
```coq
Lemma split_length {A} (l:list A) :
let (l1,l2) := split1 l in
length l1 = length l2 \/ length l1 = S (length l2).
```
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