Module relation

Propriétés d'une relation de transition

Section Relations.
Variable M : Set.
Variable R : M->M->Prop.

I est un invariant pour la relation R


Definition invariant [I : (M -> Prop)] : Prop
   := (x:M)(I x)->(y:M)(R x y)->(I y).

Fermeture réflexive-transitive de R


Inductive Rstar [x:M] : M -> Prop :=
        Rstar_refl : (Rstar x x)
      | Rstar_plus : (y,z:M)(Rstar x y)->(R y z)->(Rstar x z).

Enregistre les constructeurs de Rstar dans la base de Hints


Hint rstar_constr := Constructors Rstar.

Propriétés de Rstar


Lemma R_Rstar : (x,y:M)(R x y)->(Rstar x y).
EAuto.
Save.

Lemma Rstar_trans : (x,y,z:M)(Rstar x y)->(Rstar y z)->(Rstar x z).
Induction 2; EAuto.
Save.

Enregistre les lemmes R_Rstar et Rstar_trans dans la base de Hints


Hints Resolve R_Rstar Rstar_trans.

Définition inductive des points accessibles par R à partir de init

Inductive accessible [init : M -> Prop] : M -> Prop :=
    acc_init : (m:M)(init m)->(accessible init m)
  | acc_inv : (invariant (accessible init)).

Hint acc_constr := Constructors accessible.

Lien entre l'accessibilité et la fermeture transitive (accessible init y)<->(EX x:M | (init x) & (Rstar x y))

Lemma accessible_equiv :
  (init:M->Prop)(y:M)(accessible init y)<->(EX x:M | (init x) & (Rstar x y)).
Split.
Induction 1.
Intros m Im; Exists m; Auto.
Intros.
Case H1.
Intros.
Exists x0; EAuto.

Destruct 1.
Induction 2; EAuto.
Intros.
Apply (!acc_inv init y0); Trivial.
Save.

Définition co-inductive du fait que P est vrai pour tous les points accessibles à partir de x

Variable P : M -> Prop.

CoInductive allways : M -> Prop :=
  All_intro : (x:M)(P x)->((y:M)(R x y)->(allways y))->(allways x).

Lien entre allways et la fermeture transitive (allways x) <-> ((y:M)(Rstar x y)->(P y))

Lemma allways_P : (x:M)(allways x)->(P x).
Destruct 1; Auto.
Save.

Lemma allways_inv : (invariant allways).
Red.
Destruct 1; Auto.
Save.
Hints Resolve allways_inv.

Lemma allways_P_Rstar : (x:M)(allways x)->(y:M)(Rstar x y)->(allways y).
Induction 2; EAuto.
Save.
Hints Resolve allways_P_Rstar.

Lemma allways_equiv : (x:M)((allways x) <-> ((y:M)(Rstar x y)->(P y))).

Split.
Intros; Apply allways_P; EAuto.

Generalize x; Cofix F; Intros.
Constructor.
Auto.
Intros.
Apply F; EAuto.
Save.

Si un invariant I est trouvé qui implique la propriété P alors P est vraie partout

Variable I : M->Prop.
Hypothesis I_inv : (invariant I).
Hypothesis I_P : (x:M)(I x)->(P x).

CoFixpoint inv_allways : (x:M)(I x)->(allways x) :=
  [x,i](All_intro (I_P i) [y:M][h:(R x y)](inv_allways (I_inv i h))).

End Relations.