integration of statements related to last element

1 files changed, 60 insertions, 25 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 4c2bd8b874..fae766d6b9 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -281,6 +281,12 @@ Section Facts.
     induction l; simpl; auto.
   Qed.
 
+  Lemma last_length : forall (l : list A) a, length (l ++ a :: nil) = S (length l).
+  Proof.
+    intros ; rewrite app_length ; simpl.
+    rewrite <- plus_n_Sm, plus_n_O; reflexivity.
+  Qed.
+
   Lemma in_app_or : forall (l m:list A) (a:A), In a (l ++ m) -> In a l \/ In a m.
   Proof.
     intros l m a.
@@ -556,31 +562,9 @@ Section Elts.
     rewrite app_nth2; [| auto]. repeat (rewrite Nat.sub_diag). reflexivity.
   Qed.
 
-  (*****************)
-  (** ** Remove    *)
-  (*****************)
-
-  Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
-
-  Fixpoint remove (x : A) (l : list A) : list A :=
-    match l with
-      | [] => []
-      | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl)
-    end.
-
-  Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l).
-  Proof.
-    induction l as [|x l]; auto.
-    intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx].
-    apply IHl.
-    unfold not; intro HF; simpl in HF; destruct HF; auto.
-    apply (IHl y); assumption.
-  Qed.
-
-
-(******************************)
-(** ** Last element of a list *)
-(******************************)
+  (******************************)
+  (** ** Last element of a list *)
+  (******************************)
 
   (** [last l d] returns the last element of the list [l],
     or the default value [d] if [l] is empty. *)
@@ -592,6 +576,13 @@ Section Elts.
     | a :: l => last l d
   end.
 
+  Lemma last_last : forall l a d, last (l ++ [a]) d = a.
+  Proof.
+    induction l; intros; [ reflexivity | ].
+    simpl; rewrite IHl.
+    destruct l; reflexivity.
+  Qed.
+
   (** [removelast l] remove the last element of [l] *)
 
   Fixpoint removelast (l:list A) : list A :=
@@ -638,6 +629,36 @@ Section Elts.
     destruct (l++l'); [elim H0; auto|f_equal; auto].
   Qed.
 
+  Lemma removelast_last : forall l a, removelast (l ++ [a]) = l.
+  Proof.
+    intros.
+    rewrite removelast_app.
+    - apply app_nil_r.
+    - intros Heq; inversion Heq.
+  Qed.
+
+
+  (*****************)
+  (** ** Remove    *)
+  (*****************)
+
+  Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
+
+  Fixpoint remove (x : A) (l : list A) : list A :=
+    match l with
+      | [] => []
+      | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl)
+    end.
+
+  Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l).
+  Proof.
+    induction l as [|x l]; auto.
+    intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx].
+    apply IHl.
+    unfold not; intro HF; simpl in HF; destruct HF; auto.
+    apply (IHl y); assumption.
+  Qed.
+
 
   (******************************************)
   (** ** Counting occurrences of an element *)
@@ -944,6 +965,13 @@ Section Map.
     intros; rewrite IHl; auto.
   Qed.
 
+  Lemma map_last : forall l a,
+    map (l ++ [a]) = (map l) ++ [f a].
+  Proof.
+    induction l; intros; [ reflexivity | ].
+    simpl; rewrite IHl; reflexivity.
+  Qed.
+
   Lemma map_rev : forall l, map (rev l) = rev (map l).
   Proof.
     induction l; simpl; auto.
@@ -1910,6 +1938,13 @@ Section Cutting.
      inversion_clear H0.
    Qed.
 
+   Lemma removelast_firstn_len : forall l,
+     removelast l = firstn (pred (length l)) l.
+   Proof.
+     induction l; [ reflexivity | simpl ].
+     destruct l; [ | rewrite IHl ]; reflexivity.
+   Qed.
+
    Lemma firstn_removelast : forall n l, n < length l ->
      firstn n (removelast l) = firstn n l.
    Proof.