Initial import of compcert

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

9 files changed, 5563 insertions, 0 deletions

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.
diff --git a/lib/Floats.v b/lib/Floats.v
new file mode 100644
index 00000000..b95789e6
--- /dev/null
+++ b/lib/Floats.v
@@ -0,0 +1,55 @@
+(** Axiomatization of floating-point numbers. *)
+
+(** In contrast with what we do with machine integers, we do not bother
+  to formalize precisely IEEE floating-point arithmetic.  Instead, we
+  simply axiomatize a type [float] for IEEE double-precision floats
+  and the associated operations.  *)
+
+Require Import Bool.
+Require Import AST.
+Require Import Integers.
+
+Parameter float: Set.
+
+Module Float.
+
+Parameter zero: float.
+Parameter one: float.
+
+Parameter neg: float -> float.
+Parameter abs: float -> float.
+Parameter singleoffloat: float -> float.
+Parameter intoffloat: float -> int.
+Parameter floatofint: int -> float.
+Parameter floatofintu: int -> float.
+
+Parameter add: float -> float -> float.
+Parameter sub: float -> float -> float.
+Parameter mul: float -> float -> float.
+Parameter div: float -> float -> float.
+
+Parameter cmp: comparison -> float -> float -> bool.
+
+Axiom eq_dec: forall (f1 f2: float), {f1 = f2} + {f1 <> f2}.
+
+(** Below are the only properties of floating-point arithmetic that we
+  rely on in the compiler proof. *)
+
+Axiom addf_commut: forall f1 f2, add f1 f2 = add f2 f1.
+
+Axiom subf_addf_opp: forall f1 f2, sub f1 f2 = add f1 (neg f2).
+
+Axiom singleoffloat_idem:
+  forall f, singleoffloat (singleoffloat f) = singleoffloat f.
+
+Axiom cmp_ne_eq:
+  forall f1 f2, cmp Cne f1 f2 = negb (cmp Ceq f1 f2).
+Axiom cmp_le_lt_eq:
+  forall f1 f2, cmp Cle f1 f2 = cmp Clt f1 f2 || cmp Ceq f1 f2.
+Axiom cmp_ge_gt_eq:
+  forall f1 f2, cmp Cge f1 f2 = cmp Cgt f1 f2 || cmp Ceq f1 f2.
+
+Axiom eq_zero_true: cmp Ceq zero zero = true.
+Axiom eq_zero_false: forall f, f <> zero -> cmp Ceq f zero = false.
+
+End Float.
diff --git a/lib/Inclusion.v b/lib/Inclusion.v
new file mode 100644
index 00000000..1df7517f
--- /dev/null
+++ b/lib/Inclusion.v
@@ -0,0 +1,367 @@
+(** Tactics to reason about list inclusion. *)
+
+(** This file (contributed by Laurence Rideau) defines a tactic [in_tac]
+  to reason over list inclusion.  It expects goals of the following form:
+<<
+  id : In x l1
+  ============================
+     In x l2
+>>
+and succeeds if it can prove that [l1] is included in [l2].  
+The lists [l1] and [l2] must belong to the following sub-language [L]
+<<
+  L ::= L++L | E | E::L
+>>
+The tactic uses no extra fact.
+
+A second tactic, [incl_tac], handles goals of the form
+<<
+  =============================
+    incl l1 l2
+>>
+*)
+
+Require Import List.
+Require Import ArithRing.
+
+Ltac all_app e :=
+  match e with
+  | cons ?x nil => constr:(cons x nil)
+  | cons ?x ?tl => 
+      let v := all_app tl in constr:(app (cons x nil) v)
+  | app ?e1 ?e2 =>
+    let v1 := all_app e1 with v2 := all_app e2 in
+    constr:(app v1 v2)
+  | _ => e
+  end.
+
+(** This data type, [flatten], [insert_bin], [sort_bin] and a few theorem
+  are taken from the CoqArt book, chapt. 16. *)
+
+Inductive bin : Set := node : bin->bin->bin | leaf : nat->bin.
+
+Fixpoint flatten_aux (t fin:bin){struct t} : bin :=
+  match t with
+  | node t1 t2 => flatten_aux t1 (flatten_aux t2 fin)
+  | x => node x fin
+  end.
+
+Fixpoint flatten (t:bin) : bin :=
+  match t with
+  | node t1 t2 => flatten_aux t1 (flatten t2)
+  | x => x
+  end.
+
+Fixpoint nat_le_bool (n m:nat){struct m} : bool :=
+  match n, m with
+  | O, _ => true
+  | S _, O => false
+  | S n, S m => nat_le_bool n m
+  end.
+
+Fixpoint insert_bin (n:nat)(t:bin){struct t} : bin :=
+  match t with
+  | leaf m => 
+    if nat_le_bool n m then
+       node (leaf n)(leaf m)
+    else
+       node (leaf m)(leaf n)
+  | node (leaf m) t' =>
+    if nat_le_bool n m then node (leaf n) t else node (leaf m)(insert_bin n t')
+  | t => node (leaf n) t
+  end.
+
+Fixpoint sort_bin (t:bin) : bin :=
+  match t with
+  | node (leaf n) t' => insert_bin n (sort_bin t')
+  | t => t
+  end.
+
+Section assoc_eq.
+ Variables (A : Set)(f : A->A->A).
+ Hypothesis assoc : forall x y z:A, f x (f y z) = f (f x y) z.
+
+ Fixpoint bin_A (l:list A)(def:A)(t:bin){struct t} : A :=
+   match t with
+   | node t1 t2 => f (bin_A l def t1)(bin_A l def t2)
+   | leaf n => nth n l def
+   end.
+
+ Theorem flatten_aux_valid_A :
+  forall (l:list A)(def:A)(t t':bin),
+   f (bin_A l def t)(bin_A l def t') = bin_A l def (flatten_aux t t').
+ Proof.
+  intros l def t; elim t; simpl; auto.
+  intros t1 IHt1 t2 IHt2 t';  rewrite <- IHt1; rewrite <- IHt2.
+  symmetry; apply assoc.
+ Qed.
+
+ Theorem flatten_valid_A :
+  forall (l:list A)(def:A)(t:bin),
+    bin_A l def t = bin_A l def (flatten t).
+ Proof.
+  intros l def t; elim t; simpl; trivial.
+  intros t1 IHt1 t2 IHt2; rewrite <- flatten_aux_valid_A; rewrite <- IHt2.
+  trivial.
+ Qed.
+
+End assoc_eq.
+
+Ltac compute_rank l n v :=
+  match l with
+  | (cons ?X1 ?X2) =>
+    let tl := constr:X2 in
+    match constr:(X1 = v) with
+    | (?X1 = ?X1) => n
+    | _ => compute_rank tl (S n) v
+    end
+  end.
+
+Ltac term_list_app l v :=
+  match v with
+  | (app ?X1 ?X2) =>
+    let l1 := term_list_app l X2 in term_list_app l1 X1
+  | ?X1 => constr:(cons X1 l)
+  end.
+
+Ltac model_aux_app l v :=
+  match v with
+  | (app ?X1 ?X2) =>
+    let r1 := model_aux_app l X1 with r2 := model_aux_app l X2 in
+      constr:(node r1 r2)
+  | ?X1 => let n := compute_rank l 0 X1 in constr:(leaf n)
+  | _ => constr:(leaf 0)
+  end.
+
+Theorem In_permute_app_head :
+  forall A:Set, forall r:A, forall x y l:list A,
+   In r (x++y++l) -> In r (y++x++l).
+intros A r x y l; generalize r; change (incl (x++y++l)(y++x++l)).
+repeat rewrite ass_app; auto with datatypes.
+Qed.
+
+Theorem insert_bin_included : 
+  forall x:nat, forall t2:bin,
+  forall (A:Set) (r:A) (l:list (list A))(def:list A), 
+     In r (bin_A (list A) (app (A:=A)) l def (insert_bin x t2)) ->
+     In r (bin_A (list A) (app (A:=A)) l def (node (leaf x) t2)).
+intros x t2; induction t2.
+intros A r l def.
+destruct t2_1 as [t2_11 t2_12|y].
+simpl.
+repeat rewrite app_ass.
+auto.
+simpl; repeat rewrite app_ass.
+simpl; case (nat_le_bool x y); simpl.
+auto.
+intros H; apply In_permute_app_head.
+elim in_app_or with (1:= H); clear H; intros H.
+apply in_or_app; left; assumption.
+apply in_or_app; right;apply (IHt2_2 A r l);assumption.
+intros A r l def; simpl.
+case (nat_le_bool x n); simpl.
+auto.
+intros H.
+rewrite (app_nil_end (nth x l def)) in H.
+rewrite (app_nil_end (nth n l def)).
+apply In_permute_app_head; assumption.
+Qed.
+
+Theorem in_or_insert_bin :
+  forall (n:nat) (t2:bin) (A:Set)(r:A)(l:list (list A)) (def:list A),
+  In r (nth n l def) \/ In r (bin_A (list A)(app (A:=A)) l def t2) ->
+  In r (bin_A (list A)(app (A:=A)) l def (insert_bin n t2)).
+intros n t2 A r l def; induction t2.
+destruct t2_1 as [t2_11 t2_12| y].
+simpl; apply in_or_app.
+simpl; case (nat_le_bool n y); simpl.
+intros H.
+apply in_or_app.
+exact H.
+intros [H|H].
+apply in_or_app; right; apply IHt2_2; auto.
+elim in_app_or with (1:= H);clear H; intros H; apply in_or_app; auto.
+simpl; intros [H|H]; case (nat_le_bool n n0); simpl; apply in_or_app; auto.
+Qed.
+
+Theorem sort_included :
+  forall t:bin, forall (A:Set)(r:A)(l:list(list A))(def:list A),
+    In r (bin_A (list A) (app (A:=A)) l def (sort_bin t)) ->
+    In r (bin_A (list A) (app (A:=A)) l def t).
+induction t.
+destruct t1.
+simpl;intros; assumption.
+intros A r l def H; simpl in H; apply insert_bin_included.
+generalize (insert_bin_included _ _ _ _ _ _ H); clear H; intros H.
+simpl in H.
+elim in_app_or with (1 := H);clear H; intros H;
+apply in_or_insert_bin; auto.
+simpl;intros;assumption.
+Qed.
+
+Theorem sort_included2 :
+  forall t:bin, forall (A:Set)(r:A)(l:list(list A))(def:list A),
+    In r (bin_A (list A) (app (A:=A)) l def t) ->
+    In r (bin_A (list A) (app (A:=A)) l def (sort_bin t)).
+induction t.
+destruct t1.
+simpl; intros; assumption.
+intros A r l def H; simpl in H.
+simpl; apply in_or_insert_bin.
+elim in_app_or with (1:= H); auto.
+simpl; auto.
+Qed.
+
+Theorem in_remove_head :
+  forall (A:Set)(x:A)(l1 l2 l3:list A),
+  In x (l1++l2) -> (In x l2 -> In x l3) -> In x (l1++l3).
+intros A x l1 l2 l3 H H1.
+elim in_app_or with (1:= H);clear H; intros H; apply in_or_app; auto.
+Qed.
+
+Fixpoint check_all_leaves (n:nat)(t:bin) {struct t} : bool :=
+  match t with
+    leaf n1 => nateq n n1
+  | node t1 t2 => andb (check_all_leaves n t1)(check_all_leaves n t2)
+  end.
+
+Fixpoint remove_all_leaves (n:nat)(t:bin){struct t} : bin :=
+  match t with
+    leaf n => leaf n
+  | node (leaf n1) t2 =>
+    if nateq n n1 then remove_all_leaves n t2 else t
+  | _ => t
+  end.
+
+Fixpoint test_inclusion (t1 t2:bin) {struct t1} : bool :=
+  match t1 with
+    leaf n => check_all_leaves n t2
+  | node (leaf n1) t1' =>
+     check_all_leaves n1 t2 || test_inclusion t1' (remove_all_leaves n1 t2)
+  | _ => false
+  end.
+
+Theorem check_all_leaves_sound :
+  forall x t2,
+    check_all_leaves x t2 = true ->
+    forall (A:Set)(r:A)(l:list(list A))(def:list A),
+    In r (bin_A (list A) (app (A:=A)) l def t2) ->
+    In r (nth x l def).
+intros x t2; induction t2; simpl.
+destruct (check_all_leaves x t2_1);
+destruct (check_all_leaves x t2_2); simpl; intros Heq; try discriminate.
+intros A r l def H; elim in_app_or with (1:= H); clear H; intros H; auto.
+intros Heq A r l def; rewrite (nateq_prop x n); auto.
+rewrite Heq; unfold Is_true; auto.
+Qed.
+
+Theorem remove_all_leaves_sound :
+  forall x t2,
+  forall (A:Set)(r:A)(l:list(list A))(def:list A),
+  In r (bin_A (list A) (app(A:=A)) l def t2) ->
+  In r (bin_A (list A) (app(A:=A)) l def (remove_all_leaves x t2)) \/
+  In r (nth x l def).
+intros x t2; induction t2; simpl.
+destruct t2_1.
+simpl; auto.
+intros A r l def.
+generalize (refl_equal (nateq x n)); pattern (nateq x n) at -1;
+ case (nateq x n); simpl; auto.
+intros Heq_nateq.
+assert (Heq_xn : x=n).
+apply nateq_prop; rewrite Heq_nateq;unfold Is_true;auto.
+rewrite Heq_xn.
+intros H; elim in_app_or with (1:= H); auto.
+clear H; intros H.
+rewrite Heq_xn in IHt2_2; auto.
+auto.
+Qed.
+
+Theorem test_inclusion_sound :
+  forall t1 t2:bin,
+  test_inclusion t1 t2 = true ->
+  forall (A:Set)(r:A)(l:list(list A))(def:list A),
+  In r (bin_A (list A)(app(A:=A)) l def t2) ->
+  In r (bin_A (list A)(app(A:=A)) l def t1).
+intros t1; induction t1.
+destruct t1_1 as [t1_11 t1_12|x].
+simpl; intros; discriminate.
+simpl; intros t2 Heq A r l def H.
+assert 
+ (check_all_leaves x t2 = true \/ 
+  test_inclusion t1_2 (remove_all_leaves x t2) = true).
+destruct (check_all_leaves x t2);
+destruct (test_inclusion t1_2 (remove_all_leaves x t2));
+simpl in Heq; try discriminate Heq; auto.
+elim H0; clear H0; intros H0.
+apply in_or_app; left; apply check_all_leaves_sound with (1:= H0); auto.
+elim remove_all_leaves_sound with (x:=x)(1:= H); intros H'.
+apply in_or_app; right; apply IHt1_2 with (1:= H0); auto.
+apply in_or_app; auto.
+simpl; apply check_all_leaves_sound.
+Qed.
+
+Theorem inclusion_theorem :
+  forall t1 t2 : bin,
+    test_inclusion (sort_bin (flatten t1)) (sort_bin (flatten t2)) = true ->
+    forall (A:Set)(r:A)(l:list(list A))(def:list A),
+    In r (bin_A (list A) (app(A:=A)) l def t2) ->
+    In r (bin_A (list A) (app(A:=A)) l def t1).
+intros t1 t2 Heq A r l def H.
+rewrite flatten_valid_A with (t:= t1)(1:= (ass_app (A:= A))).
+apply sort_included.
+apply test_inclusion_sound with (t2 := sort_bin (flatten t2)).
+assumption.
+apply sort_included2.
+rewrite <- flatten_valid_A with (1:= (ass_app (A:= A))).
+assumption.
+Qed.
+
+Ltac in_tac :=
+  match goal with
+  | id : In ?x nil |- _ => elim id
+  | id : In ?x ?l1 |- In ?x ?l2 =>
+    let t := type of x in
+    let v1 := all_app l1 in
+    let v2 := all_app l2 in
+    (let l := term_list_app (nil (A:=list t)) v2 in
+     let term1 := model_aux_app l v1 with
+         term2 := model_aux_app l v2 in
+        (change (In x (bin_A (list t) (app(A:=t)) l (nil(A:=t)) term2));
+        apply inclusion_theorem with (t2:= term1);[apply refl_equal|exact id]))
+  end.
+
+Ltac incl_tac :=
+  match goal with
+  |- incl _ _ => intro; intro; in_tac
+  end.
+   
+(* Usage examples.
+
+Theorem ex1 : forall x y z:nat, forall l1 l2 : list nat,
+   In x (y::l1++l2) -> In x (l2++z::l1++(y::nil)).
+intros.
+in_tac.
+Qed.
+
+Fixpoint mklist (f:nat->nat)(n:nat){struct n} : list nat :=
+ match n with 0 => nil | S p => mklist f p++(f p::nil) end.
+
+(* At the time of writing these lines, this example takes about 5 seconds
+     for 40 elements and 22 seconds for 60 elements.
+   A variant to the example is to replace mklist f p++(f p::nil) with
+   f p::mklist f p, in this case the time is 6 seconds for 40 elements and
+   35 seconds for 60 elements. *)
+
+Theorem ex2 : 
+  forall x : nat, In x (mklist (fun y => y) 40) ->
+     In x (mklist (fun y => (40 - 1) - y) 40).
+lazy beta iota zeta delta [mklist minus].
+intros.
+in_tac.
+Qed.
+
+(* The tactic could be made more efficient by using binary trees and
+   numbers of type positive instead of lists and natural numbers. *)
+
+*)
diff --git a/lib/Integers.v b/lib/Integers.v
new file mode 100644
index 00000000..6b605bd7
--- /dev/null
+++ b/lib/Integers.v
@@ -0,0 +1,2184 @@
+(** Formalizations of integers modulo $2^32$ #2<sup>32</sup>#. *)
+
+Require Import Coqlib.
+Require Import AST.
+
+Definition wordsize : nat := 32%nat.
+Definition modulus : Z := two_power_nat wordsize.
+Definition half_modulus : Z := modulus / 2.
+
+(** * Representation of machine integers *)
+
+(** A machine integer (type [int]) is represented as a Coq arbitrary-precision
+  integer (type [Z]) plus a proof that it is in the range 0 (included) to
+  [modulus] (excluded. *)
+
+Definition in_range (x: Z) :=
+  match x ?= 0 with
+  | Lt => False
+  | _  =>
+    match x ?= modulus with
+    | Lt => True
+    | _  => False
+    end
+  end.
+
+Record int: Set := mkint { intval: Z; intrange: in_range intval }.
+
+Module Int.
+
+Definition max_unsigned : Z := modulus - 1.
+Definition max_signed : Z := half_modulus - 1.
+Definition min_signed : Z := - half_modulus.
+
+(** The [unsigned] and [signed] functions return the Coq integer corresponding
+  to the given machine integer, interpreted as unsigned or signed 
+  respectively. *)
+
+Definition unsigned (n: int) : Z := intval n.
+
+Definition signed (n: int) : Z :=
+  if zlt (unsigned n) half_modulus
+  then unsigned n
+  else unsigned n - modulus.
+
+Lemma mod_in_range:
+  forall x, in_range (Zmod x modulus).
+Proof.
+  intro.
+  generalize (Z_mod_lt x modulus (two_power_nat_pos wordsize)).
+  intros [A B].
+  assert (C: x mod modulus >= 0). omega.
+  red. red in C. red in B. 
+  rewrite B. destruct (x mod modulus ?= 0); auto. 
+Qed.
+
+(** Conversely, [repr] takes a Coq integer and returns the corresponding
+  machine integer.  The argument is treated modulo [modulus]. *)
+
+Definition repr (x: Z) : int := 
+  mkint (Zmod x modulus) (mod_in_range x).
+
+Definition zero := repr 0.
+Definition one  := repr 1.
+Definition mone := repr (-1).
+
+Lemma mkint_eq:
+  forall x y Px Py, x = y -> mkint x Px = mkint y Py.
+Proof.
+  intros. subst y. 
+  generalize (proof_irrelevance _ Px Py); intro.
+  subst Py. reflexivity.
+Qed.
+
+Lemma eq_dec: forall (x y: int), {x = y} + {x <> y}.
+Proof.
+  intros. destruct x; destruct y. case (zeq intval0 intval1); intro.
+  left. apply mkint_eq. auto.
+  right. red; intro. injection H. exact n.
+Qed.
+
+(** * Arithmetic and logical operations over machine integers *)
+
+Definition eq (x y: int) : bool := 
+  if zeq (unsigned x) (unsigned y) then true else false.
+Definition lt (x y: int) : bool :=
+  if zlt (signed x) (signed y) then true else false.
+Definition ltu (x y: int) : bool :=
+  if zlt (unsigned x) (unsigned y) then true else false.
+
+Definition neg (x: int) : int := repr (- unsigned x).
+Definition cast8signed (x: int) : int :=
+  let y := Zmod (unsigned x) 256 in
+  if zlt y 128 then repr y else repr (y - 256).
+Definition cast8unsigned (x: int) : int :=
+  repr (Zmod (unsigned x) 256).
+Definition cast16signed (x: int) : int :=
+  let y := Zmod (unsigned x) 65536 in
+  if zlt y 32768 then repr y else repr (y - 65536).
+Definition cast16unsigned (x: int) : int :=
+  repr (Zmod (unsigned x) 65536).
+
+Definition add (x y: int) : int :=
+  repr (unsigned x + unsigned y).
+Definition sub (x y: int) : int :=
+  repr (unsigned x - unsigned y).
+Definition mul (x y: int) : int :=
+  repr (unsigned x * unsigned y).
+
+Definition Zdiv_round (x y: Z) : Z :=
+  if zlt x 0 then
+    if zlt y 0 then (-x) / (-y) else - ((-x) / y)
+  else
+    if zlt y 0 then -(x / (-y)) else x / y.
+
+Definition Zmod_round (x y: Z) : Z :=
+  x - (Zdiv_round x y) * y.
+
+Definition divs (x y: int) : int :=
+  repr (Zdiv_round (signed x) (signed y)).
+Definition mods (x y: int) : int :=
+  repr (Zmod_round (signed x) (signed y)).
+Definition divu (x y: int) : int :=
+  repr (unsigned x / unsigned y).
+Definition modu (x y: int) : int :=
+  repr (Zmod (unsigned x) (unsigned y)).
+
+(** For bitwise operations, we need to convert between Coq integers [Z]
+  and their bit-level representations.  Bit-level representations are
+  represented as characteristic functions, that is, functions [f]
+  of type [nat -> bool] such that [f i] is the value of the [i]-th bit
+  of the number.  The values of characteristic functions for [i] greater
+  than 32 are ignored. *)
+
+Definition Z_shift_add (b: bool) (x: Z) :=
+  if b then 2 * x + 1 else 2 * x.
+
+Definition Z_bin_decomp (x: Z) : bool * Z :=
+  match x with
+  | Z0 => (false, 0)
+  | Zpos p =>
+      match p with
+      | xI q => (true, Zpos q)
+      | xO q => (false, Zpos q)
+      | xH => (true, 0)
+      end
+  | Zneg p =>
+      match p with
+      | xI q => (true, Zneg q - 1)
+      | xO q => (false, Zneg q)
+      | xH => (true, -1)
+      end
+  end.
+
+Fixpoint bits_of_Z (n: nat) (x: Z) {struct n}: Z -> bool :=
+  match n with
+  | O =>
+      (fun i: Z => false)
+  | S m =>
+      let (b, y) := Z_bin_decomp x in
+      let f := bits_of_Z m y in
+      (fun i: Z => if zeq i 0 then b else f (i - 1))
+  end.
+
+Fixpoint Z_of_bits (n: nat) (f: Z -> bool) {struct n}: Z :=
+  match n with
+  | O => 0
+  | S m => Z_shift_add (f 0) (Z_of_bits m (fun i => f (i + 1)))
+  end.
+
+(** Bitwise logical ``and'', ``or'' and ``xor'' operations. *)
+
+Definition bitwise_binop (f: bool -> bool -> bool) (x y: int) :=
+  let fx := bits_of_Z wordsize (unsigned x) in
+  let fy := bits_of_Z wordsize (unsigned y) in
+  repr (Z_of_bits wordsize (fun i => f (fx i) (fy i))).
+
+Definition and (x y: int): int := bitwise_binop andb x y.
+Definition or (x y: int): int := bitwise_binop orb x y.
+Definition xor (x y: int) : int := bitwise_binop xorb x y.
+
+Definition not (x: int) : int := xor x mone.
+
+(** Shifts and rotates. *)
+
+Definition shl (x y: int): int :=
+  let fx := bits_of_Z wordsize (unsigned x) in
+  let vy := unsigned y in
+  repr (Z_of_bits wordsize (fun i => fx (i - vy))).
+
+Definition shru (x y: int): int :=
+  let fx := bits_of_Z wordsize (unsigned x) in
+  let vy := unsigned y in
+  repr (Z_of_bits wordsize (fun i => fx (i + vy))).
+
+(** Arithmetic right shift is defined as signed division by a power of two.
+  Two such shifts are defined: [shr] rounds towards minus infinity
+  (standard behaviour for arithmetic right shift) and
+  [shrx] rounds towards zero. *)
+
+Definition shr (x y: int): int :=
+  repr (signed x / two_p (unsigned y)).
+Definition shrx (x y: int): int :=
+  divs x (shl one y).
+
+Definition shr_carry (x y: int) :=
+  sub (shrx x y) (shr x y).
+
+Definition rol (x y: int) : int :=
+  let fx := bits_of_Z wordsize (unsigned x) in
+  let vy := unsigned y in
+  repr (Z_of_bits wordsize
+         (fun i => fx (Zmod (i - vy) (Z_of_nat wordsize)))).
+
+Definition rolm (x a m: int): int := and (rol x a) m.
+
+(** Decomposition of a number as a sum of powers of two. *)
+
+Fixpoint Z_one_bits (n: nat) (x: Z) (i: Z) {struct n}: list Z :=
+  match n with
+  | O => nil
+  | S m =>
+      let (b, y) := Z_bin_decomp x in
+      if b then i :: Z_one_bits m y (i+1) else Z_one_bits m y (i+1)
+  end.
+
+Definition one_bits (x: int) : list int :=
+  List.map repr (Z_one_bits wordsize (unsigned x) 0).
+
+(** Recognition of powers of two. *)
+
+Definition is_power2 (x: int) : option int :=
+  match Z_one_bits wordsize (unsigned x) 0 with
+  | i :: nil => Some (repr i)
+  | _ => None
+  end.
+
+(** Recognition of integers that are acceptable as immediate operands
+  to the [rlwim] PowerPC instruction.  These integers are of the form
+  [000011110000] or [111100001111], that is, a run of one bits
+  surrounded by zero bits, or conversely.  We recognize these integers by
+  running the following automaton on the bits.  The accepting states are
+  2, 3, 4, 5, and 6.
+<<
+               0          1          0
+              / \        / \        / \
+              \ /        \ /        \ /
+        -0--> [1] --1--> [2] --0--> [3]
+       /     
+     [0]
+       \
+        -1--> [4] --0--> [5] --1--> [6]
+              / \        / \        / \
+              \ /        \ /        \ /
+               1          0          1
+>>
+*)
+
+Inductive rlw_state: Set :=
+  | RLW_S0 : rlw_state
+  | RLW_S1 : rlw_state
+  | RLW_S2 : rlw_state
+  | RLW_S3 : rlw_state
+  | RLW_S4 : rlw_state
+  | RLW_S5 : rlw_state
+  | RLW_S6 : rlw_state
+  | RLW_Sbad : rlw_state.
+
+Definition rlw_transition (s: rlw_state) (b: bool) : rlw_state :=
+  match s, b with
+  | RLW_S0, false => RLW_S1
+  | RLW_S0, true  => RLW_S4
+  | RLW_S1, false => RLW_S1
+  | RLW_S1, true  => RLW_S2
+  | RLW_S2, false => RLW_S3
+  | RLW_S2, true  => RLW_S2
+  | RLW_S3, false => RLW_S3
+  | RLW_S3, true  => RLW_Sbad
+  | RLW_S4, false => RLW_S5
+  | RLW_S4, true  => RLW_S4
+  | RLW_S5, false => RLW_S5
+  | RLW_S5, true  => RLW_S6
+  | RLW_S6, false => RLW_Sbad
+  | RLW_S6, true  => RLW_S6
+  | RLW_Sbad, _ => RLW_Sbad
+  end.
+
+Definition rlw_accepting (s: rlw_state) : bool :=
+  match s with
+  | RLW_S0 => false
+  | RLW_S1 => false
+  | RLW_S2 => true
+  | RLW_S3 => true
+  | RLW_S4 => true
+  | RLW_S5 => true
+  | RLW_S6 => true
+  | RLW_Sbad => false
+  end.
+
+Fixpoint is_rlw_mask_rec (n: nat) (s: rlw_state) (x: Z) {struct n} : bool :=
+  match n with
+  | O =>
+      rlw_accepting s
+  | S m =>
+      let (b, y) := Z_bin_decomp x in
+      is_rlw_mask_rec m (rlw_transition s b) y
+  end.
+
+Definition is_rlw_mask (x: int) : bool :=
+  is_rlw_mask_rec wordsize RLW_S0 (unsigned x).
+
+(** Comparisons. *)
+
+Definition cmp (c: comparison) (x y: int) : bool :=
+  match c with
+  | Ceq => eq x y
+  | Cne => negb (eq x y)
+  | Clt => lt x y
+  | Cle => negb (lt y x)
+  | Cgt => lt y x
+  | Cge => negb (lt x y)
+  end.
+
+Definition cmpu (c: comparison) (x y: int) : bool :=
+  match c with
+  | Ceq => eq x y
+  | Cne => negb (eq x y)
+  | Clt => ltu x y
+  | Cle => negb (ltu y x)
+  | Cgt => ltu y x
+  | Cge => negb (ltu x y)
+  end.
+
+Definition is_false (x: int) : Prop := x = zero.
+Definition is_true  (x: int) : Prop := x <> zero.
+Definition notbool  (x: int) : int  := if eq x zero then one else zero.
+
+(** * Properties of integers and integer arithmetic *)
+
+(** ** Properties of equality *)
+
+Theorem one_not_zero: Int.one <> Int.zero.
+Proof.
+  compute. congruence. 
+Qed.
+
+Theorem eq_sym:
+  forall x y, eq x y = eq y x.
+Proof.
+  intros; unfold eq. case (zeq (unsigned x) (unsigned y)); intro.
+  rewrite e. rewrite zeq_true. auto.
+  rewrite zeq_false. auto. auto.
+Qed.
+
+Theorem eq_spec: forall (x y: int), if eq x y then x = y else x <> y.
+Proof.
+  intros; unfold eq. case (eq_dec x y); intro.
+  subst y. rewrite zeq_true. auto.
+  rewrite zeq_false. auto. 
+  destruct x; destruct y.
+  simpl. red; intro. elim n. apply mkint_eq. auto.
+Qed.
+
+Theorem eq_true: forall x, eq x x = true.
+Proof.
+  intros. generalize (eq_spec x x); case (eq x x); intros; congruence.
+Qed.
+
+Theorem eq_false: forall x y, x <> y -> eq x y = false.
+Proof.
+  intros. generalize (eq_spec x y); case (eq x y); intros; congruence.
+Qed.
+
+(** ** Modulo arithmetic *)
+
+(** We define and state properties of equality and arithmetic modulo a
+  positive integer. *)
+
+Section EQ_MODULO.
+
+Variable modul: Z.
+Hypothesis modul_pos: modul > 0.
+
+Definition eqmod (x y: Z) : Prop := exists k, x = k * modul + y.
+
+Lemma eqmod_refl: forall x, eqmod x x.
+Proof.
+  intros; red. exists 0. omega.
+Qed.
+
+Lemma eqmod_refl2: forall x y, x = y -> eqmod x y.
+Proof.
+  intros. subst y. apply eqmod_refl.
+Qed.
+
+Lemma eqmod_sym: forall x y, eqmod x y -> eqmod y x.
+Proof.
+  intros x y [k EQ]; red. exists (-k). subst x. ring.
+Qed.
+
+Lemma eqmod_trans: forall x y z, eqmod x y -> eqmod y z -> eqmod x z.
+Proof.
+  intros x y z [k1 EQ1] [k2 EQ2]; red.
+  exists (k1 + k2). subst x; subst y. ring.
+Qed.
+
+Lemma eqmod_small_eq:
+  forall x y, eqmod x y -> 0 <= x < modul -> 0 <= y < modul -> x = y.
+Proof.
+  intros x y [k EQ] I1 I2.
+  generalize (Zdiv_unique _ _ _ _ EQ I2). intro.
+  rewrite (Zdiv_small x modul I1) in H. subst k. omega.
+Qed.
+
+Lemma eqmod_mod_eq:
+  forall x y, eqmod x y -> x mod modul = y mod modul.
+Proof.
+  intros x y [k EQ]. subst x. 
+  rewrite Zplus_comm. apply Z_mod_plus. auto.
+Qed.
+
+Lemma eqmod_mod:
+  forall x, eqmod x (x mod modul).
+Proof.
+  intros; red. exists (x / modul). 
+  rewrite Zmult_comm. apply Z_div_mod_eq. auto.
+Qed.
+
+Lemma eqmod_add:
+  forall a b c d, eqmod a b -> eqmod c d -> eqmod (a + c) (b + d).
+Proof.
+  intros a b c d [k1 EQ1] [k2 EQ2]; red.
+  subst a; subst c. exists (k1 + k2). ring.
+Qed.
+
+Lemma eqmod_neg:
+  forall x y, eqmod x y -> eqmod (-x) (-y).
+Proof.
+  intros x y [k EQ]; red. exists (-k). rewrite EQ. ring. 
+Qed.
+
+Lemma eqmod_sub:
+  forall a b c d, eqmod a b -> eqmod c d -> eqmod (a - c) (b - d).
+Proof.
+  intros a b c d [k1 EQ1] [k2 EQ2]; red.
+  subst a; subst c. exists (k1 - k2). ring.
+Qed.
+
+Lemma eqmod_mult:
+  forall a b c d, eqmod a c -> eqmod b d -> eqmod (a * b) (c * d).
+Proof.
+  intros a b c d [k1 EQ1] [k2 EQ2]; red.
+  subst a; subst b.
+  exists (k1 * k2 * modul + c * k2 + k1 * d).
+  ring.
+Qed.
+
+End EQ_MODULO.
+
+(** We then specialize these definitions to equality modulo 
+  $2^32$ #2<sup>32</sup>#. *)
+
+Lemma modulus_pos:
+  modulus > 0.
+Proof.
+  unfold modulus. apply two_power_nat_pos. 
+Qed.
+Hint Resolve modulus_pos: ints.
+
+Definition eqm := eqmod modulus.
+
+Lemma eqm_refl: forall x, eqm x x.
+Proof (eqmod_refl modulus).
+Hint Resolve eqm_refl: ints.
+
+Lemma eqm_refl2:
+  forall x y, x = y -> eqm x y.
+Proof (eqmod_refl2 modulus).
+Hint Resolve eqm_refl2: ints.
+
+Lemma eqm_sym: forall x y, eqm x y -> eqm y x.
+Proof (eqmod_sym modulus).
+Hint Resolve eqm_sym: ints.
+
+Lemma eqm_trans: forall x y z, eqm x y -> eqm y z -> eqm x z.
+Proof (eqmod_trans modulus).
+Hint Resolve eqm_trans: ints.
+
+Lemma eqm_samerepr: forall x y, eqm x y -> repr x = repr y.
+Proof.
+  intros. unfold repr. apply mkint_eq. 
+  apply eqmod_mod_eq. auto with ints. exact H.
+Qed.
+
+Lemma eqm_small_eq:
+  forall x y, eqm x y -> 0 <= x < modulus -> 0 <= y < modulus -> x = y.
+Proof (eqmod_small_eq modulus).
+Hint Resolve eqm_small_eq: ints.
+
+Lemma eqm_add:
+  forall a b c d, eqm a b -> eqm c d -> eqm (a + c) (b + d).
+Proof (eqmod_add modulus).
+Hint Resolve eqm_add: ints.
+
+Lemma eqm_neg:
+  forall x y, eqm x y -> eqm (-x) (-y).
+Proof (eqmod_neg modulus).
+Hint Resolve eqm_neg: ints.
+
+Lemma eqm_sub:
+  forall a b c d, eqm a b -> eqm c d -> eqm (a - c) (b - d).
+Proof (eqmod_sub modulus).
+Hint Resolve eqm_sub: ints.
+
+Lemma eqm_mult:
+  forall a b c d, eqm a c -> eqm b d -> eqm (a * b) (c * d).
+Proof (eqmod_mult modulus).
+Hint Resolve eqm_mult: ints.
+
+(** ** Properties of the coercions between [Z] and [int] *)
+
+Lemma eqm_unsigned_repr:
+  forall z, eqm z (unsigned (repr z)).
+Proof.
+  unfold eqm, repr, unsigned; intros; simpl.
+  apply eqmod_mod. auto with ints.
+Qed.
+Hint Resolve eqm_unsigned_repr: ints.
+
+Lemma eqm_unsigned_repr_l:
+  forall a b, eqm a b -> eqm (unsigned (repr a)) b.
+Proof.
+  intros. apply eqm_trans with a. 
+  apply eqm_sym. apply eqm_unsigned_repr. auto.
+Qed.
+Hint Resolve eqm_unsigned_repr_l: ints.
+
+Lemma eqm_unsigned_repr_r:
+  forall a b, eqm a b -> eqm a (unsigned (repr b)).
+Proof.
+  intros. apply eqm_trans with b. auto.
+  apply eqm_unsigned_repr. 
+Qed.
+Hint Resolve eqm_unsigned_repr_r: ints.
+
+Lemma eqm_signed_unsigned:
+  forall x, eqm (signed x) (unsigned x).
+Proof.
+  intro; red; unfold signed. set (y := unsigned x).
+  case (zlt y half_modulus); intro.
+  apply eqmod_refl. red; exists (-1); ring. 
+Qed.
+
+Lemma in_range_range:
+  forall z, in_range z -> 0 <= z < modulus.
+Proof.
+  intros. 
+  assert (z >= 0 /\ z < modulus).
+  generalize H. unfold in_range, Zge, Zlt.
+  destruct (z ?= 0).
+  destruct (z ?= modulus); try contradiction.
+  intuition congruence.
+  contradiction.
+  destruct (z ?= modulus); try contradiction.
+  intuition congruence.
+  omega.
+Qed.
+
+Theorem unsigned_range:
+  forall i, 0 <= unsigned i < modulus.
+Proof.
+  destruct i; simpl. 
+  apply in_range_range. auto.
+Qed.
+Hint Resolve unsigned_range: ints.
+
+Theorem unsigned_range_2:
+  forall i, 0 <= unsigned i <= max_unsigned.
+Proof.
+  intro; unfold max_unsigned. 
+  generalize (unsigned_range i). omega.
+Qed.
+Hint Resolve unsigned_range_2: ints.
+
+Theorem signed_range:
+  forall i, min_signed <= signed i <= max_signed.
+Proof.
+  intros. unfold signed. 
+  generalize (unsigned_range i). set (n := unsigned i). intros.
+  case (zlt n half_modulus); intro.
+  unfold max_signed. assert (min_signed < 0). compute. auto.
+  omega. 
+  unfold min_signed, max_signed. change modulus with (2 * half_modulus).
+  change modulus with (2 * half_modulus) in H. omega.
+Qed.  
+
+Theorem repr_unsigned:
+  forall i, repr (unsigned i) = i.
+Proof.
+  destruct i; simpl. unfold repr. apply mkint_eq.
+  apply Zmod_small. apply in_range_range; auto.
+Qed.
+Hint Resolve repr_unsigned: ints.
+
+Lemma repr_signed:
+  forall i, repr (signed i) = i.
+Proof.
+  intros. transitivity (repr (unsigned i)). 
+  apply eqm_samerepr. apply eqm_signed_unsigned. auto with ints.
+Qed.
+Hint Resolve repr_unsigned: ints.
+
+Theorem unsigned_repr:
+  forall z, 0 <= z <= max_unsigned -> unsigned (repr z) = z.
+Proof.
+  intros. unfold repr, unsigned; simpl. 
+  apply Zmod_small. unfold max_unsigned in H. omega.
+Qed.
+Hint Resolve unsigned_repr: ints.
+
+Theorem signed_repr:
+  forall z, min_signed <= z <= max_signed -> signed (repr z) = z.
+Proof.
+  intros. unfold signed. case (zle 0 z); intro.
+  replace (unsigned (repr z)) with z.
+  rewrite zlt_true. auto. unfold max_signed in H. omega.
+  symmetry. apply unsigned_repr. 
+  split. auto. apply Zle_trans with max_signed. tauto.
+  compute; intro; discriminate.
+  pose (z' := z + modulus).
+  replace (repr z) with (repr z').
+  replace (unsigned (repr z')) with z'.
+  rewrite zlt_false. unfold z'. omega.
+  unfold z'. unfold min_signed in H. 
+  change modulus with (half_modulus + half_modulus). omega.
+  symmetry. apply unsigned_repr.
+  unfold z', max_unsigned. unfold min_signed, max_signed in H.
+  change modulus with (half_modulus + half_modulus).
+  omega. 
+  apply eqm_samerepr. unfold z'; red. exists 1. omega.
+Qed.
+
+(** ** Properties of addition *)
+
+Theorem add_unsigned: forall x y, add x y = repr (unsigned x + unsigned y).
+Proof. intros; reflexivity.
+Qed.
+
+Theorem add_signed: forall x y, add x y = repr (signed x + signed y).
+Proof. 
+  intros. rewrite add_unsigned. apply eqm_samerepr.
+  apply eqm_add; apply eqm_sym; apply eqm_signed_unsigned.
+Qed.
+
+Theorem add_commut: forall x y, add x y = add y x.
+Proof. intros; unfold add. decEq. omega. Qed.
+
+Theorem add_zero: forall x, add x zero = x.
+Proof. 
+  intros; unfold add, zero. change (unsigned (repr 0)) with 0.
+  rewrite Zplus_0_r. apply repr_unsigned.
+Qed.
+
+Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z).
+Proof.
+  intros; unfold add.
+  set (x' := unsigned x).
+  set (y' := unsigned y).
+  set (z' := unsigned z).
+  apply eqm_samerepr. 
+  apply eqm_trans with ((x' + y') + z').
+  auto with ints.
+  rewrite <- Zplus_assoc. auto with ints.
+Qed.
+
+Theorem add_permut: forall x y z, add x (add y z) = add y (add x z).
+Proof.
+  intros. rewrite (add_commut y z). rewrite <- add_assoc. apply add_commut. 
+Qed.
+
+Theorem add_neg_zero: forall x, add x (neg x) = zero.
+Proof.
+  intros; unfold add, neg, zero. apply eqm_samerepr.
+  replace 0 with (unsigned x + (- (unsigned x))).
+  auto with ints. omega.
+Qed.
+
+(** ** Properties of negation *)
+
+Theorem neg_repr: forall z, neg (repr z) = repr (-z).
+Proof.
+  intros; unfold neg. apply eqm_samerepr. auto with ints.
+Qed.
+
+Theorem neg_zero: neg zero = zero.
+Proof.
+  unfold neg, zero. compute. apply mkint_eq. auto.
+Qed.
+
+Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y).
+Proof.
+  intros; unfold neg, add. apply eqm_samerepr.
+  apply eqm_trans with (- (unsigned x + unsigned y)).
+  auto with ints.
+  replace (- (unsigned x + unsigned y))
+     with ((- unsigned x) + (- unsigned y)).
+  auto with ints. omega.
+Qed.
+
+(** ** Properties of subtraction *)
+
+Theorem sub_zero_l: forall x, sub x zero = x.
+Proof.
+  intros; unfold sub. change (unsigned zero) with 0.
+  replace (unsigned x - 0) with (unsigned x). apply repr_unsigned.
+  omega.
+Qed.
+
+Theorem sub_zero_r: forall x, sub zero x = neg x.
+Proof.
+  intros; unfold sub, neg. change (unsigned zero) with 0.
+  replace (0 - unsigned x) with (- unsigned x). auto.
+  omega.
+Qed.
+
+Theorem sub_add_opp: forall x y, sub x y = add x (neg y).
+Proof.
+  intros; unfold sub, add, neg.
+  replace (unsigned x - unsigned y)
+     with (unsigned x + (- unsigned y)).
+  apply eqm_samerepr. auto with ints. omega.
+Qed.
+
+Theorem sub_idem: forall x, sub x x = zero.
+Proof.
+  intros; unfold sub. replace (unsigned x - unsigned x) with 0.
+  reflexivity. omega.
+Qed.
+
+Theorem sub_add_l: forall x y z, sub (add x y) z = add (sub x z) y.
+Proof.
+  intros. repeat rewrite sub_add_opp. 
+  repeat rewrite add_assoc. decEq. apply add_commut.
+Qed.
+
+Theorem sub_add_r: forall x y z, sub x (add y z) = add (sub x z) (neg y).
+Proof.
+  intros. repeat rewrite sub_add_opp.
+  rewrite neg_add_distr. rewrite add_permut. apply add_commut.
+Qed.
+
+Theorem sub_shifted:
+  forall x y z,
+  sub (add x z) (add y z) = sub x y.
+Proof.
+  intros. rewrite sub_add_opp. rewrite neg_add_distr.
+  rewrite add_assoc. 
+  rewrite (add_commut (neg y) (neg z)).
+  rewrite <- (add_assoc z). rewrite add_neg_zero.
+  rewrite (add_commut zero). rewrite add_zero.
+  symmetry. apply sub_add_opp.
+Qed.
+
+(** ** Properties of multiplication *)
+
+Theorem mul_commut: forall x y, mul x y = mul y x.
+Proof.
+  intros; unfold mul. decEq. ring. 
+Qed.
+
+Theorem mul_zero: forall x, mul x zero = zero.
+Proof.
+  intros; unfold mul. change (unsigned zero) with 0.
+  unfold zero. decEq. ring.
+Qed.
+
+Theorem mul_one: forall x, mul x one = x.
+Proof.
+  intros; unfold mul. change (unsigned one) with 1.
+  transitivity (repr (unsigned x)). decEq. ring.
+  apply repr_unsigned.
+Qed.
+
+Theorem mul_assoc: forall x y z, mul (mul x y) z = mul x (mul y z).
+Proof.
+  intros; unfold mul.
+  set (x' := unsigned x).
+  set (y' := unsigned y).
+  set (z' := unsigned z).
+  apply eqm_samerepr. apply eqm_trans with ((x' * y') * z').
+  auto with ints.
+  rewrite <- Zmult_assoc. auto with ints.
+Qed.
+
+Theorem mul_add_distr_l:
+  forall x y z, mul (add x y) z = add (mul x z) (mul y z).
+Proof.
+  intros; unfold mul, add.
+  apply eqm_samerepr.
+  set (x' := unsigned x).
+  set (y' := unsigned y).
+  set (z' := unsigned z).
+  apply eqm_trans with ((x' + y') * z').
+  auto with ints.
+  replace ((x' + y') * z') with (x' * z' + y' * z').
+  auto with ints.
+  ring.
+Qed.
+
+Theorem mul_add_distr_r:
+  forall x y z, mul x (add y z) = add (mul x y) (mul x z).
+Proof.
+  intros. rewrite mul_commut. rewrite mul_add_distr_l. 
+  decEq; apply mul_commut.
+Qed. 
+
+Axiom neg_mul_distr_l: forall x y, neg(mul x y) = mul (neg x) y.
+Axiom neg_mul_distr_r: forall x y, neg(mul x y) = mul x (neg y).
+
+(** ** Properties of binary decompositions *)
+
+Lemma Z_shift_add_bin_decomp:
+  forall x,
+  Z_shift_add (fst (Z_bin_decomp x)) (snd (Z_bin_decomp x)) = x.
+Proof.
+  destruct x; simpl.
+  auto.
+  destruct p; reflexivity.
+  destruct p; try reflexivity. simpl. 
+  assert (forall z, 2 * (z + 1) - 1 = 2 * z + 1). intro; omega.
+  generalize (H (Zpos p)); simpl. congruence.
+Qed.
+
+Lemma Z_shift_add_inj:
+  forall b1 x1 b2 x2,
+  Z_shift_add b1 x1 = Z_shift_add b2 x2 -> b1 = b2 /\ x1 = x2.
+Proof.
+  intros until x2.
+  unfold Z_shift_add.
+  destruct b1; destruct b2; intros;
+  ((split; [reflexivity|omega]) || omegaContradiction).
+Qed.
+
+Lemma Z_of_bits_exten:
+  forall n f1 f2,
+  (forall z, 0 <= z < Z_of_nat n -> f1 z = f2 z) ->
+  Z_of_bits n f1 = Z_of_bits n f2.
+Proof.
+  induction n; intros.
+  reflexivity.
+  simpl. rewrite inj_S in H. decEq. apply H. omega. 
+  apply IHn. intros; apply H. omega.
+Qed.
+
+Opaque Zmult.
+
+Lemma Z_of_bits_of_Z:
+  forall x, eqm (Z_of_bits wordsize (bits_of_Z wordsize x)) x.
+Proof.
+  assert (forall n x, exists k,
+    Z_of_bits n (bits_of_Z n x) = k * two_power_nat n + x).
+  induction n; intros.
+  rewrite two_power_nat_O. simpl. exists (-x). omega.
+  rewrite two_power_nat_S. simpl.
+  caseEq (Z_bin_decomp x). intros b y ZBD. simpl. 
+  replace (Z_of_bits n (fun i => if zeq (i + 1) 0 then b else bits_of_Z n y (i + 1 - 1)))
+     with (Z_of_bits n (bits_of_Z n y)).
+  elim (IHn y). intros k1 EQ1. rewrite EQ1.
+  rewrite <- (Z_shift_add_bin_decomp x). 
+  rewrite ZBD. simpl. 
+  exists k1.
+  case b; unfold Z_shift_add; ring.
+  apply Z_of_bits_exten. intros.
+  rewrite zeq_false. decEq. omega. omega. 
+  intro. exact (H wordsize x).
+Qed.
+
+Lemma bits_of_Z_zero:
+  forall n x, bits_of_Z n 0 x = false.
+Proof.
+  induction n; simpl; intros.
+  auto.
+  case (zeq x 0); intro. auto. auto.
+Qed.
+
+Remark Z_bin_decomp_2xm1:
+  forall x, Z_bin_decomp (2 * x - 1) = (true, x - 1).
+Proof.
+  intros. caseEq (Z_bin_decomp (2 * x - 1)). intros b y EQ.
+  generalize (Z_shift_add_bin_decomp (2 * x - 1)).
+  rewrite EQ; simpl.
+  replace (2 * x - 1) with (Z_shift_add true (x - 1)).
+  intro. elim (Z_shift_add_inj _ _ _ _ H); intros.
+  congruence. unfold Z_shift_add. omega.
+Qed.
+
+Lemma bits_of_Z_mone:
+  forall n x,
+  0 <= x < Z_of_nat n -> 
+  bits_of_Z n (two_power_nat n - 1) x = true.
+Proof.
+  induction n; intros.
+  simpl in H. omegaContradiction.
+  unfold bits_of_Z; fold bits_of_Z.
+  rewrite two_power_nat_S. rewrite Z_bin_decomp_2xm1.
+  rewrite inj_S in H. case (zeq x 0); intro. auto.
+  apply IHn. omega. 
+Qed.
+
+Lemma Z_bin_decomp_shift_add:
+  forall b x, Z_bin_decomp (Z_shift_add b x) = (b, x).
+Proof.
+  intros. caseEq (Z_bin_decomp (Z_shift_add b x)); intros b' x' EQ.
+  generalize (Z_shift_add_bin_decomp (Z_shift_add b x)).
+  rewrite EQ; simpl fst; simpl snd. intro.
+  elim (Z_shift_add_inj _ _ _ _ H); intros.
+  congruence.
+Qed.
+
+Lemma bits_of_Z_of_bits:
+  forall n f i,
+  0 <= i < Z_of_nat n ->
+  bits_of_Z n (Z_of_bits n f) i = f i.
+Proof.
+  induction n; intros; simpl.
+  simpl in H. omegaContradiction.
+  rewrite Z_bin_decomp_shift_add.
+  case (zeq i 0); intro.
+  congruence.
+  rewrite IHn. decEq. omega. rewrite inj_S in H. omega.
+Qed.  
+
+Lemma Z_of_bits_range:
+  forall f, 0 <= Z_of_bits wordsize f < modulus.
+Proof.
+  unfold max_unsigned, modulus.
+  generalize wordsize. induction n; simpl; intros.
+  rewrite two_power_nat_O. omega.
+  rewrite two_power_nat_S. generalize (IHn (fun i => f (i + 1))).
+  set (x := Z_of_bits n (fun i => f (i + 1))).
+  intro. destruct (f 0); unfold Z_shift_add; omega.
+Qed.
+Hint Resolve Z_of_bits_range: ints.
+
+Lemma Z_of_bits_range_2:
+  forall f, 0 <= Z_of_bits wordsize f <= max_unsigned.
+Proof.
+  intros. unfold max_unsigned.
+  generalize (Z_of_bits_range f). omega.
+Qed.
+Hint Resolve Z_of_bits_range_2: ints.
+
+Lemma bits_of_Z_below:
+  forall n x i, i < 0 -> bits_of_Z n x i = false.
+Proof.
+  induction n; simpl; intros.
+  reflexivity.
+  destruct (Z_bin_decomp x). rewrite zeq_false. apply IHn.
+  omega. omega.
+Qed.
+
+Lemma bits_of_Z_above:
+  forall n x i, i >= Z_of_nat n -> bits_of_Z n x i = false.
+Proof.
+  induction n; intros; simpl.
+  reflexivity.
+  destruct (Z_bin_decomp x). rewrite zeq_false. apply IHn.
+  rewrite inj_S in H. omega. rewrite inj_S in H. omega.
+Qed.
+
+Opaque Zmult.
+
+Lemma Z_of_bits_excl:
+  forall n f g h,
+  (forall i, 0 <= i < Z_of_nat n -> f i && g i = false) ->
+  (forall i, 0 <= i < Z_of_nat n -> f i || g i = h i) ->
+  Z_of_bits n f + Z_of_bits n g = Z_of_bits n h.
+Proof.
+  induction n.
+  intros; reflexivity.
+  intros. simpl. rewrite inj_S in H. rewrite inj_S in H0.
+  rewrite <- (IHn (fun i => f(i+1)) (fun i => g(i+1)) (fun i => h(i+1))).
+  assert (0 <= 0 < Zsucc(Z_of_nat n)). omega.
+  unfold Z_shift_add.
+  rewrite <- H0; auto.
+  set (F := Z_of_bits n (fun i => f(i + 1))).
+  set (G := Z_of_bits n (fun i => g(i + 1))).
+  caseEq (f 0); intros; caseEq (g 0); intros; simpl.
+  generalize (H 0 H1). rewrite H2; rewrite H3. simpl. intros; discriminate.
+  omega. omega. omega.
+  intros; apply H. omega.
+  intros; apply H0. omega.
+Qed.
+
+(** ** Properties of bitwise and, or, xor *)
+
+Lemma bitwise_binop_commut:
+  forall f,
+  (forall a b, f a b = f b a) ->
+  forall x y,
+  bitwise_binop f x y = bitwise_binop f y x.
+Proof.
+  unfold bitwise_binop; intros.
+  decEq. apply Z_of_bits_exten; intros. auto.
+Qed.
+
+Lemma bitwise_binop_assoc:
+  forall f,
+  (forall a b c, f a (f b c) = f (f a b) c) ->
+  forall x y z,
+  bitwise_binop f (bitwise_binop f x y) z =
+  bitwise_binop f x (bitwise_binop f y z).
+Proof.
+  unfold bitwise_binop; intros.
+  repeat rewrite unsigned_repr; auto with ints.
+  decEq. apply Z_of_bits_exten; intros.
+  repeat (rewrite bits_of_Z_of_bits; auto).
+Qed.
+
+Lemma bitwise_binop_idem:
+  forall f,
+  (forall a, f a a = a) ->
+  forall x,
+  bitwise_binop f x x = x.
+Proof.
+  unfold bitwise_binop; intros.
+  transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))).
+  decEq. apply Z_of_bits_exten; intros. auto.
+  transitivity (repr (unsigned x)).
+  apply eqm_samerepr. apply Z_of_bits_of_Z. apply repr_unsigned.
+Qed.
+
+Theorem and_commut: forall x y, and x y = and y x.
+Proof (bitwise_binop_commut andb andb_comm).
+
+Theorem and_assoc: forall x y z, and (and x y) z = and x (and y z).
+Proof (bitwise_binop_assoc andb andb_assoc).
+
+Theorem and_zero: forall x, and x zero = zero.
+Proof.
+  unfold and, bitwise_binop, zero; intros. 
+  transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize 0))).
+  decEq. apply Z_of_bits_exten. intros.
+  change (unsigned (repr 0)) with 0.
+  rewrite bits_of_Z_zero. apply andb_b_false.
+  auto with ints.
+Qed.
+
+Lemma mone_max_unsigned:
+  mone = repr max_unsigned.
+Proof.
+  unfold mone. apply eqm_samerepr. exists (-1).
+  unfold max_unsigned. omega.
+Qed.
+
+Theorem and_mone: forall x, and x mone = x.
+Proof.
+  unfold and, bitwise_binop; intros. 
+  rewrite mone_max_unsigned. unfold max_unsigned, modulus.
+  transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))).
+  decEq. apply Z_of_bits_exten. intros.
+  rewrite unsigned_repr. rewrite bits_of_Z_mone. 
+  apply andb_b_true. omega. compute. intuition congruence.
+  transitivity (repr (unsigned x)). 
+  apply eqm_samerepr. apply Z_of_bits_of_Z.
+  apply repr_unsigned.
+Qed.
+
+Theorem and_idem: forall x, and x x = x.
+Proof.
+  assert (forall b, b && b = b).
+    destruct b; reflexivity.
+  exact (bitwise_binop_idem andb H).
+Qed.
+
+Theorem or_commut: forall x y, or x y = or y x.
+Proof (bitwise_binop_commut orb orb_comm).
+
+Theorem or_assoc: forall x y z, or (or x y) z = or x (or y z).
+Proof (bitwise_binop_assoc orb orb_assoc).
+
+Theorem or_zero: forall x, or x zero = x.
+Proof.
+  unfold or, bitwise_binop, zero; intros. 
+  transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))).
+  decEq. apply Z_of_bits_exten. intros.
+  change (unsigned (repr 0)) with 0.
+  rewrite bits_of_Z_zero. apply orb_b_false.
+  transitivity (repr (unsigned x)); auto with ints.
+  apply eqm_samerepr. apply Z_of_bits_of_Z.
+Qed.
+
+Theorem or_mone: forall x, or x mone = mone.
+Proof.
+  rewrite mone_max_unsigned. 
+  unfold or, bitwise_binop; intros.
+  decEq. 
+  transitivity (Z_of_bits wordsize (bits_of_Z wordsize max_unsigned)).
+  apply Z_of_bits_exten. intros.
+  change (unsigned (repr max_unsigned)) with max_unsigned.
+  unfold max_unsigned, modulus. rewrite bits_of_Z_mone; auto.
+  apply orb_b_true. 
+  apply eqm_small_eq; auto with ints. compute; intuition congruence.
+Qed.
+
+Theorem or_idem: forall x, or x x = x.
+Proof.
+  assert (forall b, b || b = b).
+    destruct b; reflexivity.
+  exact (bitwise_binop_idem orb H).
+Qed.
+
+Theorem and_or_distrib:
+  forall x y z,
+  and x (or y z) = or (and x y) (and x z).
+Proof.
+  intros; unfold and, or, bitwise_binop.
+  decEq. repeat rewrite unsigned_repr; auto with ints.
+  apply Z_of_bits_exten; intros.
+  repeat rewrite bits_of_Z_of_bits; auto.
+  apply demorgan1.
+Qed.  
+
+Theorem xor_commut: forall x y, xor x y = xor y x.
+Proof (bitwise_binop_commut xorb xorb_comm).
+
+Theorem xor_assoc: forall x y z, xor (xor x y) z = xor x (xor y z).
+Proof.
+  assert (forall a b c, xorb a (xorb b c) = xorb (xorb a b) c).
+  symmetry. apply xorb_assoc.
+  exact (bitwise_binop_assoc xorb H).
+Qed.
+
+Theorem xor_zero: forall x, xor x zero = x.
+Proof.
+  unfold xor, bitwise_binop, zero; intros. 
+  transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))).
+  decEq. apply Z_of_bits_exten. intros.
+  change (unsigned (repr 0)) with 0.
+  rewrite bits_of_Z_zero. apply xorb_false.
+  transitivity (repr (unsigned x)); auto with ints.
+  apply eqm_samerepr. apply Z_of_bits_of_Z.
+Qed.
+
+Theorem xor_zero_one: xor zero one = one.
+Proof. reflexivity. Qed.
+
+Theorem xor_one_one: xor one one = zero.
+Proof. reflexivity. Qed.
+
+Theorem and_xor_distrib:
+  forall x y z,
+  and x (xor y z) = xor (and x y) (and x z).
+Proof.
+  intros; unfold and, xor, bitwise_binop.
+  decEq. repeat rewrite unsigned_repr; auto with ints.
+  apply Z_of_bits_exten; intros.
+  repeat rewrite bits_of_Z_of_bits; auto.
+  assert (forall a b c, a && (xorb b c) = xorb (a && b) (a && c)).
+    destruct a; destruct b; destruct c; reflexivity.
+  auto.
+Qed.  
+
+(** ** Properties of shifts and rotates *)
+
+Lemma Z_of_bits_shift:
+  forall n f,
+  exists k,
+  Z_of_bits n (fun i => f (i - 1)) =
+    k * two_power_nat n + Z_shift_add (f (-1)) (Z_of_bits n f).
+Proof.
+  induction n; intros.
+  simpl. rewrite two_power_nat_O. unfold Z_shift_add.
+  exists (if f (-1) then (-1) else 0).
+  destruct (f (-1)); omega.
+  rewrite two_power_nat_S. simpl. 
+  elim (IHn (fun i => f (i + 1))). intros k' EQ.
+  replace (Z_of_bits n (fun i => f (i - 1 + 1)))
+     with (Z_of_bits n (fun i => f (i + 1 - 1))) in EQ.
+  rewrite EQ.
+  change (-1 + 1) with 0.
+  exists k'.
+  unfold Z_shift_add; destruct (f (-1)); destruct (f 0); ring.
+  apply Z_of_bits_exten; intros.
+  decEq. omega.
+Qed.
+
+Lemma Z_of_bits_shifts:
+  forall m f,
+  0 <= m ->
+  (forall i, i < 0 -> f i = false) ->
+  eqm (Z_of_bits wordsize (fun i => f (i - m)))
+      (two_p m * Z_of_bits wordsize f).
+Proof.
+  intros. pattern m. apply natlike_ind.
+  apply eqm_refl2. transitivity (Z_of_bits wordsize f).
+  apply Z_of_bits_exten; intros. decEq. omega.
+  simpl two_p. omega.
+  intros. rewrite two_p_S; auto.
+  set (f' := fun i => f (i - x)).
+  apply eqm_trans with (Z_of_bits wordsize (fun i => f' (i - 1))).
+  apply eqm_refl2. apply Z_of_bits_exten; intros.
+  unfold f'. decEq. omega.
+  apply eqm_trans with (Z_shift_add (f' (-1)) (Z_of_bits wordsize f')).
+  exact (Z_of_bits_shift wordsize f').
+  unfold f'. unfold Z_shift_add. rewrite H0. 
+  rewrite <- Zmult_assoc. apply eqm_mult. apply eqm_refl.
+  apply H2. omega. assumption.
+Qed.
+
+Lemma shl_mul_two_p:
+  forall x y,
+  shl x y = mul x (repr (two_p (unsigned y))).
+Proof.
+  intros. unfold shl, mul. 
+  apply eqm_samerepr. 
+  eapply eqm_trans.
+  apply Z_of_bits_shifts.
+  generalize (unsigned_range y). omega.
+  intros; apply bits_of_Z_below; auto.
+  rewrite Zmult_comm. apply eqm_mult.
+  apply Z_of_bits_of_Z. apply eqm_unsigned_repr.
+Qed.
+
+Theorem shl_zero: forall x, shl x zero = x.
+Proof.
+  intros. rewrite shl_mul_two_p. 
+  change (repr (two_p (unsigned zero))) with one.
+  apply mul_one.
+Qed.
+
+Theorem shl_mul:
+  forall x y,
+  shl x y = mul x (shl one y).
+Proof.
+  intros. 
+  assert (shl one y = repr (two_p (unsigned y))).
+  rewrite shl_mul_two_p. rewrite mul_commut. rewrite mul_one. auto.
+  rewrite H. apply shl_mul_two_p.
+Qed.
+
+Theorem shl_rolm:
+  forall x n,
+  ltu n (repr (Z_of_nat wordsize)) = true ->
+  shl x n = rolm x n (shl mone n).
+Proof.
+  intros x n. unfold ltu. 
+  rewrite unsigned_repr. case (zlt (unsigned n) (Z_of_nat wordsize)); intros LT XX.
+  unfold shl, rolm, rol, and, bitwise_binop.
+  decEq. apply Z_of_bits_exten; intros.
+  repeat rewrite unsigned_repr; auto with ints.
+  repeat rewrite bits_of_Z_of_bits; auto. 
+  case (zlt z (unsigned n)); intro LT2.
+  assert (z - unsigned n < 0). omega.
+  rewrite (bits_of_Z_below wordsize (unsigned x) _ H0).
+  rewrite (bits_of_Z_below wordsize (unsigned mone) _ H0).
+  symmetry. apply andb_b_false. 
+  assert (z - unsigned n < Z_of_nat wordsize).
+    generalize (unsigned_range n). omega. 
+  replace (unsigned mone) with (two_power_nat wordsize - 1).
+  rewrite bits_of_Z_mone. rewrite andb_b_true. decEq.
+  rewrite Zmod_small. auto. omega. omega. 
+  rewrite mone_max_unsigned. reflexivity. 
+  discriminate.
+  compute; intuition congruence. 
+Qed.
+
+Lemma bitwise_binop_shl:
+  forall f x y n,
+  f false false = false ->
+  bitwise_binop f (shl x n) (shl y n) = shl (bitwise_binop f x y) n.
+Proof.
+  intros. unfold bitwise_binop, shl.
+  decEq. repeat rewrite unsigned_repr; auto with ints.
+  apply Z_of_bits_exten; intros.
+  case (zlt (z - unsigned n) 0); intro.
+  transitivity false. repeat rewrite bits_of_Z_of_bits; auto.
+  repeat rewrite bits_of_Z_below; auto.
+  rewrite bits_of_Z_below; auto.
+  repeat rewrite bits_of_Z_of_bits; auto.
+  generalize (unsigned_range n). omega.
+Qed.
+
+Lemma and_shl:
+  forall x y n,
+  and (shl x n) (shl y n) = shl (and x y) n.
+Proof.
+  unfold and; intros. apply bitwise_binop_shl. reflexivity.
+Qed.
+
+Theorem shru_rolm:
+  forall x n,
+  ltu n (repr (Z_of_nat wordsize)) = true ->
+  shru x n = rolm x (sub (repr (Z_of_nat wordsize)) n) (shru mone n).
+Proof.
+  intros x n. unfold ltu. 
+  rewrite unsigned_repr. 
+  case (zlt (unsigned n) (Z_of_nat wordsize)); intros LT XX.
+  unfold shru, rolm, rol, and, bitwise_binop.
+  decEq. apply Z_of_bits_exten; intros.
+  repeat rewrite unsigned_repr; auto with ints.
+  repeat rewrite bits_of_Z_of_bits; auto. 
+  unfold sub. 
+  change (unsigned (repr (Z_of_nat wordsize)))
+    with (Z_of_nat wordsize).
+  rewrite unsigned_repr. 
+  case (zlt (z + unsigned n) (Z_of_nat wordsize)); intro LT2.
+  replace (unsigned mone) with (two_power_nat wordsize - 1).
+  rewrite bits_of_Z_mone. rewrite andb_b_true.
+  decEq. 
+  replace (z - (Z_of_nat wordsize - unsigned n))
+     with ((z + unsigned n) + (-1) * Z_of_nat wordsize).
+  rewrite Z_mod_plus. symmetry. apply Zmod_small.
+  generalize (unsigned_range n). omega. omega. omega. 
+  generalize (unsigned_range n). omega. 
+  reflexivity.
+  rewrite (bits_of_Z_above wordsize (unsigned x) _ LT2).
+  rewrite (bits_of_Z_above wordsize (unsigned mone) _ LT2).
+  symmetry. apply andb_b_false.
+  split. omega. apply Zle_trans with (Z_of_nat wordsize).
+  generalize (unsigned_range n); omega. compute; intuition congruence.
+  discriminate.
+  split. omega. compute; intuition congruence.
+Qed.
+
+Lemma bitwise_binop_shru:
+  forall f x y n,
+  f false false = false ->
+  bitwise_binop f (shru x n) (shru y n) = shru (bitwise_binop f x y) n.
+Proof.
+  intros. unfold bitwise_binop, shru.
+  decEq. repeat rewrite unsigned_repr; auto with ints.
+  apply Z_of_bits_exten; intros.
+  case (zlt (z + unsigned n) (Z_of_nat wordsize)); intro.
+  repeat rewrite bits_of_Z_of_bits; auto.
+  generalize (unsigned_range n); omega.
+  transitivity false. repeat rewrite bits_of_Z_of_bits; auto.
+  repeat rewrite bits_of_Z_above; auto.
+  rewrite bits_of_Z_above; auto.
+Qed.
+
+Lemma and_shru:
+  forall x y n,
+  and (shru x n) (shru y n) = shru (and x y) n.
+Proof.
+  unfold and; intros. apply bitwise_binop_shru. reflexivity.
+Qed.
+
+Theorem rol_zero:
+  forall x,
+  rol x zero = x.
+Proof.
+  intros. unfold rol. transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))).
+  decEq. 
+  transitivity (repr (unsigned x)).
+  decEq. apply eqm_small_eq. apply Z_of_bits_of_Z. 
+  auto with ints. auto with ints. auto with ints. 
+Qed.
+
+Lemma bitwise_binop_rol:
+  forall f x y n,
+  bitwise_binop f (rol x n) (rol y n) = rol (bitwise_binop f x y) n.
+Proof.
+  intros. unfold bitwise_binop, rol.
+  decEq. repeat (rewrite unsigned_repr; auto with ints).
+  apply Z_of_bits_exten; intros.
+  repeat rewrite bits_of_Z_of_bits; auto.
+  apply Z_mod_lt. compute. auto. 
+Qed.
+
+Theorem rol_and:
+  forall x y n,
+  rol (and x y) n = and (rol x n) (rol y n).
+Proof.
+  intros. symmetry. unfold and. apply bitwise_binop_rol.
+Qed.
+
+Theorem rol_rol:
+  forall x n m,
+  rol (rol x n) m = rol x (modu (add n m) (repr (Z_of_nat wordsize))).
+Proof.
+  intros. unfold rol. decEq.
+  repeat (rewrite unsigned_repr; auto with ints).
+  apply Z_of_bits_exten; intros.
+  repeat rewrite bits_of_Z_of_bits; auto.
+  decEq. unfold modu, add. 
+  set (W := Z_of_nat wordsize).
+  set (M := unsigned m); set (N := unsigned n).
+  assert (W > 0). compute; auto.
+  assert (forall a, eqmod W a (unsigned (repr a))).
+    intro. elim (eqm_unsigned_repr a). intros k EQ.
+    red. exists (k * (modulus / W)). 
+    replace (k * (modulus / W) * W) with (k * modulus). auto.
+    rewrite <- Zmult_assoc. reflexivity.
+  apply eqmod_mod_eq. auto.
+  change (unsigned (repr W)) with W.
+  apply eqmod_trans with (z - (N + M) mod W).
+  apply eqmod_trans with ((z - M) - N).
+  apply eqmod_sub. apply eqmod_sym. apply eqmod_mod. auto.
+  apply eqmod_refl. 
+  replace (z - M - N) with (z - (N + M)).
+  apply eqmod_sub. apply eqmod_refl. apply eqmod_mod. auto.
+  omega.
+  apply eqmod_sub. apply eqmod_refl. 
+  eapply eqmod_trans; [idtac|apply H1].
+  eapply eqmod_trans; [idtac|apply eqmod_mod].
+  apply eqmod_sym. eapply eqmod_trans; [idtac|apply eqmod_mod].
+  apply eqmod_sym. apply H1. auto. auto. 
+  apply Z_mod_lt. compute; auto.
+Qed.
+
+Theorem rolm_zero:
+  forall x m,
+  rolm x zero m = and x m.
+Proof.
+  intros. unfold rolm. rewrite rol_zero. auto.
+Qed.
+
+Theorem rolm_rolm:
+  forall x n1 m1 n2 m2,
+  rolm (rolm x n1 m1) n2 m2 =
+    rolm x (modu (add n1 n2) (repr (Z_of_nat wordsize)))
+           (and (rol m1 n2) m2).
+Proof.
+  intros.
+  unfold rolm. rewrite rol_and. rewrite and_assoc. 
+  rewrite rol_rol. reflexivity.
+Qed.
+
+Theorem rol_or:
+  forall x y n,
+  rol (or x y) n = or (rol x n) (rol y n).
+Proof.
+  intros. symmetry. unfold or. apply bitwise_binop_rol.
+Qed.
+
+Theorem or_rolm:
+  forall x n m1 m2,
+  or (rolm x n m1) (rolm x n m2) = rolm x n (or m1 m2).
+Proof.
+  intros; unfold rolm. symmetry. apply and_or_distrib. 
+Qed.
+
+(** ** Relation between shifts and powers of 2 *)
+
+Fixpoint powerserie (l: list Z): Z :=
+  match l with
+  | nil => 0
+  | x :: xs => two_p x + powerserie xs
+  end.
+
+Lemma Z_bin_decomp_range:
+  forall x n,
+  0 <= x < 2 * n -> 0 <= snd (Z_bin_decomp x) < n.
+Proof.
+  intros. rewrite <- (Z_shift_add_bin_decomp x) in H.
+  unfold Z_shift_add in H. destruct (fst (Z_bin_decomp x)); omega.
+Qed.
+
+Lemma Z_one_bits_powerserie:
+  forall x, 0 <= x < modulus -> x = powerserie (Z_one_bits wordsize x 0).
+Proof.
+  assert (forall n x i, 
+    0 <= i ->
+    0 <= x < two_power_nat n ->
+    x * two_p i = powerserie (Z_one_bits n x i)).
+  induction n; intros.
+  simpl. rewrite two_power_nat_O in H0. 
+  assert (x = 0). omega. subst x. omega.
+  rewrite two_power_nat_S in H0. simpl Z_one_bits.
+  generalize (Z_shift_add_bin_decomp x).
+  generalize (Z_bin_decomp_range x _ H0).
+  case (Z_bin_decomp x). simpl. intros b y RANGE SHADD. 
+  subst x. unfold Z_shift_add.
+  destruct b. simpl powerserie. rewrite <- IHn. 
+  rewrite two_p_is_exp. change (two_p 1) with 2. ring.
+  auto. omega. omega. auto.
+  rewrite <- IHn. 
+  rewrite two_p_is_exp. change (two_p 1) with 2. ring.
+  auto. omega. omega. auto.
+  intros. rewrite <- H. change (two_p 0) with 1. omega.
+  omega. exact H0.
+Qed.
+
+Lemma Z_one_bits_range:
+  forall x i, In i (Z_one_bits wordsize x 0) -> 0 <= i < Z_of_nat wordsize.
+Proof.
+  assert (forall n x i j,
+    In j (Z_one_bits n x i) -> i <= j < i + Z_of_nat n).
+  induction n; simpl In.
+  intros; elim H.
+  intros x i j. destruct (Z_bin_decomp x). case b.
+  rewrite inj_S. simpl. intros [A|B]. subst j. omega.
+  generalize (IHn _ _ _ B). omega.
+  intros B. rewrite inj_S. generalize (IHn _ _ _ B). omega.
+  intros. generalize (H wordsize x 0 i H0). omega.
+Qed.
+
+Lemma is_power2_rng:
+  forall n logn,
+  is_power2 n = Some logn ->
+  0 <= unsigned logn < Z_of_nat wordsize.
+Proof.
+  intros n logn. unfold is_power2.
+  generalize (Z_one_bits_range (unsigned n)).
+  destruct (Z_one_bits wordsize (unsigned n) 0).
+  intros; discriminate.
+  destruct l.
+  intros. injection H0; intro; subst logn; clear H0.
+  assert (0 <= z < Z_of_nat wordsize).
+  apply H. auto with coqlib.
+  rewrite unsigned_repr. auto.
+  assert (Z_of_nat wordsize < max_unsigned). compute. auto.
+  omega.
+  intros; discriminate.
+Qed.
+
+Theorem is_power2_range:
+  forall n logn,
+  is_power2 n = Some logn -> ltu logn (repr (Z_of_nat wordsize)) = true.
+Proof.
+  intros. unfold ltu.
+  change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
+  generalize (is_power2_rng _ _ H). 
+  case (zlt (unsigned logn) (Z_of_nat wordsize)); intros.
+  auto. omegaContradiction. 
+Qed. 
+
+Lemma is_power2_correct:
+  forall n logn,
+  is_power2 n = Some logn ->
+  unsigned n = two_p (unsigned logn).
+Proof.
+  intros n logn. unfold is_power2.
+  generalize (Z_one_bits_powerserie (unsigned n) (unsigned_range n)).
+  generalize (Z_one_bits_range (unsigned n)).
+  destruct (Z_one_bits wordsize (unsigned n) 0).
+  intros; discriminate.
+  destruct l.
+  intros. simpl in H0. injection H1; intros; subst logn; clear H1.
+  rewrite unsigned_repr. replace (two_p z) with (two_p z + 0).
+  auto. omega. elim (H z); intros. 
+  assert (Z_of_nat wordsize < max_unsigned). compute; auto.
+  omega. auto with coqlib. 
+  intros; discriminate.
+Qed.
+
+Theorem mul_pow2:
+  forall x n logn,
+  is_power2 n = Some logn ->
+  mul x n = shl x logn.
+Proof.
+  intros. generalize (is_power2_correct n logn H); intro.
+  rewrite shl_mul_two_p. rewrite <- H0. rewrite repr_unsigned.
+  auto.
+Qed.
+
+Lemma Z_of_bits_shift_rev:
+  forall n f,
+  (forall i, i >= Z_of_nat n -> f i = false) ->
+  Z_of_bits n f = Z_shift_add (f 0) (Z_of_bits n (fun i => f(i + 1))).
+Proof.
+  induction n; intros.
+  simpl. rewrite H. reflexivity. unfold Z_of_nat. omega.
+  simpl. rewrite (IHn (fun i => f (i + 1))).
+  reflexivity. 
+  intros. apply H. rewrite inj_S. omega.
+Qed.
+
+Lemma Z_of_bits_shifts_rev:
+  forall m f,
+  0 <= m ->
+  (forall i, i >= Z_of_nat wordsize -> f i = false) ->
+  exists k,
+  Z_of_bits wordsize f = k + two_p m * Z_of_bits wordsize (fun i => f(i + m))
+  /\ 0 <= k < two_p m.
+Proof.
+  intros. pattern m. apply natlike_ind.
+  exists 0. change (two_p 0) with 1. split.
+  transitivity (Z_of_bits wordsize (fun i => f (i + 0))).
+  apply Z_of_bits_exten. intros. decEq. omega.
+  omega. omega.
+  intros x POSx [k [EQ1 RANGE1]].
+  set (f' := fun i => f (i + x)) in *.
+  assert (forall i, i >= Z_of_nat wordsize -> f' i = false).
+  intros. unfold f'. apply H0. omega.  
+  generalize (Z_of_bits_shift_rev wordsize f' H1). intro.
+  rewrite EQ1. rewrite H2. 
+  set (z := Z_of_bits wordsize (fun i => f (i + Zsucc x))).
+  replace (Z_of_bits wordsize (fun i => f' (i + 1))) with z.
+  rewrite two_p_S.
+  case (f' 0); unfold Z_shift_add.
+  exists (k + two_p x). split. ring. omega. 
+  exists k. split. ring. omega.
+  auto. 
+  unfold z. apply Z_of_bits_exten; intros. unfold f'.
+  decEq. omega. 
+  auto.
+Qed.
+
+Lemma shru_div_two_p:
+  forall x y,
+  shru x y = repr (unsigned x / two_p (unsigned y)).
+Proof.
+  intros. unfold shru. 
+  set (x' := unsigned x). set (y' := unsigned y).
+  elim (Z_of_bits_shifts_rev y' (bits_of_Z wordsize x')).
+  intros k [EQ RANGE].
+  replace (Z_of_bits wordsize (bits_of_Z wordsize x')) with x' in EQ.
+  rewrite Zplus_comm in EQ. rewrite Zmult_comm in EQ.
+  generalize (Zdiv_unique _ _ _ _ EQ RANGE). intros.
+  rewrite H. auto.
+  apply eqm_small_eq. apply eqm_sym. apply Z_of_bits_of_Z. 
+  unfold x'. apply unsigned_range. 
+  auto with ints.
+  generalize (unsigned_range y). unfold y'. omega.
+  intros. apply bits_of_Z_above. auto.
+Qed.
+
+Theorem shru_zero:
+  forall x, shru x zero = x.
+Proof.
+  intros. rewrite shru_div_two_p. change (two_p (unsigned zero)) with 1.
+  transitivity (repr (unsigned x)). decEq. apply Zdiv_unique with 0.
+  omega. omega. auto with ints.
+Qed.
+
+Theorem shr_zero:
+  forall x, shr x zero = x.
+Proof.
+  intros. unfold shr. change (two_p (unsigned zero)) with 1.
+  replace (signed x / 1) with (signed x).
+  apply repr_signed.
+  symmetry. apply Zdiv_unique with 0. omega. omega. 
+Qed.
+
+Theorem divu_pow2:
+  forall x n logn,
+  is_power2 n = Some logn ->
+  divu x n = shru x logn.
+Proof.
+  intros. generalize (is_power2_correct n logn H). intro.
+  symmetry. unfold divu. rewrite H0. apply shru_div_two_p.
+Qed.
+
+Lemma modu_divu_Euclid:
+  forall x y, y <> zero -> x = add (mul (divu x y) y) (modu x y).
+Proof.
+  intros. unfold add, mul, divu, modu.
+  transitivity (repr (unsigned x)). auto with ints. 
+  apply eqm_samerepr. 
+  set (x' := unsigned x). set (y' := unsigned y).
+  apply eqm_trans with ((x' / y') * y' + x' mod y').
+  apply eqm_refl2. rewrite Zmult_comm. apply Z_div_mod_eq.
+  generalize (unsigned_range y); intro.
+  assert (unsigned y <> 0). red; intro. 
+  elim H. rewrite <- (repr_unsigned y). unfold zero. congruence.
+  unfold y'. omega.
+  auto with ints.
+Qed.
+
+Theorem modu_divu:
+  forall x y, y <> zero -> modu x y = sub x (mul (divu x y) y).
+Proof.
+  intros. 
+  assert (forall a b c, a = add b c -> c = sub a b).
+  intros. subst a. rewrite sub_add_l. rewrite sub_idem.
+  rewrite add_commut. rewrite add_zero. auto.
+  apply H0. apply modu_divu_Euclid. auto.
+Qed.
+
+Theorem mods_divs:
+  forall x y, mods x y = sub x (mul (divs x y) y).
+Proof.
+  intros; unfold mods, sub, mul, divs.
+  apply eqm_samerepr.
+  unfold Zmod_round.
+  apply eqm_sub. apply eqm_signed_unsigned. 
+  apply eqm_unsigned_repr_r. 
+  apply eqm_mult. auto with ints. apply eqm_signed_unsigned.
+Qed.
+
+Theorem divs_pow2:
+  forall x n logn,
+  is_power2 n = Some logn ->
+  divs x n = shrx x logn.
+Proof.
+  intros. generalize (is_power2_correct _ _ H); intro.
+  unfold shrx. rewrite shl_mul_two_p.
+  rewrite mul_commut. rewrite mul_one.
+  rewrite <- H0. rewrite repr_unsigned. auto.
+Qed.
+
+Theorem shrx_carry:
+  forall x y,
+  add (shr x y) (shr_carry x y) = shrx x y.
+Proof.
+  intros. unfold shr_carry. 
+  rewrite sub_add_opp. rewrite add_permut. 
+  rewrite add_neg_zero. apply add_zero.
+Qed.
+
+Lemma add_and:
+  forall x y z,
+  and y z = zero ->
+  or y z = mone ->
+  add (and x y) (and x z) = x.
+Proof.
+  intros. unfold add. transitivity (repr (unsigned x)); auto with ints.
+  decEq. unfold and, bitwise_binop.
+  repeat rewrite unsigned_repr; auto with ints.
+  transitivity (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x))).
+  apply Z_of_bits_excl. intros. 
+  assert (forall a b c, a && b && (a && c) = a && (b && c)).
+    destruct a; destruct b; destruct c; reflexivity.
+  rewrite H2. 
+  replace (bits_of_Z wordsize (unsigned y) i &&
+           bits_of_Z wordsize (unsigned z) i)
+     with (bits_of_Z wordsize (unsigned (and y z)) i).
+  rewrite H. change (unsigned zero) with 0. 
+  rewrite bits_of_Z_zero. apply andb_b_false.
+  unfold and, bitwise_binop. 
+  rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits. 
+  reflexivity. auto. 
+  intros. rewrite <- demorgan1. 
+  replace (bits_of_Z wordsize (unsigned y) i ||
+           bits_of_Z wordsize (unsigned z) i)
+     with (bits_of_Z wordsize (unsigned (or y z)) i).
+  rewrite H0. change (unsigned mone) with (two_power_nat wordsize - 1).
+  rewrite bits_of_Z_mone; auto. apply andb_b_true.
+  unfold or, bitwise_binop. 
+  rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits; auto.
+  apply eqm_small_eq; auto with ints. apply Z_of_bits_of_Z. 
+Qed.
+
+(** To prove equalities involving modulus and bitwise ``and'', we need to
+  show complicated integer equalities involving one integer variable
+  that ranges between 0 and 31.  Rather than proving these equalities,
+  we ask Coq to check them by computing the 32 values of the 
+  left and right-hand sides and checking that they are equal.
+  This is an instance of proving by reflection. *)
+
+Section REFLECTION.
+
+Variables (f g: int -> int).
+
+Fixpoint check_equal_on_range (n: nat) : bool :=
+  match n with
+  | O => true
+  | S n => if eq (f (repr (Z_of_nat n))) (g (repr (Z_of_nat n)))
+           then check_equal_on_range n
+           else false
+  end.
+
+Lemma check_equal_on_range_correct:
+  forall n, 
+  check_equal_on_range n = true ->
+  forall z, 0 <= z < Z_of_nat n -> f (repr z) = g (repr z).
+Proof.
+  induction n.
+  simpl; intros;  omegaContradiction.
+  simpl check_equal_on_range.
+  set (fn := f (repr (Z_of_nat n))).
+  set (gn := g (repr (Z_of_nat n))).
+  generalize (eq_spec fn gn).
+  case (eq fn gn); intros.
+  rewrite inj_S in H1. 
+  assert (0 <= z < Z_of_nat n \/ z = Z_of_nat n). omega.
+  elim H2; intro.
+  apply IHn. auto. auto.
+  subst z; auto. 
+  discriminate. 
+Qed.
+
+Lemma equal_on_range:
+  check_equal_on_range wordsize = true ->
+  forall n, 0 <= unsigned n < Z_of_nat wordsize ->
+  f n = g n.
+Proof.
+  intros. replace n with (repr (unsigned n)). 
+  apply check_equal_on_range_correct with wordsize; auto.
+  apply repr_unsigned.
+Qed.
+
+End REFLECTION.
+
+(** Here are the three equalities that we prove by reflection. *)
+
+Remark modu_and_masks_1:
+  forall logn, 0 <= unsigned logn < Z_of_nat wordsize ->
+  rol (shru mone logn) logn = shl mone logn.
+Proof (equal_on_range
+        (fun l => rol (shru mone l) l)
+        (fun l => shl mone l)
+        (refl_equal true)).
+Remark modu_and_masks_2:
+  forall logn, 0 <= unsigned logn < Z_of_nat wordsize ->
+  and (shl mone logn) (sub (repr (two_p (unsigned logn))) one) = zero.
+Proof (equal_on_range
+        (fun l => and (shl mone l)
+                      (sub (repr (two_p (unsigned l))) one))
+        (fun l => zero) 
+        (refl_equal true)).
+Remark modu_and_masks_3:
+  forall logn, 0 <= unsigned logn < Z_of_nat wordsize ->
+  or (shl mone logn) (sub (repr (two_p (unsigned logn))) one) = mone.
+Proof (equal_on_range
+        (fun l => or (shl mone l)
+                      (sub (repr (two_p (unsigned l))) one))
+        (fun l => mone)
+        (refl_equal true)).
+
+Theorem modu_and:
+  forall x n logn,
+  is_power2 n = Some logn ->
+  modu x n = and x (sub n one).
+Proof.
+  intros. generalize (is_power2_correct _ _ H); intro.
+  generalize (is_power2_rng _ _ H); intro.
+  assert (n <> zero). 
+    red; intro. subst n. change (unsigned zero) with 0 in H0.
+    assert (two_p (unsigned logn) > 0). apply two_p_gt_ZERO. omega.
+    omegaContradiction.
+  generalize (modu_divu_Euclid x n H2); intro.
+  assert (forall a b c, add a b = add a c -> b = c).
+    intros. assert (sub (add a b) a = sub (add a c) a). congruence.
+    repeat rewrite sub_add_l in H5. repeat rewrite sub_idem in H5.
+    rewrite add_commut in H5; rewrite add_zero in H5.
+    rewrite add_commut in H5; rewrite add_zero in H5.
+    auto.
+  apply H4 with (mul (divu x n) n).
+  rewrite <- H3. 
+  rewrite (divu_pow2 x n logn H). 
+  rewrite (mul_pow2 (shru x logn) n logn H). 
+  rewrite shru_rolm. rewrite shl_rolm. rewrite rolm_rolm.
+  rewrite sub_add_opp. rewrite add_assoc. 
+  replace (add (neg logn) logn) with zero.
+  rewrite add_zero.
+  change (modu (repr (Z_of_nat wordsize)) (repr (Z_of_nat wordsize)))
+    with zero.
+  rewrite rolm_zero. 
+  symmetry.
+  replace n with (repr (two_p (unsigned logn))).
+  rewrite modu_and_masks_1; auto.
+  rewrite and_idem.
+  apply add_and. apply modu_and_masks_2; auto. apply modu_and_masks_3; auto.
+  transitivity (repr (unsigned n)). decEq. auto. auto with ints.
+  rewrite add_commut. rewrite add_neg_zero. auto.
+  unfold ltu. apply zlt_true. 
+  change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
+  omega.
+  unfold ltu. apply zlt_true. 
+  change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
+  omega.
+Qed.
+
+(** ** Properties of integer zero extension and sign extension. *)
+
+Theorem cast8unsigned_and:
+  forall x, cast8unsigned x = and x (repr 255).
+Proof.
+  intros; unfold cast8unsigned. 
+  change (repr (unsigned x mod 256)) with (modu x (repr 256)).
+  change (repr 255) with (sub (repr 256) one).
+  apply modu_and with (repr 8). reflexivity.
+Qed.
+
+Theorem cast16unsigned_and:
+  forall x, cast16unsigned x = and x (repr 65535).
+Proof.
+  intros; unfold cast16unsigned. 
+  change (repr (unsigned x mod 65536)) with (modu x (repr 65536)).
+  change (repr 65535) with (sub (repr 65536) one).
+  apply modu_and with (repr 16). reflexivity.
+Qed.
+
+Lemma eqmod_256_unsigned_repr:
+  forall a, eqmod 256 a (unsigned (repr a)).
+Proof.
+  intros. generalize (eqm_unsigned_repr a). unfold eqm, eqmod.
+  intros [k EQ]. exists (k * (modulus / 256)). 
+  replace (k * (modulus / 256) * 256)  
+     with (k * ((modulus / 256) * 256)).
+  exact EQ. ring. 
+Qed.
+
+Lemma eqmod_65536_unsigned_repr:
+  forall a, eqmod 65536 a (unsigned (repr a)).
+Proof.
+  intros. generalize (eqm_unsigned_repr a). unfold eqm, eqmod.
+  intros [k EQ]. exists (k * (modulus / 65536)). 
+  replace (k * (modulus / 65536) * 65536)  
+     with (k * ((modulus / 65536) * 65536)).
+  exact EQ. ring. 
+Qed.
+
+Theorem cast8_signed_unsigned:
+  forall n, cast8signed (cast8unsigned n) = cast8signed n.
+Proof.
+  intros; unfold cast8signed, cast8unsigned.
+  set (N := unsigned n).
+  rewrite unsigned_repr. 
+  replace ((N mod 256) mod 256) with (N mod 256).
+  auto.
+  symmetry. apply Zmod_small. apply Z_mod_lt. omega.
+  assert (0 <= N mod 256 < 256). apply Z_mod_lt. omega.
+  assert (256 < max_unsigned). compute; auto.
+  omega.
+Qed.
+
+Theorem cast8_unsigned_signed:
+  forall n, cast8unsigned (cast8signed n) = cast8unsigned n.
+Proof.
+  intros; unfold cast8signed, cast8unsigned.
+  set (N := unsigned n mod 256).
+  assert (0 <= N < 256). unfold N; apply Z_mod_lt. omega.
+  assert (N mod 256 = N). apply Zmod_small. auto.
+  assert (256 <= max_unsigned). compute; congruence.
+  decEq. 
+  case (zlt N 128); intro.
+  rewrite unsigned_repr. auto. omega.
+  transitivity (N mod 256); auto. 
+  apply eqmod_mod_eq. omega. 
+  apply eqmod_trans with (N - 256). apply eqmod_sym. apply eqmod_256_unsigned_repr.
+  assert (eqmod 256 (N - 256) (N - 0)).
+    apply eqmod_sub. apply eqmod_refl. 
+    red. exists 1; reflexivity.
+  replace (N - 0) with N in H2. auto. omega.
+Qed.
+
+Theorem cast16_unsigned_signed:
+  forall n, cast16unsigned (cast16signed n) = cast16unsigned n.
+Proof.
+  intros; unfold cast16signed, cast16unsigned.
+  set (N := unsigned n mod 65536).
+  assert (0 <= N < 65536). unfold N; apply Z_mod_lt. omega.
+  assert (N mod 65536 = N). apply Zmod_small. auto.
+  assert (65536 <= max_unsigned). compute; congruence.
+  decEq. 
+  case (zlt N 32768); intro.
+  rewrite unsigned_repr. auto. omega.
+  transitivity (N mod 65536); auto. 
+  apply eqmod_mod_eq. omega. 
+  apply eqmod_trans with (N - 65536). apply eqmod_sym. apply eqmod_65536_unsigned_repr.
+  assert (eqmod 65536 (N - 65536) (N - 0)).
+    apply eqmod_sub. apply eqmod_refl. 
+    red. exists 1; reflexivity.
+  replace (N - 0) with N in H2. auto. omega.
+Qed.
+
+Theorem cast8_unsigned_idem:
+  forall n, cast8unsigned (cast8unsigned n) = cast8unsigned n.
+Proof.
+  intros. repeat rewrite cast8unsigned_and. 
+  rewrite and_assoc. reflexivity. 
+Qed.
+
+Theorem cast16_unsigned_idem:
+  forall n, cast16unsigned (cast16unsigned n) = cast16unsigned n.
+Proof.
+  intros. repeat rewrite cast16unsigned_and. 
+  rewrite and_assoc. reflexivity. 
+Qed.
+
+Theorem cast8_signed_idem:
+  forall n, cast8signed (cast8signed n) = cast8signed n.
+Proof.
+  intros; unfold cast8signed.
+  set (N := unsigned n mod 256).
+  assert (256 < max_unsigned). compute; auto.
+  assert (0 <= N < 256). unfold N. apply Z_mod_lt. omega. 
+  case (zlt N 128); intro.
+  assert (unsigned (repr N) = N).
+    apply unsigned_repr. omega.
+  rewrite H1.
+  replace (N mod 256) with N. apply zlt_true. auto.
+  symmetry. apply Zmod_small. auto.
+  set (M := (unsigned (repr (N - 256)) mod 256)).
+  assert (M = N).
+    unfold M, N. apply eqmod_mod_eq. omega. 
+    apply eqmod_trans with (unsigned n mod 256 - 256).
+    apply eqmod_sym. apply eqmod_256_unsigned_repr. 
+    apply eqmod_trans with (unsigned n - 0).
+    apply eqmod_sub. 
+    apply eqmod_sym. apply eqmod_mod. omega.
+    unfold eqmod. exists 1; omega.
+    apply eqmod_refl2. omega.
+  rewrite H1. rewrite zlt_false; auto.
+Qed.
+
+Theorem cast16_signed_idem:
+  forall n, cast16signed (cast16signed n) = cast16signed n.
+Proof.
+  intros; unfold cast16signed.
+  set (N := unsigned n mod 65536).
+  assert (65536 < max_unsigned). compute; auto.
+  assert (0 <= N < 65536). unfold N. apply Z_mod_lt. omega. 
+  case (zlt N 32768); intro.
+  assert (unsigned (repr N) = N).
+    apply unsigned_repr. omega.
+  rewrite H1.
+  replace (N mod 65536) with N. apply zlt_true. auto.
+  symmetry. apply Zmod_small. auto.
+  set (M := (unsigned (repr (N - 65536)) mod 65536)).
+  assert (M = N).
+    unfold M, N. apply eqmod_mod_eq. omega. 
+    apply eqmod_trans with (unsigned n mod 65536 - 65536).
+    apply eqmod_sym. apply eqmod_65536_unsigned_repr. 
+    apply eqmod_trans with (unsigned n - 0).
+    apply eqmod_sub. 
+    apply eqmod_sym. apply eqmod_mod. omega.
+    unfold eqmod. exists 1; omega.
+    apply eqmod_refl2. omega.
+  rewrite H1. rewrite zlt_false; auto.
+Qed.
+
+Theorem cast8_signed_equal_if_unsigned_equal:
+  forall x y, 
+  cast8unsigned x = cast8unsigned y ->
+  cast8signed x = cast8signed y.
+Proof.
+  unfold cast8unsigned, cast8signed; intros until y.
+  set (x' := unsigned x mod 256).
+  set (y' := unsigned y mod 256).
+  intro. 
+  assert (eqm x' y').
+    apply eqm_trans with (unsigned (repr x')). apply eqm_unsigned_repr.
+    rewrite H. apply eqm_sym. apply eqm_unsigned_repr.
+  assert (forall z, 0 <= z mod 256 < modulus).
+    intros. 
+    assert (0 <= z mod 256 < 256). apply Z_mod_lt. omega.
+    assert (256 <= modulus). compute. congruence.
+    omega.
+  assert (x' = y').
+    apply eqm_small_eq; unfold x', y'; auto. 
+  rewrite H2. auto.
+Qed.
+
+Theorem cast16_signed_equal_if_unsigned_equal:
+  forall x y, 
+  cast16unsigned x = cast16unsigned y ->
+  cast16signed x = cast16signed y.
+Proof.
+  unfold cast16unsigned, cast16signed; intros until y.
+  set (x' := unsigned x mod 65536).
+  set (y' := unsigned y mod 65536).
+  intro. 
+  assert (eqm x' y').
+    apply eqm_trans with (unsigned (repr x')). apply eqm_unsigned_repr.
+    rewrite H. apply eqm_sym. apply eqm_unsigned_repr.
+  assert (forall z, 0 <= z mod 65536 < modulus).
+    intros. 
+    assert (0 <= z mod 65536 < 65536). apply Z_mod_lt. omega.
+    assert (65536 <= modulus). compute. congruence.
+    omega.
+  assert (x' = y').
+    apply eqm_small_eq; unfold x', y'; auto. 
+  rewrite H2. auto.
+Qed.
+
+(** ** Properties of [one_bits] (decomposition in sum of powers of two) *)
+
+Opaque Z_one_bits. (* Otherwise, next Qed blows up! *)
+
+Theorem one_bits_range:
+  forall x i, In i (one_bits x) -> ltu i (repr (Z_of_nat wordsize)) = true.
+Proof.
+  intros. unfold one_bits in H.
+  elim (list_in_map_inv _ _ _ H). intros i0 [EQ IN].
+  subst i. unfold ltu. apply zlt_true. 
+  generalize (Z_one_bits_range _ _ IN). intros.
+  assert (0 <= Z_of_nat wordsize <= max_unsigned).
+    compute. intuition congruence.
+  repeat rewrite unsigned_repr; omega.
+Qed.
+
+Fixpoint int_of_one_bits (l: list int) : int :=
+  match l with
+  | nil => zero
+  | a :: b => add (shl one a) (int_of_one_bits b)
+  end.
+
+Theorem one_bits_decomp:
+  forall x, x = int_of_one_bits (one_bits x).
+Proof.
+  intros. 
+  transitivity (repr (powerserie (Z_one_bits wordsize (unsigned x) 0))).
+  transitivity (repr (unsigned x)).
+  auto with ints. decEq. apply Z_one_bits_powerserie.
+  auto with ints.
+  unfold one_bits. 
+  generalize (Z_one_bits_range (unsigned x)).
+  generalize (Z_one_bits wordsize (unsigned x) 0).
+  induction l.
+  intros; reflexivity.
+  intros; simpl. rewrite <- IHl. unfold add. apply eqm_samerepr.
+  apply eqm_add. rewrite shl_mul_two_p. rewrite mul_commut. 
+  rewrite mul_one. apply eqm_unsigned_repr_r. 
+  rewrite unsigned_repr. auto with ints.
+  generalize (H a (in_eq _ _)). 
+  assert (Z_of_nat wordsize < max_unsigned). compute; auto. omega.
+  auto with ints.
+  intros; apply H; auto with coqlib.
+Qed.
+
+(** ** Properties of comparisons *)
+
+Theorem negate_cmp:
+  forall c x y, cmp (negate_comparison c) x y = negb (cmp c x y).
+Proof.
+  intros. destruct c; simpl; try rewrite negb_elim; auto.
+Qed.
+
+Theorem negate_cmpu:
+  forall c x y, cmpu (negate_comparison c) x y = negb (cmpu c x y).
+Proof.
+  intros. destruct c; simpl; try rewrite negb_elim; auto.
+Qed.
+
+Theorem swap_cmp:
+  forall c x y, cmp (swap_comparison c) x y = cmp c y x.
+Proof.
+  intros. destruct c; simpl; auto. apply eq_sym. decEq. apply eq_sym.
+Qed.
+
+Theorem swap_cmpu:
+  forall c x y, cmpu (swap_comparison c) x y = cmpu c y x.
+Proof.
+  intros. destruct c; simpl; auto. apply eq_sym. decEq. apply eq_sym.
+Qed.
+
+Lemma translate_eq:
+  forall x y d,
+  eq (add x d) (add y d) = eq x y.
+Proof.
+  intros. unfold eq. case (zeq (unsigned x) (unsigned y)); intro.
+  unfold add. rewrite e. apply zeq_true.
+  apply zeq_false. unfold add. red; intro. apply n. 
+  apply eqm_small_eq; auto with ints.
+  replace (unsigned x) with ((unsigned x + unsigned d) - unsigned d).
+  replace (unsigned y) with ((unsigned y + unsigned d) - unsigned d).
+  apply eqm_sub. apply eqm_trans with (unsigned (repr (unsigned x + unsigned d))).
+  eauto with ints. apply eqm_trans with (unsigned (repr (unsigned y + unsigned d))).
+  eauto with ints. eauto with ints. eauto with ints.
+  omega. omega.
+Qed.
+
+Lemma translate_lt:
+  forall x y d,
+  min_signed <= signed x + signed d <= max_signed ->
+  min_signed <= signed y + signed d <= max_signed ->
+  lt (add x d) (add y d) = lt x y.
+Proof.
+  intros. repeat rewrite add_signed. unfold lt.
+  repeat rewrite signed_repr; auto. case (zlt (signed x) (signed y)); intro.
+  apply zlt_true. omega.
+  apply zlt_false. omega.
+Qed.
+
+Theorem translate_cmp:
+  forall c x y d,
+  min_signed <= signed x + signed d <= max_signed ->
+  min_signed <= signed y + signed d <= max_signed ->
+  cmp c (add x d) (add y d) = cmp c x y.
+Proof.
+  intros. unfold cmp.
+  rewrite translate_eq. repeat rewrite translate_lt; auto.
+Qed.  
+
+Theorem notbool_isfalse_istrue:
+  forall x, is_false x -> is_true (notbool x).
+Proof.
+  unfold is_false, is_true, notbool; intros; subst x. 
+  simpl. discriminate.
+Qed.
+
+Theorem notbool_istrue_isfalse:
+  forall x, is_true x -> is_false (notbool x).
+Proof.
+  unfold is_false, is_true, notbool; intros.
+  generalize (eq_spec x zero). case (eq x zero); intro.
+  contradiction. auto.
+Qed.
+
+End Int.
diff --git a/lib/Lattice.v b/lib/Lattice.v
new file mode 100644
index 00000000..7adcffba
--- /dev/null
+++ b/lib/Lattice.v
@@ -0,0 +1,331 @@
+(** Constructions of semi-lattices. *)
+
+Require Import Coqlib.
+Require Import Maps.
+
+(** * Signatures of semi-lattices *)
+
+(** A semi-lattice is a type [t] equipped with a decidable equality [eq],
+  a partial order [ge], a smallest element [bot], and an upper
+  bound operation [lub].  Note that we do not demand that [lub] computes
+  the least upper bound. *)
+
+Module Type SEMILATTICE.
+
+  Variable t: Set.
+  Variable eq: forall (x y: t), {x=y} + {x<>y}.
+  Variable ge: t -> t -> Prop.
+  Hypothesis ge_refl: forall x, ge x x.
+  Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+  Variable bot: t.
+  Hypothesis ge_bot: forall x, ge x bot.
+  Variable lub: t -> t -> t.
+  Hypothesis lub_commut: forall x y, lub x y = lub y x.
+  Hypothesis ge_lub_left: forall x y, ge (lub x y) x.
+
+End SEMILATTICE.
+
+(** A semi-lattice ``with top'' is similar, but also has a greatest
+  element [top]. *)
+
+Module Type SEMILATTICE_WITH_TOP.
+
+  Variable t: Set.
+  Variable eq: forall (x y: t), {x=y} + {x<>y}.
+  Variable ge: t -> t -> Prop.
+  Hypothesis ge_refl: forall x, ge x x.
+  Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+  Variable bot: t.
+  Hypothesis ge_bot: forall x, ge x bot.
+  Variable top: t.
+  Hypothesis ge_top: forall x, ge top x.
+  Variable lub: t -> t -> t.
+  Hypothesis lub_commut: forall x y, lub x y = lub y x.
+  Hypothesis ge_lub_left: forall x y, ge (lub x y) x.
+
+End SEMILATTICE_WITH_TOP.
+
+(** * Semi-lattice over maps *)
+
+(** Given a semi-lattice with top [L], the following functor implements
+  a semi-lattice structure over finite maps from positive numbers to [L.t].
+  The default value for these maps is either [L.top] or [L.bot]. *)
+
+Module LPMap(L: SEMILATTICE_WITH_TOP) <: SEMILATTICE_WITH_TOP.
+
+Inductive t_ : Set :=
+  | Bot_except: PTree.t L.t -> t_
+  | Top_except: PTree.t L.t -> t_.
+
+Definition t: Set := t_.
+
+Lemma eq: forall (x y: t), {x=y} + {x<>y}.
+Proof.
+  assert (forall m1 m2: PTree.t L.t, {m1=m2} + {m1<>m2}).
+  apply PTree.eq. exact L.eq.
+  decide equality.
+Qed.
+
+Definition get (p: positive) (x: t) : L.t :=
+  match x with
+  | Bot_except m =>
+      match m!p with None => L.bot | Some x => x end
+  | Top_except m =>
+      match m!p with None => L.top | Some x => x end
+  end.
+
+Definition set (p: positive) (v: L.t) (x: t) : t :=
+  match x with
+  | Bot_except m =>
+      Bot_except (PTree.set p v m)
+  | Top_except m =>
+      Top_except (PTree.set p v m)
+  end.
+
+Lemma gss:
+  forall p v x,
+  get p (set p v x) = v.
+Proof.
+  intros. destruct x; simpl; rewrite PTree.gss; auto.
+Qed.
+
+Lemma gso:
+  forall p q v x,
+  p <> q -> get p (set q v x) = get p x.
+Proof.
+  intros. destruct x; simpl; rewrite PTree.gso; auto.
+Qed.
+
+Definition ge (x y: t) : Prop :=
+  forall p, L.ge (get p x) (get p y).
+
+Lemma ge_refl: forall x, ge x x.
+Proof.
+  unfold ge; intros. apply L.ge_refl.
+Qed.
+
+Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+Proof.
+  unfold ge; intros. apply L.ge_trans with (get p y); auto.
+Qed.
+
+Definition bot := Bot_except (PTree.empty L.t).
+
+Lemma get_bot: forall p, get p bot = L.bot.
+Proof.
+  unfold bot; intros; simpl. rewrite PTree.gempty. auto.
+Qed.
+
+Lemma ge_bot: forall x, ge x bot.
+Proof.
+  unfold ge; intros. rewrite get_bot. apply L.ge_bot.
+Qed.
+
+Definition top := Top_except (PTree.empty L.t).
+
+Lemma get_top: forall p, get p top = L.top.
+Proof.
+  unfold top; intros; simpl. rewrite PTree.gempty. auto.
+Qed.
+
+Lemma ge_top: forall x, ge top x.
+Proof.
+  unfold ge; intros. rewrite get_top. apply L.ge_top.
+Qed.
+
+Definition lub (x y: t) : t :=
+  match x, y with
+  | Bot_except m, Bot_except n =>
+      Bot_except
+        (PTree.combine 
+           (fun a b =>
+              match a, b with
+              | Some u, Some v => Some (L.lub u v)
+              | None, _ => b
+              | _, None => a
+              end)
+           m n)
+  | Bot_except m, Top_except n =>
+      Top_except
+        (PTree.combine
+           (fun a b =>
+              match a, b with
+              | Some u, Some v => Some (L.lub u v)
+              | None, _ => b
+              | _, None => None
+              end)
+        m n)             
+  | Top_except m, Bot_except n =>
+      Top_except
+        (PTree.combine
+           (fun a b =>
+              match a, b with
+              | Some u, Some v => Some (L.lub u v)
+              | None, _ => None
+              | _, None => a
+              end)
+        m n)             
+  | Top_except m, Top_except n =>
+      Top_except
+        (PTree.combine 
+           (fun a b =>
+              match a, b with
+              | Some u, Some v => Some (L.lub u v)
+              | _, _ => None
+              end)
+           m n)
+  end.
+
+Lemma lub_commut:
+  forall x y, lub x y = lub y x.
+Proof.
+  destruct x; destruct y; unfold lub; decEq; 
+  apply PTree.combine_commut; intros;
+  (destruct i; destruct j; auto; decEq; apply L.lub_commut).
+Qed.
+
+Lemma ge_lub_left:
+  forall x y, ge (lub x y) x.
+Proof.
+  unfold ge, get, lub; intros; destruct x; destruct y.
+
+  rewrite PTree.gcombine. 
+  destruct t0!p. destruct t1!p. apply L.ge_lub_left.
+  apply L.ge_refl. destruct t1!p. apply L.ge_bot. apply L.ge_refl.
+  auto.
+
+  rewrite PTree.gcombine. 
+  destruct t0!p. destruct t1!p. apply L.ge_lub_left.
+  apply L.ge_top. destruct t1!p. apply L.ge_bot. apply L.ge_bot.
+  auto.
+
+  rewrite PTree.gcombine. 
+  destruct t0!p. destruct t1!p. apply L.ge_lub_left.
+  apply L.ge_refl. apply L.ge_refl. auto.
+
+  rewrite PTree.gcombine. 
+  destruct t0!p. destruct t1!p. apply L.ge_lub_left.
+  apply L.ge_top. apply L.ge_refl.
+  auto.
+Qed.
+
+End LPMap.
+
+(** * Flat semi-lattice *)
+
+(** Given a type with decidable equality [X], the following functor
+  returns a semi-lattice structure over [X.t] complemented with
+  a top and a bottom element.  The ordering is the flat ordering
+  [Bot < Inj x < Top]. *) 
+
+Module LFlat(X: EQUALITY_TYPE) <: SEMILATTICE_WITH_TOP.
+
+Inductive t_ : Set :=
+  | Bot: t_
+  | Inj: X.t -> t_
+  | Top: t_.
+
+Definition t : Set := t_.
+
+Lemma eq: forall (x y: t), {x=y} + {x<>y}.
+Proof.
+  decide equality. apply X.eq.
+Qed.
+
+Definition ge (x y: t) : Prop :=
+  match x, y with
+  | Top, _ => True
+  | _, Bot => True
+  | Inj a, Inj b => a = b
+  | _, _ => False
+  end.
+
+Lemma ge_refl: forall x, ge x x.
+Proof.
+  unfold ge; destruct x; auto.
+Qed.
+
+Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+Proof.
+  unfold ge; destruct x; destruct y; try destruct z; intuition.
+  transitivity t1; auto.
+Qed.
+
+Definition bot: t := Bot.
+
+Lemma ge_bot: forall x, ge x bot.
+Proof.
+  destruct x; simpl; auto.
+Qed.
+
+Definition top: t := Top.
+
+Lemma ge_top: forall x, ge top x.
+Proof.
+  destruct x; simpl; auto.
+Qed.
+
+Definition lub (x y: t) : t :=
+  match x, y with
+  | Bot, _ => y
+  | _, Bot => x
+  | Top, _ => Top
+  | _, Top => Top
+  | Inj a, Inj b => if X.eq a b then Inj a else Top
+  end.
+
+Lemma lub_commut: forall x y, lub x y = lub y x.
+Proof.
+  destruct x; destruct y; simpl; auto.
+  case (X.eq t0 t1); case (X.eq t1 t0); intros; congruence.
+Qed.
+
+Lemma ge_lub_left: forall x y, ge (lub x y) x.
+Proof.
+  destruct x; destruct y; simpl; auto.
+  case (X.eq t0 t1); simpl; auto.
+Qed.
+
+End LFlat.
+  
+(** * Boolean semi-lattice *)
+
+(** This semi-lattice has only two elements, [bot] and [top], trivially
+  ordered. *)
+
+Module LBoolean <: SEMILATTICE_WITH_TOP.
+
+Definition t := bool.
+
+Lemma eq: forall (x y: t), {x=y} + {x<>y}.
+Proof. decide equality. Qed.
+
+Definition ge (x y: t) : Prop := x = y \/ x = true.
+
+Lemma ge_refl: forall x, ge x x.
+Proof. unfold ge; tauto. Qed.
+
+Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+Proof. unfold ge; intuition congruence. Qed.
+
+Definition bot := false.
+
+Lemma ge_bot: forall x, ge x bot.
+Proof. destruct x; compute; tauto. Qed.
+
+Definition top := true.
+
+Lemma ge_top: forall x, ge top x.
+Proof. unfold ge, top; tauto. Qed.
+
+Definition lub (x y: t) := x || y.
+
+Lemma lub_commut: forall x y, lub x y = lub y x.
+Proof. intros; unfold lub. apply orb_comm. Qed.
+
+Lemma ge_lub_left: forall x y, ge (lub x y) x.
+Proof. destruct x; destruct y; compute; tauto. Qed.
+
+End LBoolean.
+
+
diff --git a/lib/Maps.v b/lib/Maps.v
new file mode 100644
index 00000000..69690918
--- /dev/null
+++ b/lib/Maps.v
@@ -0,0 +1,1034 @@
+(** Applicative finite maps are the main data structure used in this
+  project.  A finite map associates data to keys.  The two main operations
+  are [set k d m], which returns a map identical to [m] except that [d]
+  is associated to [k], and [get k m] which returns the data associated
+  to key [k] in map [m].  In this library, we distinguish two kinds of maps:
+- Trees: the [get] operation returns an option type, either [None]
+  if no data is associated to the key, or [Some d] otherwise.
+- Maps: the [get] operation always returns a data.  If no data was explicitly
+  associated with the key, a default data provided at map initialization time
+  is returned.
+
+  In this library, we provide efficient implementations of trees and
+  maps whose keys range over the type [positive] of binary positive
+  integers or any type that can be injected into [positive].  The
+  implementation is based on radix-2 search trees (uncompressed
+  Patricia trees) and guarantees logarithmic-time operations.  An
+  inefficient implementation of maps as functions is also provided.
+*)
+
+Require Import Coqlib.
+
+Set Implicit Arguments.
+
+(** * The abstract signatures of trees *)
+
+Module Type TREE.
+  Variable elt: Set.
+  Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}.
+  Variable t: Set -> Set.
+  Variable eq: forall (A: Set), (forall (x y: A), {x=y} + {x<>y}) ->
+                forall (a b: t A), {a = b} + {a <> b}.
+  Variable empty: forall (A: Set), t A.
+  Variable get: forall (A: Set), elt -> t A -> option A.
+  Variable set: forall (A: Set), elt -> A -> t A -> t A.
+  Variable remove: forall (A: Set), elt -> t A -> t A.
+
+  (** The ``good variables'' properties for trees, expressing
+    commutations between [get], [set] and [remove]. *)
+  Hypothesis gempty:
+    forall (A: Set) (i: elt), get i (empty A) = None.
+  Hypothesis gss:
+    forall (A: Set) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.
+  Hypothesis gso:
+    forall (A: Set) (i j: elt) (x: A) (m: t A),
+    i <> j -> get i (set j x m) = get i m.
+  Hypothesis gsspec:
+    forall (A: Set) (i j: elt) (x: A) (m: t A),
+    get i (set j x m) = if elt_eq i j then Some x else get i m.
+  Hypothesis gsident:
+    forall (A: Set) (i: elt) (m: t A) (v: A),
+    get i m = Some v -> set i v m = m.
+  (* We could implement the following, but it's not needed for the moment.
+    Hypothesis grident:
+      forall (A: Set) (i: elt) (m: t A) (v: A),
+      get i m = None -> remove i m = m.
+  *)
+  Hypothesis grs:
+    forall (A: Set) (i: elt) (m: t A), get i (remove i m) = None.
+  Hypothesis gro:
+    forall (A: Set) (i j: elt) (m: t A),
+    i <> j -> get i (remove j m) = get i m.
+
+  (** Applying a function to all data of a tree. *)
+  Variable map:
+    forall (A B: Set), (elt -> A -> B) -> t A -> t B.
+  Hypothesis gmap:
+    forall (A B: Set) (f: elt -> A -> B) (i: elt) (m: t A),
+    get i (map f m) = option_map (f i) (get i m).
+
+  (** Applying a function pairwise to all data of two trees. *)
+  Variable combine:
+    forall (A: Set), (option A -> option A -> option A) -> t A -> t A -> t A.
+  Hypothesis gcombine:
+    forall (A: Set) (f: option A -> option A -> option A)
+           (m1 m2: t A) (i: elt),
+    f None None = None ->
+    get i (combine f m1 m2) = f (get i m1) (get i m2).
+  Hypothesis combine_commut:
+    forall (A: Set) (f g: option A -> option A -> option A),
+    (forall (i j: option A), f i j = g j i) ->
+    forall (m1 m2: t A),
+    combine f m1 m2 = combine g m2 m1.
+
+  (** Enumerating the bindings of a tree. *)
+  Variable elements:
+    forall (A: Set), t A -> list (elt * A).
+  Hypothesis elements_correct:
+    forall (A: Set) (m: t A) (i: elt) (v: A),
+    get i m = Some v -> In (i, v) (elements m).
+  Hypothesis elements_complete:
+    forall (A: Set) (m: t A) (i: elt) (v: A),
+    In (i, v) (elements m) -> get i m = Some v.
+  Hypothesis elements_keys_norepet:
+    forall (A: Set) (m: t A), 
+    list_norepet (List.map (@fst elt A) (elements m)).
+
+  (** Folding a function over all bindings of a tree. *)
+  Variable fold:
+    forall (A B: Set), (B -> elt -> A -> B) -> t A -> B -> B.
+  Hypothesis fold_spec:
+    forall (A B: Set) (f: B -> elt -> A -> B) (v: B) (m: t A),
+    fold f m v =
+    List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v.
+End TREE.
+
+(** * The abstract signatures of maps *)
+
+Module Type MAP.
+  Variable elt: Set.
+  Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}.
+  Variable t: Set -> Set.
+  Variable init: forall (A: Set), A -> t A.
+  Variable get: forall (A: Set), elt -> t A -> A.
+  Variable set: forall (A: Set), elt -> A -> t A -> t A.
+  Hypothesis gi:
+    forall (A: Set) (i: elt) (x: A), get i (init x) = x.
+  Hypothesis gss:
+    forall (A: Set) (i: elt) (x: A) (m: t A), get i (set i x m) = x.
+  Hypothesis gso:
+    forall (A: Set) (i j: elt) (x: A) (m: t A),
+    i <> j -> get i (set j x m) = get i m.
+  Hypothesis gsspec:
+    forall (A: Set) (i j: elt) (x: A) (m: t A),
+    get i (set j x m) = if elt_eq i j then x else get i m.
+  Hypothesis gsident:
+    forall (A: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
+  Variable map: forall (A B: Set), (A -> B) -> t A -> t B.
+  Hypothesis gmap:
+    forall (A B: Set) (f: A -> B) (i: elt) (m: t A),
+    get i (map f m) = f(get i m).
+End MAP.
+
+(** * An implementation of trees over type [positive] *)
+
+Module PTree <: TREE.
+  Definition elt := positive.
+  Definition elt_eq := peq.
+
+  Inductive tree (A : Set) : Set :=
+    | Leaf : tree A
+    | Node : tree A -> option A -> tree A -> tree A
+  .
+  Implicit Arguments Leaf [A].
+  Implicit Arguments Node [A].
+
+  Definition t := tree.
+
+  Theorem eq : forall (A : Set),
+    (forall (x y: A), {x=y} + {x<>y}) ->
+    forall (a b : t A), {a = b} + {a <> b}.
+  Proof.
+    intros A eqA.
+    decide equality.
+    generalize o o0; decide equality.
+  Qed.
+
+  Definition empty (A : Set) := (Leaf : t A).
+
+  Fixpoint get (A : Set) (i : positive) (m : t A) {struct i} : option A :=
+    match m with
+    | Leaf => None
+    | Node l o r =>
+        match i with
+        | xH => o
+        | xO ii => get ii l
+        | xI ii => get ii r
+        end
+    end.
+
+  Fixpoint set (A : Set) (i : positive) (v : A) (m : t A) {struct i} : t A :=
+    match m with
+    | Leaf =>
+        match i with
+        | xH => Node Leaf (Some v) Leaf
+        | xO ii => Node (set ii v Leaf) None Leaf
+        | xI ii => Node Leaf None (set ii v Leaf)
+        end
+    | Node l o r =>
+        match i with
+        | xH => Node l (Some v) r
+        | xO ii => Node (set ii v l) o r
+        | xI ii => Node l o (set ii v r)
+        end
+    end.
+
+  Fixpoint remove (A : Set) (i : positive) (m : t A) {struct i} : t A :=
+    match i with
+    | xH =>
+        match m with
+        | Leaf => Leaf
+        | Node Leaf o Leaf => Leaf
+        | Node l o r => Node l None r
+        end
+    | xO ii =>
+        match m with
+        | Leaf => Leaf
+        | Node l None Leaf =>
+            match remove ii l with
+            | Leaf => Leaf
+            | mm => Node mm None Leaf
+            end
+        | Node l o r => Node (remove ii l) o r
+        end
+    | xI ii =>
+        match m with
+        | Leaf => Leaf
+        | Node Leaf None r =>
+            match remove ii r with
+            | Leaf => Leaf
+            | mm => Node Leaf None mm
+            end
+        | Node l o r => Node l o (remove ii r)
+        end
+    end.
+
+  Theorem gempty:
+    forall (A: Set) (i: positive), get i (empty A) = None.
+  Proof.
+    induction i; simpl; auto.
+  Qed.
+
+  Theorem gss:
+    forall (A: Set) (i: positive) (x: A) (m: t A), get i (set i x m) = Some x.
+  Proof.
+    induction i; destruct m; simpl; auto.
+  Qed.
+
+    Lemma gleaf : forall (A : Set) (i : positive), get i (Leaf : t A) = None.
+    Proof. exact gempty. Qed.
+
+  Theorem gso:
+    forall (A: Set) (i j: positive) (x: A) (m: t A),
+    i <> j -> get i (set j x m) = get i m.
+  Proof.
+    induction i; intros; destruct j; destruct m; simpl;
+       try rewrite <- (gleaf A i); auto; try apply IHi; congruence.
+  Qed.
+
+  Theorem gsspec:
+    forall (A: Set) (i j: positive) (x: A) (m: t A),
+    get i (set j x m) = if peq i j then Some x else get i m.
+  Proof.
+    intros.
+    destruct (peq i j); [ rewrite e; apply gss | apply gso; auto ].
+  Qed.
+
+  Theorem gsident:
+    forall (A: Set) (i: positive) (m: t A) (v: A),
+    get i m = Some v -> set i v m = m.
+  Proof.
+    induction i; intros; destruct m; simpl; simpl in H; try congruence.
+     rewrite (IHi m2 v H); congruence.
+     rewrite (IHi m1 v H); congruence.
+  Qed.
+
+    Lemma rleaf : forall (A : Set) (i : positive), remove i (Leaf : t A) = Leaf.
+    Proof. destruct i; simpl; auto. Qed.
+
+  Theorem grs:
+    forall (A: Set) (i: positive) (m: t A), get i (remove i m) = None.
+  Proof.
+    induction i; destruct m.
+     simpl; auto.
+     destruct m1; destruct o; destruct m2 as [ | ll oo rr]; simpl; auto.
+      rewrite (rleaf A i); auto.
+      cut (get i (remove i (Node ll oo rr)) = None).
+        destruct (remove i (Node ll oo rr)); auto; apply IHi.
+        apply IHi.
+     simpl; auto.
+     destruct m1 as [ | ll oo rr]; destruct o; destruct m2; simpl; auto.
+      rewrite (rleaf A i); auto.
+      cut (get i (remove i (Node ll oo rr)) = None).
+        destruct (remove i (Node ll oo rr)); auto; apply IHi.
+        apply IHi.
+     simpl; auto.
+     destruct m1; destruct m2; simpl; auto.
+  Qed.
+
+  Theorem gro:
+    forall (A: Set) (i j: positive) (m: t A),
+    i <> j -> get i (remove j m) = get i m.
+  Proof.
+    induction i; intros; destruct j; destruct m;
+        try rewrite (rleaf A (xI j));
+        try rewrite (rleaf A (xO j));
+        try rewrite (rleaf A 1); auto;
+        destruct m1; destruct o; destruct m2;
+        simpl;
+        try apply IHi; try congruence;
+        try rewrite (rleaf A j); auto;
+        try rewrite (gleaf A i); auto.
+     cut (get i (remove j (Node m2_1 o m2_2)) = get i (Node m2_1 o m2_2));
+        [ destruct (remove j (Node m2_1 o m2_2)); try rewrite (gleaf A i); auto
+        | apply IHi; congruence ].
+     destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf A i);
+        auto.
+     destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf A i);
+        auto.
+     cut (get i (remove j (Node m1_1 o0 m1_2)) = get i (Node m1_1 o0 m1_2));
+        [ destruct (remove j (Node m1_1 o0 m1_2)); try rewrite (gleaf A i); auto
+        | apply IHi; congruence ].
+     destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf A i);
+        auto.
+     destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf A i);
+        auto.
+  Qed.
+
+    Fixpoint append (i j : positive) {struct i} : positive :=
+      match i with
+      | xH => j
+      | xI ii => xI (append ii j)
+      | xO ii => xO (append ii j)
+      end.
+
+    Lemma append_assoc_0 : forall (i j : positive),
+                           append i (xO j) = append (append i (xO xH)) j.
+    Proof.
+      induction i; intros; destruct j; simpl;
+      try rewrite (IHi (xI j));
+      try rewrite (IHi (xO j));
+      try rewrite <- (IHi xH);
+      auto.
+    Qed.
+
+    Lemma append_assoc_1 : forall (i j : positive),
+                           append i (xI j) = append (append i (xI xH)) j.
+    Proof.
+      induction i; intros; destruct j; simpl;
+      try rewrite (IHi (xI j));
+      try rewrite (IHi (xO j));
+      try rewrite <- (IHi xH);
+      auto.
+    Qed.
+
+    Lemma append_neutral_r : forall (i : positive), append i xH = i.
+    Proof.
+      induction i; simpl; congruence.
+    Qed.
+
+    Lemma append_neutral_l : forall (i : positive), append xH i = i.
+    Proof.
+      simpl; auto.
+    Qed.
+
+    Fixpoint xmap (A B : Set) (f : positive -> A -> B) (m : t A) (i : positive)
+             {struct m} : t B :=
+      match m with
+      | Leaf => Leaf
+      | Node l o r => Node (xmap f l (append i (xO xH)))
+                           (option_map (f i) o)
+                           (xmap f r (append i (xI xH)))
+      end.
+
+  Definition map (A B : Set) (f : positive -> A -> B) m := xmap f m xH.
+
+    Lemma xgmap:
+      forall (A B: Set) (f: positive -> A -> B) (i j : positive) (m: t A),
+      get i (xmap f m j) = option_map (f (append j i)) (get i m).
+    Proof.
+      induction i; intros; destruct m; simpl; auto.
+      rewrite (append_assoc_1 j i); apply IHi.
+      rewrite (append_assoc_0 j i); apply IHi.
+      rewrite (append_neutral_r j); auto.
+    Qed.
+
+  Theorem gmap:
+    forall (A B: Set) (f: positive -> A -> B) (i: positive) (m: t A),
+    get i (map f m) = option_map (f i) (get i m).
+  Proof.
+    intros.
+    unfold map.
+    replace (f i) with (f (append xH i)).
+    apply xgmap.
+    rewrite append_neutral_l; auto.
+  Qed.
+
+    Fixpoint xcombine_l (A : Set) (f : option A -> option A -> option A)
+                       (m : t A) {struct m} : t A :=
+      match m with
+      | Leaf => Leaf
+      | Node l o r => Node (xcombine_l f l) (f o None) (xcombine_l f r)
+      end.
+
+    Lemma xgcombine_l :
+          forall (A : Set) (f : option A -> option A -> option A)
+                 (i : positive) (m : t A),
+          f None None = None -> get i (xcombine_l f m) = f (get i m) None.
+    Proof.
+      induction i; intros; destruct m; simpl; auto.
+    Qed.
+
+    Fixpoint xcombine_r (A : Set) (f : option A -> option A -> option A)
+                       (m : t A) {struct m} : t A :=
+      match m with
+      | Leaf => Leaf
+      | Node l o r => Node (xcombine_r f l) (f None o) (xcombine_r f r)
+      end.
+
+    Lemma xgcombine_r :
+          forall (A : Set) (f : option A -> option A -> option A)
+                 (i : positive) (m : t A),
+          f None None = None -> get i (xcombine_r f m) = f None (get i m).
+    Proof.
+      induction i; intros; destruct m; simpl; auto.
+    Qed.
+
+  Fixpoint combine (A : Set) (f : option A -> option A -> option A)
+                   (m1 m2 : t A) {struct m1} : t A :=
+    match m1 with
+    | Leaf => xcombine_r f m2
+    | Node l1 o1 r1 =>
+        match m2 with
+        | Leaf => xcombine_l f m1
+        | Node l2 o2 r2 => Node (combine f l1 l2) (f o1 o2) (combine f r1 r2)
+        end
+    end.
+
+    Lemma xgcombine:
+      forall (A: Set) (f: option A -> option A -> option A) (i: positive)
+             (m1 m2: t A),
+      f None None = None ->
+      get i (combine f m1 m2) = f (get i m1) (get i m2).
+    Proof.
+      induction i; intros; destruct m1; destruct m2; simpl; auto;
+      try apply xgcombine_r; try apply xgcombine_l; auto.
+    Qed.
+
+  Theorem gcombine:
+    forall (A: Set) (f: option A -> option A -> option A)
+           (m1 m2: t A) (i: positive),
+    f None None = None ->
+    get i (combine f m1 m2) = f (get i m1) (get i m2).
+  Proof.
+    intros A f m1 m2 i H; exact (xgcombine f i m1 m2 H).
+  Qed.
+
+    Lemma xcombine_lr :
+      forall (A : Set) (f g : option A -> option A -> option A) (m : t A),
+      (forall (i j : option A), f i j = g j i) ->
+      xcombine_l f m = xcombine_r g m.
+    Proof.
+      induction m; intros; simpl; auto.
+      rewrite IHm1; auto.
+      rewrite IHm2; auto.
+      rewrite H; auto.
+    Qed.
+
+  Theorem combine_commut:
+    forall (A: Set) (f g: option A -> option A -> option A),
+    (forall (i j: option A), f i j = g j i) ->
+    forall (m1 m2: t A),
+    combine f m1 m2 = combine g m2 m1.
+  Proof.
+    intros A f g EQ1.
+    assert (EQ2: forall (i j: option A), g i j = f j i).
+      intros; auto.
+    induction m1; intros; destruct m2; simpl;
+      try rewrite EQ1;
+      repeat rewrite (xcombine_lr f g);
+      repeat rewrite (xcombine_lr g f);
+      auto.
+     rewrite IHm1_1.
+     rewrite IHm1_2.
+     auto. 
+  Qed.
+
+    Fixpoint xelements (A : Set) (m : t A) (i : positive) {struct m}
+             : list (positive * A) :=
+      match m with
+      | Leaf => nil
+      | Node l None r =>
+          (xelements l (append i (xO xH))) ++ (xelements r (append i (xI xH)))
+      | Node l (Some x) r =>
+          (xelements l (append i (xO xH)))
+          ++ ((i, x) :: xelements r (append i (xI xH)))
+      end.
+
+  (* Note: function [xelements] above is inefficient.  We should apply
+     deforestation to it, but that makes the proofs even harder. *)
+
+  Definition elements A (m : t A) := xelements m xH.
+
+    Lemma xelements_correct:
+      forall (A: Set) (m: t A) (i j : positive) (v: A),
+      get i m = Some v -> In (append j i, v) (xelements m j).
+    Proof.
+      induction m; intros.
+       rewrite (gleaf A i) in H; congruence.
+       destruct o; destruct i; simpl; simpl in H.
+        rewrite append_assoc_1; apply in_or_app; right; apply in_cons;
+          apply IHm2; auto.
+        rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto.
+        rewrite append_neutral_r; apply in_or_app; injection H;
+          intro EQ; rewrite EQ; right; apply in_eq.
+        rewrite append_assoc_1; apply in_or_app; right; apply IHm2; auto.
+        rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto.
+        congruence.
+    Qed.
+
+  Theorem elements_correct:
+    forall (A: Set) (m: t A) (i: positive) (v: A),
+    get i m = Some v -> In (i, v) (elements m).
+  Proof.
+    intros A m i v H.
+    exact (xelements_correct m i xH H).
+  Qed.
+
+    Fixpoint xget (A : Set) (i j : positive) (m : t A) {struct j} : option A :=
+      match i, j with
+      | _, xH => get i m
+      | xO ii, xO jj => xget ii jj m
+      | xI ii, xI jj => xget ii jj m
+      | _, _ => None
+      end.
+
+    Lemma xget_left :
+      forall (A : Set) (j i : positive) (m1 m2 : t A) (o : option A) (v : A),
+      xget i (append j (xO xH)) m1 = Some v -> xget i j (Node m1 o m2) = Some v.
+    Proof.
+      induction j; intros; destruct i; simpl; simpl in H; auto; try congruence.
+      destruct i; congruence.
+    Qed.
+
+    Lemma xelements_ii :
+      forall (A: Set) (m: t A) (i j : positive) (v: A),
+      In (xI i, v) (xelements m (xI j)) -> In (i, v) (xelements m j).
+    Proof.
+      induction m.
+       simpl; auto.
+       intros; destruct o; simpl; simpl in H; destruct (in_app_or _ _ _ H);
+         apply in_or_app.
+        left; apply IHm1; auto.
+        right; destruct (in_inv H0).
+         injection H1; intros EQ1 EQ2; rewrite EQ1; rewrite EQ2; apply in_eq.
+         apply in_cons; apply IHm2; auto.
+        left; apply IHm1; auto.
+        right; apply IHm2; auto.
+    Qed.
+
+    Lemma xelements_io :
+      forall (A: Set) (m: t A) (i j : positive) (v: A),
+      ~In (xI i, v) (xelements m (xO j)).
+    Proof.
+      induction m.
+       simpl; auto.
+       intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H).
+        apply (IHm1 _ _ _ H0).
+        destruct (in_inv H0).
+         congruence.
+         apply (IHm2 _ _ _ H1).
+        apply (IHm1 _ _ _ H0).
+        apply (IHm2 _ _ _ H0).
+    Qed.
+
+    Lemma xelements_oo :
+      forall (A: Set) (m: t A) (i j : positive) (v: A),
+      In (xO i, v) (xelements m (xO j)) -> In (i, v) (xelements m j).
+    Proof.
+      induction m.
+       simpl; auto.
+       intros; destruct o; simpl; simpl in H; destruct (in_app_or _ _ _ H);
+         apply in_or_app.
+        left; apply IHm1; auto.
+        right; destruct (in_inv H0).
+         injection H1; intros EQ1 EQ2; rewrite EQ1; rewrite EQ2; apply in_eq.
+         apply in_cons; apply IHm2; auto.
+        left; apply IHm1; auto.
+        right; apply IHm2; auto.
+    Qed.
+
+    Lemma xelements_oi :
+      forall (A: Set) (m: t A) (i j : positive) (v: A),
+      ~In (xO i, v) (xelements m (xI j)).
+    Proof.
+      induction m.
+       simpl; auto.
+       intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H).
+        apply (IHm1 _ _ _ H0).
+        destruct (in_inv H0).
+         congruence.
+         apply (IHm2 _ _ _ H1).
+        apply (IHm1 _ _ _ H0).
+        apply (IHm2 _ _ _ H0).
+    Qed.
+
+    Lemma xelements_ih :
+      forall (A: Set) (m1 m2: t A) (o: option A) (i : positive) (v: A),
+      In (xI i, v) (xelements (Node m1 o m2) xH) -> In (i, v) (xelements m2 xH).
+    Proof.
+      destruct o; simpl; intros; destruct (in_app_or _ _ _ H).
+        absurd (In (xI i, v) (xelements m1 2)); auto; apply xelements_io; auto.
+        destruct (in_inv H0).
+         congruence.
+         apply xelements_ii; auto.
+        absurd (In (xI i, v) (xelements m1 2)); auto; apply xelements_io; auto.
+        apply xelements_ii; auto.
+    Qed.
+
+    Lemma xelements_oh :
+      forall (A: Set) (m1 m2: t A) (o: option A) (i : positive) (v: A),
+      In (xO i, v) (xelements (Node m1 o m2) xH) -> In (i, v) (xelements m1 xH).
+    Proof.
+      destruct o; simpl; intros; destruct (in_app_or _ _ _ H).
+        apply xelements_oo; auto.
+        destruct (in_inv H0).
+         congruence.
+         absurd (In (xO i, v) (xelements m2 3)); auto; apply xelements_oi; auto.
+        apply xelements_oo; auto.
+        absurd (In (xO i, v) (xelements m2 3)); auto; apply xelements_oi; auto.
+    Qed.
+
+    Lemma xelements_hi :
+      forall (A: Set) (m: t A) (i : positive) (v: A),
+      ~In (xH, v) (xelements m (xI i)).
+    Proof.
+      induction m; intros.
+       simpl; auto.
+       destruct o; simpl; intro H; destruct (in_app_or _ _ _ H).
+        generalize H0; apply IHm1; auto.
+        destruct (in_inv H0).
+         congruence.
+         generalize H1; apply IHm2; auto.
+        generalize H0; apply IHm1; auto.
+        generalize H0; apply IHm2; auto.
+    Qed.
+
+    Lemma xelements_ho :
+      forall (A: Set) (m: t A) (i : positive) (v: A),
+      ~In (xH, v) (xelements m (xO i)).
+    Proof.
+      induction m; intros.
+       simpl; auto.
+       destruct o; simpl; intro H; destruct (in_app_or _ _ _ H).
+        generalize H0; apply IHm1; auto.
+        destruct (in_inv H0).
+         congruence.
+         generalize H1; apply IHm2; auto.
+        generalize H0; apply IHm1; auto.
+        generalize H0; apply IHm2; auto.
+    Qed.
+
+    Lemma get_xget_h :
+      forall (A: Set) (m: t A) (i: positive), get i m = xget i xH m.
+    Proof.
+      destruct i; simpl; auto.
+    Qed.
+
+    Lemma xelements_complete:
+      forall (A: Set) (i j : positive) (m: t A) (v: A),
+      In (i, v) (xelements m j) -> xget i j m = Some v.
+    Proof.
+      induction i; simpl; intros; destruct j; simpl.
+       apply IHi; apply xelements_ii; auto.
+       absurd (In (xI i, v) (xelements m (xO j))); auto; apply xelements_io.
+       destruct m.
+        simpl in H; tauto.
+        rewrite get_xget_h. apply IHi. apply (xelements_ih _ _ _ _ _ H).
+       absurd (In (xO i, v) (xelements m (xI j))); auto; apply xelements_oi.
+       apply IHi; apply xelements_oo; auto.
+       destruct m.
+        simpl in H; tauto.
+        rewrite get_xget_h. apply IHi. apply (xelements_oh _ _ _ _ _ H).
+       absurd (In (xH, v) (xelements m (xI j))); auto; apply xelements_hi.
+       absurd (In (xH, v) (xelements m (xO j))); auto; apply xelements_ho.
+       destruct m.
+        simpl in H; tauto.
+        destruct o; simpl in H; destruct (in_app_or _ _ _ H).
+         absurd (In (xH, v) (xelements m1 (xO xH))); auto; apply xelements_ho.
+         destruct (in_inv H0).
+          congruence.
+          absurd (In (xH, v) (xelements m2 (xI xH))); auto; apply xelements_hi.
+         absurd (In (xH, v) (xelements m1 (xO xH))); auto; apply xelements_ho.
+         absurd (In (xH, v) (xelements m2 (xI xH))); auto; apply xelements_hi.
+    Qed.
+
+  Theorem elements_complete:
+    forall (A: Set) (m: t A) (i: positive) (v: A),
+    In (i, v) (elements m) -> get i m = Some v.
+  Proof.
+    intros A m i v H.
+    unfold elements in H.
+    rewrite get_xget_h.
+    exact (xelements_complete i xH m v H).
+  Qed.
+
+  Lemma in_xelements:
+    forall (A: Set) (m: t A) (i k: positive) (v: A),
+    In (k, v) (xelements m i) ->
+    exists j, k = append i j.
+  Proof.
+    induction m; simpl; intros.
+    tauto.
+    assert (k = i \/ In (k, v) (xelements m1 (append i 2))
+                  \/ In (k, v) (xelements m2 (append i 3))).
+      destruct o.
+      elim (in_app_or _ _ _ H); simpl; intuition.
+      replace k with i. tauto. congruence.
+      elim (in_app_or _ _ _ H); simpl; intuition.
+    elim H0; intro.
+    exists xH. rewrite append_neutral_r. auto.
+    elim H1; intro.
+    elim (IHm1 _ _ _ H2). intros k1 EQ. rewrite EQ.
+    rewrite <- append_assoc_0. exists (xO k1); auto.
+    elim (IHm2 _ _ _ H2). intros k1 EQ. rewrite EQ.
+    rewrite <- append_assoc_1. exists (xI k1); auto.
+  Qed.
+
+  Definition xkeys (A: Set) (m: t A) (i: positive) :=
+    List.map (@fst positive A) (xelements m i).
+
+  Lemma in_xkeys:
+    forall (A: Set) (m: t A) (i k: positive),
+    In k (xkeys m i) ->
+    exists j, k = append i j.
+  Proof.
+    unfold xkeys; intros. 
+    elim (list_in_map_inv _ _ _ H). intros [k1 v1] [EQ IN].
+    simpl in EQ; subst k1. apply in_xelements with A m v1. auto.
+  Qed.
+
+  Remark list_append_cons_norepet:
+    forall (A: Set) (l1 l2: list A) (x: A),
+    list_norepet l1 -> list_norepet l2 -> list_disjoint l1 l2 ->
+    ~In x l1 -> ~In x l2 ->
+    list_norepet (l1 ++ x :: l2).
+  Proof.
+    intros. apply list_norepet_append_commut. simpl; constructor.
+    red; intros. elim (in_app_or _ _ _ H4); intro; tauto.
+    apply list_norepet_append; auto. 
+    apply list_disjoint_sym; auto.
+  Qed.
+
+  Lemma append_injective:
+    forall i j1 j2, append i j1 = append i j2 -> j1 = j2.
+  Proof.
+    induction i; simpl; intros.
+    apply IHi. congruence.
+    apply IHi. congruence.
+    auto.
+  Qed.
+
+  Lemma xelements_keys_norepet:
+    forall (A: Set) (m: t A) (i: positive),
+    list_norepet (xkeys m i).
+  Proof.
+    induction m; unfold xkeys; simpl; fold xkeys; intros.
+    constructor.
+    assert (list_disjoint (xkeys m1 (append i 2)) (xkeys m2 (append i 3))).
+      red; intros; red; intro. subst y. 
+      elim (in_xkeys _ _ _ H); intros j1 EQ1.
+      elim (in_xkeys _ _ _ H0); intros j2 EQ2.
+      rewrite EQ1 in EQ2. 
+      rewrite <- append_assoc_0 in EQ2. 
+      rewrite <- append_assoc_1 in EQ2. 
+      generalize (append_injective _ _ _ EQ2). congruence.
+    assert (forall (m: t A) j,
+            j = 2%positive \/ j = 3%positive ->
+            ~In i (xkeys m (append i j))).
+      intros; red; intros. 
+      elim (in_xkeys _ _ _ H1); intros k EQ.
+      assert (EQ1: append i xH = append (append i j) k).
+        rewrite append_neutral_r. auto.
+      elim H0; intro; subst j;
+      try (rewrite <- append_assoc_0 in EQ1);
+      try (rewrite <- append_assoc_1 in EQ1);
+      generalize (append_injective _ _ _ EQ1); congruence.
+    destruct o; rewrite list_append_map; simpl;
+    change (List.map (@fst positive A) (xelements m1 (append i 2)))
+      with (xkeys m1 (append i 2));
+    change (List.map (@fst positive A) (xelements m2 (append i 3)))
+      with (xkeys m2 (append i 3)).
+    apply list_append_cons_norepet; auto. 
+    apply list_norepet_append; auto.
+  Qed.
+
+  Theorem elements_keys_norepet:
+    forall (A: Set) (m: t A), 
+    list_norepet (List.map (@fst elt A) (elements m)).
+  Proof.
+    intros. change (list_norepet (xkeys m 1)). apply xelements_keys_norepet.
+  Qed.
+
+  Definition fold (A B : Set) (f: B -> positive -> A -> B) (tr: t A) (v: B) :=
+     List.fold_left (fun a p => f a (fst p) (snd p)) (elements tr) v.
+
+  Theorem fold_spec:
+    forall (A B: Set) (f: B -> positive -> A -> B) (v: B) (m: t A),
+    fold f m v =
+    List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v.
+  Proof.
+    intros; unfold fold; auto.
+  Qed.
+
+End PTree.
+
+(** * An implementation of maps over type [positive] *)
+
+Module PMap <: MAP.
+  Definition elt := positive.
+  Definition elt_eq := peq.
+
+  Definition t (A : Set) : Set := (A * PTree.t A)%type.
+
+  Definition init (A : Set) (x : A) :=
+    (x, PTree.empty A).
+
+  Definition get (A : Set) (i : positive) (m : t A) :=
+    match PTree.get i (snd m) with
+    | Some x => x
+    | None => fst m
+    end.
+
+  Definition set (A : Set) (i : positive) (x : A) (m : t A) :=
+    (fst m, PTree.set i x (snd m)).
+
+  Theorem gi:
+    forall (A: Set) (i: positive) (x: A), get i (init x) = x.
+  Proof.
+    intros. unfold init. unfold get. simpl. rewrite PTree.gempty. auto.
+  Qed.
+
+  Theorem gss:
+    forall (A: Set) (i: positive) (x: A) (m: t A), get i (set i x m) = x.
+  Proof.
+    intros. unfold get. unfold set. simpl. rewrite PTree.gss. auto.
+  Qed.
+
+  Theorem gso:
+    forall (A: Set) (i j: positive) (x: A) (m: t A),
+    i <> j -> get i (set j x m) = get i m.
+  Proof.
+    intros. unfold get. unfold set. simpl. rewrite PTree.gso; auto.
+  Qed.
+
+  Theorem gsspec:
+    forall (A: Set) (i j: positive) (x: A) (m: t A),
+    get i (set j x m) = if peq i j then x else get i m.
+  Proof.
+    intros. destruct (peq i j).
+     rewrite e. apply gss. auto.
+     apply gso. auto.
+  Qed.
+
+  Theorem gsident:
+    forall (A: Set) (i j: positive) (m: t A),
+    get j (set i (get i m) m) = get j m.
+  Proof.
+    intros. destruct (peq i j).
+     rewrite e. rewrite gss. auto.
+     rewrite gso; auto.
+  Qed.
+
+  Definition map (A B : Set) (f : A -> B) (m : t A) : t B :=
+    (f (fst m), PTree.map (fun _ => f) (snd m)).
+
+  Theorem gmap:
+    forall (A B: Set) (f: A -> B) (i: positive) (m: t A),
+    get i (map f m) = f(get i m).
+  Proof.
+    intros. unfold map. unfold get. simpl. rewrite PTree.gmap.
+    unfold option_map. destruct (PTree.get i (snd m)); auto.
+  Qed.
+
+End PMap.
+
+(** * An implementation of maps over any type that injects into type [positive] *)
+
+Module Type INDEXED_TYPE.
+  Variable t: Set.
+  Variable index: t -> positive.
+  Hypothesis index_inj: forall (x y: t), index x = index y -> x = y.
+  Variable eq: forall (x y: t), {x = y} + {x <> y}.
+End INDEXED_TYPE.
+
+Module IMap(X: INDEXED_TYPE).
+
+  Definition elt := X.t.
+  Definition elt_eq := X.eq.
+  Definition t : Set -> Set := PMap.t.
+  Definition init (A: Set) (x: A) := PMap.init x.
+  Definition get (A: Set) (i: X.t) (m: t A) := PMap.get (X.index i) m.
+  Definition set (A: Set) (i: X.t) (v: A) (m: t A) := PMap.set (X.index i) v m.
+  Definition map (A B: Set) (f: A -> B) (m: t A) : t B := PMap.map f m.
+
+  Lemma gi:
+    forall (A: Set) (x: A) (i: X.t), get i (init x) = x.
+  Proof.
+    intros. unfold get, init. apply PMap.gi. 
+  Qed.
+
+  Lemma gss:
+    forall (A: Set) (i: X.t) (x: A) (m: t A), get i (set i x m) = x.
+  Proof.
+    intros. unfold get, set. apply PMap.gss.
+  Qed.
+
+  Lemma gso:
+    forall (A: Set) (i j: X.t) (x: A) (m: t A),
+    i <> j -> get i (set j x m) = get i m.
+  Proof.
+    intros. unfold get, set. apply PMap.gso. 
+    red. intro. apply H. apply X.index_inj; auto. 
+  Qed.
+
+  Lemma gsspec:
+    forall (A: Set) (i j: X.t) (x: A) (m: t A),
+    get i (set j x m) = if X.eq i j then x else get i m.
+  Proof.
+    intros. unfold get, set. 
+    rewrite PMap.gsspec.
+    case (X.eq i j); intro.
+    subst j. rewrite peq_true. reflexivity.
+    rewrite peq_false. reflexivity. 
+    red; intro. elim n. apply X.index_inj; auto.
+  Qed.
+
+  Lemma gmap:
+    forall (A B: Set) (f: A -> B) (i: X.t) (m: t A),
+    get i (map f m) = f(get i m).
+  Proof.
+    intros. unfold map, get. apply PMap.gmap. 
+  Qed.
+
+End IMap.
+
+Module ZIndexed.
+  Definition t := Z.
+  Definition index (z: Z): positive :=
+    match z with
+    | Z0 => xH
+    | Zpos p => xO p
+    | Zneg p => xI p
+    end.
+  Lemma index_inj: forall (x y: Z), index x = index y -> x = y.
+  Proof.
+    unfold index; destruct x; destruct y; intros;
+    try discriminate; try reflexivity.
+    congruence.
+    congruence.
+  Qed.
+  Definition eq := zeq.
+End ZIndexed.
+
+Module ZMap := IMap(ZIndexed).
+
+Module NIndexed.
+  Definition t := N.
+  Definition index (n: N): positive :=
+    match n with
+    | N0 => xH
+    | Npos p => xO p
+    end.
+  Lemma index_inj: forall (x y: N), index x = index y -> x = y.
+  Proof.
+    unfold index; destruct x; destruct y; intros;
+    try discriminate; try reflexivity.
+    congruence.
+  Qed.
+  Lemma eq: forall (x y: N), {x = y} + {x <> y}.
+  Proof.
+    decide equality. apply peq.
+  Qed.
+End NIndexed.
+
+Module NMap := IMap(NIndexed).
+
+(** * An implementation of maps over any type with decidable equality *)
+
+Module Type EQUALITY_TYPE.
+  Variable t: Set.
+  Variable eq: forall (x y: t), {x = y} + {x <> y}.
+End EQUALITY_TYPE.
+
+Module EMap(X: EQUALITY_TYPE) <: MAP.
+
+  Definition elt := X.t.
+  Definition elt_eq := X.eq.
+  Definition t (A: Set) := X.t -> A.
+  Definition init (A: Set) (v: A) := fun (_: X.t) => v.
+  Definition get (A: Set) (x: X.t) (m: t A) := m x.
+  Definition set (A: Set) (x: X.t) (v: A) (m: t A) :=
+    fun (y: X.t) => if X.eq y x then v else m y.
+  Lemma gi:
+    forall (A: Set) (i: elt) (x: A), init x i = x.
+  Proof.
+    intros. reflexivity.
+  Qed.
+  Lemma gss:
+    forall (A: Set) (i: elt) (x: A) (m: t A), (set i x m) i = x.
+  Proof.
+    intros. unfold set. case (X.eq i i); intro.
+    reflexivity. tauto.
+  Qed.
+  Lemma gso:
+    forall (A: Set) (i j: elt) (x: A) (m: t A),
+    i <> j -> (set j x m) i = m i.
+  Proof.
+    intros. unfold set. case (X.eq i j); intro.
+    congruence. reflexivity.
+  Qed.
+  Lemma gsspec:
+    forall (A: Set) (i j: elt) (x: A) (m: t A),
+    get i (set j x m) = if elt_eq i j then x else get i m.
+  Proof.
+    intros. unfold get, set, elt_eq. reflexivity.
+  Qed.
+  Lemma gsident:
+    forall (A: Set) (i j: elt) (m: t A), get j (set i (get i m) m) = get j m.
+  Proof.
+    intros. unfold get, set. case (X.eq j i); intro.
+    congruence. reflexivity.
+  Qed.
+  Definition map (A B: Set) (f: A -> B) (m: t A) :=
+    fun (x: X.t) => f(m x).
+  Lemma gmap:
+    forall (A B: Set) (f: A -> B) (i: elt) (m: t A),
+    get i (map f m) = f(get i m).
+  Proof.
+    intros. unfold get, map. reflexivity.
+  Qed.
+  Lemma exten:
+    forall (A: Set) (m1 m2: t A),
+    (forall x: X.t, m1 x = m2 x) -> m1 = m2.
+  Proof.
+    intros. unfold t. apply extensionality. assumption.
+  Qed.
+End EMap.
+
+(** * Useful notations *)
+
+Notation "a ! b" := (PTree.get b a) (at level 1).
+Notation "a !! b" := (PMap.get b a) (at level 1).
+
+(* $Id: Maps.v,v 1.12.4.4 2006/01/07 11:46:55 xleroy Exp $ *)
diff --git a/lib/Ordered.v b/lib/Ordered.v
new file mode 100644
index 00000000..1747bbb9
--- /dev/null
+++ b/lib/Ordered.v
@@ -0,0 +1,156 @@
+(** Constructions of ordered types, for use with the [FSet] functors
+  for finite sets. *)
+
+Require Import FSet.
+Require Import Coqlib.
+Require Import Maps.
+
+(** The ordered type of positive numbers *)
+
+Module OrderedPositive <: OrderedType.
+
+Definition t := positive.
+Definition eq (x y: t) := x = y.
+Definition lt := Plt.
+
+Lemma eq_refl : forall x : t, eq x x.
+Proof (@refl_equal t). 
+Lemma eq_sym : forall x y : t, eq x y -> eq y x.
+Proof (@sym_equal t).
+Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
+Proof (@trans_equal t).
+Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+Proof Plt_trans.
+Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+Proof Plt_ne.
+Lemma compare : forall x y : t, Compare lt eq x y.
+Proof.
+  intros. case (plt x y); intro.
+  apply Lt. auto.
+  case (peq x y); intro.
+  apply Eq. auto.
+  apply Gt. red; unfold Plt in *. 
+  assert (Zpos x <> Zpos y). congruence. omega.
+Qed.
+
+End OrderedPositive.
+
+(** Indexed types (those that inject into [positive]) are ordered. *)
+
+Module OrderedIndexed(A: INDEXED_TYPE) <: OrderedType.
+
+Definition t := A.t.
+Definition eq (x y: t) := x = y.
+Definition lt (x y: t) := Plt (A.index x) (A.index y).
+
+Lemma eq_refl : forall x : t, eq x x.
+Proof (@refl_equal t). 
+Lemma eq_sym : forall x y : t, eq x y -> eq y x.
+Proof (@sym_equal t).
+Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
+Proof (@trans_equal t).
+
+Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+Proof.
+  unfold lt; intros. eapply Plt_trans; eauto.
+Qed.
+
+Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+Proof.
+  unfold lt; unfold eq; intros.
+  red; intro. subst y. apply Plt_strict with (A.index x). auto.
+Qed.
+
+Lemma compare : forall x y : t, Compare lt eq x y.
+Proof.
+  intros. case (OrderedPositive.compare (A.index x) (A.index y)); intro.
+  apply Lt. exact l. 
+  apply Eq. red; red in e. apply A.index_inj; auto.
+  apply Gt. exact l.
+Qed.
+
+End OrderedIndexed.
+
+(** The product of two ordered types is ordered. *)
+
+Module OrderedPair (A B: OrderedType) <: OrderedType.
+
+Definition t := (A.t * B.t)%type.
+
+Definition eq (x y: t) :=
+  A.eq (fst x) (fst y) /\ B.eq (snd x) (snd y).
+
+Lemma eq_refl : forall x : t, eq x x.
+Proof.
+  intros; split; auto.
+Qed.
+
+Lemma eq_sym : forall x y : t, eq x y -> eq y x.
+Proof.
+  unfold eq; intros. intuition auto.
+Qed.
+
+Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
+Proof.
+  unfold eq; intros. intuition eauto.
+Qed.
+
+Definition lt (x y: t) :=
+  A.lt (fst x) (fst y) \/
+  (A.eq (fst x) (fst y) /\ B.lt (snd x) (snd y)).
+
+Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+Proof.
+  unfold lt; intros.
+  elim H; elim H0; intros.
+
+  left. apply A.lt_trans with (fst y); auto.
+
+  left.  elim H1; intros.
+  case (A.compare (fst x) (fst z)); intro.
+  assumption.
+  generalize (A.lt_not_eq H2); intro. elim H5.
+  apply A.eq_trans with (fst z). auto. auto.
+  generalize (@A.lt_not_eq (fst z) (fst y)); intro.
+  elim H5. apply A.lt_trans with (fst x); auto.
+  apply A.eq_sym; auto.
+
+  left. elim H2; intros.
+  case (A.compare (fst x) (fst z)); intro.
+  assumption.
+  generalize (A.lt_not_eq H1); intro. elim H5.
+  apply A.eq_trans with (fst x). 
+  apply A.eq_sym. auto. auto.
+  generalize (@A.lt_not_eq (fst y) (fst x)); intro.
+  elim H5. apply A.lt_trans with (fst z); auto.
+  apply A.eq_sym; auto.
+
+  right. elim H1; elim H2; intros.
+  split. apply A.eq_trans with (fst y); auto.
+  apply B.lt_trans with (snd y); auto.
+Qed.
+
+Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+Proof.
+  unfold lt, eq, not; intros.
+  elim H0; intros.
+  elim H; intro.
+  apply (@A.lt_not_eq _ _ H3 H1).
+  elim H3; intros.
+  apply (@B.lt_not_eq _ _ H5 H2).
+Qed.
+  
+Lemma compare : forall x y : t, Compare lt eq x y.
+Proof.
+  intros.
+  case (A.compare (fst x) (fst y)); intro.
+  apply Lt. red. left. auto.
+  case (B.compare (snd x) (snd y)); intro.
+  apply Lt. red. right. tauto.
+  apply Eq. red. tauto.
+  apply Gt. red. right. split. apply A.eq_sym. auto. auto.
+  apply Gt. red. left. auto.
+Qed.
+
+End OrderedPair.
+
diff --git a/lib/Sets.v b/lib/Sets.v
new file mode 100644
index 00000000..bfc49b11
--- /dev/null
+++ b/lib/Sets.v
@@ -0,0 +1,190 @@
+(** Finite sets.  This module implements finite sets over any type
+  that is equipped with a tree (partial finite mapping) structure.
+  The set structure forms a semi-lattice, ordered by set inclusion.
+
+  It would have been better to use the [FSet] library, which provides
+  sets over any totally ordered type.  However, there are technical
+  mismatches between the [FSet] export signature and our signature for
+  semi-lattices.  For now, we keep this somewhat redundant
+  implementation of sets.
+*)
+
+Require Import Relations.
+Require Import Coqlib.
+Require Import Maps.
+Require Import Lattice.
+
+Set Implicit Arguments.
+
+Module MakeSet (P: TREE) <: SEMILATTICE.
+
+(** Sets of elements of type [P.elt] are implemented as a partial mapping
+  from [P.elt] to the one-element type [unit]. *)
+
+  Definition elt := P.elt.
+
+  Definition t := P.t unit.
+
+  Lemma eq: forall (a b: t), {a=b} + {a<>b}.
+  Proof.
+    unfold t; intros. apply P.eq. 
+    intros. left. destruct x; destruct y; auto.
+  Qed.
+
+  Definition empty := P.empty unit.
+
+  Definition mem (r: elt) (s: t) :=
+    match P.get r s with None => false | Some _ => true end.
+
+  Definition add (r: elt) (s: t) := P.set r tt s.
+
+  Definition remove (r: elt) (s: t) := P.remove r s.
+
+  Definition union (s1 s2: t) :=
+    P.combine
+      (fun e1 e2 =>
+        match e1, e2 with
+        | None, None => None
+        | _, _ => Some tt
+        end)
+      s1 s2.
+
+  Lemma mem_empty:
+    forall r, mem r empty = false.
+  Proof.
+    intro; unfold mem, empty. rewrite P.gempty. auto.
+  Qed.
+
+  Lemma mem_add_same:
+    forall r s, mem r (add r s) = true.
+  Proof.
+    intros; unfold mem, add. rewrite P.gss. auto.
+  Qed.
+
+  Lemma mem_add_other:
+    forall r r' s, r <> r' -> mem r' (add r s) = mem r' s.
+  Proof.
+    intros; unfold mem, add. rewrite P.gso; auto.
+  Qed.
+
+  Lemma mem_remove_same:
+    forall r s, mem r (remove r s) = false.
+  Proof.
+    intros; unfold mem, remove. rewrite P.grs; auto.
+  Qed.
+
+  Lemma mem_remove_other:
+    forall r r' s, r <> r' -> mem r' (remove r s) = mem r' s.
+  Proof.
+    intros; unfold mem, remove. rewrite P.gro; auto.
+  Qed.
+
+  Lemma mem_union:
+    forall r s1 s2, mem r (union s1 s2) = (mem r s1 || mem r s2).
+  Proof.
+    intros; unfold union, mem. rewrite P.gcombine. 
+    case (P.get r s1); case (P.get r s2); auto.
+    auto.
+  Qed.
+
+  Definition elements (s: t) :=
+    List.map (@fst elt unit) (P.elements s).
+
+  Lemma elements_correct:
+    forall r s, mem r s = true -> In r (elements s).
+  Proof.
+    intros until s. unfold mem, elements. caseEq (P.get r s).
+    intros. change r with (fst (r, u)). apply in_map. 
+    apply P.elements_correct. auto.
+    intros; discriminate.
+  Qed.
+    
+  Lemma elements_complete:
+    forall r s, In r (elements s) -> mem r s = true.
+  Proof.
+    unfold mem, elements. intros. 
+    generalize (list_in_map_inv _ _ _ H).
+    intros [p [EQ IN]].
+    destruct p. simpl in EQ. subst r.
+    rewrite (P.elements_complete _ _ _ IN). auto.
+  Qed.
+
+  Definition fold (A: Set) (f: A -> elt -> A) (s: t) (x: A) :=
+    P.fold (fun (x: A) (r: elt) (z: unit) => f x r) s x.
+
+  Lemma fold_spec:
+    forall (A: Set) (f: A -> elt -> A) (s: t) (x: A),
+    fold f s x = List.fold_left f (elements s) x.
+  Proof.
+    intros. unfold fold. rewrite P.fold_spec.
+    unfold elements. generalize x; generalize (P.elements s).
+    induction l; simpl; auto.
+  Qed.
+
+  Definition for_all (f: elt -> bool) (s: t) :=
+    fold (fun b x => andb b (f x)) s true.
+
+  Lemma for_all_spec:
+    forall f s x,
+    for_all f s = true -> mem x s = true -> f x = true.
+  Proof.
+    intros until x. unfold for_all. rewrite fold_spec.
+    assert (forall l b0,
+      fold_left (fun (b : bool) (x : elt) => b && f x) l b0 = true ->
+      b0 = true).
+    induction l; simpl; intros.
+    auto.
+    generalize (IHl _ H). intro.
+    elim (andb_prop _ _ H0); intros. auto.
+    assert (forall l,
+      fold_left (fun (b : bool) (x : elt) => b && f x) l true = true ->
+      In x l -> f x = true).
+    induction l; simpl; intros.
+    elim H1.
+    generalize (H _ _ H0); intro. 
+    elim H1; intros.
+    subst x. auto.
+    apply IHl. rewrite H2 in H0; auto. auto.
+    intros. eapply H0; eauto.
+    apply elements_correct. auto.
+  Qed.
+
+  Definition ge (s1 s2: t) : Prop :=
+    forall r, mem r s2 = true -> mem r s1 = true.
+
+  Lemma ge_refl: forall x, ge x x.
+  Proof.
+    unfold ge; intros. auto.
+  Qed.
+
+  Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
+  Proof.
+    unfold ge; intros. auto.
+  Qed.
+
+  Definition bot := empty.
+  Definition lub := union.
+
+  Lemma ge_bot: forall (x:t), ge x bot.
+  Proof.
+    unfold ge; intros. rewrite mem_empty in H. discriminate.
+  Qed.
+
+  Lemma lub_commut: forall (x y: t), lub x y = lub y x.
+  Proof.
+    intros. unfold lub; unfold union. apply P.combine_commut.
+    intros; case i; case j; auto.
+  Qed.
+
+  Lemma ge_lub_left: forall (x y: t), ge (lub x y) x.
+  Proof.
+    unfold ge, lub; intros. 
+    rewrite mem_union. rewrite H. reflexivity.
+  Qed.
+
+  Lemma ge_lub_right: forall (x y: t), ge (lub x y) y.
+  Proof.
+    intros. rewrite lub_commut. apply ge_lub_left.
+  Qed.
+
+End MakeSet.
diff --git a/lib/union_find.v b/lib/union_find.v
new file mode 100644
index 00000000..61817d76
--- /dev/null
+++ b/lib/union_find.v
@@ -0,0 +1,537 @@
+(** A purely functional union-find algorithm *)
+
+Require Import Wf.
+
+(** The ``union-find'' algorithm is used to represent equivalence classes
+  over a given type.  It maintains a data structure representing a partition
+  of the type into equivalence classes. Three operations are provided:
+- [empty], which returns the finest partition: each element of the type
+  is equivalent to itself only.
+- [repr part x] returns a canonical representative for the equivalence
+  class of element [x] in partition [part].  Two elements [x] and [y] 
+  are in the same equivalence class if and only if
+  [repr part x = repr part y].
+- [identify part x y] returns a new partition where the equivalence
+  classes of [x] and [y] are merged, and all equivalences valid in [part]
+  are still valid.
+
+  The partitions are represented by partial mappings from elements 
+  to elements.  If [part] maps [x] to [y], this means that [x] and [y]
+  are in the same equivalence class.  The canonical representative
+  of the class of [x] is obtained by iteratively following these mappings
+  until an element not mapped to anything is reached; this element is the
+  canonical representative, as returned by [repr].
+
+  In algorithm textbooks, the mapping is maintained imperatively by
+  storing pointers within elements.  Here, we give a purely functional
+  presentation where the mapping is a separate functional data structure.
+*)
+
+Ltac CaseEq name :=
+  generalize (refl_equal name); pattern name at -1 in |- *; case name.
+
+Ltac IntroElim :=
+  match goal with
+  |  |- (forall id : exists x : _, _, _) =>
+      intro id; elim id; clear id; IntroElim
+  |  |- (forall id : _ /\ _, _) => intro id; elim id; clear id; IntroElim
+  |  |- (forall id : _ \/ _, _) => intro id; elim id; clear id; IntroElim
+  |  |- (_ -> _) => intro; IntroElim
+  | _ => idtac
+  end.
+
+Ltac MyElim n := elim n; IntroElim.
+
+(** The elements of equivalence classes are represented by the following
+  signature: a type with a decidable equality. *)
+
+Module Type ELEMENT.
+  Variable T: Set.
+  Variable eq: forall (a b: T), {a = b} + {a <> b}.
+End ELEMENT.
+
+(** The mapping structure over elements is represented by the following
+  signature. *)
+
+Module Type MAP.
+  Variable elt: Set.
+  Variable T: Set.
+  Variable empty: T.
+  Variable get: elt -> T -> option elt.
+  Variable add: elt -> elt -> T -> T.
+
+  Hypothesis get_empty: forall (x: elt), get x empty = None.
+  Hypothesis get_add_1:
+   forall (x y: elt) (m: T), get x (add x y m) = Some y.
+  Hypothesis get_add_2:
+   forall (x y z: elt) (m: T), z <> x -> get z (add x y m) = get z m.
+End MAP.
+
+(** Our implementation of union-find is a functor, parameterized by
+  a structure for elements and a structure for maps.  It returns a
+  module with the following structure. *)
+
+Module Type UNIONFIND.
+  Variable elt: Set.
+  (** The type of partitions. *)
+  Variable T: Set.
+
+  (** The operations over partitions. *)
+  Variable empty: T.
+  Variable repr: T -> elt -> elt.
+  Variable identify: T -> elt -> elt -> T.
+
+  (** The relation implied by the partition [m]. *)
+  Definition sameclass (m: T) (x y: elt) : Prop := repr m x = repr m y.
+
+  (* [sameclass] is an equivalence relation *)
+  Hypothesis sameclass_refl:
+    forall (m: T) (x: elt), sameclass m x x.
+  Hypothesis sameclass_sym:
+    forall (m: T) (x y: elt), sameclass m x y -> sameclass m y x.
+  Hypothesis sameclass_trans:
+    forall (m: T) (x y z: elt),
+    sameclass m x y -> sameclass m y z -> sameclass m x z.
+
+  (* [repr m x] is a canonical representative of the equivalence class
+     of [x] in partition [m]. *)
+  Hypothesis repr_repr:
+    forall (m: T) (x: elt), repr m (repr m x) = repr m x.
+  Hypothesis sameclass_repr:
+    forall (m: T) (x: elt), sameclass m x (repr m x).
+
+  (* [empty] is the finest partition *)
+  Hypothesis repr_empty:
+    forall (x: elt), repr empty x = x.
+  Hypothesis sameclass_empty:
+    forall (x y: elt), sameclass empty x y -> x = y.
+
+  (* [identify] preserves existing equivalences and adds an equivalence
+     between the two elements provided. *)
+  Hypothesis sameclass_identify_1:
+    forall (m: T) (x y: elt), sameclass (identify m x y) x y.
+  Hypothesis sameclass_identify_2:
+    forall (m: T) (x y u v: elt),
+    sameclass m u v -> sameclass (identify m x y) u v.
+
+End UNIONFIND.
+
+(** Implementation of the union-find algorithm. *)
+
+Module Unionfind (E: ELEMENT) (M: MAP with Definition elt := E.T) 
+          <: UNIONFIND with Definition elt := E.T.
+
+Definition elt := E.T.
+
+(* A set of equivalence classes over [elt] is represented by a map [m].
+- [M.get a m = Some a'] means that [a] is in the same class as [a'].
+- [M.get a m = None] means that [a] is the canonical representative
+     for its equivalence class.
+*)
+
+(** Such a map induces an ordering over type [elt]:
+   [repr_order m a a'] if and only if [M.get a' m = Some a].
+   This ordering must be well founded (no cycles). *)
+
+Definition repr_order (m: M.T) (a a': elt) : Prop :=
+  M.get a' m = Some a.
+
+(** The canonical representative of an element.  
+  Needs Noetherian recursion. *)
+
+Lemma option_sum:
+  forall (x: option elt), {y: elt | x = Some y} + {x = None}.
+Proof.
+  intro x. case x.
+  left. exists e. auto.
+  right. auto.
+Qed.
+
+Definition repr_rec
+  (m: M.T) (a: elt) (rec: forall b: elt, repr_order m b a -> elt) :=
+     match option_sum (M.get a m) with
+     | inleft (exist b P) => rec b P
+     | inright _ => a
+     end.
+
+Definition repr_aux
+    (m: M.T) (wf: well_founded (repr_order m)) (a: elt) : elt :=
+  Fix wf (fun (_: elt) => elt) (repr_rec m) a.
+
+Lemma repr_rec_ext:
+  forall (m: M.T) (x: elt) (f g: forall y:elt, repr_order m y x -> elt),
+  (forall (y: elt) (p: repr_order m y x), f y p = g y p) ->
+  repr_rec m x f = repr_rec m x g.
+Proof.
+  intros. unfold repr_rec. 
+  case (option_sum (M.get x m)).
+  intros. elim s; intros. apply H.
+  intros. auto.
+Qed.
+
+Lemma repr_aux_none:
+  forall (m: M.T) (wf: well_founded (repr_order m)) (a: elt),
+  M.get a m = None ->
+  repr_aux m wf a = a.
+Proof.
+  intros. 
+  generalize (Fix_eq wf (fun (_:elt) => elt) (repr_rec m) (repr_rec_ext m) a). 
+  intro. unfold repr_aux. rewrite H0. 
+  unfold repr_rec. 
+  case (option_sum (M.get a m)).
+  intro s; elim s; intros.
+  rewrite H in p; discriminate.
+  intros. auto.
+Qed.
+
+Lemma repr_aux_some:
+  forall (m: M.T) (wf: well_founded (repr_order m)) (a a': elt),
+  M.get a m = Some a' ->
+  repr_aux m wf a = repr_aux m wf a'.
+Proof.
+  intros. 
+  generalize (Fix_eq wf (fun (_:elt) => elt) (repr_rec m) (repr_rec_ext m) a). 
+  intro. unfold repr_aux. rewrite H0. unfold repr_rec.
+  case (option_sum (M.get a m)).
+  intro s; elim s; intros.
+  rewrite H in p. injection p; intros. rewrite H1. auto.
+  intros. rewrite H in e. discriminate.
+Qed.
+ 
+Lemma repr_aux_canon:
+  forall (m: M.T) (wf: well_founded (repr_order m)) (a: elt),
+  M.get (repr_aux m wf a) m = None.
+Proof.
+  intros.
+  apply (well_founded_ind wf (fun (a: elt) => M.get (repr_aux m wf a) m = None)).
+  intros.
+  generalize (Fix_eq wf (fun (_:elt) => elt) (repr_rec m) (repr_rec_ext m) x). 
+  intro. unfold repr_aux. rewrite H0. 
+  unfold repr_rec.
+  case (option_sum (M.get x m)).
+  intro s; elim s; intros. 
+  unfold repr_aux in H. apply H.
+  unfold repr_order. auto.
+  intro. auto.
+Qed.
+
+(** The empty partition (each element in its own class) is well founded. *)
+
+Lemma wf_empty:
+  well_founded (repr_order M.empty).
+Proof.
+  red. intro. apply Acc_intro.
+  intros b RO.
+  red in RO.
+  rewrite M.get_empty in RO.
+  discriminate.
+Qed.
+
+(** Merging two equivalence classes. *)
+
+Section IDENTIFY.
+
+Variable m: M.T.
+Hypothesis mwf: well_founded (repr_order m).
+Variable a b: elt.
+Hypothesis a_diff_b: a <> b.
+Hypothesis a_canon: M.get a m = None.
+Hypothesis b_canon: M.get b m = None.
+
+(** Identifying two distinct canonical representatives [a] and [b] 
+  is achieved by mapping one to the other. *)
+
+Definition identify_base: M.T := M.add a b m.
+
+Lemma identify_base_b_canon:
+  M.get b identify_base = None.
+Proof.
+  unfold identify_base.
+  rewrite M.get_add_2.
+  auto.
+  apply sym_not_eq. auto.
+Qed.
+
+Lemma identify_base_a_maps_to_b:
+  M.get a identify_base = Some b.
+Proof.
+  unfold identify_base. rewrite M.get_add_1. auto.
+Qed.
+
+Lemma identify_base_repr_order:
+  forall (x y: elt),
+  repr_order identify_base x y ->
+  repr_order m x y \/ (y = a /\ x = b).
+Proof.
+  intros x y. unfold identify_base.
+  unfold repr_order.
+  case (E.eq a y); intro.
+  rewrite e. rewrite M.get_add_1.
+  intro. injection H. intro. rewrite H0. tauto.
+  rewrite M.get_add_2; auto.
+Qed.
+
+(** [identify_base] preserves well foundation. *)
+
+Lemma identify_base_order_wf:
+  well_founded (repr_order identify_base).
+Proof.
+  red. 
+  cut (forall (x: elt), Acc (repr_order m) x -> Acc (repr_order identify_base) x).
+  intro CUT. intro x. apply CUT. apply mwf.
+
+  induction 1.
+  apply Acc_intro. intros.
+  MyElim (identify_base_repr_order y x H1).
+  apply H0; auto.
+  rewrite H3.
+  apply Acc_intro.
+  intros z H4.
+  red in H4. rewrite identify_base_b_canon in H4. discriminate.
+Qed.
+
+Lemma identify_aux_decomp:
+  forall (x: elt),
+     (M.get x m = None /\ M.get x identify_base = None)
+  \/ (x = a /\ M.get x m = None /\ M.get x identify_base = Some b)
+  \/ (exists y, M.get x m = Some y /\ M.get x identify_base = Some y).
+Proof.
+  intro x.
+  unfold identify_base.
+  case (E.eq a x); intro.
+  rewrite <- e. rewrite M.get_add_1.
+  tauto.
+  rewrite M.get_add_2; auto.
+  case (M.get x m); intros.
+  right; right; exists e; tauto.
+  tauto.
+Qed.
+
+Lemma identify_base_repr:
+  forall (x: elt),
+  repr_aux identify_base identify_base_order_wf x =
+  (if E.eq (repr_aux m mwf x) a then b else repr_aux m mwf x).
+Proof.
+  intro x0.
+  apply (well_founded_ind mwf
+    (fun (x: elt) =>
+      repr_aux identify_base identify_base_order_wf x =
+      (if E.eq (repr_aux m mwf x) a then b else repr_aux m mwf x)));
+  intros.
+  MyElim (identify_aux_decomp x).
+
+  rewrite (repr_aux_none identify_base).
+  rewrite (repr_aux_none m mwf x).
+  case (E.eq x a); intro.
+  subst x.
+  rewrite identify_base_a_maps_to_b in H1.
+  discriminate.
+  auto. auto. auto.
+
+  subst x. rewrite (repr_aux_none m mwf a); auto.
+  case (E.eq a a); intro.
+  rewrite (repr_aux_some identify_base identify_base_order_wf a b).
+  rewrite (repr_aux_none identify_base identify_base_order_wf b).
+  auto. apply identify_base_b_canon. auto. 
+  tauto.
+
+  rewrite (repr_aux_some identify_base identify_base_order_wf x x1); auto.
+  rewrite (repr_aux_some m mwf x x1); auto.
+Qed.
+
+Lemma identify_base_sameclass_1:
+  forall (x y: elt),
+  repr_aux m mwf x = repr_aux m mwf y ->
+  repr_aux identify_base identify_base_order_wf x =
+    repr_aux identify_base identify_base_order_wf y.
+Proof.
+  intros.
+  rewrite identify_base_repr.
+  rewrite identify_base_repr.
+  rewrite H.
+  auto.
+Qed.
+
+Lemma identify_base_sameclass_2:
+  forall (x y: elt),
+  repr_aux m mwf x = a ->
+  repr_aux m mwf y = b ->
+  repr_aux identify_base identify_base_order_wf x =
+  repr_aux identify_base identify_base_order_wf y.
+Proof.
+  intros.
+  rewrite identify_base_repr.
+  rewrite identify_base_repr.
+  rewrite H. 
+  case (E.eq a a); intro.
+  case (E.eq (repr_aux m mwf y) a); auto.
+  tauto.
+Qed.
+
+End IDENTIFY.
+
+(** The union-find data structure is a record encapsulating a mapping
+  and a proof of well foundation. *)
+
+Record unionfind : Set := mkunionfind
+  { map: M.T; wf: well_founded (repr_order map) }.
+
+Definition T := unionfind.
+
+Definition repr (uf: unionfind) (a: elt) : elt :=
+  repr_aux (map uf) (wf uf) a.
+
+Lemma repr_repr:
+  forall (uf: unionfind) (a: elt), repr uf (repr uf a) = repr uf a.
+Proof.
+  intros.
+  unfold repr.
+  rewrite (repr_aux_none (map uf) (wf uf) (repr_aux (map uf) (wf uf) a)).
+  auto.
+  apply repr_aux_canon. 
+Qed.
+
+Definition empty := mkunionfind M.empty wf_empty.
+
+(** [identify] computes canonical representatives for the two elements
+  and adds a mapping from one to the other, unless they are already
+  equal. *)
+
+Definition identify (uf: unionfind) (a b: elt) : unionfind :=
+  match E.eq (repr uf a) (repr uf b) with
+  | left EQ =>
+      uf
+  | right NOTEQ =>
+      mkunionfind
+        (identify_base (map uf) (repr uf a) (repr uf b))
+        (identify_base_order_wf (map uf) (wf uf)
+            (repr uf a) (repr uf b)
+            NOTEQ
+            (repr_aux_canon (map uf) (wf uf) b))
+  end.
+
+Definition sameclass (uf: unionfind) (a b: elt) : Prop :=
+  repr uf a = repr uf b.
+
+Lemma sameclass_refl:
+  forall (uf: unionfind) (a: elt), sameclass uf a a.
+Proof.
+  intros. red. auto.
+Qed.
+
+Lemma sameclass_sym:
+  forall (uf: unionfind) (a b: elt), sameclass uf a b -> sameclass uf b a.
+Proof.
+  intros. red. symmetry. exact H.
+Qed.
+
+Lemma sameclass_trans:
+  forall (uf: unionfind) (a b c: elt),
+  sameclass uf a b -> sameclass uf b c -> sameclass uf a c.
+Proof.
+  intros. red. transitivity (repr uf b). exact H. exact H0.
+Qed.
+
+Lemma sameclass_repr:
+  forall (uf: unionfind) (a: elt), sameclass uf a (repr uf a).
+Proof.
+  intros. red. symmetry. rewrite repr_repr. auto.
+Qed.
+
+Lemma repr_empty:
+  forall (a: elt), repr empty a = a.
+Proof.
+  intro a. unfold repr; unfold empty.
+  simpl.
+  apply repr_aux_none.
+  apply M.get_empty.
+Qed.
+
+Lemma sameclass_empty:
+  forall (a b: elt), sameclass empty a b -> a = b.
+Proof.
+  intros. red in H. rewrite repr_empty in H.
+  rewrite repr_empty in H. auto.
+Qed.
+
+Lemma sameclass_identify_2:
+  forall (uf: unionfind) (a b x y: elt),
+  sameclass uf x y -> sameclass (identify uf a b) x y.
+Proof.
+  intros.
+  unfold identify.
+  case (E.eq (repr uf a) (repr uf b)).
+  intro. auto.
+  intros; red; unfold repr; simpl.
+  apply identify_base_sameclass_1.
+  apply repr_aux_canon.
+  exact H.
+Qed.
+
+Lemma sameclass_identify_1:
+  forall (uf: unionfind) (a b: elt),
+  sameclass (identify uf a b) a b.
+Proof.
+  intros.
+  unfold identify.
+  case (E.eq (repr uf a) (repr uf b)).
+  intro. auto.
+  intros.
+  red; unfold repr; simpl.
+  apply identify_base_sameclass_2.
+  apply repr_aux_canon.
+  auto.
+  auto.
+Qed.
+
+End Unionfind.
+
+(* Example of use 1: with association lists *)
+
+(*
+
+Require Import List.
+
+Module AListMap(E: ELEMENT) : MAP.
+
+Definition elt := E.T.
+Definition T := list (elt * elt).
+Definition empty : T := nil.
+Fixpoint get (x: elt) (m: T) {struct m} : option elt :=
+  match m with
+  | nil => None
+  | (a,b) :: t =>
+      match E.eq x a with
+      | left _ => Some b
+      | right _ => get x t
+      end
+  end.
+Definition add (x y: elt) (m: T) := (x,y) :: m.
+
+Lemma get_empty: forall (x: elt), get x empty = None.
+Proof.
+  intro. unfold empty. simpl. auto.
+Qed.
+
+Lemma get_add_1:
+  forall (x y: elt) (m: T), get x (add x y m) = Some y.
+Proof.
+  intros. unfold add. simpl. 
+  case (E.eq x x); intro.
+  auto.
+  tauto.
+Qed.
+
+Lemma get_add_2:
+   forall (x y z: elt) (m: T), z <> x -> get z (add x y m) = get z m.
+Proof.
+  intros. unfold add. simpl.
+  case (E.eq z x); intro.
+  subst z; tauto.
+  auto.
+Qed.
+
+End AListMap.
+
+*)
+