From dcbebcfd078b47f85a20b5a97b2e5ed851494103 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 26 Jul 2013 17:47:08 +0000 Subject: 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 --- theories/Wellfounded/Lexicographic_Exponentiation.v | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'theories/Wellfounded') 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. -- cgit v1.2.3