Intégration et formattage du développement de Pierre Castéran sur les

définitions alternatives de la transitivé d'une relation



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11462 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 397 insertions, 69 deletions

diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 4a6d58ec2..22582f75d 100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -8,13 +8,15 @@
 
 (*i $Id$ i*)
 
-(****************************************************************************)
-(*                            Bruno Barras                                  *)
-(****************************************************************************)
+(************************************************************************)
+(** * Some properties of the operators on relations                     *)
+(************************************************************************)
+(** * Initial version by Bruno Barras                                   *)
+(************************************************************************)
 
 Require Import Relation_Definitions.
 Require Import Relation_Operators.
-
+Require Import Setoid.
 
 Section Properties.
 
@@ -25,6 +27,8 @@ Section Properties.
   
   Section Clos_Refl_Trans.
 
+    (** Correctness of the reflexive-transitive closure operator *)
+
     Lemma clos_rt_is_preorder : preorder A (clos_refl_trans A R).
     Proof.
       apply Build_preorder.
@@ -33,6 +37,8 @@ Section Properties.
       exact (rt_trans A R).
     Qed.
 
+    (** Idempotency of the reflexive-transitive closure operator *)
+
     Lemma clos_rt_idempotent :
       incl (clos_refl_trans A (clos_refl_trans A R)) (clos_refl_trans A R).
     Proof.
@@ -42,32 +48,13 @@ Section Properties.
       apply rt_trans with y; auto with sets.
     Qed.
 
-    Lemma clos_refl_trans_ind_left :
-      forall (A:Type) (R:A -> A -> Prop) (M:A) (P:A -> Prop),
-	P M ->
-	(forall P0 N:A, clos_refl_trans A R M P0 -> P P0 -> R P0 N -> P N) ->
-	forall a:A, clos_refl_trans A R M a -> P a.
-    Proof.
-      intros.
-      generalize H H0.
-      clear H H0.
-      elim H1; intros; auto with sets.
-      apply H2 with x; auto with sets.
-      
-      apply H3.
-      apply H0; auto with sets.
-
-      intros.
-      apply H5 with P0; auto with sets.
-      apply rt_trans with y; auto with sets.
-    Qed.
-
-
   End Clos_Refl_Trans.
 
-
   Section Clos_Refl_Sym_Trans.
 
+    (** Reflexive-transitive closure is included in the
+        reflexive-symmetric-transitive closure *)
+
     Lemma clos_rt_clos_rst :
       inclusion A (clos_refl_trans A R) (clos_refl_sym_trans A R).
     Proof.
@@ -76,14 +63,18 @@ Section Properties.
       apply rst_trans with y; auto with sets.
     Qed.
 
+    (** Correctness of the reflexive-symmetric-transitive closure *)
+
     Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans A R).
     Proof.
       apply Build_equivalence.
       exact (rst_refl A R).
       exact (rst_trans A R).
-      exact (rst_sym A R).
+      exact (fun x y => rst_sym A R y x).
     Qed.
 
+    (** Idempotency of the reflexive-symmetric-transitive closure operator *)
+
     Lemma clos_rst_idempotent :
       incl (clos_refl_sym_trans A (clos_refl_sym_trans A R))
       (clos_refl_sym_trans A R).
@@ -92,7 +83,294 @@ Section Properties.
       induction 1; auto with sets.
       apply rst_trans with y; auto with sets.
     Qed.
-  
+
   End Clos_Refl_Sym_Trans.
 
