From f7693b3d897b90fd3bc2533be002dc0bdcd9f6c2 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 6 Oct 2012 15:46:47 +0000 Subject: Merge of branch seq-and-or. See Changelog for details. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Coqlib.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'lib/Coqlib.v') diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 50535fb1..29e65bba 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -909,6 +909,20 @@ Qed. Definition list_disjoint (A: Type) (l1 l2: list A) : Prop := forall (x y: A), In x l1 -> In y l2 -> x <> y. +Lemma list_disjoint_cons_l: + forall (A: Type) (a: A) (l1 l2: list A), + list_disjoint l1 l2 -> ~In a l2 -> list_disjoint (a :: l1) l2. +Proof. + unfold list_disjoint; simpl; intros. destruct H1. congruence. apply H; auto. +Qed. + +Lemma list_disjoint_cons_r: + forall (A: Type) (a: A) (l1 l2: list A), + list_disjoint l1 l2 -> ~In a l1 -> list_disjoint l1 (a :: l2). +Proof. + unfold list_disjoint; simpl; intros. destruct H2. congruence. apply H; auto. +Qed. + Lemma list_disjoint_cons_left: forall (A: Type) (a: A) (l1 l2: list A), list_disjoint (a :: l1) l2 -> list_disjoint l1 l2. -- cgit