Commit 4b679663 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

td4 in english

parent e5996c86
TD4 : Inductive definitions of predicates
=========================================
M2 LMFI
Pierre Letouzey (from A. Miquel)
### Reflexive-transitive closure, version 1 ###
First, let us consider a particular domain:
```
Parameter T:Type.
```
On this type `T`, we now aim at defining the reflexive-transitive
closure of a relation `R:T->T->Prop`, i.e. the smallest relation `R*`
which is reflexive and transitive and contains `R`. It is natural
to define this relation inductively, based on the three following
rules:
* Inclusion : If `R(x,y)` then `R*(x,y)`
* Reflexivity : We always have `R*(x,x)`
* Transitivity : If `R*(x,y)` and `R*(y,z)` then `R*(x,z)`
1. How can we express the fact that `R*` is the smallest relation
satisfying these three properties ?
In Coq, this inductive definition is done in the following way:
```
Inductive clos1 (R : T -> T -> Prop) : T -> T -> Prop :=
| cl1_base : forall x y, R x y -> clos1 R x y
| cl1_refl : forall x, clos1 R x x
| cl1_trans : forall x y z, clos1 R x y -> clos1 R y z -> clos1 R x z.
```
This Coq definition, which is parameterized by the relation `R`,
generates several elements:
* A *relation transformer* `clos1 : (T -> T -> Prop) -> (T -> T -> Prop)`
which associates to each binary relation `R` its
reflexive-transitive closure `clos1 R`.
* Three constants `cl1_base` and `cl1_refl` and `cl1_trans`
corresponding to the three constructing rules of `clos1 R`
(these constants are called the *constructors* of the inductive predicate).
* An induction principle `clos1_ind` expressing that `clos1 R`
is the smallest reflexive-transitive relation containing `R`.
2. Compare this induction principle `clos1_ind` generated by Coq
with your answer to the previous question.
3. Show that if `R` is symmetric, then so is `clos1 R`.
(Hint: define a predicate on relations `Symmetric : (T->T->Prop)->Prop`).
4. Show that the reflexive-transitive closure is an idempotent operation:
`forall x y, clos1 (clos1 R) x y -> clos1 R x y`.
### Reflexive-transitive closure, version 2 ###
During proofs, it is often more convenient to define the
reflexive-transitive closure in a slightly different manner,
as the smallest relation `R*` satisfying the two following rules :
- Reflexivity : `R*(x,x)`
- Transitivity-Inclusion : If `R*(x,y)` and `R(y,z)` then `R*(x,z)`
Note the use of `R` (and not `R*`) in the middle of the previous rule.
This alternative definition correspond to the following Coq inductive
predicate:
```
Inductive clos2 (R : T -> T -> Prop) : T -> T -> Prop :=
| cl2_refl : forall x, clos2 R x x
| cl2_next : forall x y z, clos2 R x y -> R y z -> clos2 R x z.
```
We will here show that these two definitions `clos1` and `clos2` are
actually equivalent. This can be done in the following intermediate steps:
1. Show that `clos2 R x y` implies `clos1 R x y` (for all `x y:T`).
2. Show that `R x y` implies `clos2 R x y` (for all `x y:T`).
3. Show that `clos2 R` is a transitive relation.
4. Conclude that `clos1 R x y` implies `clos2 R x y` (for all `x y:T`).
### Reflexive-transitive closure, version 3 ###
In Coq, another possible approach is to rely on functions and
recursivity to define predicate.
1. Define the identity relation `id:T->T->Prop`.
2. Define the composition of relations
`comp:(T->T->Prop)->(T->T->Prop)->(T->T->Prop)`.
3. Define a power function on relations
`pow:(T->T->Prop)->nat->(T->T->Prop)`
such that `pow R n` computes the n-th power of the relation
(with respect to composition).
A third possible definition of the reflexive-transitive closure of a
relation `R` is then given by the union of all powers of `R`:
```
Definition clos3 (R : T -> T -> Prop) (x y : T) := exists n, pow R n x y.
```
4. Show that this definition is equivalent to the two previous ones
`clos1` and `clos2`.
......@@ -84,10 +84,10 @@ et `clos2`, en suivant les étapes intermédiaires suivantes:
En Coq, on peut également profiter de la récursivité pour définir des
prédicats.
1. Définir la relation identité `id:T->T->Prop` ainsi que
l'opérateur de composition de relations
`comp:(T->T->Prop)->(T->T->Prop)->(T->T->Prop`.
2. Définir une fonction
1. Définir la relation identité `id:T->T->Prop`
2. Définir l'opérateur de composition de relations
`comp:(T->T->Prop)->(T->T->Prop)->(T->T->Prop)`.
3. Définir une fonction
`puiss:(T->T->Prop)->nat->(T->T->Prop)`
telle que `puiss R n` calcule la puissance n-ième de
la relation (par l'opération de composition).
......@@ -99,5 +99,5 @@ relation `R` est alors donnée par la réunion des puissances successives de
Definition clos3 (R : T -> T -> Prop) (x y : T) := exists n, puiss R n x y.
```
3. Montrer que cette définition est équivalente aux deux
4. Montrer que cette définition est équivalente aux deux
précédentes `clos1` et `clos2`.
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