+  Section Equivalences.
+
+  (** *** Equivalences between the different definition of the reflexive,
+      symmetric, transitive closures *)
+
+  (** *** Contributed by P. Casteran *)
+
+    (** Direct transitive closure vs left-step extension *)
+
+    Lemma t1n_trans : forall x y, clos_trans_1n A R x y -> clos_trans A R x y.
+    Proof.
+     induction 1.
+     left; assumption.
+     right with y; auto.
+     left; auto.
+    Qed.
+
+    Lemma trans_t1n : forall x y, clos_trans A R x y -> clos_trans_1n A R x y.
+    Proof.
+      induction 1.
+      left; assumption.
+      generalize IHclos_trans2; clear IHclos_trans2; induction IHclos_trans1.
+      right with y; auto.
+      right with y; auto.
+      eapply IHIHclos_trans1; auto.
+      apply t1n_trans; auto.
+    Qed.
+
+    Lemma t1n_trans_equiv : forall x y, 
+        clos_trans A R x y <-> clos_trans_1n A R x y.
+    Proof.
+      split.
+      apply trans_t1n.
+      apply t1n_trans.
+    Qed.
+
+    (** Direct transitive closure vs right-step extension *)
+
+    Lemma tn1_trans : forall x y, clos_trans_n1 A R x y -> clos_trans A R x y.
+    Proof.
+      induction 1.
+      left; assumption.
+      right with y; auto.
+      left; assumption.
+    Qed.
+
+    Lemma trans_tn1 :  forall x y, clos_trans A R x y -> clos_trans_n1 A R x y.
+    Proof.
+      induction 1.
+      left; assumption.
+      elim IHclos_trans2.
+      intro y0; right with y.
+      auto.
+      auto.
+      intros.
+      right with y0; auto.
+    Qed.
+
+    Lemma tn1_trans_equiv : forall x y, 
+        clos_trans A R x y <-> clos_trans_n1 A R x y.
+    Proof.
+      split.
+      apply trans_tn1.
+      apply tn1_trans.
+    Qed.
+
+    (** Direct reflexive-transitive closure is equivalent to 
+        transitivity by left-step extension *)
+
+    Lemma R_rt1n : forall x y, R x y -> clos_refl_trans_1n A R x y.
+    Proof.
+      intros x y H.
+      right with y;[assumption|left].
+    Qed.
+
+    Lemma R_rtn1 : forall x y, R x y -> clos_refl_trans_n1 A R x y.
+    Proof.
+      intros x y H.
+      right with x;[assumption|left].
+    Qed.
+
+    Lemma rt1n_trans : forall x y, 
+        clos_refl_trans_1n A R x y -> clos_refl_trans A R x y.
+    Proof.
+      induction 1.
+      constructor 2.
+      constructor 3 with y; auto.
+      constructor 1; auto.
+    Qed.
+
+    Lemma trans_rt1n : forall x y, 
+        clos_refl_trans A R x y -> clos_refl_trans_1n A R x y.
+    Proof.
+      induction 1.
+      apply R_rt1n; assumption.
+      left.
+      generalize IHclos_refl_trans2; clear IHclos_refl_trans2;
+        induction IHclos_refl_trans1; auto.
+
+      right with y; auto.
+      eapply IHIHclos_refl_trans1; auto.
+      apply rt1n_trans; auto.
+    Qed.
+
+    Lemma rt1n_trans_equiv : forall x y, 
+      clos_refl_trans A R x y <-> clos_refl_trans_1n A R x y.
+    Proof.
+      split.
+      apply trans_rt1n.
+      apply rt1n_trans.
+    Qed.
+
+    (** Direct reflexive-transitive closure is equivalent to 
+        transitivity by right-step extension *)
+
+    Lemma rtn1_trans : forall x y,
+        clos_refl_trans_n1 A R x y -> clos_refl_trans A R x y.
+    Proof.
+      induction 1.
+      constructor 2.
+      constructor 3 with y; auto.
+      constructor 1; assumption.
+    Qed.
+
+    Lemma trans_rtn1 :  forall x y, 
+        clos_refl_trans A R x y -> clos_refl_trans_n1 A R x y.
+    Proof.
+      induction 1.
+      apply R_rtn1; auto.
+      left.
+      elim IHclos_refl_trans2; auto.
+      intros.
+      right with y0; auto.
+    Qed.
+
+    Lemma rtn1_trans_equiv : forall x y, 
+        clos_refl_trans A R x y <-> clos_refl_trans_n1 A R x y.
+    Proof.
+      split.
+      apply trans_rtn1.
+      apply rtn1_trans.
+    Qed.
+
+    (** Induction on the left transitive step *)
+
+    Lemma clos_refl_trans_ind_left :
+      forall (x:A) (P:A -> Prop), P x ->
+	(forall y z:A, clos_refl_trans A R x y -> P y -> R y z -> P z) ->
+	forall z:A, clos_refl_trans A R x z -> P z.
+    Proof.
+      intros.
+      revert H H0.
+      induction H1; intros; auto with sets.
+      apply H1 with x; auto with sets.
+      
+      apply IHclos_refl_trans2.
+      apply IHclos_refl_trans1; auto with sets.
+
+      intros.
+      apply H0 with y0; auto with sets.
+      apply rt_trans with y; auto with sets.
+    Qed.
+
+    (** Induction on the right transitive step *)
+
+    Lemma rt1n_ind_right : forall (P : A -> Prop) (z:A),
+      P z ->
+      (forall x y, R x y -> clos_refl_trans_1n A R y z -> P y -> P x) ->
+      forall x, clos_refl_trans_1n A R x z -> P x.
+      induction 3; auto.
+      apply H0 with y; auto.
+    Qed.
+
+    Lemma clos_refl_trans_ind_right : forall (P : A -> Prop) (z:A),
+      P z ->
+      (forall x y, R x y -> P y -> clos_refl_trans A R y z -> P x) ->
+      forall x, clos_refl_trans A R x z -> P x.
+      intros.
+      rewrite rt1n_trans_equiv in H1.
+      elim H1 using rt1n_ind_right; auto.
+      intros; rewrite  <- rt1n_trans_equiv in *.
+      eauto.
+    Qed.
+
+    (** Direct reflexive-symmetric-transitive closure is equivalent to 
+        transitivity by symmetric left-step extension *)
+
+    Lemma rts1n_rts  : forall x y, 
+      clos_refl_sym_trans_1n A R x y -> clos_refl_sym_trans A R x y.
+    Proof.
+      induction 1.
+      constructor 2.
+      constructor 4 with y; auto.
+      case H;[constructor 1|constructor 3; constructor 1]; auto.
+    Qed.
+
+    Lemma rts_1n_trans : forall x y, clos_refl_sym_trans_1n A R x y ->
+      forall z, clos_refl_sym_trans_1n A R y z -> 
+        clos_refl_sym_trans_1n A R x z.
+      induction 1.
+      auto.
+      intros; right with y; eauto.
+    Qed.
+
+    Lemma rts1n_sym : forall x y, clos_refl_sym_trans_1n A R x y ->
+      clos_refl_sym_trans_1n A R y x.
+    Proof.
+      intros x y H; elim H.
+      constructor 1.
+      intros x0 y0 z D H0 H1; apply rts_1n_trans with y0; auto.
+      right with x0.
+      tauto.
+      left.
+    Qed.
+
+    Lemma rts_rts1n  : forall x y, 
+      clos_refl_sym_trans A R x y -> clos_refl_sym_trans_1n A R x y.
+      induction 1.
+      constructor 2 with y; auto.
+      constructor 1.
+      constructor 1.
+      apply rts1n_sym; auto.
+      eapply rts_1n_trans; eauto.
+    Qed.
+
+    Lemma rts_rts1n_equiv : forall x y, 
+      clos_refl_sym_trans A R x y <-> clos_refl_sym_trans_1n A R x y.
+    Proof.
+      split.
+      apply rts_rts1n.
+      apply rts1n_rts.
+    Qed.
+
+    (** Direct reflexive-symmetric-transitive closure is equivalent to 
+        transitivity by symmetric right-step extension *)
+
+    Lemma rtsn1_rts : forall x y, 
+      clos_refl_sym_trans_n1 A R x y -> clos_refl_sym_trans A R x y.
+    Proof.
+      induction 1.
+      constructor 2.
+      constructor 4 with y; auto.
+      case H;[constructor 1|constructor 3; constructor 1]; auto.
+    Qed.
+
+    Lemma rtsn1_trans : forall y z, clos_refl_sym_trans_n1 A R y z->
+      forall x, clos_refl_sym_trans_n1 A R x y -> 
+        clos_refl_sym_trans_n1 A R x z.
+    Proof.
+      induction 1.
+      auto.
+      intros.
+      right with y0; eauto.
+    Qed.
+
+    Lemma rtsn1_sym : forall x y, clos_refl_sym_trans_n1 A R x y ->
+      clos_refl_sym_trans_n1 A R y x.
+    Proof.
+      intros x y H; elim H.
+      constructor 1.
+      intros y0 z D H0 H1. apply rtsn1_trans with y0; auto.
+      right with z.
+      tauto.
+      left.
+    Qed.
+
+    Lemma rts_rtsn1 : forall x y, 
+      clos_refl_sym_trans A R x y -> clos_refl_sym_trans_n1 A R x y.
+    Proof.
+      induction 1.
+      constructor 2 with x; auto.
+      constructor 1.
+      constructor 1.
+      apply rtsn1_sym; auto.
+      eapply rtsn1_trans; eauto.
+    Qed.
+
+    Lemma rts_rtsn1_equiv : forall x y, 
+      clos_refl_sym_trans A R x y <-> clos_refl_sym_trans_n1 A R x y.
+    Proof.
+      split.
+      apply rts_rtsn1.
+      apply rtsn1_rts.
+    Qed.
+
+  End Equivalences.
+
 End Properties.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index a5ad269d4..2793da5b1 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -8,66 +8,117 @@
 
 (*i $Id$ i*)
 
