TD8: Définitions inductives de prédicats

Page du cours

TD8 : Définitions inductives de prédicats

M1 Informatique - Preuves Assistées par Ordinateur

Pierre Letouzey (d’après A. Miquel)

Clôture réflexive-transitive, version 1

Commençons par considérer un type de données particulier:

Parameter T:Type.

Sur ce type T, on cherche à définir la clôture réflexive-transitive d’une relation R:T->T->Prop, à savoir la plus petite relation réflexive et transitive R* contenant R. Il est naturel de définir inductivement cette relation à partir des trois règles suivantes:

  • Inclusion : Si R(x,y) alors R*(x,y)
  • Réflexivité : On a toujours R*(x,x)
  • Transitivité : Si R*(x,y) et R*(y,z) alors R*(x,z)

1. Comment exprime-t-on ensuite le faire que R* est la plus petite relation satisfaisant ces trois propriétés ?

Pour toute relation $R’$ satisfaisant ces trois propriétés, si $R^\ast(x, y)$, alors $R’(x, y)$.

En Coq, cette définition inductive s’effectue de la manière suivante:

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.

La définition Coq ci-dessus, qui est paramétrée par la relation R, engendre en réalité:

  • un transformateur de relation clos1 : (T -> T -> Prop) -> (T -> T -> Prop) qui à chaque relation binaire R associe sa clôture réflexive-transitive clos1 R
  • trois constantes cl1_base, cl1_refl et cl1_trans correspondant aux trois règles de constructions de clos1 R (on parle aussi de constructeurs pour ces constantes).
  • un principe d’induction clos1_ind exprimant que clos1 R est bien la plus petite relation réflexive et transitive contenant R.

2. Comparer le principe d’induction clos1_ind obtenu avec celui formulé à la question précédente.

Print clos1_ind.

clos1_ind =
fun (R P : T -> T -> Prop) (f : forall x y : T, R x y -> P x y)
  (f0 : forall x : T, P x x)
  (f1 : forall x y z : T,
        clos1 R x y -> P x y -> clos1 R y z -> P y z -> P x z) =>
fix F (t t0 : T) (c : clos1 R t t0) {struct c} : P t t0 :=
  match c in (clos1 _ t1 t2) return (P t1 t2) with
  | cl1_base _ x y y0 => f x y y0
  | cl1_refl _ x => f0 x
  | cl1_trans _ x y z c0 c1 => f1 x y z c0 (F x y c0) c1 (F y z c1)
  end
     : forall R P : T -> T -> Prop,
       (forall x y : T, R x y -> P x y) ->
       (forall x : T, P x x) ->
       (forall x y z : T,
        clos1 R x y -> P x y -> clos1 R y z -> P y z -> P x z) ->
       forall t t0 : T, clos1 R t t0 -> P t t0

3. Montrer que si R est symétrique, alors clos1 R l’est aussi.

Definition symmetric (R: T -> T -> Prop) : Prop := forall x y, R x y -> R y x.

Theorem inherited_sym : forall R, symmetric R -> symmetric (clos1 R).
Proof.
  intros.
  unfold symmetric in H.
  unfold symmetric; intros.
  induction H0.
  - constructor.
    now apply H.
  - apply cl1_refll.
  - eapply cl1_transs.
    apply IHclos1_2.
    apply IHclos1_1.
Qed.

4. Montrer que l’opération de clôture réflexive-transitive est idempotente: clos1 (clos1 R) x y -> clos1 R x y pour tous x y:T.

Theorem idempotent_closure : forall x y:T, forall R, clos1 (clos1 R) x y -> clos1 R x y.
Proof.
  intros.
  induction H.
  - easy.
  - now constructor.
  - now apply cl1_trans with y.
Qed.

Clôture réflexive-transitive, version 2

Dans les démonstrations cependant, il est souvent plus commode de définir la clôture réflexive-transitive d’une manière un peu différente, à savoir comme la relation R* engendrée par les deux règles suivantes:

  • Réflexivité : R*(x,x)
  • Transitivité-Inclusion : si R*(x,y) et R(y,z) alors R*(x,z)

Notez l’usage de R (et non R*) au milieu de la règle précédente. Cette définition alternative se modélise en Coq au moyen de la définition inductive suivante:

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.

Nous allons montrer ici l’équivalence des deux définitions clos1 et clos2, en suivant les étapes intermédiaires suivantes:

1. Montrer que clos2 R x y entraîne clos1 R x y (pour tous x y:T).

Theorem clos2_to_clos1 : forall x y:T, forall R, clos2 R x y -> clos1 R x y.
Proof.
  intros.
  induction H.
  - now constructor.
  - apply cl1_base in H0.
    now apply cl1_trans with y.
Qed.

2. Montrer que R x y entraîne clos2 R x y (pour tous x y:T).

Theorem clos2_base : forall x y:T, forall R: T -> T -> Prop, R x y -> clos2 R x y.
Proof.
  intros.
  assert (clos2 R x x).
  now constructor.
  now apply cl2_next with x.
Qed.

3. Montrer que clos2 R est une relation transitive.

Theorem cl2_trans : forall x y z, forall R: T -> T -> Prop, clos2 R x y -> clos2 R y z -> clos2 R x z.
Proof.
  intros.
  induction H0.
  easy.
  apply IHclos2 in H.
  now apply cl2_next with y.
Qed.

4. En déduire que clos1 R x y entraîne clos2 R x y (pour tous x y:T).

Theorem cl1_to_cl2 : forall x y, forall R: T -> T -> Prop, clos1 R x y -> clos2 R x y.
Proof.
  intros.
  induction H.
  - now apply clos2_base.
  - now constructor.
  - now apply cl2_trans with y.
Qed.

Clôture réflexive-transitive, version 3

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 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).

Une troisième définition de la clôture réflexive-transitive d’une relation R est alors donnée par la réunion des puissances successives de R, c’est-à-dire par:

Definition clos3 (R : T -> T -> Prop) (x y : T) := exists n, puiss R n x y.
  1. Montrer que cette définition est équivalente aux deux précédentes clos1 et clos2.

Leave a comment