From f00d64c419351ec25fe84050d233c651bd0c76a0 Mon Sep 17 00:00:00 2001
From: Sébastien Hinderer <Sebastien.Hinderer@inria.fr>
Date: Fri, 9 Jan 2015 17:30:32 +0100
Subject: Add two lemmas about firstn to the List standard library.

---
 theories/Lists/List.v | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

(limited to 'theories/Lists')

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 940b2f1e4..85e364c01 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1655,6 +1655,15 @@ Section Cutting.
     - apply Peano.le_n_S, iHk.
   Qed.
 
+  Lemma firstn_length_le: forall l:list A, forall n:nat,
+    n <= length l -> length (firstn n l) = n.
+  Proof. induction l as [|x xs Hrec].
+    - simpl. intros n H. apply le_n_0_eq in H. rewrite <- H. now simpl.
+    - destruct n.
+      * now simpl.
+      * simpl. intro H. apply le_S_n in H. now rewrite (Hrec n H).
+  Qed.
+
   Lemma firstn_app n:
     forall l1 l2,
     firstn n (l1 ++ l2) = (firstn n l1) ++ (firstn (n - length l1) l2).
@@ -1679,6 +1688,19 @@ Section Cutting.
         rewrite H0, firstn_all2; [reflexivity | auto with arith].
   Qed.
 
+  Lemma firstn_firstn:
+    forall l:list A,
+    forall i j : nat,
+    firstn i (firstn j l) = firstn (min i j) l.
+  Proof. induction l as [|x xs Hl].
+    - intros. simpl. now rewrite ?firstn_nil.
+    - destruct i.
+      * intro. now simpl.
+      * destruct j.
+        + now simpl.
+        + simpl. f_equal. apply Hl.
+  Qed.
+
   Fixpoint skipn (n:nat)(l:list A) : list A :=
     match n with
       | 0 => l
-- 
cgit v1.2.3