-(****************************************************************************)
-(*                      Bruno Barras, Cristina Cornes                       *)
-(*                                                                          *)
-(*  Some of these definitons were taken from :                              *)
-(*     Constructing Recursion Operators in Type Theory                      *)
-(*     L. Paulson  JSC (1986) 2, 325-355                                    *)
-(****************************************************************************)
+(************************************************************************)
+(** *                   Bruno Barras, Cristina Cornes                   *)
+(** *                                                                   *)
+(** * Some of these definitions were taken from :                       *)
+(** *    Constructing Recursion Operators in Type Theory                *)
+(** *    L. Paulson  JSC (1986) 2, 325-355                              *)
+(************************************************************************)
 
 Require Import Relation_Definitions.
 Require Import List.
 
-(** Some operators to build relations *)
+(** * Some operators to build relations *)
+
+(** ** Transitive closure *)
 
 Section Transitive_Closure.
   Variable A : Type.
   Variable R : relation A.
-  
+
+  (** Definition by direct transitive closure *)
+
   Inductive clos_trans (x: A) : A -> Prop :=
-    | t_step : forall y:A, R x y -> clos_trans x y
-    | t_trans :
-        forall y z:A, clos_trans x y -> clos_trans y z -> clos_trans x z.
+    | t_step (y:A) : R x y -> clos_trans x y
+    | t_trans (y z:A) : clos_trans x y -> clos_trans y z -> clos_trans x z.
+
+  (** Alternative definition by transitive extension on the left *)
+
+  Inductive clos_trans_1n (x: A) : A -> Prop :=
+    | t1n_step (y:A) : R x y -> clos_trans_1n x y
+    | t1n_trans (y z:A) : R x y -> clos_trans_1n y z -> clos_trans_1n x z.
+
+  (** Alternative definition by transitive extension on the right *)
+
+  Inductive clos_trans_n1 (x: A) : A -> Prop :=
+    | tn1_step (y:A) : R x y -> clos_trans_n1 x y
+    | tn1_trans (y z:A) : R y z -> clos_trans_n1 x y -> clos_trans_n1 x z.
+
 End Transitive_Closure.
 
