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.

eauto using star.
Qed.

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

Proof.

induction 1; eauto using star.
Qed.

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.

eauto using star, plus.
Qed.

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

Proof.

intros. inversion H. eauto using star.
Qed.

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

Proof.

intros. inversion H. eauto using plus, star_trans.
Qed.

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

Proof.

intros. inversion H0. inversion H; eauto using plus, star, star_trans.
Qed.

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

Proof.

eauto using star_plus_trans, plus_one.
Qed.

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.

  intros. exists (fun b => b = a); split.
  auto.
  intros. subst a1. exists a; auto.
Qed.

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.

  intros a0 ALL0.
  exists all_seq_inf; split; auto.
  intros a1 ALL1. destruct (ALL1 a1) as [a2 R12]. constructor.
  exists a2; split; auto.
  intros a3 S23. destruct (ALL1 a3) as [a4 R23]. apply star_step with a2; auto.
  exists a4; auto.
Qed.

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.

intros a0 (f & F0 & Fn). exists (fun a => exists i, f i = a); split.
- exists 0; auto.
- intros a1 (i1 & F1). subst a1. exists (f (1 + i1)); split; auto. exists (1 + i1); auto.
Qed.

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.

intros a (X & Xa & XP). destruct (XP a Xa) as (b & Rab & Xb).
exists b; split; auto. exists X; auto.
Qed.

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.

  intros X H a0 Xa0.
  exists (fun a => exists b, star a b /\ X b); split.
- exists a0; auto using star_refl.
- intros a1 (a2 & S12 & X2). inversion S12; subst.
  + destruct (H a2 X2) as (a3 & P23 & X3). inversion P23; subst.
    exists b; split; auto. exists a3; auto.
  + exists b; split; auto. exists a2; auto.
Qed.

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.

induction 1; intros.
- auto.
- inversion H1; subst.
+ right. eauto using star.
+ assert (b = b0) by (eapply R_functional; eauto). subst b0.
apply IHstar; auto.
Qed.

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

Proof.

intros. destruct (star_star_inv H H1).
- inversion H3; subst. auto. elim (H0 _ H4).
- inversion H3; subst. auto. elim (H2 _ H4).
Qed.

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.

  intros a b Rab Ia.
  destruct (infseq_inv Ia) as (b' & Rab' & Xb').
  assert (b' = b) by (eapply R_functional; eauto).
  subst b'. auto.
Qed.

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

Proof.

induction 1; intros.
- auto.
- apply IHstar. apply infseq_inv' with a; auto.
Qed.

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

Proof.

  intros.
  destruct (@infseq_inv b) as (c & Rbc & _). eapply infseq_star_inv; eauto.
  apply (H0 c); auto.
Qed.

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.

  intros. unfold all_seq_inf. intros.
  destruct (@infseq_inv b) as (c & Rbc & _). eapply infseq_star_inv; eauto.
  exists c; auto.
Qed.

End SEQUENCES.