Merge branch 'kvx-work' into PseudoAsmblock

1 files changed, 85 insertions, 0 deletions

diff --git a/kvx/lib/IterList.v b/kvx/lib/IterList.v
new file mode 100644
index 00000000..b9eb5922
--- /dev/null
+++ b/kvx/lib/IterList.v
@@ -0,0 +1,85 @@
+Require Import Coqlib.
+
+(** TODO: are these def and lemma already defined in the standard library ?
+
+In this case, it should be better to reuse those of the standard library !
+
+*)
+
+Fixpoint iter {A} (n:nat) (f: A -> A) (x: A) {struct n}: A :=
+  match n with
+  | O => x
+  | S n0 => iter n0 f (f x)
+  end.
+
+Lemma iter_S A (n:nat) (f: A -> A): forall x, iter (S n) f x = f (iter n f x).
+Proof.
+  induction n; simpl; auto.
+  intros; erewrite <- IHn; simpl; auto.
+Qed.
+
+Lemma iter_plus A (n m:nat) (f: A -> A): forall x, iter (n+m) f x = iter m f (iter n f x).
+Proof.
+  induction n; simpl; auto.
+Qed.
+
+Definition iter_tail {A} (n:nat) (l: list A) := iter n (@tl A) l.
+
+Lemma iter_tail_S {A} (n:nat) (l: list A): iter_tail (S n) l = tl (iter_tail n l).
+Proof.
+  apply iter_S.
+Qed.
+
+Lemma iter_tail_plus A (n m:nat) (l: list A): iter_tail (n+m) l = iter_tail m (iter_tail n l).
+Proof.
+  apply iter_plus.
+Qed.
+
+Lemma iter_tail_length A l1: forall (l2: list A), iter_tail (length l1) (l1 ++ l2) = l2.
+Proof.
+  induction l1; auto.
+Qed.
+
+Lemma iter_tail_nil A n: @iter_tail A n nil = nil.
+Proof.
+  unfold iter_tail; induction n; simpl; auto.
+Qed.
+
+Lemma iter_tail_reach_nil A (l: list A): iter_tail (length l) l = nil.
+Proof.
+  rewrite (app_nil_end l) at 2.
+  rewrite iter_tail_length. 
+  auto.
+Qed.
+
+Lemma length_iter_tail {A} (n:nat): forall (l: list A), (n <= List.length l)%nat -> (List.length l = n + List.length (iter_tail n l))%nat.
+Proof.
+  unfold iter_tail; induction n; auto.
+  intros l; destruct l. { simpl; omega. }
+  intros; simpl. erewrite IHn; eauto.
+  simpl in *; omega.
+Qed.
+
+Lemma iter_tail_S_ex {A} (n:nat): forall (l: list A), (n < length l)%nat -> exists x, iter_tail n l = x::(iter_tail (S n) l).
+Proof.
+  unfold iter_tail; induction n; simpl.
+  - intros l; destruct l; simpl; omega || eauto.
+  - intros l H; destruct (IHn (tl l)) as (x & H1).
+    + destruct l; simpl in *; try omega.
+    + rewrite H1; eauto.
+Qed.
+
+Lemma iter_tail_inject1 {A} (n1 n2:nat) (l: list A): (n1 <= List.length l)%nat -> (n2 <= List.length l)%nat -> iter_tail n1 l = iter_tail n2 l -> n1=n2.
+Proof.
+  intros H1 H2 EQ; exploit (length_iter_tail n1 l); eauto.
+  rewrite EQ.
+  rewrite (length_iter_tail n2 l); eauto.
+  omega.
+Qed.
+
+Lemma iter_tail_nil_inject {A} (n:nat) (l: list A): iter_tail n l = nil -> (List.length l <= n)%nat.
+Proof.
+  destruct (le_lt_dec n (List.length l)); try omega.
+  intros; exploit (iter_tail_inject1 n (length l) l); try omega.
+  rewrite iter_tail_reach_nil. auto.
+Qed.
\ No newline at end of file