+(** ** Reflexive-transitive closure *)
 
 Section Reflexive_Transitive_Closure.
   Variable A : Type.
   Variable R : relation A.
 
-  Inductive clos_refl_trans (x:A) : A -> Prop:=
-    | rt_step : forall y:A, R x y -> clos_refl_trans x y
+  (** Definition by direct reflexive-transitive closure *)
+
+  Inductive clos_refl_trans (x:A) : A -> Prop :=
+    | rt_step (y:A) : R x y -> clos_refl_trans x y
     | rt_refl : clos_refl_trans x x
-    | rt_trans :
-        forall y z:A,
+    | rt_trans (y z:A) :
           clos_refl_trans x y -> clos_refl_trans y z -> clos_refl_trans x z.
+
+  (** Alternative definition by transitive extension on the left *)
+
+  Inductive clos_refl_trans_1n (x: A) : A -> Prop :=
+    | rt1n_refl : clos_refl_trans_1n x x
+    | rt1n_trans (y z:A) : 
+         R x y -> clos_refl_trans_1n y z -> clos_refl_trans_1n x z.
+
+  (** Alternative definition by transitive extension on the right *)
+
+ Inductive clos_refl_trans_n1 (x: A) : A -> Prop :=
+    | rtn1_refl : clos_refl_trans_n1 x x
+    | rtn1_trans (y z:A) :
+        R y z -> clos_refl_trans_n1 x y -> clos_refl_trans_n1 x z.
+
 End Reflexive_Transitive_Closure.
 
