From c98440cad6b7a9c793aded892ec61a8ed50cac28 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 2 Mar 2007 15:43:35 +0000
Subject: Suppression de lib/Sets.v, utilisation de FSet a la place. 
 Generalisation de Lattice pour utiliser une notion d'egalite possiblement
 differente de =.  Adaptation de Kildall et de ses utilisateurs en
 consequence.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/Allocation.v    |   4 +-
 backend/Allocproof.v    |  87 +++++++++++++++++---------------
 backend/Coloring.v      |   6 +--
 backend/Coloringproof.v | 131 +++++++++++++++++++++++-------------------------
 backend/Constprop.v     |  31 ++++++++----
 backend/InterfGraph.v   |  44 ++++++++--------
 backend/Kildall.v       |  31 ++++++++----
 backend/Linearize.v     |   1 -
 backend/Registers.v     |   6 ++-
 9 files changed, 185 insertions(+), 156 deletions(-)

(limited to 'backend')

diff --git a/backend/Allocation.v b/backend/Allocation.v
index c66d6b08..74c85cfe 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -3,6 +3,7 @@
 
 Require Import Coqlib.
 Require Import Maps.
+Require Import Lattice.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
@@ -100,7 +101,8 @@ Definition transfer
     general framework for backward dataflow analysis provided by
     module [Kildall].  *)
 
-Module DS := Backward_Dataflow_Solver(Regset)(NodeSetBackward).
+Module RegsetLat := LFSet(Regset).
+Module DS := Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward).
 
 Definition analyze (f: RTL.function): option (PMap.t Regset.t) :=
   DS.fixpoint (successors f) f.(fn_nextpc) (transfer f) nil.
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 0b252d56..f0b2968f 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -2,6 +2,8 @@
   RTL to LTL). *)
 
 Require Import Relations.
+Require Import FSets.
+Require Import SetoidList.
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
@@ -83,7 +85,7 @@ Lemma analyze_correct:
   f.(fn_code)!n <> None ->
   f.(fn_code)!s <> None ->
   In s (successors f n) ->
-  Regset.ge live!!n (transfer f s live!!s).
+  RegsetLat.ge live!!n (transfer f s live!!s).
 Proof.
   intros.
   eapply DS.fixpoint_solution.
@@ -188,6 +190,7 @@ End REGALLOC_PROPERTIES.
 (** * Semantic agreement between RTL registers and LTL locations *)
 
 Require Import LTL.
+Module RegsetP := Properties(Regset).
 
 Section AGREE.
 
@@ -212,7 +215,7 @@ Hypothesis REGALLOC: regalloc f flive (live0 f flive) env = Some assign.
   of [assign r] can be arbitrary. *)
 
 Definition agree (live: Regset.t) (rs: regset) (ls: locset) : Prop :=
