Set Implicit Arguments.

(** *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.