+(** ** Reflexive-symmetric-transitive closure *)
 
 Section Reflexive_Symetric_Transitive_Closure.
   Variable A : Type.
   Variable R : relation A.
   
-  Inductive clos_refl_sym_trans : relation A :=
-    | rst_step : forall x y:A, R x y -> clos_refl_sym_trans x y
-    | rst_refl : forall x:A, clos_refl_sym_trans x x
-    | rst_sym :
-      forall x y:A, clos_refl_sym_trans x y -> clos_refl_sym_trans y x
-    | rst_trans :
-      forall x y z:A,
+  (** Definition by direct reflexive-symmetric-transitive closure *)
+
+  Inductive clos_refl_sym_trans (x:A) : A -> Prop :=
+    | rst_step (y:A) : R x y -> clos_refl_sym_trans x y
+    | rst_refl : clos_refl_sym_trans x x
+    | rst_sym (y:A) : clos_refl_sym_trans y x -> clos_refl_sym_trans x y
+    | rst_trans (y z:A) :
         clos_refl_sym_trans x y ->
         clos_refl_sym_trans y z -> clos_refl_sym_trans x z.
+
+  (** Alternative definition by symmetric-transitive extension on the left *)
+
+  Inductive clos_refl_sym_trans_1n (x: A) : A -> Prop :=
+    | rts1n_refl : clos_refl_sym_trans_1n x x
+    | rts1n_trans (y z:A) : R x y \/ R y x ->
+         clos_refl_sym_trans_1n y z -> clos_refl_sym_trans_1n x z.
+
+  (** Alternative definition by symmetric-transitive extension on the right *)
+
+  Inductive clos_refl_sym_trans_n1 (x: A) : A -> Prop :=
+    | rtsn1_refl : clos_refl_sym_trans_n1 x x
+    | rtsn1_trans (y z:A) : R y z \/ R z y -> 
+         clos_refl_sym_trans_n1 x y -> clos_refl_sym_trans_n1 x z.
+
 End Reflexive_Symetric_Transitive_Closure.
 
+(** ** Converse of a relation *)
 
-Section Transposee.
+Section Converse.
   Variable A : Type.
   Variable R : relation A.
 
   Definition transp (x y:A) := R y x.