-  forall (r: reg), Regset.mem r live = true -> ls (assign r) = rs#r.
+  forall (r: reg), Regset.In r live -> ls (assign r) = rs#r.
 
 (** What follows is a long list of lemmas expressing properties
   of the [agree_live_regs] predicate that are useful for the 
@@ -222,7 +225,7 @@ Definition agree (live: Regset.t) (rs: regset) (ls: locset) : Prop :=
 
 Lemma agree_increasing:
   forall live1 live2 rs ls,
-  Regset.ge live1 live2 -> agree live1 rs ls ->
+  RegsetLat.ge live1 live2 -> agree live1 rs ls ->
   agree live2 rs ls.
 Proof.
   unfold agree; intros. 
@@ -231,14 +234,13 @@ Qed.
 
 (** Some useful special cases of [agree_increasing]. *)
 
+
 Lemma agree_reg_live:
   forall r live rs ls,
   agree (reg_live r live) rs ls -> agree live rs ls.
 Proof.
-  intros. apply agree_increasing with (reg_live r live).
-  red; intros. case (Reg.eq r r0); intro.
-  subst r0. apply Regset.mem_add_same.
-  rewrite Regset.mem_add_other; auto. auto.
+  intros. apply agree_increasing with (reg_live r live); auto.
+  red. apply RegsetP.subset_add_2. apply RegsetP.subset_refl.
 Qed.
 
 Lemma agree_reg_list_live:
@@ -266,7 +268,7 @@ Lemma agree_eval_reg:
   forall r live rs ls,
   agree (reg_live r live) rs ls -> ls (assign r) = rs#r.
 Proof.
-  intros. apply H. apply Regset.mem_add_same.
+  intros. apply H. apply Regset.add_1. auto. 
 Qed.
 
 (** Same, for a list of registers. *)
@@ -304,13 +306,13 @@ Qed.
 
 Lemma agree_assign_dead:
   forall live r rs ls v,
-  Regset.mem r live = false ->
+  ~Regset.In r live ->
   agree live rs ls ->
   agree live (rs#r <- v) ls.
 Proof.
   unfold agree; intros.
   case (Reg.eq r r0); intro.
-  subst r0. congruence.
+  subst r0. contradiction.
   rewrite Regmap.gso; auto. 
 Qed.
 
@@ -322,7 +324,7 @@ Qed.
 Lemma agree_assign_live:
   forall live r rs ls ls' v,
   (forall s,
-     Regset.mem s live = true -> s <> r -> assign s <> assign r) ->
+     Regset.In s live -> s <> r -> assign s <> assign r) ->
   ls' (assign r) = v ->
   (forall l, Loc.diff l (assign r) -> Loc.notin l temporaries -> ls' l = ls l) ->
   agree (reg_dead r live) rs ls ->
@@ -332,8 +334,8 @@ Proof.
   case (Reg.eq r r0); intro.
   subst r0. rewrite Regmap.gss. assumption.
   rewrite Regmap.gso; auto.
-  rewrite H1. apply H2. rewrite Regset.mem_remove_other. auto.
-  auto.  eapply regalloc_noteq_diff. eauto. apply H. auto.  auto.
+  rewrite H1. apply H2. apply Regset.remove_2; auto. 
+  eapply regalloc_noteq_diff. eauto. apply H. auto.  auto.
   eapply regalloc_not_temporary; eauto.
 Qed.
 
@@ -347,7 +349,7 @@ Qed.
 Lemma agree_move_live:
   forall live arg res rs (ls ls': locset),
   (forall r,
-     Regset.mem r live = true -> r <> res -> r <> arg -> 
+     Regset.In r live -> r <> res -> r <> arg -> 
      assign r <> assign res) ->
   ls' (assign res) = ls (assign arg) ->
   (forall l, Loc.diff l (assign res) -> Loc.notin l temporaries -> ls' l = ls l) ->
@@ -357,17 +359,16 @@ Proof.
   unfold agree; intros. 
   case (Reg.eq res r); intro.
   subst r. rewrite Regmap.gss. rewrite H0. apply H2.
-  apply Regset.mem_add_same.
+  apply Regset.add_1; auto.
   rewrite Regmap.gso; auto.
   case (Loc.eq (assign r) (assign res)); intro.
   rewrite e. rewrite H0.
   case (Reg.eq arg r); intro.
-  subst r. apply H2. apply Regset.mem_add_same.
+  subst r. apply H2. apply Regset.add_1; auto.
   elim (H r); auto.
   rewrite H1. apply H2. 
-  case (Reg.eq arg r); intro. subst r. apply Regset.mem_add_same.
-  rewrite Regset.mem_add_other; auto.
-  rewrite Regset.mem_remove_other; auto.
+  case (Reg.eq arg r); intro. subst r. apply Regset.add_1; auto.
+  apply Regset.add_2. apply Regset.remove_2. auto. auto. 
   eapply regalloc_noteq_diff; eauto.
   eapply regalloc_not_temporary; eauto.
 Qed.
@@ -379,11 +380,10 @@ Qed.
 Lemma agree_call:
   forall live args ros res rs v (ls ls': locset),
   (forall r,
-    Regset.mem r live = true ->
-    r <> res ->
+    Regset.In r live -> r <> res ->
     ~(In (assign r) Conventions.destroyed_at_call)) ->
   (forall r,
-    Regset.mem r live = true -> r <> res -> assign r <> assign res) ->
+    Regset.In r live -> r <> res -> assign r <> assign res) ->
   ls' (assign res) = v ->
   (forall l,
     Loc.notin l destroyed_at_call -> loc_acceptable l -> Loc.diff l (assign res) ->
@@ -399,7 +399,7 @@ Proof.
   case (Reg.eq r res); intro.
   subst r. rewrite Regmap.gss. assumption.
   rewrite Regmap.gso; auto. rewrite H2. apply H4.
-  rewrite Regset.mem_remove_other; auto.
+  apply Regset.remove_2; auto. 
   eapply regalloc_notin_notin; eauto. 
   eapply regalloc_acceptable; eauto.
   eapply regalloc_noteq_diff; eauto.
@@ -411,7 +411,7 @@ Qed.
 Lemma agree_init_regs:
   forall rl vl ls live,
   (forall r1 r2,
-    In r1 rl -> Regset.mem r2 live = true -> r1 <> r2 ->
+    In r1 rl -> Regset.In r2 live -> r1 <> r2 ->
     assign r1 <> assign r2) ->
   List.map ls (List.map assign rl) = vl ->
   agree (reg_list_dead rl live) (Regmap.init Vundef) ls ->
@@ -421,15 +421,13 @@ Proof.
   assumption.
   destruct vl. discriminate. 
   assert (agree (reg_dead a live) (init_regs vl rl) ls).
-  apply IHrl. intros. apply H. tauto. 
-  case (Reg.eq a r2); intro. subst r2. 
-  rewrite Regset.mem_remove_same in H3. discriminate.
-  rewrite Regset.mem_remove_other in H3; auto.
+  apply IHrl. intros. apply H. tauto.
+  eapply Regset.remove_3; eauto.
   auto. congruence. assumption.
   red; intros. case (Reg.eq a r); intro.
   subst r. rewrite Regmap.gss. congruence. 
-  rewrite Regmap.gso; auto. apply H2. 
-  rewrite Regset.mem_remove_other; auto.
+  rewrite Regmap.gso; auto. apply H2.
+  apply Regset.remove_2; auto. 
 Qed.
 
 Lemma agree_parameters:
@@ -437,7 +435,7 @@ Lemma agree_parameters:
   let params := f.(RTL.fn_params) in
   List.map ls (List.map assign params) = vl ->
   (forall r,
-     Regset.mem r (reg_list_dead params (live0 f flive)) = true ->
+     Regset.In r (reg_list_dead params (live0 f flive)) ->
      ls (assign r) = Vundef) ->
   agree (live0 f flive) (init_regs vl params) ls.
 Proof.
@@ -1373,6 +1371,7 @@ Proof.
   intros; red; intros; CleanupHyps.
   caseEq (Regset.mem res live!!pc); intro LV;
   rewrite LV in AG.
+  generalize (Regset.mem_2 _ _ LV). intro LV'.
   assert (LL: (List.length (List.map assign args) <= 3)%nat).
     rewrite list_length_map. 
     inversion WTI. simpl; omega. simpl; omega.
@@ -1409,7 +1408,8 @@ Proof.
   exists ls. split.
   CleanupGoal. rewrite LV. 
   apply exec_Bgoto; apply exec_refl.
-  apply agree_assign_dead; assumption.
+  apply agree_assign_dead; auto. 
+  red; intro. exploit Regset.mem_1; eauto. congruence.
 Qed.
 
 Lemma transl_Iload_correct:
@@ -1426,6 +1426,7 @@ Proof.
   caseEq (Regset.mem dst live!!pc); intro LV;
   rewrite LV in AG.
   (* dst is live *)
+  exploit Regset.mem_2; eauto. intro LV'.
   assert (LL: (List.length (List.map assign args) <= 2)%nat).
     rewrite list_length_map. 
     inversion WTI. 
@@ -1453,6 +1454,7 @@ Proof.
   CleanupGoal. rewrite LV. 
   apply exec_Bgoto; apply exec_refl.
   apply agree_assign_dead; auto.
+  red; intro; exploit Regset.mem_1; eauto. congruence.
 Qed.
 
 Lemma transl_Istore_correct:
@@ -1681,16 +1683,15 @@ Qed.
 
 Remark regset_mem_reg_list_dead:
   forall rl r live,
-  Regset.mem r (reg_list_dead rl live) = true ->
-  ~(In r rl) /\ Regset.mem r live = true.
+  Regset.In r (reg_list_dead rl live) ->
+  ~(In r rl) /\ Regset.In r live.
 Proof.
   induction rl; simpl; intros.
   tauto.
   elim (IHrl r (reg_dead a live) H). intros.
-  assert (a <> r). red; intro; subst r. 
-  rewrite Regset.mem_remove_same in H1. discriminate.
-  rewrite Regset.mem_remove_other in H1; auto.
-  tauto. 
+  assert (a <> r). red; intro; subst r.
+  exploit Regset.remove_1; eauto. 
+  intuition. eapply Regset.remove_3; eauto.
 Qed. 
 
 Lemma transf_entrypoint_correct:
@@ -1733,7 +1734,9 @@ Proof.
     intros [p [AP INP]]. clear INAP; subst ap.
     generalize (list_in_map_inv _ _ _ INAU).
     intros [u [AU INU]]. clear INAU; subst au.
-    generalize (Regset.elements_complete _ _ INU). intro.
+    assert (INU': InA Regset.E.eq u undefs).
+      rewrite InA_alt. exists u; intuition. 
+    generalize (Regset.elements_2 _ _ INU'). intro.
     generalize (regset_mem_reg_list_dead _ _ _ H4).
     intros [A B]. 
     eapply regalloc_noteq_diff; eauto.
@@ -1761,7 +1764,11 @@ Proof.
   rewrite PARAMS1. assumption.
   fold oldentry; fold params. intros.
   apply UNDEFS1. apply in_map. 
-  unfold undefs; apply Regset.elements_correct; auto.
+  unfold undefs.
+  change (transfer f oldentry live!!oldentry)
+    with (live0 f live).
+  exploit Regset.elements_1; eauto.
+  rewrite InA_alt. intros [r' [C D]]. hnf in C. subst r'. auto.
 Qed.
 
 Lemma transl_function_correct:
diff --git a/backend/Coloring.v b/backend/Coloring.v
index 0a2487cb..0b8a4ccc 100644
--- a/backend/Coloring.v
+++ b/backend/Coloring.v
@@ -81,8 +81,8 @@ Require Import InterfGraph.
 
 Definition add_interf_live
     (filter: reg -> bool) (res: reg) (live: Regset.t) (g: graph): graph :=
-  Regset.fold
-    (fun g r => if filter r then add_interf r res g else g) live g.
+  Regset.fold graph
+    (fun r g => if filter r then add_interf r res g else g) live g.
 
 Definition add_interf_op
     (res: reg) (live: Regset.t) (g: graph): graph :=
@@ -101,7 +101,7 @@ Definition add_interf_move
 Definition add_interf_call
     (live: Regset.t) (destroyed: list mreg) (g: graph): graph :=
   List.fold_left
-    (fun g mr => Regset.fold (fun g r => add_interf_mreg r mr g) live g)
+    (fun g mr => Regset.fold graph (fun r g => add_interf_mreg r mr g) live g)
     destroyed g.
 
 Fixpoint add_prefs_call
diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v
index 54d24cc4..f3801d07 100644
--- a/backend/Coloringproof.v
+++ b/backend/Coloringproof.v
@@ -1,5 +1,6 @@
 (** Correctness of graph coloring. *)
 
+Require Import SetoidList.
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
@@ -51,37 +52,36 @@ Lemma add_interf_live_incl:
   forall (filter: reg -> bool) res live g,
   graph_incl g (add_interf_live filter res live g).
 Proof.
-  intros. unfold add_interf_live. rewrite Regset.fold_spec.
+  intros. unfold add_interf_live. rewrite Regset.fold_1.
   apply add_interf_live_incl_aux.
 Qed.
 
 Lemma add_interf_live_correct_aux:
-  forall filter res live g r,
-  In r live ->  filter r = true ->
+  forall filter res r live,
+  InA Regset.E.eq r live -> filter r = true ->
+  forall g,
   interfere r res
     (List.fold_left
       (fun g r => if filter r then add_interf r res g else g)
       live g).
 Proof.
-  induction live; simpl; intros.
-  contradiction.
-  elim H; intros.
-  subst a. rewrite H0. 
-  generalize (add_interf_live_incl_aux filter res live (add_interf r res g)).
+  induction 1; simpl; intros.
+  hnf in H. subst y. rewrite H0.
+  generalize (add_interf_live_incl_aux filter res l (add_interf r res g)).
   intros [A B].
   apply A. apply add_interf_correct.
-  apply IHlive; auto.
+  apply IHInA; auto.
 Qed.
 
 Lemma add_interf_live_correct:
   forall filter res live g r,
-  Regset.mem r live = true ->
+  Regset.In r live ->
   filter r = true ->
   interfere r res (add_interf_live filter res live g).
 Proof.
-  intros.  unfold add_interf_live. rewrite Regset.fold_spec.
+  intros.  unfold add_interf_live. rewrite Regset.fold_1.
   apply add_interf_live_correct_aux; auto.
-  apply Regset.elements_correct. auto.
+  apply Regset.elements_1. auto.
 Qed.
 
 Lemma add_interf_op_incl: 
@@ -93,15 +93,13 @@ Qed.
 
 Lemma add_interf_op_correct:
   forall res live g r,
-  Regset.mem r live = true ->
+  Regset.In r live ->
   r <> res ->
   interfere r res (add_interf_op res live g).
 Proof.
   intros.  unfold add_interf_op.
   apply add_interf_live_correct.
-  auto. 
-  case (Reg.eq r res); intro.
-  contradiction. auto.
+  auto. destruct (Reg.eq r res); congruence. 
 Qed.
 
 Lemma add_interf_move_incl: 
@@ -113,18 +111,14 @@ Qed.
 
 Lemma add_interf_move_correct:
   forall arg res live g r,
-  Regset.mem r live = true ->
+  Regset.In r live ->
   r <> arg -> r <> res ->
   interfere r res (add_interf_move arg res live g).
 Proof.
   intros.  unfold add_interf_move.
   apply add_interf_live_correct.
-  auto. 
-  case (Reg.eq r res); intro.
-  contradiction. 
-  case (Reg.eq r arg); intro.
-  contradiction. 
   auto.
+  rewrite dec_eq_false; auto. rewrite dec_eq_false; auto.
 Qed.
 
 Lemma add_interf_call_incl_aux_1:
@@ -142,9 +136,9 @@ Qed.
 Lemma add_interf_call_incl_aux_2:
   forall mr live g,
   graph_incl g
-    (Regset.fold (fun g r => add_interf_mreg r mr g) live g).
+    (Regset.fold graph (fun r g => add_interf_mreg r mr g) live g).
 Proof.
-  intros. rewrite Regset.fold_spec. apply add_interf_call_incl_aux_1.
+  intros. rewrite Regset.fold_1. apply add_interf_call_incl_aux_1.
 Qed.
 
 Lemma add_interf_call_incl:
@@ -176,33 +170,32 @@ Proof.
 Qed.
 
 Lemma add_interf_call_correct_aux_1:
-  forall mr live g r,
-  In r live ->
+  forall mr r live,
+  InA Regset.E.eq r live ->
+  forall g,
   interfere_mreg r mr
     (List.fold_left (fun g r => add_interf_mreg r mr g) live g).
 Proof.
-  induction live; simpl; intros.
-  elim H.
-  elim H; intros.
-  subst a. eapply interfere_mreg_incl. 
+  induction 1; simpl; intros.
+  hnf in H; subst y. eapply interfere_mreg_incl. 
   apply add_interf_call_incl_aux_1.
   apply add_interf_mreg_correct.
-  apply IHlive; auto.
+  auto.
 Qed.
 
 Lemma add_interf_call_correct_aux_2:
   forall mr live g r,
-  Regset.mem r live = true ->
+  Regset.In r live ->
   interfere_mreg r mr
-    (Regset.fold (fun g r => add_interf_mreg r mr g) live g).
+    (Regset.fold graph (fun r g => add_interf_mreg r mr g) live g).
 Proof.
-  intros. rewrite Regset.fold_spec. apply add_interf_call_correct_aux_1.
-  apply Regset.elements_correct; auto.
+  intros. rewrite Regset.fold_1. apply add_interf_call_correct_aux_1.
+  apply Regset.elements_1. auto.
 Qed.
 
 Lemma add_interf_call_correct:
   forall live destroyed g r mr,
-  Regset.mem r live = true ->
+  Regset.In r live ->
   In mr destroyed ->
   interfere_mreg r mr (add_interf_call live destroyed g).
 Proof.
@@ -240,7 +233,7 @@ Qed.
 Lemma add_interf_entry_correct:
   forall params live g r1 r2,
   In r1 params ->
-  Regset.mem r2 live = true ->
+  Regset.In r2 live ->
   r1 <> r2 ->
   interfere r1 r2 (add_interf_entry params live g).
 Proof.
@@ -351,37 +344,37 @@ Definition correct_interf_instr
       match is_move_operation op args with
       | Some arg =>
           forall r,
-          Regset.mem res live = true ->
-          Regset.mem r live = true ->
+          Regset.In res live ->
+          Regset.In r live ->
           r <> res -> r <> arg -> interfere r res g
       | None =>
           forall r,
-          Regset.mem res live = true ->
-          Regset.mem r live = true ->
+          Regset.In res live ->
+          Regset.In r live ->
           r <> res -> interfere r res g
       end
   | Iload chunk addr args res s =>
       forall r,
-      Regset.mem res live = true ->
-      Regset.mem r live = true ->
+      Regset.In res live ->
+      Regset.In r live ->
       r <> res -> interfere r res g
   | Icall sig ros args res s =>
       (forall r mr,
-        Regset.mem r live = true ->
+        Regset.In r live ->
         In mr destroyed_at_call_regs ->
         r <> res ->
         interfere_mreg r mr g)
    /\ (forall r,
-        Regset.mem r live = true ->
+        Regset.In r live ->
         r <> res -> interfere r res g)
   | Ialloc arg res s =>
       (forall r mr,
-        Regset.mem r live = true ->
+        Regset.In r live ->
         In mr destroyed_at_call_regs ->
         r <> res ->
         interfere_mreg r mr g)
    /\ (forall r,
-        Regset.mem r live = true ->
+        Regset.In r live ->
         r <> res -> interfere r res g)
   | _ =>
       True
@@ -414,11 +407,11 @@ Proof.
   intros.
   destruct instr; unfold add_edges_instr; unfold correct_interf_instr; auto.
   destruct (is_move_operation o l); intros.
-  rewrite H. eapply interfere_incl. 
+  rewrite Regset.mem_1; auto. eapply interfere_incl. 
   apply add_pref_incl. apply add_interf_move_correct; auto.
-  rewrite H. apply add_interf_op_correct; auto. 
+  rewrite Regset.mem_1; auto. apply add_interf_op_correct; auto. 
 
-  intros. rewrite H. apply add_interf_op_correct; auto.
+  intros. rewrite Regset.mem_1; auto. apply add_interf_op_correct; auto.
 
   split; intros.
   apply interfere_mreg_incl with
@@ -427,7 +420,7 @@ Proof.
   eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
   apply add_interf_op_incl.
   apply add_interf_call_correct; auto.
-  rewrite Regset.mem_remove_other; auto.
+  apply Regset.remove_2; auto. 
 
   eapply interfere_incl.
   eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
@@ -441,7 +434,7 @@ Proof.
   eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
   apply add_interf_op_incl.
   apply add_interf_call_correct; auto.
-  rewrite Regset.mem_remove_other; auto.
+  apply Regset.remove_2; auto.
 
   eapply interfere_incl.
   eapply graph_incl_trans; apply add_pref_mreg_incl.
@@ -534,7 +527,7 @@ Qed.
 Lemma interf_graph_correct_3:
   forall f live live0 r1 r2,
   In r1 f.(fn_params) ->
-  Regset.mem r2 live0 = true ->
+  Regset.In r2 live0 ->
   r1 <> r2 ->
   interfere r1 r2 (interf_graph f live live0).
 Proof.
@@ -617,8 +610,10 @@ Lemma check_coloring_3_correct:
   loc_acceptable (coloring r) /\ env r = Loc.type (coloring r).
 Proof.
   unfold check_coloring_3; intros.
-  generalize (Regset.for_all_spec _ H H0). intro.
-  elim (andb_prop _ _ H1); intros.
+  exploit Regset.for_all_2; eauto.
+  red; intros. hnf in H1. congruence.
+  apply Regset.mem_2. eauto.
+  simpl. intro. elim (andb_prop _ _ H1); intros.
   split. apply loc_is_acceptable_correct; auto.
   apply same_typ_correct; auto.
 Qed.
@@ -649,7 +644,7 @@ Proof.
   elim (andb_prop _ _ H); intros.
   generalize (all_interf_regs_correct_1 _ _ _ H0).
   intros [A B].
-  unfold allregs. rewrite A; rewrite B.
+  unfold allregs. rewrite Regset.mem_1; auto. rewrite Regset.mem_1; auto.
   eapply check_coloring_1_correct; eauto.
 Qed.
 
@@ -663,7 +658,7 @@ Proof.
   elim (andb_prop _ _ H); intros.
   elim (andb_prop _ _ H2); intros.
   generalize (all_interf_regs_correct_2 _ _ _ H0). intros.
-  unfold allregs. rewrite H5. 
+  unfold allregs. rewrite Regset.mem_1; auto. 
   eapply check_coloring_2_correct; eauto.
 Qed.
 
@@ -709,35 +704,35 @@ Definition correct_alloc_instr
       match is_move_operation op args with
       | Some arg =>
           forall r,
-          Regset.mem res live!!pc = true ->
-          Regset.mem r live!!pc = true ->
+          Regset.In res live!!pc ->
+          Regset.In r live!!pc ->
           r <> res -> r <> arg -> alloc r <> alloc res
       | None =>
           forall r,
-          Regset.mem res live!!pc = true ->
-          Regset.mem r live!!pc = true ->
+          Regset.In res live!!pc ->
+          Regset.In r live!!pc ->
           r <> res -> alloc r <> alloc res
       end
   | Iload chunk addr args res s =>
       forall r,
-      Regset.mem res live!!pc = true ->
-      Regset.mem r live!!pc = true ->
+      Regset.In res live!!pc ->
+      Regset.In r live!!pc ->
       r <> res -> alloc r <> alloc res
   | Icall sig ros args res s =>
       (forall r,
-        Regset.mem r live!!pc = true ->
+        Regset.In r live!!pc ->
         r <> res ->
         ~(In (alloc r) Conventions.destroyed_at_call))
    /\ (forall r,
-        Regset.mem r live!!pc = true ->
+        Regset.In r live!!pc ->
         r <> res -> alloc r <> alloc res)
   | Ialloc arg res s =>
       (forall r,
-        Regset.mem r live!!pc = true ->
+        Regset.In r live!!pc ->
         r <> res ->
         ~(In (alloc r) Conventions.destroyed_at_call))
    /\ (forall r,
-        Regset.mem r live!!pc = true ->
+        Regset.In r live!!pc ->
         r <> res -> alloc r <> alloc res)
   | _ =>
       True
@@ -869,7 +864,7 @@ Lemma regalloc_correct_3:
   forall r1 r2,
   regalloc f live live0 env = Some alloc ->
   In r1 f.(fn_params) ->
-  Regset.mem r2 live0 = true ->
+  Regset.In r2 live0 ->
   r1 <> r2 ->
   alloc r1 <> alloc r2.
 Proof.
diff --git a/backend/Constprop.v b/backend/Constprop.v
index 330857cd..d34c6eed 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -36,7 +36,11 @@ Inductive approx : Set :=
 
 Module Approx <: SEMILATTICE_WITH_TOP.
   Definition t := approx.
-  Lemma eq: forall (x y: t), {x=y} + {x<>y}.
+  Definition eq (x y: t) := (x = y).
+  Definition eq_refl: forall x, eq x x := (@refl_equal t).
+  Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t).
+  Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t).
+  Lemma eq_dec: forall (x y: t), {x=y} + {x<>y}.
   Proof.
     decide equality.
     apply Int.eq_dec.
@@ -44,16 +48,25 @@ Module Approx <: SEMILATTICE_WITH_TOP.
     apply Int.eq_dec.
     apply ident_eq.
   Qed.
+  Definition beq (x y: t) := if eq_dec x y then true else false.
+  Lemma beq_correct: forall x y, beq x y = true -> x = y.
+  Proof.
+    unfold beq; intros.  destruct (eq_dec x y). auto. congruence.
+  Qed.
   Definition ge (x y: t) : Prop :=
     x = Unknown \/ y = Novalue \/ x = y.
-  Lemma ge_refl: forall x, ge x x.
+  Lemma ge_refl: forall x y, eq x y -> ge x y.
   Proof.
-    unfold ge; tauto.
+    unfold eq, 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.
+  Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.
+  Proof.
+    unfold eq, ge; intros; congruence.
+  Qed.
   Definition bot := Novalue.
   Definition top := Unknown.
   Lemma ge_bot: forall x, ge x bot.
@@ -65,23 +78,23 @@ Module Approx <: SEMILATTICE_WITH_TOP.
     unfold ge, bot; tauto.
   Qed.
   Definition lub (x y: t) : t :=
-    if eq x y then x else
+    if eq_dec x y then x else
     match x, y with
     | Novalue, _ => y
     | _, Novalue => x
     | _, _ => Unknown
     end.
-  Lemma lub_commut: forall x y, lub x y = lub y x.
+  Lemma lub_commut: forall x y, eq (lub x y) (lub y x).
   Proof.
-    unfold lub; intros.
-    case (eq x y); case (eq y x); intros; try congruence.
+    unfold lub, eq; intros.
+    case (eq_dec x y); case (eq_dec y x); intros; try congruence.
     destruct x; destruct y; auto.
   Qed.
   Lemma ge_lub_left: forall x y, ge (lub x y) x.
   Proof.
     unfold lub; intros.
-    case (eq x y); intro.
-    apply ge_refl.
+    case (eq_dec x y); intro.
+    apply ge_refl. apply eq_refl.
     destruct x; destruct y; unfold ge; tauto.
   Qed.
 End Approx.
diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v
index 78112c33..5dc4fe9e 100644
--- a/backend/InterfGraph.v
+++ b/backend/InterfGraph.v
@@ -214,6 +214,7 @@ Definition all_interf_regs (g: graph) : Regset.t :=
       g.(interf_reg_mreg)
       Regset.empty).
 
+(*
 Lemma mem_add_tail:
   forall r r' u,
   Regset.mem r u = true -> Regset.mem r (Regset.add r' u) = true.
@@ -222,28 +223,29 @@ Proof.
   subst r'. apply Regset.mem_add_same.
   rewrite Regset.mem_add_other; auto.
 Qed.
-
+*)
 Lemma in_setregreg_fold:
   forall g r1 r2 u,
-  SetRegReg.In (r1, r2) g \/ Regset.mem r1 u = true /\ Regset.mem r2 u = true ->
-  Regset.mem r1 (SetRegReg.fold _ add_intf2 g u) = true /\
-  Regset.mem r2 (SetRegReg.fold _ add_intf2 g u) = true.
+  SetRegReg.In (r1, r2) g \/ Regset.In r1 u /\ Regset.In r2 u ->
+  Regset.In r1 (SetRegReg.fold _ add_intf2 g u) /\
+  Regset.In r2 (SetRegReg.fold _ add_intf2 g u).
 Proof.
   set (add_intf2' := fun u r1r2 => add_intf2 r1r2 u).
   assert (forall l r1 r2 u,
-    InA OrderedRegReg.eq (r1,r2) l \/ Regset.mem r1 u = true /\ Regset.mem r2 u = true ->
-    Regset.mem r1 (List.fold_left add_intf2' l u) = true /\
-    Regset.mem r2 (List.fold_left add_intf2' l u) = true).
+    InA OrderedRegReg.eq (r1,r2) l \/ Regset.In r1 u /\ Regset.In r2 u ->
+    Regset.In r1 (List.fold_left add_intf2' l u) /\
+    Regset.In r2 (List.fold_left add_intf2' l u)).
   induction l; intros; simpl.
   elim H; intro. inversion H0. auto.
   apply IHl. destruct a as [a1 a2].
   elim H; intro. inversion H0; subst. 
   red in H2. simpl in H2. destruct H2. red in H1. red in H2. subst r1 r2.
-  right; unfold add_intf2', add_intf2; simpl; split. 
-  apply Regset.mem_add_same. apply mem_add_tail. apply Regset.mem_add_same.
+  right; unfold add_intf2', add_intf2; simpl; split.
+  apply Regset.add_1. auto. 
+  apply Regset.add_2. apply Regset.add_1. auto. 
   tauto.
   right; unfold add_intf2', add_intf2; simpl; split;
-  apply mem_add_tail; apply mem_add_tail; tauto.
+  apply Regset.add_2; apply Regset.add_2; tauto.
 
   intros. rewrite SetRegReg.fold_1. apply H. 
   intuition. left. apply SetRegReg.elements_1. auto.
@@ -251,8 +253,8 @@ Qed.
 
 Lemma in_setregreg_fold':
   forall g r u,
-  Regset.mem r u = true ->
-  Regset.mem r (SetRegReg.fold _ add_intf2 g u) = true.
+  Regset.In r u ->
+  Regset.In r (SetRegReg.fold _ add_intf2 g u).
 Proof.
   intros. exploit in_setregreg_fold. eauto. 
   intros [A B]. eauto.
@@ -260,23 +262,23 @@ Qed.
 
 Lemma in_setregmreg_fold:
   forall g r1 mr2 u,
-  SetRegMreg.In (r1, mr2) g \/ Regset.mem r1 u = true ->
-  Regset.mem r1 (SetRegMreg.fold _ add_intf1 g u) = true.
+  SetRegMreg.In (r1, mr2) g \/ Regset.In r1 u ->
+  Regset.In r1 (SetRegMreg.fold _ add_intf1 g u).
 Proof.
   set (add_intf1' := fun u r1mr2 => add_intf1 r1mr2 u).
   assert (forall l r1 mr2 u,
-    InA OrderedRegMreg.eq (r1,mr2) l \/ Regset.mem r1 u = true ->
-    Regset.mem r1 (List.fold_left add_intf1' l u) = true).
+    InA OrderedRegMreg.eq (r1,mr2) l \/ Regset.In r1 u ->
+    Regset.In r1 (List.fold_left add_intf1' l u)).
   induction l; intros; simpl.
   elim H; intro. inversion H0. auto.
   apply IHl with mr2. destruct a as [a1 a2].
   elim H; intro. inversion H0; subst. 
   red in H2. simpl in H2. destruct H2. red in H1. red in H2. subst r1 mr2.
   right; unfold add_intf1', add_intf1; simpl.
-  apply Regset.mem_add_same. 
+  apply Regset.add_1; auto.
   tauto.
   right; unfold add_intf1', add_intf1; simpl.
-  apply mem_add_tail; auto.
+  apply Regset.add_2; auto.
 
   intros. rewrite SetRegMreg.fold_1. apply H with mr2. 
   intuition. left. apply SetRegMreg.elements_1. auto.
@@ -285,8 +287,8 @@ Qed.
 Lemma all_interf_regs_correct_1:
   forall r1 r2 g,
   SetRegReg.In (r1, r2) g.(interf_reg_reg) ->
-  Regset.mem r1 (all_interf_regs g) = true /\
-  Regset.mem r2 (all_interf_regs g) = true.
+  Regset.In r1 (all_interf_regs g) /\
+  Regset.In r2 (all_interf_regs g).
 Proof.
   intros. unfold all_interf_regs. 
   apply in_setregreg_fold. tauto.
@@ -295,7 +297,7 @@ Qed.
 Lemma all_interf_regs_correct_2:
   forall r1 mr2 g,
   SetRegMreg.In (r1, mr2) g.(interf_reg_mreg) ->
-  Regset.mem r1 (all_interf_regs g) = true.
+  Regset.In r1 (all_interf_regs g).
 Proof.
   intros. unfold all_interf_regs.
   apply in_setregreg_fold'. eapply in_setregmreg_fold. eauto.
diff --git a/backend/Kildall.v b/backend/Kildall.v
index a04528e5..2a4b4bda 100644
--- a/backend/Kildall.v
+++ b/backend/Kildall.v
@@ -179,7 +179,7 @@ Definition start_state :=
 Definition propagate_succ (s: state) (out: L.t) (n: positive) :=
   let oldl := s.(st_in)!!n in
   let newl := L.lub oldl out in
-  if L.eq oldl newl
+  if L.beq oldl newl
   then s
   else mkstate (PMap.set n newl s.(st_in)) (NS.add n s.(st_wrk)).
 
@@ -225,7 +225,7 @@ Definition in_incr (in1 in2: PMap.t L.t) : Prop :=
 Lemma in_incr_refl:
   forall in1, in_incr in1 in1.
 Proof.
-  unfold in_incr; intros. apply L.ge_refl.
+  unfold in_incr; intros. apply L.ge_refl. apply L.eq_refl.
 Qed.
 
 Lemma in_incr_trans:
@@ -239,11 +239,11 @@ Lemma propagate_succ_incr:
   in_incr st.(st_in) (propagate_succ st out n).(st_in).
 Proof.
   unfold in_incr, propagate_succ; simpl; intros.
-  case (L.eq st.(st_in)!!n (L.lub st.(st_in)!!n out)); intro.
-  apply L.ge_refl.
+  case (L.beq st.(st_in)!!n (L.lub st.(st_in)!!n out)).
+  apply L.ge_refl. apply L.eq_refl.
   simpl. case (peq n n0); intro.
   subst n0. rewrite PMap.gss. apply L.ge_lub_left.
-  rewrite PMap.gso; auto. apply L.ge_refl.
+  rewrite PMap.gso; auto. apply L.ge_refl. apply L.eq_refl.
 Qed.
 
 Lemma propagate_succ_list_incr:
@@ -309,11 +309,18 @@ Lemma propagate_succ_charact:
   (forall s, n <> s -> st'.(st_in)!!s = st.(st_in)!!s).
 Proof.
   unfold propagate_succ; intros; simpl.
-  case (L.eq (st_in st) !! n (L.lub (st_in st) !! n out)); intro.
-  split. rewrite e. rewrite L.lub_commut. apply L.ge_lub_left.
+  predSpec L.beq L.beq_correct
+           ((st_in st) !! n) (L.lub (st_in st) !! n out).
+  split.
+  eapply L.ge_trans. apply L.ge_refl. apply H; auto.
+  eapply L.ge_compat. apply L.lub_commut. apply L.eq_refl. 
+  apply L.ge_lub_left. 
   auto.
+
   simpl. split.
-  rewrite PMap.gss. rewrite L.lub_commut. apply L.ge_lub_left.
+  rewrite PMap.gss.
+  eapply L.ge_compat. apply L.lub_commut. apply L.eq_refl. 
+  apply L.ge_lub_left. 
   intros. rewrite PMap.gso; auto.
 Qed.
 
@@ -344,7 +351,7 @@ Lemma propagate_succ_incr_worklist:
   NS.In x st.(st_wrk) -> NS.In x (propagate_succ st out n).(st_wrk).
 Proof.
   intros. unfold propagate_succ. 
-  case (L.eq (st_in st) !! n (L.lub (st_in st) !! n out)); intro.
+  case (L.beq (st_in st) !! n (L.lub (st_in st) !! n out)).
   auto.
   simpl. rewrite NS.add_spec. auto.
 Qed.
@@ -364,7 +371,7 @@ Lemma propagate_succ_records_changes:
   NS.In s st'.(st_wrk) \/ st'.(st_in)!!s = st.(st_in)!!s.
 Proof.
   simpl. intros. unfold propagate_succ. 
-  case (L.eq (st_in st) !! n (L.lub (st_in st) !! n out)); intro.
+  case (L.beq (st_in st) !! n (L.lub (st_in st) !! n out)).
   right; auto.
   case (peq s n); intro.
   subst s. left. simpl. rewrite NS.add_spec. auto.
@@ -465,7 +472,9 @@ Proof.
   induction ep; simpl; intros.
   elim H.
   elim H; intros.
-  subst a. rewrite PMap.gss. rewrite L.lub_commut. apply L.ge_lub_left.
+  subst a. rewrite PMap.gss.
+  eapply L.ge_compat. apply L.lub_commut. apply L.eq_refl. 
+  apply L.ge_lub_left.
   destruct a. rewrite PMap.gsspec. case (peq n p); intro.
   subst p. apply L.ge_trans with (start_state_in ep)!!n.
   apply L.ge_lub_left. auto.
diff --git a/backend/Linearize.v b/backend/Linearize.v
index 667b5d41..3151628c 100644
--- a/backend/Linearize.v
+++ b/backend/Linearize.v
@@ -3,7 +3,6 @@
 
 Require Import Coqlib.
 Require Import Maps.
-Require Import Sets.
 Require Import AST.
 Require Import Values.
 Require Import Globalenvs.
diff --git a/backend/Registers.v b/backend/Registers.v
index 5b1c7230..578e4b87 100644
--- a/backend/Registers.v
+++ b/backend/Registers.v
@@ -7,7 +7,9 @@
 Require Import Coqlib.
 Require Import AST.
 Require Import Maps.
-Require Import Sets.
+Require Import Ordered.
+Require Import FSets.
+Require FSetAVL.
 
 Definition reg: Set := positive.
 
@@ -45,4 +47,4 @@ Notation "a # b <- c" := (Regmap.set b c a) (at level 1, b at next level).
 
 (** Sets of registers *)
 
-Module Regset := MakeSet(PTree).
+Module Regset := FSetAVL.Make(OrderedPositive).
-- 
cgit