diff options
| -rw-r--r-- | lib/Coqlib.v | 62 | ||||
| -rw-r--r-- | powerpc/macosx/Conventions.v | 17 |
2 files changed, 37 insertions, 42 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 02fa7ba..0c58da0 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 6272362..1954c91 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. |