diff options
Diffstat (limited to 'theories/Wellfounded/Lexicographic_Exponentiation.v')
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Exponentiation.v | 269 |
1 files changed, 100 insertions, 169 deletions
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index fb3ef1be..dd9e4c98 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -13,8 +13,11 @@ Require Import List. Require Import Relation_Operators. +Require Import Operators_Properties. Require Import Transitive_Closure. +Import ListNotations. + Section Wf_Lexicographic_Exponentiation. Variable A : Set. Variable leA : A -> A -> Prop. @@ -25,14 +28,11 @@ Section Wf_Lexicographic_Exponentiation. Notation Descl := (Desc A leA). Notation List := (list A). - Notation Nil := (nil (A:=A)). - (* useless but symmetric *) - Notation Cons := (cons (A:=A)). Notation "<< x , y >>" := (exist Descl x y) (at level 0, x, y at level 100). (* Hint Resolve d_one d_nil t_step. *) - Lemma left_prefix : forall x y z:List, ltl (x ++ y) z -> ltl x z. + Lemma left_prefix : forall x y z : List, ltl (x ++ y) z -> ltl x z. Proof. simple induction x. simple induction z. @@ -50,8 +50,9 @@ Section Wf_Lexicographic_Exponentiation. Lemma right_prefix : - forall x y z:List, - ltl x (y ++ z) -> ltl x y \/ (exists y' : List, x = y ++ y' /\ ltl y' z). + forall x y z : List, + ltl x (y ++ z) -> + ltl x y \/ (exists y' : List, x = y ++ y' /\ ltl y' z). Proof. intros x y; generalize x. elim y; simpl. @@ -70,172 +71,98 @@ Section Wf_Lexicographic_Exponentiation. right; exists x2; auto with sets. Qed. - Lemma desc_prefix : forall (x:List) (a:A), Descl (x ++ Cons a Nil) -> Descl x. + Lemma desc_prefix : forall (x : List) (a : A), Descl (x ++ [a]) -> Descl x. Proof. intros. inversion H. - generalize (app_cons_not_nil _ _ _ H1); simple induction 1. - cut (x ++ Cons a Nil = Cons x0 Nil); auto with sets. - intro. - generalize (app_eq_unit _ _ H0). - simple induction 1; simple induction 1; intros. - rewrite H4; auto using d_nil with sets. - discriminate H5. - generalize (app_inj_tail _ _ _ _ H0). - simple induction 1; intros. - rewrite <- H4; auto with sets. + - apply app_cons_not_nil in H1 as (). + - assert (x ++ [a] = [x0]) by auto with sets. + apply app_eq_unit in H0 as [(->, _)| (_, [=])]. + auto using d_nil. + - apply app_inj_tail in H0 as (<-, _). + assumption. Qed. Lemma desc_tail : - forall (x:List) (a b:A), - Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b. + forall (x : List) (a b : A), + Descl (b :: x ++ [a]) -> 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). - intros. - - inversion H. - cut (Cons b (Cons a Nil) = (Nil ++ Cons b Nil) ++ Cons a Nil); - auto with sets; intro. - generalize H0. - intro. - generalize (app_inj_tail (l ++ Cons y Nil) (Nil ++ Cons b Nil) _ _ H4); - simple induction 1. - intros. - - generalize (app_inj_tail _ _ _ _ H6); simple induction 1; intros. - generalize H1. - rewrite <- H10; rewrite <- H7; intro. - apply (t_step A leA); auto with sets. - - intros. - inversion H0. - generalize (app_cons_not_nil _ _ _ H3); intro. - elim H1. - - generalize H0. - generalize (app_comm_cons (l ++ Cons x0 Nil) (Cons a Nil) b); - simple induction 1. - intro. - 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 t_step. - generalize H1. - rewrite H4; intro. - - generalize (app_inj_tail _ _ _ _ H8); simple induction 1. - intros. - generalize H2; generalize (app_comm_cons l (Cons x0 Nil) b). - intro. - generalize H10. - rewrite H12; intro. - generalize (app_inj_tail _ _ _ _ H13); simple induction 1. - intros. - rewrite <- H11; rewrite <- H16; auto with sets. + (P := + fun x : List => + forall a b : A, Descl (b :: x ++ [a]) -> clos_refl_trans A leA a b); + intros. + - inversion H. + assert ([b; a] = ([] ++ [b]) ++ [a]) by auto with sets. + destruct (app_inj_tail (l ++ [y]) ([] ++ [b]) _ _ H0) as ((?, <-)/app_inj_tail, <-). + inversion H1; subst; [ apply rt_step; assumption | apply rt_refl ]. + - inversion H0. + + apply app_cons_not_nil in H3 as (). + + rewrite app_comm_cons in H0, H1. apply desc_prefix in H0. + pose proof (H x0 b H0). + apply rt_trans with (y := x0); auto with sets. + enough (H5 : clos_refl A leA a x0) + by (inversion H5; subst; [ apply rt_step | apply rt_refl ]; + assumption). + apply app_inj_tail in H1 as (H1, ->). + rewrite app_comm_cons in H1. + apply app_inj_tail in H1 as (_, <-). + assumption. Qed. Lemma dist_aux : - forall z:List, Descl z -> forall x y:List, z = x ++ y -> Descl x /\ Descl y. + forall z : List, + Descl z -> forall x y : List, z = x ++ y -> Descl x /\ Descl y. Proof. intros z D. - elim D. - intros. - cut (x ++ y = Nil); auto with sets; intro. - generalize (app_eq_nil _ _ H0); simple induction 1. - intros. - rewrite H2; rewrite H3; split; apply d_nil. - - intros. - cut (x0 ++ y = Cons x Nil); auto with sets. - intros E. - generalize (app_eq_unit _ _ E); simple induction 1. - simple induction 1; intros. - rewrite H2; rewrite H3; split. - apply d_nil. - - apply d_one. - - simple induction 1; intros. - rewrite H2; rewrite H3; split. - apply d_one. - - apply d_nil. - - do 5 intro. - intros Hind. - do 2 intro. - generalize x0. - apply rev_ind with - (A := A) - (P := fun y0:List => - forall x0:List, - (l ++ Cons y Nil) ++ Cons x Nil = x0 ++ y0 -> - Descl x0 /\ Descl y0). - - intro. - generalize (app_nil_end x1); simple induction 1; simple induction 1. - split. apply d_conc; auto with sets. - - apply d_nil. - - do 3 intro. - generalize x1. - apply rev_ind with - (A := A) - (P := fun l0:List => - forall (x1:A) (x0:List), - (l ++ Cons y Nil) ++ Cons x Nil = x0 ++ l0 ++ Cons x1 Nil -> - Descl x0 /\ Descl (l0 ++ Cons x1 Nil)). - - - simpl. - split. - generalize (app_inj_tail _ _ _ _ H2); simple induction 1. - simple induction 1; auto with sets. - - apply d_one. - do 5 intro. - generalize (app_ass x4 (l1 ++ Cons x2 Nil) (Cons x3 Nil)). - simple induction 1. - generalize (app_ass x4 l1 (Cons x2 Nil)); simple induction 1. - intro E. - generalize (app_inj_tail _ _ _ _ E). - simple induction 1; intros. - generalize (app_inj_tail _ _ _ _ H6); simple induction 1; intros. - rewrite <- H7; rewrite <- H10; generalize H6. - generalize (app_ass x4 l1 (Cons x2 Nil)); intro E1. - rewrite E1. - intro. - generalize (Hind x4 (l1 ++ Cons x2 Nil) H11). - simple induction 1; split. - auto with sets. - - generalize H14. - rewrite <- H10; intro. - apply d_conc; auto with sets. + induction D as [| | * H D Hind]; intros. + - assert (H0 : x ++ y = []) by auto with sets. + apply app_eq_nil in H0 as (->, ->). + split; apply d_nil. + - assert (E : x0 ++ y = [x]) by auto with sets. + apply app_eq_unit in E as [(->, ->)| (->, ->)]. + + split. + apply d_nil. + apply d_one. + + split. + apply d_one. + apply d_nil. + - induction y0 using rev_ind in x0, H0 |- *. + + rewrite <- app_nil_end in H0. + rewrite <- H0. + split. + apply d_conc; auto with sets. + apply d_nil. + + induction y0 using rev_ind in x1, x0, H0 |- *. + * simpl. + split. + apply app_inj_tail in H0 as (<-, _). assumption. + apply d_one. + * rewrite <- 2!app_assoc_reverse in H0. + apply app_inj_tail in H0 as (H0, <-). + pose proof H0 as H0'. + apply app_inj_tail in H0' as (_, ->). + rewrite app_assoc_reverse in H0. + apply Hind in H0 as (). + split. + assumption. + apply d_conc; auto with sets. Qed. Lemma dist_Desc_concat : - forall x y:List, Descl (x ++ y) -> Descl x /\ Descl y. + forall x y : List, Descl (x ++ y) -> Descl x /\ Descl y. Proof. intros. apply (dist_aux (x ++ y) H x y); auto with sets. Qed. Lemma desc_end : - forall (a b:A) (x:List), - Descl (x ++ Cons a Nil) /\ ltl (x ++ Cons a Nil) (Cons b Nil) -> - clos_trans A leA a b. + forall (a b : A) (x : List), + Descl (x ++ [a]) /\ ltl (x ++ [a]) [b] -> clos_trans A leA a b. Proof. intros a b x. case x. @@ -246,11 +173,11 @@ Section Wf_Lexicographic_Exponentiation. inversion H3. simple induction 1. - generalize (app_comm_cons l (Cons a Nil) a0). + generalize (app_comm_cons l [a] a0). 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. @@ -259,9 +186,8 @@ Section Wf_Lexicographic_Exponentiation. Lemma ltl_unit : - forall (x:List) (a b:A), - Descl (x ++ Cons a Nil) -> - ltl (x ++ Cons a Nil) (Cons b Nil) -> ltl x (Cons b Nil). + forall (x : List) (a b : A), + Descl (x ++ [a]) -> ltl (x ++ [a]) [b] -> ltl x [b]. Proof. intro. case x. @@ -276,9 +202,10 @@ Section Wf_Lexicographic_Exponentiation. Lemma acc_app : - forall (x1 x2:List) (y1:Descl (x1 ++ x2)), + forall (x1 x2 : List) (y1 : Descl (x1 ++ x2)), Acc Lex_Exp << x1 ++ x2, y1 >> -> - forall (x:List) (y:Descl x), ltl x (x1 ++ x2) -> Acc Lex_Exp << x, y >>. + forall (x : List) (y : Descl x), + ltl x (x1 ++ x2) -> Acc Lex_Exp << x, y >>. Proof. intros. apply (Acc_inv (R:=Lex_Exp) (x:=<< x1 ++ x2, y1 >>)). @@ -297,8 +224,10 @@ Section Wf_Lexicographic_Exponentiation. unfold lex_exp at 1; simpl. apply rev_ind with (A := A) - (P := fun x:List => - forall (x0:List) (y:Descl x0), ltl x0 x -> Acc Lex_Exp << x0, y >>). + (P := + fun x : List => + forall (x0 : List) (y : Descl x0), + ltl x0 x -> Acc Lex_Exp << x0, y >>). intros. inversion_clear H0. @@ -306,14 +235,15 @@ Section Wf_Lexicographic_Exponentiation. generalize (well_founded_ind (wf_clos_trans A leA H)). intros GR. apply GR with - (P := fun x0:A => - forall l:List, - (forall (x1:List) (y:Descl x1), - ltl x1 l -> Acc Lex_Exp << x1, y >>) -> - forall (x1:List) (y:Descl x1), - ltl x1 (l ++ Cons x0 Nil) -> Acc Lex_Exp << x1, y >>). + (P := + fun x0 : A => + forall l : List, + (forall (x1 : List) (y : Descl x1), + ltl x1 l -> Acc Lex_Exp << x1, y >>) -> + forall (x1 : List) (y : Descl x1), + ltl x1 (l ++ [x0]) -> Acc Lex_Exp << x1, y >>). intro; intros HInd; intros. - generalize (right_prefix x2 l (Cons x1 Nil) H1). + generalize (right_prefix x2 l [x1] H1). simple induction 1. intro; apply (H0 x2 y1 H3). @@ -324,9 +254,10 @@ Section Wf_Lexicographic_Exponentiation. rewrite H2. apply rev_ind with (A := A) - (P := fun x3:List => - forall y1:Descl (l ++ x3), - ltl x3 (Cons x1 Nil) -> Acc Lex_Exp << l ++ x3, y1 >>). + (P := + fun x3 : List => + forall y1 : Descl (l ++ x3), + ltl x3 [x1] -> Acc Lex_Exp << l ++ x3, y1 >>). intros. generalize (app_nil_end l); intros Heq. generalize y1. @@ -340,15 +271,15 @@ Section Wf_Lexicographic_Exponentiation. apply (H0 x4 y3); auto with sets. intros. - generalize (dist_Desc_concat l (l0 ++ Cons x4 Nil) y1). + generalize (dist_Desc_concat l (l0 ++ [x4]) y1). simple induction 1. intros. generalize (desc_end x4 x1 l0 (conj H8 H5)); intros. generalize y1. - rewrite <- (app_ass l l0 (Cons x4 Nil)); intro. + rewrite <- (app_assoc_reverse l l0 [x4]); intro. generalize (HInd x4 H9 (l ++ l0)); intros HInd2. generalize (ltl_unit l0 x4 x1 H8 H5); intro. - generalize (dist_Desc_concat (l ++ l0) (Cons x4 Nil) y2). + generalize (dist_Desc_concat (l ++ l0) [x4] y2). simple induction 1; intros. generalize (H4 H12 H10); intro. generalize (Acc_inv H14). |