Module Sequences

Une bibliothèque d'opérateurs sur les relations pour définir les suites de transitions et leurs propriétés.

Set Implicit Arguments.

Section SEQUENCES.

Variable A: Type. (* le type des états *)
Variable R: A -> A -> Prop. (* la relation de transition entre états *)

Suites finies de transitions


Zéro, une ou plusieurs transitions: fermeture réflexive transitive de R.

Inductive star: A -> A -> Prop :=
  | star_refl: forall a,
      star a a
  | star_step: forall a b c,
      R a b -> star b c -> star a c.

Lemma star_one:
  forall (a b: A), R a b -> star a b.
Proof.

Lemma star_trans:
  forall (a b: A), star a b -> forall c, star b c -> star a c.
Proof.

Une ou plusieurs transitions: fermeture transitive de R.

Inductive plus: A -> A -> Prop :=
  | plus_left: forall a b c,
      R a b -> star b c -> plus a c.

Lemma plus_one:
  forall a b, R a b -> plus a b.
Proof.

Lemma plus_star:
  forall a b,
  plus a b -> star a b.
Proof.

Lemma plus_star_trans:
  forall a b c, plus a b -> star b c -> plus a c.
Proof.

Lemma star_plus_trans:
  forall a b c, star a b -> plus b c -> plus a c.
Proof.

Lemma plus_right:
  forall a b c, star a b -> R b c -> plus a c.
Proof.

Absence de transition depuis un état.

Definition irred (a: A) : Prop := forall b, ~(R a b).

Suites infinies de transitions


On peut facilement caractériser le cas où toutes les suites de transitions issues d'un état a sont infinies: il suffit de dire que toute suite finie issue de a peut être prolongée par une transition de plus.

Definition all_seq_inf (a: A) : Prop :=
  forall b, star a b -> exists c, R b c.

Cependant, ce n'est pas le cas que nous voulons caractériser: le cas où il existe au moins une suite infinie de transitions issue de a, a --> a1 --> a2 --> ... -> aN -> ..., sans que toutes les suites issues de a soient nécessairement infinies. Exemple: prenons A = nat et R telle que R 0 0 et R 0 1. all_seq_inf 0 n'est pas vrai car la suite 0 -->* 1 ne peut pas être prolongée. Et pourtant R admet une suite infinie, à savoir 0 --> 0 --> .... On pourrait représenter la suite infinie a0 --> a1 --> a2 --> ... -> aN -> ... explicitement, comme une fonction f: nat -> A telle que f i est le i-ème état ai de la suite.

Definition infseq_with_function (a: A) : Prop :=
  exists f: nat -> A, f 0 = a /\ forall i, R (f i) (f (1 + i)).

C'est une caractérisation correcte, mais peu pratique en Coq: très souvent, la fonction f n'est pas calculable et ne peut donc être définie en Coq. Cependant, nous n'avons pas vraiment besoin de la fonction f. Son ensemble image X nous suffit! Ce qui importe c'est qu'il existe un ensemble X tel que a est dans X et tout b dans X peut faire une transition vers un autre élément de X. Cela suffit pour qu'il existe une suite infinie de transitions depuis a.

Definition infseq (a: A) : Prop :=
  exists X: A -> Prop,
  X a /\ (forall a1, X a1 -> exists a2, R a1 a2 /\ X a2).

Cette définition est essentiellement un principe de coinduction. Montrons quelques propriétés attendues. Par exemple: si la relation R contient un cycle, elle admet une suite infinie.

Remark cycle_infseq:
  forall a, R a a -> infseq a.
Proof.

Plus généralement: si toutes les suites issues de a sont infinies, il existe une suite infinie issue de a.

Lemma infseq_if_all_seq_inf:
  forall a, all_seq_inf a -> infseq a.
Proof.

De même, la caractérisation à base de fonctions infseq_with_function implique infseq.

Lemma infseq_from_function:
  forall a, infseq_with_function a -> infseq a.
Proof.

Un lemme d'inversion sur infseq: si infseq a, i.e. il existe une suite infinie issue de a, alors a peut faire une transition vers un état b qui lui aussi vérifie infseq b.

Lemma infseq_inv:
  forall a, infseq a -> exists b, R a b /\ infseq b.
Proof.

Une variante très utile du principe de coinduction s'appuie sur un ensemble X tel que pour tout a dans X, nous pouvons faire une *ou plusieurs* transitions pour atteindre un état b qui est dans X.

Lemma infseq_coinduction_principle:
  forall (X: A -> Prop),
  (forall a, X a -> exists b, plus a b /\ X b) ->
  forall a, X a -> infseq a.
Proof.

Propriétés de déterminisme des relations de transition fonctionnelles


Une relation de transition est fonctionnelle si tout état peut faire une transition vers au plus un autre état.

Hypothesis R_functional:
  forall a b c, R a b -> R a c -> b = c.

Propriétés d'unicité des suites finies de transitions.

Lemma star_star_inv:
  forall a b, star a b -> forall c, star a c -> star b c \/ star c b.
Proof.

Lemma finseq_unique:
  forall a b b',
  star a b -> irred b ->
  star a b' -> irred b' ->
  b = b'.
Proof.

Un état ne peut à la fois diverger et terminer sur un état irréductible.

Lemma infseq_inv':
  forall a b, R a b -> infseq a -> infseq b.
Proof.

Lemma infseq_star_inv:
  forall a b, star a b -> infseq a -> infseq b.
Proof.

Lemma infseq_finseq_excl:
  forall a b,
  star a b -> irred b -> infseq a -> False.
Proof.

S'il existe une suite infinie de transitions depuis a, toutes les suites de transitions depuis a sont infinies.

Lemma infseq_all_seq_inf:
  forall a, infseq a -> all_seq_inf a.
Proof.

End SEQUENCES.