diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-10-06 15:46:47 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-10-06 15:46:47 +0000 |
| commit | f7693b3d897b90fd3bc2533be002dc0bdcd9f6c2 (patch) | |
| tree | 93ea9491693324d2d690c4236a2c88c3b461e225 /lib/Coqlib.v | |
| parent | 261ef24f7fd2ef443f73c468b9b1fa496371f3bf (diff) | |
| download | compcert-kvx-f7693b3d897b90fd3bc2533be002dc0bdcd9f6c2.tar.gz compcert-kvx-f7693b3d897b90fd3bc2533be002dc0bdcd9f6c2.zip | |
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
Diffstat (limited to 'lib/Coqlib.v')
| -rw-r--r-- | lib/Coqlib.v | 14 |
1 files changed, 14 insertions, 0 deletions
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. |