From ac9f225940357ffd9841f1df277c4f78964df313 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 5 Aug 2014 15:20:08 +0200 Subject: Testing beautifying on an example. --- .../Wellfounded/Lexicographic_Exponentiation.v | 132 +++++++++++---------- 1 file changed, 69 insertions(+), 63 deletions(-) (limited to 'theories/Wellfounded') diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index b64d7f290..fe4fd179e 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -16,6 +16,8 @@ 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. @@ -26,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. @@ -51,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. @@ -71,56 +71,59 @@ 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. - - apply app_cons_not_nil in H1 as []. - - assert (x ++ Cons a Nil = Cons x0 Nil) by auto with sets. - apply app_eq_unit in H0 as [(->,_)|(_,[=])]. + - 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 (<-,_). + - 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_refl_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 - (P := fun x:List => - forall a b:A, - Descl (Cons b (x ++ Cons a Nil)) -> clos_refl_trans A leA a b); intros. + (P := + fun x : List => + forall a b : A, Descl (b :: x ++ [a]) -> clos_refl_trans A leA a b); + intros. - inversion H. - assert (Cons b (Cons a Nil) = (Nil ++ Cons b Nil) ++ Cons a Nil) by - auto with sets. - destruct (app_inj_tail (l ++ Cons y Nil) (Nil ++ Cons b Nil) _ _ H0) as (H6,<-). - apply app_inj_tail in H6 as (?,<-). - inversion H1; subst; [apply rt_step; assumption|apply rt_refl]. + assert ([b; a] = ([] ++ [b]) ++ [a]) by auto with sets. + destruct (app_inj_tail (l ++ [y]) ([] ++ [b]) _ _ H0) as (H6, <-). + apply app_inj_tail in H6 as (?, <-). + inversion H1; subst; [ apply rt_step; assumption | apply rt_refl ]. - inversion H0. - + apply app_cons_not_nil in H3 as []. + + 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,->). + 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 (_,<-). + 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. - induction D as [ | |* H D Hind]; intros. - - assert (H0 : x ++ y = Nil) by auto with sets. - apply app_eq_nil in H0 as (->,->). + 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 = Cons x Nil) by auto with sets. - apply app_eq_unit in E as [(->,->)|(->,->)]. + - assert (E : x0 ++ y = [x]) by auto with sets. + apply app_eq_unit in E as [(->, ->)| (->, ->)]. + split. apply d_nil. apply d_one. @@ -136,14 +139,14 @@ Section Wf_Lexicographic_Exponentiation. + induction y0 using rev_ind in x1, x0, H0 |- *. * simpl. split. - apply app_inj_tail in H0 as (<-,_). assumption. + apply app_inj_tail in H0 as (<-, _). assumption. apply d_one. - * rewrite <- 2!app_ass in H0. - apply app_inj_tail in H0 as (H0,<-). + * 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_ass in H0. - apply Hind in H0 as []. + 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. @@ -152,16 +155,15 @@ Section Wf_Lexicographic_Exponentiation. 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. @@ -172,11 +174,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. - eapply clos_rt_t; [eassumption|apply t_step; assumption]. + eapply clos_rt_t; [ eassumption | apply t_step; assumption ]. inversion H4. Qed. @@ -185,9 +187,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. @@ -202,9 +203,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 >>)). @@ -223,8 +225,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. @@ -232,14 +236,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). @@ -250,9 +255,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. @@ -266,15 +272,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). -- cgit v1.2.3