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

3 files changed, 45 insertions, 9 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.
 
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index 13db01a36..24f5d308a 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -13,6 +13,7 @@
 
 Require Import List.
 Require Import Relation_Operators.
+Require Import Operators_Properties.
 Require Import Transitive_Closure.
 
 Section Wf_Lexicographic_Exponentiation.
@@ -88,14 +89,14 @@ Section Wf_Lexicographic_Exponentiation.
 
   Lemma desc_tail :
     forall (x:List) (a b:A),
-      Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b.
+      Descl (Cons b (x ++ Cons a Nil)) -> clos_refl_trans A leA a b.
   Proof.
     intro.
     apply rev_ind with
       (A := A)
       (P := fun x:List =>
         forall a b:A,
-          Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b).
+          Descl (Cons b (x ++ Cons a Nil)) -> clos_refl_trans A leA a b).
     intros.
 
     inversion H.
@@ -110,7 +111,7 @@ Section Wf_Lexicographic_Exponentiation.
     generalize (app_inj_tail _ _ _ _ H6); simple induction 1; intros.
     generalize H1.
     rewrite <- H10; rewrite <- H7; intro.
-    apply (t_step A leA); auto with sets.
+    inversion H11; subst; [apply rt_step; assumption|apply rt_refl].
 
     intros.
     inversion H0.
@@ -124,9 +125,10 @@ Section Wf_Lexicographic_Exponentiation.
     generalize (desc_prefix (Cons b (l ++ Cons x0 Nil)) a H5); intro.
     generalize (H x0 b H6).
     intro.
-    apply t_trans with (A := A) (y := x0); auto with sets.
+    apply rt_trans with (A := A) (y := x0); auto with sets.
 
-    apply t_step.
+    match goal with [ |- clos_refl_trans ?A ?R ?x ?y ] => cut (clos_refl A R x y) end.
+    intros; inversion H8; subst; [apply rt_step|apply rt_refl]; assumption.
     generalize H1.
     rewrite H4; intro.
 
@@ -137,8 +139,7 @@ Section Wf_Lexicographic_Exponentiation.
     generalize H10.
     rewrite H12; intro.
     generalize (app_inj_tail _ _ _ _ H13); simple induction 1.
-    intros.
-    rewrite <- H11; rewrite <- H16; auto with sets.
+    intros; subst; assumption.
   Qed.
 
 
@@ -250,7 +251,7 @@ Section Wf_Lexicographic_Exponentiation.
     intros E; rewrite <- E; intros.
     generalize (desc_tail l a a0 H0); intro.
     inversion H1.
-    apply t_trans with (y := a0); auto with sets.
+    eapply clos_rt_t; [eassumption|apply t_step; assumption].
 
     inversion H4.
   Qed.