From 210352d90e5972aabfb253f7c8a38349f53917b3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 22 Oct 2006 16:54:24 +0000 Subject: Lever la restriction sur les fonctions externes, restriction qui exigeait que tous les arguments resident en registres git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Coqlib.v | 44 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 3bcc8a69..b5d59b86 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -637,6 +637,21 @@ Proof. apply sym_not_equal. apply H; auto. Qed. +Lemma list_disjoint_dec: + forall (A: Set) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l1 l2: list A), + {list_disjoint l1 l2} + {~list_disjoint l1 l2}. +Proof. + induction l1; intros. + left; red; intros. elim H. + case (In_dec eqA_dec a l2); intro. + right; red; intro. apply (H a a); auto with coqlib. + case (IHl1 l2); intro. + left; red; intros. elim H; intro. + red; intro; subst a y. contradiction. + apply l; auto. + right; red; intros. elim n0. eapply list_disjoint_cons_left; eauto. +Defined. + (** [list_norepet l] holds iff the list [l] contains no repetitions, i.e. no element occurs twice. *) @@ -658,7 +673,7 @@ Proof. right. red; intro. inversion H. contradiction. left. constructor; auto. right. red; intro. inversion H. contradiction. -Qed. +Defined. Lemma list_map_norepet: forall (A B: Set) (f: A -> B) (l: list A), @@ -803,3 +818,30 @@ Proof. destruct l; simpl. constructor. inversion H. inversion H3. auto. Qed. +Lemma list_map_drop1: + forall (A B: Set) (f: A -> B) (l: list A), list_drop1 (map f l) = map f (list_drop1 l). +Proof. + intros; destruct l; reflexivity. +Qed. + +Lemma list_map_drop2: + forall (A B: Set) (f: A -> B) (l: list A), list_drop2 (map f l) = map f (list_drop2 l). +Proof. + intros; destruct l. reflexivity. destruct l; reflexivity. +Qed. + +(** * Definitions and theorems over boolean types *) + +Definition proj_sumbool (P Q: Prop) (a: {P} + {Q}) : bool := + if a then true else false. + +Implicit Arguments proj_sumbool [P Q]. + +Coercion proj_sumbool: sumbool >-> bool. + +Lemma proj_sumbool_true: + forall (P Q: Prop) (a: {P}+{Q}), proj_sumbool a = true -> P. +Proof. + intros P Q a. destruct a; simpl. auto. congruence. +Qed. + -- cgit