Testing beautifying on an example.

1 files changed, 69 insertions, 63 deletions

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).