-End Transposee.
+End Converse.
 
+(** ** Union of relations *)
 
 Section Union.
   Variable A : Type.
@@ -76,6 +127,7 @@ Section Union.
   Definition union (x y:A) := R1 x y \/ R2 x y.
 End Union.
 
+(** ** Disjoint union of relations *)
 
 Section Disjoint_Union.
 Variables A B : Type.
@@ -83,16 +135,15 @@ Variable leA : A -> A -> Prop.
 Variable leB : B -> B -> Prop.
 
 Inductive le_AsB : A + B -> A + B -> Prop :=
-  | le_aa : forall x y:A, leA x y -> le_AsB (inl _ x) (inl _ y)
-  | le_ab : forall (x:A) (y:B), le_AsB (inl _ x) (inr _ y)
-  | le_bb : forall x y:B, leB x y -> le_AsB (inr _ x) (inr _ y).
+  | le_aa (x y:A) : leA x y -> le_AsB (inl _ x) (inl _ y)
+  | le_ab (x:A) (y:B) : le_AsB (inl _ x) (inr _ y)
+  | le_bb (x y:B) : leB x y -> le_AsB (inr _ x) (inr _ y).
 
 End Disjoint_Union. 
 
-
+(** ** Lexicographic order on dependent pairs *)
 
 Section Lexicographic_Product.
-  (* Lexicographic order on dependent pairs *)
 
   Variable A : Type.
   Variable B : A -> Type.
@@ -106,8 +157,10 @@ Section Lexicographic_Product.
     | right_lex :
       forall (x:A) (y y':B x),
         leB x y y' -> lexprod (existS B x y) (existS B x y').
+
 End Lexicographic_Product.
 
+(** ** Product of relations *)
 
 Section Symmetric_Product.
   Variable A : Type.
@@ -123,16 +176,15 @@ Section Symmetric_Product.
 
 End Symmetric_Product.
 
+(** ** Multiset of two relations *)
 
 Section Swap.
   Variable A : Type.
   Variable R : A -> A -> Prop.
 
   Inductive swapprod : A * A -> A * A -> Prop :=
-    | sp_noswap : forall x x':A * A, symprod A A R R x x' -> swapprod x x'
-    | sp_swap :
-      forall (x y:A) (p:A * A),
-        symprod A A R R (x, y) p -> swapprod (y, x) p.
+    | sp_noswap x y (p:A * A) : symprod A A R R (x, y) p -> swapprod (x, y) p
+    | sp_swap x y (p:A * A) : symprod A A R R (x, y) p -> swapprod (y, x) p.
 End Swap.
 
 
@@ -144,16 +196,14 @@ Section Lexicographic_Exponentiation.
   Let List := list A.
   
   Inductive Ltl : List -> List -> Prop :=
-    | Lt_nil : forall (a:A) (x:List), Ltl Nil (a :: x)
-    | Lt_hd : forall a b:A, leA a b -> forall x y:list A, Ltl (a :: x) (b :: y)
-    | Lt_tl : forall (a:A) (x y:List), Ltl x y -> Ltl (a :: x) (a :: y).
-
+    | Lt_nil (a:A) (x:List) : Ltl Nil (a :: x)
+    | Lt_hd (a b:A) : leA a b -> forall x y:list A, Ltl (a :: x) (b :: y)
+    | Lt_tl (a:A) (x y:List) : Ltl x y -> Ltl (a :: x) (a :: y).
 
   Inductive Desc : List -> Prop :=
     | d_nil : Desc Nil
-    | d_one : forall x:A, Desc (x :: Nil)
-    | d_conc :
-      forall (x y:A) (l:List),
+    | d_one (x:A) : Desc (x :: Nil)
+    | d_conc (x y:A) (l:List) :
         leA x y -> Desc (l ++ y :: Nil) -> Desc ((l ++ y :: Nil) ++ x :: Nil).
 
   Definition Pow : Set := sig Desc.