From 01f1bf7a06abdd62a5d7eb7d13034836211c5d09 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 18 Nov 2009 08:28:44 +0000
Subject: Cleaned up list_drop.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1178 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 lib/Coqlib.v                 | 62 ++++++++++++++++++++------------------------
 powerpc/macosx/Conventions.v | 17 ++++++------
 2 files changed, 37 insertions(+), 42 deletions(-)

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 02fa7bab..0c58da09 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -376,6 +376,15 @@ Proof.
   rewrite two_power_nat_S. rewrite inj_S. rewrite two_p_S. omega. omega.
 Qed.
 
+Lemma two_p_strict:
+  forall x, x >= 0 -> x < two_p x.
+Proof.
+  intros x0 GT. pattern x0. apply natlike_ind.
+  simpl. omega.
+  intros. rewrite two_p_S; auto. generalize (two_p_gt_ZERO x H). omega. 
+  omega.
+Qed.
+
 (** Properties of [Zmin] and [Zmax] *)
 
 Lemma Zmin_spec:
@@ -1038,49 +1047,34 @@ Proof.
   intros. auto with coqlib.
 Qed.
 
-(** Dropping the first or first two elements of a list. *)
-
-Definition list_drop1 (A: Type) (x: list A) :=
-  match x with nil => nil | hd :: tl => tl end.
-Definition list_drop2 (A: Type) (x: list A) :=
-  match x with nil => nil | hd :: nil => nil | hd1 :: hd2 :: tl => tl end.
-
-Lemma list_drop1_incl:
-  forall (A: Type) (x: A) (l: list A), In x (list_drop1 l) -> In x l.
-Proof.
-  intros. destruct l. elim H. simpl in H. auto with coqlib.
-Qed.
-
-Lemma list_drop2_incl:
-  forall (A: Type) (x: A) (l: list A), In x (list_drop2 l) -> In x l.
-Proof.
-  intros. destruct l. elim H. destruct l. elim H.
-  simpl in H. auto with coqlib.
-Qed.
+(** Dropping the first N elements of a list. *)
 
-Lemma list_drop1_norepet:
-  forall (A: Type) (l: list A), list_norepet l -> list_norepet (list_drop1 l).
-Proof.
-  intros. destruct l; simpl. constructor. inversion H. auto.
-Qed.
+Fixpoint list_drop (A: Type) (n: nat) (x: list A) {struct n} : list A :=
+  match n with
+  | O => x
+  | S n' => match x with nil => nil | hd :: tl => list_drop n' tl end
+  end.
 
-Lemma list_drop2_norepet:
-  forall (A: Type) (l: list A), list_norepet l -> list_norepet (list_drop2 l).
+Lemma list_drop_incl:
+  forall (A: Type) (x: A) n (l: list A), In x (list_drop n l) -> In x l.
 Proof.
-  intros. destruct l; simpl. constructor.
-  destruct l; simpl. constructor. inversion H. inversion H3. auto.
+  induction n; simpl; intros. auto. 
+  destruct l; auto with coqlib.
 Qed.
 
-Lemma list_map_drop1:
-  forall (A B: Type) (f: A -> B) (l: list A), list_drop1 (map f l) = map f (list_drop1 l).
+Lemma list_drop_norepet:
+  forall (A: Type) n (l: list A), list_norepet l -> list_norepet (list_drop n l).
 Proof.
-  intros; destruct l; reflexivity.
+  induction n; simpl; intros. auto.
+  inv H. constructor. auto.
 Qed.
 
-Lemma list_map_drop2:
-  forall (A B: Type) (f: A -> B) (l: list A), list_drop2 (map f l) = map f (list_drop2 l).
+Lemma list_map_drop:
+  forall (A B: Type) (f: A -> B) n (l: list A),
+  list_drop n (map f l) = map f (list_drop n l).
 Proof.
-  intros; destruct l. reflexivity. destruct l; reflexivity.
+  induction n; simpl; intros. auto. 
+  destruct l; simpl; auto.
 Qed.
 
 (** * Definitions and theorems over boolean types *)
diff --git a/powerpc/macosx/Conventions.v b/powerpc/macosx/Conventions.v
index 62723627..1954c912 100644
--- a/powerpc/macosx/Conventions.v
+++ b/powerpc/macosx/Conventions.v
@@ -401,7 +401,7 @@ Fixpoint loc_arguments_rec
       | nil =>
           S (Outgoing ofs Tfloat) :: loc_arguments_rec tys iregl nil (ofs + 2)
       | freg :: fregs =>
-          R freg :: loc_arguments_rec tys (list_drop2 iregl) fregs ofs
+          R freg :: loc_arguments_rec tys (list_drop 2%nat iregl) fregs ofs
       end
   end.
 
@@ -432,7 +432,7 @@ Fixpoint size_arguments_rec
   | Tfloat :: tys =>
       match fregl with
       | nil => size_arguments_rec tys iregl nil (ofs + 2)
-      | freg :: fregs => size_arguments_rec tys (list_drop2 iregl) fregs ofs
+      | freg :: fregs => size_arguments_rec tys (list_drop 2%nat iregl) fregs ofs
       end
   end.
 
@@ -465,6 +465,7 @@ Remark loc_arguments_rec_charact:
   | S _ => False
   end.
 Proof.
+Opaque list_drop.
   induction tyl; simpl loc_arguments_rec; intros.
   elim H.
   destruct a. 
@@ -478,7 +479,7 @@ Proof.
   generalize (IHtyl _ _ _ _ H0). destruct l; auto. destruct s; auto. omega.
   subst l. auto with coqlib.
   generalize (IHtyl _ _ _ _ H0). destruct l; auto.
-  intros [A|B]. left; apply list_drop2_incl; auto. right; auto with coqlib.
+  intros [A|B]. left; eapply list_drop_incl; eauto. right; auto with coqlib.
 Qed.
 
 Lemma loc_arguments_acceptable:
@@ -511,7 +512,7 @@ Proof.
   destruct fregl; simpl. auto.
   simpl in H0. split. apply sym_not_equal. tauto.
   apply IHtyl. 
-  red; intro. apply H. apply list_drop2_incl. auto.
+  red; intro. apply H. eapply list_drop_incl. eauto.
   tauto.
 Qed.
 
@@ -562,11 +563,11 @@ Proof.
   destruct fregl; constructor.
   apply loc_arguments_rec_notin_outgoing. simpl; omega. auto.
   apply loc_arguments_rec_notin_reg.
-  red; intro. apply (H1 m m). apply list_drop2_incl; auto. 
+  red; intro. apply (H1 m m). eapply list_drop_incl; eauto. 
   auto with coqlib. auto. inv H0; auto.
-  apply IHtyl. apply list_drop2_norepet; auto.
+  apply IHtyl. eapply list_drop_norepet; eauto.
   inv H0; auto. 
-  red; intros. apply H1. apply list_drop2_incl; auto. auto with coqlib.
+  red; intros. apply H1. eapply list_drop_incl; eauto. auto with coqlib.
 
   intro. unfold loc_arguments. apply H.
   unfold int_param_regs. NoRepet.
@@ -687,7 +688,7 @@ Proof.
   auto.
   destruct a; [destruct iregl|destruct fregl]; simpl;
   f_equal; eauto with coqlib.
-  apply IHtyl. intros. apply H. apply list_drop2_incl; auto.
+  apply IHtyl. intros. apply H. eapply list_drop_incl; eauto.
   eauto with coqlib.
 
   intros. unfold loc_arguments. apply H. 
-- 
cgit