From 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 9 Feb 2006 14:55:48 +0000
Subject: Initial import of compcert

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 lib/Coqlib.v | 709 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 709 insertions(+)
 create mode 100644 lib/Coqlib.v

(limited to 'lib/Coqlib.v')

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
new file mode 100644
index 00000000..039dd03b
--- /dev/null
+++ b/lib/Coqlib.v
@@ -0,0 +1,709 @@
+(** This file collects a number of definitions and theorems that are
+    used throughout the development.  It complements the Coq standard
+    library. *)
+
+Require Export ZArith.
+Require Export List.
+Require Import Wf_nat.
+
+(** * Logical axioms *)
+
+(** We use two logical axioms that are not provable in Coq but consistent
+  with the logic: function extensionality and proof irrelevance.
+  These are used in the memory model to show that two memory states
+  that have identical contents are equal. *)
+
+Axiom extensionality:
+  forall (A B: Set) (f g : A -> B),
+  (forall x, f x = g x) -> f = g.
+
+Axiom proof_irrelevance:
+  forall (P: Prop) (p1 p2: P), p1 = p2.
+
+(** * Useful tactics *)
+
+Ltac predSpec pred predspec x y :=
+  generalize (predspec x y); case (pred x y); intro.
+
+Ltac caseEq name :=
+  generalize (refl_equal name); pattern name at -1 in |- *; case name.
+
+Ltac destructEq name :=
+  generalize (refl_equal name); pattern name at -1 in |- *; destruct name; intro.
+
+Ltac decEq :=
+  match goal with
+  | [ |- (_, _) = (_, _) ] =>
+      apply injective_projections; unfold fst,snd; try reflexivity
+  | [ |- (@Some ?T _ = @Some ?T _) ] =>
+      apply (f_equal (@Some T)); try reflexivity
+  | [ |- (?X _ _ _ _ _ = ?X _ _ _ _ _) ] =>
+      apply (f_equal5 X); try reflexivity
+  | [ |- (?X _ _ _ _ = ?X _ _ _ _) ] =>
+      apply (f_equal4 X); try reflexivity
+  | [ |- (?X _ _ _ = ?X _ _ _) ] =>
+      apply (f_equal3 X); try reflexivity
+  | [ |- (?X _ _ = ?X _ _) ] =>
+      apply (f_equal2 X); try reflexivity
+  | [ |- (?X _ = ?X _) ] =>
+      apply (f_equal X); try reflexivity
+  | [ |- (?X ?A <> ?X ?B) ] =>
+      cut (A <> B); [intro; congruence | try discriminate]
+  end.
+
+Ltac byContradiction :=
+  cut False; [contradiction|idtac].
+
+Ltac omegaContradiction :=
+  cut False; [contradiction|omega].
+
+(** * Definitions and theorems over the type [positive] *)
+
+Definition peq (x y: positive): {x = y} + {x <> y}.
+Proof.
+  intros. caseEq (Pcompare x y Eq).
+  intro. left. apply Pcompare_Eq_eq; auto.
+  intro. right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
+  intro. right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
+Qed.
+
+Lemma peq_true:
+  forall (A: Set) (x: positive) (a b: A), (if peq x x then a else b) = a.
+Proof.
+  intros. case (peq x x); intros.
+  auto.
+  elim n; auto.
+Qed.
+
+Lemma peq_false:
+  forall (A: Set) (x y: positive) (a b: A), x <> y -> (if peq x y then a else b) = b.
+Proof.
+  intros. case (peq x y); intros.
+  elim H; auto.
+  auto.
+Qed.  
+
+Definition Plt (x y: positive): Prop := Zlt (Zpos x) (Zpos y).
+
+Lemma Plt_ne:
+  forall (x y: positive), Plt x y -> x <> y.
+Proof.
+  unfold Plt; intros. red; intro. subst y. omega.
+Qed.
+Hint Resolve Plt_ne: coqlib.
+
+Lemma Plt_trans:
+  forall (x y z: positive), Plt x y -> Plt y z -> Plt x z.
+Proof.
+  unfold Plt; intros; omega.
+Qed.
+
+Remark Psucc_Zsucc:
+  forall (x: positive), Zpos (Psucc x) = Zsucc (Zpos x).
+Proof.
+  intros. rewrite Pplus_one_succ_r. 
+  reflexivity.
+Qed.
+
+Lemma Plt_succ:
+  forall (x: positive), Plt x (Psucc x).
+Proof.
+  intro. unfold Plt. rewrite Psucc_Zsucc. omega.
+Qed.
+Hint Resolve Plt_succ: coqlib.
+
+Lemma Plt_trans_succ:
+  forall (x y: positive), Plt x y -> Plt x (Psucc y).
+Proof.
+  intros. apply Plt_trans with y. assumption. apply Plt_succ.
+Qed.
+Hint Resolve Plt_succ: coqlib.
+
+Lemma Plt_succ_inv:
+  forall (x y: positive), Plt x (Psucc y) -> Plt x y \/ x = y.
+Proof.
+  intros x y. unfold Plt. rewrite Psucc_Zsucc. 
+  intro. assert (A: (Zpos x < Zpos y)%Z \/ Zpos x = Zpos y). omega.
+  elim A; intro. left; auto. right; injection H0; auto.
+Qed.
+
+Definition plt (x y: positive) : {Plt x y} + {~ Plt x y}.
+Proof.
+ intros. unfold Plt. apply Z_lt_dec.
+Qed.
+
+Definition Ple (p q: positive) := Zle (Zpos p) (Zpos q).
+
+Lemma Ple_refl: forall (p: positive), Ple p p.
+Proof.
+  unfold Ple; intros; omega.
+Qed.
+
+Lemma Ple_trans: forall (p q r: positive), Ple p q -> Ple q r -> Ple p r.
+Proof.
+  unfold Ple; intros; omega.
+Qed.
+
+Lemma Plt_Ple: forall (p q: positive), Plt p q -> Ple p q.
+Proof.
+  unfold Plt, Ple; intros; omega.
+Qed.
+
+Lemma Ple_succ: forall (p: positive), Ple p (Psucc p).
+Proof.
+  intros. apply Plt_Ple. apply Plt_succ.
+Qed.
+
+Lemma Plt_Ple_trans:
+  forall (p q r: positive), Plt p q -> Ple q r -> Plt p r.
+Proof.
+  unfold Plt, Ple; intros; omega.
+Qed.
+
+Lemma Plt_strict: forall p, ~ Plt p p.
+Proof.
+  unfold Plt; intros. omega.
+Qed.
+
+Hint Resolve Ple_refl Plt_Ple Ple_succ Plt_strict: coqlib.
+
+(** Peano recursion over positive numbers. *)
+
+Section POSITIVE_ITERATION.
+
+Lemma Plt_wf: well_founded Plt.
+Proof.
+  apply well_founded_lt_compat with nat_of_P.
+  intros. apply nat_of_P_lt_Lt_compare_morphism. exact H.
+Qed.
+
+Variable A: Set.
+Variable v1: A.
+Variable f: positive -> A -> A.
+
+Lemma Ppred_Plt:
+  forall x, x <> xH -> Plt (Ppred x) x.
+Proof.
+  intros. elim (Psucc_pred x); intro. contradiction.
+  set (y := Ppred x) in *. rewrite <- H0. apply Plt_succ.
+Qed.
+
+Let iter (x: positive) (P: forall y, Plt y x -> A) : A :=
+  match peq x xH with
+  | left EQ => v1
+  | right NOTEQ => f (Ppred x) (P (Ppred x) (Ppred_Plt x NOTEQ))
+  end.
+
+Definition positive_rec : positive -> A :=
+  Fix Plt_wf (fun _ => A) iter.
+
+Lemma unroll_positive_rec:
+  forall x,
+  positive_rec x = iter x (fun y _ => positive_rec y).
+Proof.
+  unfold positive_rec. apply (Fix_eq Plt_wf (fun _ => A) iter).
+  intros. unfold iter. case (peq x 1); intro. auto. decEq. apply H.
+Qed.
+
+Lemma positive_rec_base:
+  positive_rec 1%positive = v1.
+Proof.
+  rewrite unroll_positive_rec. unfold iter. case (peq 1 1); intro.
+  auto. elim n; auto.
+Qed.
+
+Lemma positive_rec_succ:
+  forall x, positive_rec (Psucc x) = f x (positive_rec x).
+Proof.
+  intro. rewrite unroll_positive_rec. unfold iter.
+  case (peq (Psucc x) 1); intro.
+  destruct x; simpl in e; discriminate.
+  rewrite Ppred_succ. auto.
+Qed.
+
+Lemma positive_Peano_ind:
+  forall (P: positive -> Prop),
+  P xH ->
+  (forall x, P x -> P (Psucc x)) ->
+  forall x, P x.
+Proof.
+  intros.
+  apply (well_founded_ind Plt_wf P).
+  intros. 
+  case (peq x0 xH); intro.
+  subst x0; auto.
+  elim (Psucc_pred x0); intro. contradiction. rewrite <- H2.
+  apply H0. apply H1. apply Ppred_Plt. auto. 
+Qed.
+
+End POSITIVE_ITERATION.
+
+(** * Definitions and theorems over the type [Z] *)
+
+Definition zeq: forall (x y: Z), {x = y} + {x <> y} := Z_eq_dec.
+
+Lemma zeq_true:
+  forall (A: Set) (x: Z) (a b: A), (if zeq x x then a else b) = a.
+Proof.
+  intros. case (zeq x x); intros.
+  auto.
+  elim n; auto.
+Qed.
+
+Lemma zeq_false:
+  forall (A: Set) (x y: Z) (a b: A), x <> y -> (if zeq x y then a else b) = b.
+Proof.
+  intros. case (zeq x y); intros.
+  elim H; auto.
+  auto.
+Qed.  
+
+Open Scope Z_scope.
+
+Definition zlt: forall (x y: Z), {x < y} + {x >= y} := Z_lt_ge_dec.
+
+Lemma zlt_true:
+  forall (A: Set) (x y: Z) (a b: A), 
+  x < y -> (if zlt x y then a else b) = a.
+Proof.
+  intros. case (zlt x y); intros.
+  auto.
+  omegaContradiction.
+Qed.
+
+Lemma zlt_false:
+  forall (A: Set) (x y: Z) (a b: A), 
+  x >= y -> (if zlt x y then a else b) = b.
+Proof.
+  intros. case (zlt x y); intros.
+  omegaContradiction.
+  auto.
+Qed.
+
+Definition zle: forall (x y: Z), {x <= y} + {x > y} := Z_le_gt_dec.
+
+Lemma zle_true:
+  forall (A: Set) (x y: Z) (a b: A), 
+  x <= y -> (if zle x y then a else b) = a.
+Proof.
+  intros. case (zle x y); intros.
+  auto.
+  omegaContradiction.
+Qed.
+
+Lemma zle_false:
+  forall (A: Set) (x y: Z) (a b: A), 
+  x > y -> (if zle x y then a else b) = b.
+Proof.
+  intros. case (zle x y); intros.
+  omegaContradiction.
+  auto.
+Qed.
+
+(** Properties of powers of two. *)
+
+Lemma two_power_nat_O : two_power_nat O = 1.
+Proof. reflexivity. Qed.
+
+Lemma two_power_nat_pos : forall n : nat, two_power_nat n > 0.
+Proof.
+  induction n. rewrite two_power_nat_O. omega.
+  rewrite two_power_nat_S. omega.
+Qed.
+
+(** Properties of [Zmin] and [Zmax] *)
+
+Lemma Zmin_spec:
+  forall x y, Zmin x y = if zlt x y then x else y.
+Proof.
+  intros. case (zlt x y); unfold Zlt, Zge; intros.
+  unfold Zmin. rewrite z. auto.
+  unfold Zmin. caseEq (x ?= y); intro. 
+  apply Zcompare_Eq_eq. auto.
+  contradiction.
+  reflexivity.
+Qed.
+
+Lemma Zmax_spec:
+  forall x y, Zmax x y = if zlt y x then x else y.
+Proof.
+  intros. case (zlt y x); unfold Zlt, Zge; intros.
+  unfold Zmax. rewrite <- (Zcompare_antisym y x).
+  rewrite z. simpl. auto.
+  unfold Zmax. rewrite <- (Zcompare_antisym y x).
+  caseEq (y ?= x); intro; simpl.
+  symmetry. apply Zcompare_Eq_eq. auto.
+  contradiction. reflexivity.
+Qed.
+
+Lemma Zmax_bound_l:
+  forall x y z, x <= y -> x <= Zmax y z.
+Proof.
+  intros. generalize (Zmax1 y z). omega.
+Qed.
+Lemma Zmax_bound_r:
+  forall x y z, x <= z -> x <= Zmax y z.
+Proof.
+  intros. generalize (Zmax2 y z). omega.
+Qed.
+
+(** Properties of Euclidean division and modulus. *)
+
+Lemma Zdiv_small:
+  forall x y, 0 <= x < y -> x / y = 0.
+Proof.
+  intros. assert (y > 0). omega. 
+  assert (forall a b,
+    0 <= a < y ->
+    0 <= y * b + a < y ->
+    b = 0).
+  intros. 
+  assert (b = 0 \/ b > 0 \/ (-b) > 0). omega.
+  elim H3; intro.
+  auto.
+  elim H4; intro.
+  assert (y * b >= y * 1). apply Zmult_ge_compat_l. omega. omega. 
+  omegaContradiction. 
+  assert (y * (-b) >= y * 1). apply Zmult_ge_compat_l. omega. omega.
+  rewrite <- Zopp_mult_distr_r in H6. omegaContradiction.
+  apply H1 with (x mod y). 
+  apply Z_mod_lt. auto.
+  rewrite <- Z_div_mod_eq. auto. auto.
+Qed.
+
+Lemma Zmod_small:
+  forall x y, 0 <= x < y -> x mod y = x.
+Proof.
+  intros. assert (y > 0). omega.
+  generalize (Z_div_mod_eq x y H0). 
+  rewrite (Zdiv_small x y H). omega.
+Qed.
+
+Lemma Zmod_unique:
+  forall x y a b,
+  x = a * y + b -> 0 <= b < y -> x mod y = b.
+Proof.
+  intros. subst x. rewrite Zplus_comm. 
+  rewrite Z_mod_plus. apply Zmod_small. auto. omega.
+Qed.
+
+Lemma Zdiv_unique:
+  forall x y a b,
+  x = a * y + b -> 0 <= b < y -> x / y = a.
+Proof.
+  intros. subst x. rewrite Zplus_comm.
+  rewrite Z_div_plus. rewrite (Zdiv_small b y H0). omega. omega.
+Qed.
+
+(** Alignment: [align n amount] returns the smallest multiple of [amount]
+  greater than or equal to [n]. *)
+
+Definition align (n: Z) (amount: Z) :=
+  ((n + amount - 1) / amount) * amount.
+
+Lemma align_le: forall x y, y > 0 -> x <= align x y.
+Proof.
+  intros. unfold align. 
+  generalize (Z_div_mod_eq (x + y - 1) y H). intro.
+  replace ((x + y - 1) / y * y) 
+     with ((x + y - 1) - (x + y - 1) mod y).
+  generalize (Z_mod_lt (x + y - 1) y H). omega.
+  rewrite Zmult_comm. omega.
+Qed.
+
+(** * Definitions and theorems on the data types [option], [sum] and [list] *)
+
+Set Implicit Arguments.
+
+(** Mapping a function over an option type. *)
+
+Definition option_map (A B: Set) (f: A -> B) (x: option A) : option B :=
+  match x with
+  | None => None
+  | Some y => Some (f y)
+  end.
+
+(** Mapping a function over a sum type. *)
+
+Definition sum_left_map (A B C: Set) (f: A -> B) (x: A + C) : B + C :=
+  match x with
+  | inl y => inl C (f y)
+  | inr z => inr B z
+  end.
+
+(** Properties of [List.nth] (n-th element of a list). *)
+
+Hint Resolve in_eq in_cons: coqlib.
+
+Lemma nth_error_in:
+  forall (A: Set) (n: nat) (l: list A) (x: A),
+  List.nth_error l n = Some x -> In x l.
+Proof.
+  induction n; simpl.
+   destruct l; intros.
+    discriminate.
+    injection H; intro; subst a. apply in_eq.
+   destruct l; intros.
+    discriminate.
+    apply in_cons. auto.
+Qed.
+Hint Resolve nth_error_in: coqlib.
+
+Lemma nth_error_nil:
+  forall (A: Set) (idx: nat), nth_error (@nil A) idx = None.
+Proof.
+  induction idx; simpl; intros; reflexivity.
+Qed.
+Hint Resolve nth_error_nil: coqlib.
+
+(** Properties of [List.incl] (list inclusion). *)
+
+Lemma incl_cons_inv:
+  forall (A: Set) (a: A) (b c: list A),
+  incl (a :: b) c -> incl b c.
+Proof.
+  unfold incl; intros. apply H. apply in_cons. auto.
+Qed.
+Hint Resolve incl_cons_inv: coqlib.
+
+Lemma incl_app_inv_l:
+  forall (A: Set) (l1 l2 m: list A),
+  incl (l1 ++ l2) m -> incl l1 m.
+Proof.
+  unfold incl; intros. apply H. apply in_or_app. left; assumption.
+Qed.
+
+Lemma incl_app_inv_r:
+  forall (A: Set) (l1 l2 m: list A),
+  incl (l1 ++ l2) m -> incl l2 m.
+Proof.
+  unfold incl; intros. apply H. apply in_or_app. right; assumption.
+Qed.
+
+Hint Resolve  incl_tl incl_refl incl_app_inv_l incl_app_inv_r: coqlib.
+
+Lemma incl_same_head:
+  forall (A: Set) (x: A) (l1 l2: list A),
+  incl l1 l2 -> incl (x::l1) (x::l2).
+Proof.
+  intros; red; simpl; intros. intuition. 
+Qed.
+
+(** Properties of [List.map] (mapping a function over a list). *)
+
+Lemma list_map_exten:
+  forall (A B: Set) (f f': A -> B) (l: list A),
+  (forall x, In x l -> f x = f' x) ->
+  List.map f' l = List.map f l.
+Proof.
+  induction l; simpl; intros.
+  reflexivity.
+  rewrite <- H. rewrite IHl. reflexivity.
+  intros. apply H. tauto.
+  tauto.
+Qed.
+
+Lemma list_map_compose:
+  forall (A B C: Set) (f: A -> B) (g: B -> C) (l: list A),
+  List.map g (List.map f l) = List.map (fun x => g(f x)) l.
+Proof.
+  induction l; simpl. reflexivity. rewrite IHl; reflexivity.
+Qed.
+
+Lemma list_map_nth:
+  forall (A B: Set) (f: A -> B) (l: list A) (n: nat),
+  nth_error (List.map f l) n = option_map f (nth_error l n).
+Proof.
+  induction l; simpl; intros.
+  repeat rewrite nth_error_nil. reflexivity.
+  destruct n; simpl. reflexivity. auto.
+Qed.
+
+Lemma list_length_map:
+  forall (A B: Set) (f: A -> B) (l: list A),
+  List.length (List.map f l) = List.length l.
+Proof.
+  induction l; simpl; congruence.
+Qed.
+
+Lemma list_in_map_inv:
+  forall (A B: Set) (f: A -> B) (l: list A) (y: B),
+  In y (List.map f l) -> exists x:A, y = f x /\ In x l.
+Proof.
+  induction l; simpl; intros.
+  contradiction.
+  elim H; intro. 
+  exists a; intuition auto.
+  generalize (IHl y H0). intros [x [EQ IN]]. 
+  exists x; tauto.
+Qed.
+
+Lemma list_append_map:
+  forall (A B: Set) (f: A -> B) (l1 l2: list A),
+  List.map f (l1 ++ l2) = List.map f l1 ++ List.map f l2.
+Proof.
+  induction l1; simpl; intros.
+  auto. rewrite IHl1. auto.
+Qed.
+
+(** [list_disjoint l1 l2] holds iff [l1] and [l2] have no elements 
+  in common. *)
+
+Definition list_disjoint (A: Set) (l1 l2: list A) : Prop :=
+  forall (x y: A), In x l1 -> In y l2 -> x <> y.
+
+Lemma list_disjoint_cons_left:
+  forall (A: Set) (a: A) (l1 l2: list A),
+  list_disjoint (a :: l1) l2 -> list_disjoint l1 l2.
+Proof.
+  unfold list_disjoint; simpl; intros. apply H; tauto. 
+Qed.
+
+Lemma list_disjoint_cons_right:
+  forall (A: Set) (a: A) (l1 l2: list A),
+  list_disjoint l1 (a :: l2) -> list_disjoint l1 l2.
+Proof.
+  unfold list_disjoint; simpl; intros. apply H; tauto. 
+Qed.
+
+Lemma list_disjoint_notin:
+  forall (A: Set) (l1 l2: list A) (a: A),
+  list_disjoint l1 l2 -> In a l1 -> ~(In a l2).
+Proof.
+  unfold list_disjoint; intros; red; intros. 
+  apply H with a a; auto.
+Qed.
+
+Lemma list_disjoint_sym:
+  forall (A: Set) (l1 l2: list A),
+  list_disjoint l1 l2 -> list_disjoint l2 l1.
+Proof.
+  unfold list_disjoint; intros. 
+  apply sym_not_equal. apply H; auto.
+Qed.
+
+(** [list_norepet l] holds iff the list [l] contains no repetitions,
+  i.e. no element occurs twice. *)
+
+Inductive list_norepet (A: Set) : list A -> Prop :=
+  | list_norepet_nil:
+      list_norepet nil
+  | list_norepet_cons:
+      forall hd tl,
+      ~(In hd tl) -> list_norepet tl -> list_norepet (hd :: tl).
+
+Lemma list_norepet_dec:
+  forall (A: Set) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l: list A),
+  {list_norepet l} + {~list_norepet l}.
+Proof.
+  induction l.
+  left; constructor.
+  destruct IHl. 
+  case (In_dec eqA_dec a l); intro.
+  right. red; intro. inversion H. contradiction. 
+  left. constructor; auto.
+  right. red; intro. inversion H. contradiction.
+Qed.
+
+Lemma list_map_norepet:
+  forall (A B: Set) (f: A -> B) (l: list A),
+  list_norepet l ->
+  (forall x y, In x l -> In y l -> x <> y -> f x <> f y) ->
+  list_norepet (List.map f l).
+Proof.
+  induction 1; simpl; intros.
+  constructor.
+  constructor.
+  red; intro. generalize (list_in_map_inv f _ _ H2).
+  intros [x [EQ IN]]. generalize EQ. change (f hd <> f x).
+  apply H1. tauto. tauto. 
+  red; intro; subst x. contradiction.
+  apply IHlist_norepet. intros. apply H1. tauto. tauto. auto.
+Qed.
+
+Remark list_norepet_append_commut:
+  forall (A: Set) (a b: list A),
+  list_norepet (a ++ b) -> list_norepet (b ++ a).
+Proof.
+  intro A.
+  assert (forall (x: A) (b: list A) (a: list A), 
+           list_norepet (a ++ b) -> ~(In x a) -> ~(In x b) -> 
+           list_norepet (a ++ x :: b)).
+    induction a; simpl; intros.
+    constructor; auto.
+    inversion H. constructor. red; intro.
+    elim (in_app_or _ _ _ H6); intro.
+    elim H4. apply in_or_app. tauto.
+    elim H7; intro. subst a. elim H0. left. auto. 
+    elim H4. apply in_or_app. tauto.
+    auto.
+  induction a; simpl; intros.
+  rewrite <- app_nil_end. auto.
+  inversion H0. apply H. auto. 
+  red; intro; elim H3. apply in_or_app. tauto.
+  red; intro; elim H3. apply in_or_app. tauto.
+Qed.
+
+Lemma list_norepet_append:
+  forall (A: Set) (l1 l2: list A),
+  list_norepet l1 -> list_norepet l2 -> list_disjoint l1 l2 ->
+  list_norepet (l1 ++ l2).
+Proof.
+  induction l1; simpl; intros.
+  auto.
+  inversion H. subst hd tl. 
+  constructor. red; intro. apply (H1 a a). auto with coqlib. 
+  elim (in_app_or _ _ _ H2); tauto. auto.
+  apply IHl1. auto. auto. 
+  red; intros; apply H1; auto with coqlib. 
+Qed.
+
+Lemma list_norepet_append_right:
+  forall (A: Set) (l1 l2: list A),
+  list_norepet (l1 ++ l2) -> list_norepet l2.
+Proof.
+  induction l1; intros.
+  assumption.
+  simpl in H. inversion H. eauto. 
+Qed.
+
+Lemma list_norepet_append_left:
+  forall (A: Set) (l1 l2: list A),
+  list_norepet (l1 ++ l2) -> list_norepet l1.
+Proof.
+  intros. apply list_norepet_append_right with l2. 
+  apply list_norepet_append_commut. auto.
+Qed.
+
+(** [list_forall2 P [x1 ... xN] [y1 ... yM] holds iff [N = M] and
+  [P xi yi] holds for all [i]. *)
+
+Section FORALL2.
+
+Variable A: Set.
+Variable B: Set.
+Variable P: A -> B -> Prop.
+
+Inductive list_forall2: list A -> list B -> Prop :=
+  | list_forall2_nil:
+      list_forall2 nil nil
+  | list_forall2_cons:
+      forall a1 al b1 bl,
+      P a1 b1 ->
+      list_forall2 al bl ->
+      list_forall2 (a1 :: al) (b1 :: bl).
+
+End FORALL2.
+
+Lemma list_forall2_imply:
+  forall (A B: Set) (P1: A -> B -> Prop) (l1: list A) (l2: list B),
+  list_forall2 P1 l1 l2 ->
+  forall (P2: A -> B -> Prop),
+  (forall v1 v2, In v1 l1 -> In v2 l2 -> P1 v1 v2 -> P2 v1 v2) ->
+  list_forall2 P2 l1 l2.
+Proof.
+  induction 1; intros.
+  constructor.
+  constructor. auto with coqlib. apply IHlist_forall2; auto. 
+  intros. auto with coqlib.
+Qed.
-- 
cgit