Fixing #3089. This implied tweaking the definition of the lexicographic

product of lists, hence possibly introducing incompatibilities.

Parts of the patch by Chantal Keller.

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

2 files changed, 36 insertions, 1 deletions

diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 779c3d9a2..e599669f8 100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -17,6 +17,7 @@ Require Import Relation_Operators.
 
 Section Properties.
 
+  Arguments clos_refl [A] R x _.
   Arguments clos_refl_trans [A] R x _.
   Arguments clos_refl_trans_1n [A] R x _.
   Arguments clos_refl_trans_n1 [A] R x _.
@@ -71,6 +72,26 @@ Section Properties.
       apply rst_trans with y; auto with sets.
     Qed.
 
+    (** Reflexive closure is included in the
+        reflexive-transitive closure *)
+
+    Lemma clos_r_clos_rt :
+      inclusion (clos_refl R) (clos_refl_trans R).
+    Proof.
+      induction 1 as [? ?| ].
+      constructor; auto.
+      constructor 2.
+    Qed.
+
+    Lemma clos_rt_t : forall x y z,
+      clos_refl_trans R x y -> clos_trans R y z ->
+      clos_trans R x z.
+    Proof.
+      induction 1 as [b d H1|b|a b d H1 H2 IH1 IH2]; auto.
+      intro H. apply t_trans with (y:=d); auto.
+      constructor. auto.
+    Qed.
+
     (** Correctness of the reflexive-symmetric-transitive closure *)
 
     Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans R).
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index b71595784..6e686d5c8 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -46,6 +46,20 @@ Section Transitive_Closure.
 
 End Transitive_Closure.
 
+(** ** Reflexive closure *)
+
+Section Reflexive_Closure.
+  Variable A : Type.
+  Variable R : relation A.
+
+  (** Definition by direct transitive closure *)
+
+  Inductive clos_refl (x: A) : A -> Prop :=
+    | r_step (y:A) : R x y -> clos_refl x y
+    | r_refl (y z:A) : clos_refl x x.
+
+End Reflexive_Closure.
+
 (** ** Reflexive-transitive closure *)
 
 Section Reflexive_Transitive_Closure.
@@ -204,7 +218,7 @@ Section Lexicographic_Exponentiation.
     | d_nil : Desc Nil
     | 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).
+        clos_refl A leA x y -> Desc (l ++ y :: Nil) -> Desc ((l ++ y :: Nil) ++ x :: Nil).
 
   Definition Pow : Set := sig Desc.