Set Implicit Arguments.

(** *Proprie'te'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 := ...

(** Fermeture re'flexive-transitive de [R] *)
Inductive Rstar [x:M] : M -> Prop := ...

(** Enregistre les constructeurs de [Rstar] dans la base de Hints *)
Hint rstar_constr := Constructors Rstar.

(** Proprie'te's de [Rstar] *)
Lemma R_Rstar : (x,y:M)(R x y)->(Rstar x y).

Lemma Rstar_trans : (x,y,z:M)(Rstar x y)->(Rstar y z)->(Rstar x z).

(** Enregistre les lemmes [R_Rstar] et [Rstar_trans] dans la base de Hints *)
Hints Resolve R_Rstar Rstar_trans.

(** De'finition inductive des points accessibles par [R] a` partir de [init] *)
Inductive accessible [init : M -> Prop] : M -> Prop := ...

Hint acc_constr := Constructors accessible.

(** Lien entre l'accessibilite' 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)).


(** De'finition co-inductive du fait que [P] est vrai pour tous 
    les points accessibles a` partir de [x] *)

Variable P : M -> Prop.

CoInductive allways : M -> Prop := ...

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

Lemma allways_inv : (invariant allways).

Hints Resolve allways_inv.

Lemma allways_P_Rstar : (x:M)(allways x)->(y:M)(Rstar x y)->(allways y).

Hints Resolve allways_P_Rstar.

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

(** Si un invariant [I] est trouve' qui implique la proprie'te' [P] 
    alors [P] est vrai 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) := 

End Relations.