summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-03-09 17:28:10 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-03-09 17:28:10 +0000
commite29b0c71f446ea6267711c7cc19294fd93fb81ad (patch)
tree0317ddbba0cc4a81175f6e05e337d56211a29a26
parent20eea14b1c678722642da5c22afd6e87b6cdf686 (diff)
Assorted cleanups, esp. to avoid generating _rec and _rect recursors in
submodules. (Extraction does not remove them, then.) common/Switch: replaced use of FMaps by our own Maps. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2139 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--backend/Kildall.v4
-rw-r--r--common/Globalenvs.v29
-rw-r--r--common/Memory.v4
-rw-r--r--common/Switch.v97
-rw-r--r--lib/Camlcoq.ml2
-rw-r--r--lib/Heaps.v161
-rw-r--r--lib/Integers.v4
-rw-r--r--lib/Lattice.v4
-rw-r--r--lib/Maps.v26
-rw-r--r--lib/UnionFind.v144
10 files changed, 260 insertions, 215 deletions
diff --git a/backend/Kildall.v b/backend/Kildall.v
index e1e6ea5..9dc7866 100644
--- a/backend/Kildall.v
+++ b/backend/Kildall.v
@@ -17,6 +17,10 @@ Require Import Iteration.
Require Import Maps.
Require Import Lattice.
+(* To avoid useless definitions of inductors in extracted code. *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
(** A forward dataflow problem is a set of inequations of the form
- [X(s) >= transf n X(n)]
if program point [s] is a successor of program point [n]
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index d426440..3d9f499 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -53,6 +53,23 @@ Local Open Scope error_monad_scope.
Set Implicit Arguments.
+(** Auxiliary function for initialization of global variables. *)
+
+Function store_zeros (m: mem) (b: block) (p: Z) (n: Z) {wf (Zwf 0) n}: option mem :=
+ if zle n 0 then Some m else
+ match Mem.store Mint8unsigned m b p Vzero with
+ | Some m' => store_zeros m' b (p + 1) (n - 1)
+ | None => None
+ end.
+Proof.
+ intros. red. omega.
+ apply Zwf_well_founded.
+Qed.
+
+(* To avoid useless definitions of inductors in extracted code. *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
Module Genv.
(** * Global environments *)
@@ -486,18 +503,6 @@ Proof.
destruct i; simpl; try omega. generalize (Zle_max_r z 0). omega.
Qed.
-Function store_zeros (m: mem) (b: block) (p: Z) (n: Z) {wf (Zwf 0) n}: option mem :=
- if zle n 0 then Some m else
- let n' := n - 1 in
- match Mem.store Mint8unsigned m b p Vzero with
- | Some m' => store_zeros m' b (p + 1) n'
- | None => None
- end.
-Proof.
- intros. red. omega.
- apply Zwf_well_founded.
-Qed.
-
Definition store_init_data (m: mem) (b: block) (p: Z) (id: init_data) : option mem :=
match id with
| Init_int8 n => Mem.store Mint8unsigned m b p (Vint n)
diff --git a/common/Memory.v b/common/Memory.v
index 04a3dda..bfaf67d 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -36,6 +36,10 @@ Require Import Values.
Require Export Memdata.
Require Export Memtype.
+(* To avoid useless definitions of inductors in extracted code. *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
Local Notation "a # b" := (ZMap.get b a) (at level 1).
Module Mem <: MEM.
diff --git a/common/Switch.v b/common/Switch.v
index 0ba6186..3e25851 100644
--- a/common/Switch.v
+++ b/common/Switch.v
@@ -17,14 +17,34 @@
to comparison trees. *)
Require Import EqNat.
-Require Import FMaps.
-Require FMapAVL.
Require Import Coqlib.
+Require Import Maps.
Require Import Integers.
-Require Import Ordered.
-Module IntMap := FMapAVL.Make(OrderedInt).
-Module IntMapF := FMapFacts.Facts(IntMap).
+Module IntIndexed <: INDEXED_TYPE.
+
+ Definition t := int.
+
+ Definition index (n: int) : positive :=
+ match Int.unsigned n with
+ | Z0 => xH
+ | Zpos p => xO p
+ | Zneg p => xI p (**r never happens *)
+ end.
+
+ Lemma index_inj: forall n m, index n = index m -> n = m.
+ Proof.
+ unfold index; intros.
+ rewrite <- (Int.repr_unsigned n). rewrite <- (Int.repr_unsigned m).
+ f_equal.
+ destruct (Int.unsigned n); destruct (Int.unsigned m); congruence.
+ Qed.
+
+ Definition eq := Int.eq_dec.
+
+End IntIndexed.
+
+Module IntMap := IMap(IntIndexed).
(** A multi-way branch is composed of a list of (key, action) pairs,
plus a default action. *)
@@ -93,14 +113,14 @@ Fixpoint split_eq (pivot: int) (cases: table)
else (same, (key, act) :: others)
end.
-Fixpoint split_between (ofs sz: int) (cases: table)
+Fixpoint split_between (dfl: nat) (ofs sz: int) (cases: table)
{struct cases} : IntMap.t nat * table :=
match cases with
- | nil => (IntMap.empty nat, nil)
+ | nil => (IntMap.init dfl, nil)
| (key, act) :: rem =>
- let (inside, outside) := split_between ofs sz rem in
+ let (inside, outside) := split_between dfl ofs sz rem in
if Int.ltu (Int.sub key ofs) sz
- then (IntMap.add key act inside, outside)
+ then (IntMap.set key act inside, outside)
else (inside, (key, act) :: outside)
end.
@@ -110,13 +130,13 @@ Definition refine_low_bound (v lo: Z) :=
Definition refine_high_bound (v hi: Z) :=
if zeq v hi then hi - 1 else hi.
-Fixpoint validate_jumptable (cases: IntMap.t nat) (default: nat)
+Fixpoint validate_jumptable (cases: IntMap.t nat)
(tbl: list nat) (n: int) {struct tbl} : bool :=
match tbl with
| nil => true
| act :: rem =>
- beq_nat act (match IntMap.find n cases with Some a => a | None => default end)
- && validate_jumptable cases default rem (Int.add n Int.one)
+ beq_nat act (IntMap.get n cases)
+ && validate_jumptable cases rem (Int.add n Int.one)
end.
Fixpoint validate (default: nat) (cases: table) (t: comptree)
@@ -147,11 +167,11 @@ Fixpoint validate (default: nat) (cases: table) (t: comptree)
end
| CTjumptable ofs sz tbl t' =>
let tbl_len := list_length_z tbl in
- match split_between ofs sz cases with
+ match split_between default ofs sz cases with
| (inside, outside) =>
zle (Int.unsigned sz) tbl_len
&& zle tbl_len Int.max_signed
- && validate_jumptable inside default tbl ofs
+ && validate_jumptable inside tbl ofs
&& validate default outside t' lo hi
end
end.
@@ -207,33 +227,33 @@ Qed.
Lemma split_between_prop:
forall v default ofs sz cases inside outside,
- split_between ofs sz cases = (inside, outside) ->
+ split_between default ofs sz cases = (inside, outside) ->
switch_target v default cases =
(if Int.ltu (Int.sub v ofs) sz
- then match IntMap.find v inside with Some a => a | None => default end
+ then IntMap.get v inside
else switch_target v default outside).
Proof.
- induction cases; intros until outside; simpl.
- intros. inv H. simpl. destruct (Int.ltu (Int.sub v ofs) sz); auto.
- destruct a as [key act]. case_eq (split_between ofs sz cases). intros ins outs SEQ.
- rewrite (IHcases _ _ SEQ).
- case_eq (Int.ltu (Int.sub key ofs) sz); intros; inv H0; simpl.
- rewrite IntMapF.add_o.
- predSpec Int.eq Int.eq_spec v key.
- subst v. rewrite H. rewrite dec_eq_true. auto.
- rewrite dec_eq_false; auto.
- case_eq (Int.ltu (Int.sub v ofs) sz); intros; auto.
- predSpec Int.eq Int.eq_spec v key.
- subst v. congruence.
- auto.
+ induction cases; intros until outside; simpl; intros SEQ.
+- inv SEQ. destruct (Int.ltu (Int.sub v ofs) sz); auto. rewrite IntMap.gi. auto.
+- destruct a as [key act].
+ destruct (split_between default ofs sz cases) as [ins outs].
+ erewrite IHcases; eauto.
+ destruct (Int.ltu (Int.sub key ofs) sz) eqn:LT; inv SEQ.
+ + predSpec Int.eq Int.eq_spec v key.
+ subst v. rewrite LT. rewrite IntMap.gss. auto.
+ destruct (Int.ltu (Int.sub v ofs) sz).
+ rewrite IntMap.gso; auto.
+ auto.
+ + simpl. destruct (Int.ltu (Int.sub v ofs) sz) eqn:LT'.
+ rewrite Int.eq_false. auto. congruence.
+ auto.
Qed.
Lemma validate_jumptable_correct_rec:
- forall cases default tbl base v,
- validate_jumptable cases default tbl base = true ->
+ forall cases tbl base v,
+ validate_jumptable cases tbl base = true ->
0 <= Int.unsigned v < list_length_z tbl ->
- list_nth_z tbl (Int.unsigned v) =
- Some(match IntMap.find (Int.add base v) cases with Some a => a | None => default end).
+ list_nth_z tbl (Int.unsigned v) = Some(IntMap.get (Int.add base v) cases).
Proof.
induction tbl; intros until v; simpl.
unfold list_length_z; simpl. intros. omegaContradiction.
@@ -254,16 +274,15 @@ Proof.
Qed.
Lemma validate_jumptable_correct:
- forall cases default tbl ofs v sz,
- validate_jumptable cases default tbl ofs = true ->
+ forall cases tbl ofs v sz,
+ validate_jumptable cases tbl ofs = true ->
Int.ltu (Int.sub v ofs) sz = true ->
Int.unsigned sz <= list_length_z tbl ->
- list_nth_z tbl (Int.unsigned (Int.sub v ofs)) =
- Some(match IntMap.find v cases with Some a => a | None => default end).
+ list_nth_z tbl (Int.unsigned (Int.sub v ofs)) = Some(IntMap.get v cases).
Proof.
intros.
exploit Int.ltu_inv; eauto. intros.
- rewrite (validate_jumptable_correct_rec cases default tbl ofs).
+ rewrite (validate_jumptable_correct_rec cases tbl ofs).
rewrite Int.sub_add_opp. rewrite Int.add_permut. rewrite <- Int.sub_add_opp.
rewrite Int.sub_idem. rewrite Int.add_zero. auto.
auto.
@@ -312,7 +331,7 @@ Opaque Int.sub.
eapply IHt1. eauto. omega.
eapply IHt2. eauto. omega.
(* jumptable node *)
- case_eq (split_between i i0 cases). intros ins outs EQ V RANGE.
+ case_eq (split_between default i i0 cases). intros ins outs EQ V RANGE.
destruct (andb_prop _ _ V). clear V.
destruct (andb_prop _ _ H). clear H.
destruct (andb_prop _ _ H1). clear H1.
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 4f697b9..d99e20f 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -62,6 +62,7 @@ module P = struct
let gt x y = (Pos.compare x y = Gt)
let le x y = (Pos.compare x y <> Gt)
let ge x y = (Pos.compare x y <> Lt)
+ let compare x y = match Pos.compare x y with Lt -> -1 | Eq -> 0 | Gt -> 1
let rec to_int = function
| Coq_xI p -> (to_int p lsl 1) + 1
@@ -129,6 +130,7 @@ module Z = struct
let gt x y = (Z.compare x y = Gt)
let le x y = (Z.compare x y <> Gt)
let ge x y = (Z.compare x y <> Lt)
+ let compare x y = match Z.compare x y with Lt -> -1 | Eq -> 0 | Gt -> 1
let to_int = function
| Z0 -> 0
diff --git a/lib/Heaps.v b/lib/Heaps.v
index a5c0d61..0ee07a5 100644
--- a/lib/Heaps.v
+++ b/lib/Heaps.v
@@ -25,6 +25,10 @@ Require Import Coqlib.
Require Import FSets.
Require Import Ordered.
+(* To avoid useless definitions of inductors in extracted code. *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
Module SplayHeapSet(E: OrderedType).
(** "Raw" implementation. The "is a binary search tree" invariant
@@ -36,7 +40,7 @@ Inductive heap: Type :=
| Empty
| Node (l: heap) (x: E.t) (r: heap).
-Function partition (pivot: E.t) (h: heap) { struct h } : heap * heap :=
+Fixpoint partition (pivot: E.t) (h: heap) { struct h } : heap * heap :=
match h with
| Empty => (Empty, Empty)
| Node a x b =>
@@ -83,7 +87,7 @@ Fixpoint findMin (h: heap) : option E.t :=
| Node a x b => findMin a
end.
-Function deleteMin (h: heap) : heap :=
+Fixpoint deleteMin (h: heap) : heap :=
match h with
| Empty => Empty
| Node Empty x b => b
@@ -98,7 +102,7 @@ Fixpoint findMax (h: heap) : option E.t :=
| Node a x b => findMax b
end.
-Function deleteMax (h: heap) : heap :=
+Fixpoint deleteMax (h: heap) : heap :=
match h with
| Empty => Empty
| Node b x Empty => b
@@ -106,6 +110,13 @@ Function deleteMax (h: heap) : heap :=
| Node a x (Node b y c) => Node (Node a x b) y (deleteMax c)
end.
+(** Induction principles for some of the operators. *)
+
+Scheme heap_ind := Induction for heap Sort Prop.
+Functional Scheme partition_ind := Induction for partition Sort Prop.
+Functional Scheme deleteMin_ind := Induction for deleteMin Sort Prop.
+Functional Scheme deleteMax_ind := Induction for deleteMax Sort Prop.
+
(** Specification *)
Fixpoint In (x: E.t) (h: heap) : Prop :=
@@ -191,50 +202,38 @@ Lemma In_partition:
forall h, bst h -> (In x h <-> In x (fst (partition pivot h)) \/ In x (snd (partition pivot h))).
Proof.
intros x pivot NEQ h0. functional induction (partition pivot h0); simpl; intros.
- tauto.
- intuition. elim NEQ. eapply E.eq_trans; eauto.
- intuition.
- intuition. elim NEQ. eapply E.eq_trans; eauto.
- rewrite e3 in IHp; simpl in IHp. intuition.
- rewrite e3 in IHp; simpl in IHp. intuition.
- intuition.
- intuition. elim NEQ. eapply E.eq_trans; eauto.
- rewrite e3 in IHp; simpl in IHp. intuition.
- rewrite e3 in IHp; simpl in IHp. intuition.
+- tauto.
+- tauto.
+- rewrite e3 in *; simpl in *; intuition.
+- intuition. elim NEQ. eapply E.eq_trans; eauto.
+- rewrite e3 in *; simpl in *; intuition.
+- intuition. elim NEQ. eapply E.eq_trans; eauto.
+- intuition.
+- rewrite e3 in *; simpl in *; intuition.
+- intuition. elim NEQ. eapply E.eq_trans; eauto.
+- rewrite e3 in *; simpl in *; intuition.
Qed.
Lemma partition_lt:
forall x pivot h,
lt_heap h x -> lt_heap (fst (partition pivot h)) x /\ lt_heap (snd (partition pivot h)) x.
Proof.
- intros x pivot h0. functional induction (partition pivot h0); simpl.
- tauto.
- tauto.
- tauto.
- tauto.
- rewrite e3 in IHp; simpl in IHp. tauto.
- rewrite e3 in IHp; simpl in IHp. tauto.
- tauto.
- tauto.
- rewrite e3 in IHp; simpl in IHp. tauto.
- rewrite e3 in IHp; simpl in IHp. tauto.
+ intros x pivot h0. functional induction (partition pivot h0); simpl; try tauto.
+- rewrite e3 in *; simpl in *; tauto.
+- rewrite e3 in *; simpl in *; tauto.
+- rewrite e3 in *; simpl in *; tauto.
+- rewrite e3 in *; simpl in *; tauto.
Qed.
Lemma partition_gt:
forall x pivot h,
gt_heap h x -> gt_heap (fst (partition pivot h)) x /\ gt_heap (snd (partition pivot h)) x.
Proof.
- intros x pivot h0. functional induction (partition pivot h0); simpl.
- tauto.
- tauto.
- tauto.
- tauto.
- rewrite e3 in IHp; simpl in IHp. tauto.
- rewrite e3 in IHp; simpl in IHp. tauto.
- tauto.
- tauto.
- rewrite e3 in IHp; simpl in IHp. tauto.
- rewrite e3 in IHp; simpl in IHp. tauto.
+ intros x pivot h0. functional induction (partition pivot h0); simpl; try tauto.
+- rewrite e3 in *; simpl in *; tauto.
+- rewrite e3 in *; simpl in *; tauto.
+- rewrite e3 in *; simpl in *; tauto.
+- rewrite e3 in *; simpl in *; tauto.
Qed.
Lemma partition_split:
@@ -242,28 +241,32 @@ Lemma partition_split:
bst h -> lt_heap (fst (partition pivot h)) pivot /\ gt_heap (snd (partition pivot h)) pivot.
Proof.
intros pivot h0. functional induction (partition pivot h0); simpl.
- tauto.
- intuition. eapply lt_heap_trans; eauto. red; auto. eapply gt_heap_trans; eauto. red; left; apply E.eq_sym; auto.
- intuition. eapply lt_heap_trans; eauto. red; auto.
- intuition. eapply lt_heap_trans; eauto. red; auto.
- eapply lt_heap_trans; eauto. red; auto.
- apply gt_heap_trans with y; auto. red. left; apply E.eq_sym; auto.
- rewrite e3 in IHp; simpl in IHp. intuition.
- eapply lt_heap_trans; eauto. red; auto.
- eapply lt_heap_trans; eauto. red; auto.
- rewrite e3 in IHp; simpl in IHp. intuition.
- eapply lt_heap_trans; eauto. red; auto.
- apply gt_heap_trans with y; eauto. red; auto.
- intuition. eapply gt_heap_trans; eauto. red; auto.
- intuition. apply lt_heap_trans with y; eauto. red; auto.
- eapply gt_heap_trans; eauto. red; left; apply E.eq_sym; auto.
- eapply gt_heap_trans; eauto. red; auto.
- rewrite e3 in IHp; simpl in IHp. intuition.
- apply lt_heap_trans with y; eauto. red; auto.
- eapply gt_heap_trans; eauto. red; auto.
- rewrite e3 in IHp; simpl in IHp. intuition.
- apply gt_heap_trans with y; eauto. red; auto.
- apply gt_heap_trans with x; eauto. red; auto.
+- tauto.
+- intuition. eapply lt_heap_trans; eauto. red; auto.
+- rewrite e3 in *; simpl in *. intuition.
+ eapply lt_heap_trans; eauto. red; auto.
+ eapply lt_heap_trans; eauto. red; auto.
+- intuition.
+ eapply lt_heap_trans; eauto. red; auto.
+ eapply lt_heap_trans; eauto. red; auto.
+ eapply gt_heap_trans with y; eauto. red. left. apply E.eq_sym; auto.
+- rewrite e3 in *; simpl in *; intuition.
+ eapply lt_heap_trans; eauto. red; auto.
+ eapply gt_heap_trans with y; eauto. red; auto.
+- intuition.
+ eapply lt_heap_trans; eauto. red; auto.
+ eapply gt_heap_trans; eauto. red; auto.
+- intuition. eapply gt_heap_trans; eauto. red; auto.
+- rewrite e3 in *; simpl in *. intuition.
+ eapply lt_heap_trans with y; eauto. red; auto.
+ eapply gt_heap_trans; eauto. red; auto.
+- intuition.
+ eapply lt_heap_trans with y; eauto. red; auto.
+ eapply gt_heap_trans; eauto. red; auto.
+ eapply gt_heap_trans with x; eauto. red; auto.
+- rewrite e3 in *; simpl in *; intuition.
+ eapply gt_heap_trans; eauto. red; auto.
+ eapply gt_heap_trans; eauto. red; auto.
Qed.
Lemma partition_bst:
@@ -271,25 +274,19 @@ Lemma partition_bst:
bst h ->
bst (fst (partition pivot h)) /\ bst (snd (partition pivot h)).
Proof.
- intros pivot h0. functional induction (partition pivot h0); simpl.
- tauto.
- tauto.
- tauto.
- tauto.
- rewrite e3 in IHp; simpl in IHp. intuition.
+ intros pivot h0. functional induction (partition pivot h0); simpl; try tauto.
+- rewrite e3 in *; simpl in *. intuition.
apply lt_heap_trans with x; auto. red; auto.
generalize (partition_gt y pivot b2 H7). rewrite e3; simpl. tauto.
- rewrite e3 in IHp; simpl in IHp. intuition.
+- rewrite e3 in *; simpl in *. intuition.
generalize (partition_gt x pivot b1 H3). rewrite e3; simpl. tauto.
generalize (partition_lt y pivot b1 H4). rewrite e3; simpl. tauto.
- tauto.
- tauto.
- rewrite e3 in IHp; simpl in IHp. intuition.
+- rewrite e3 in *; simpl in *. intuition.
generalize (partition_gt y pivot a2 H6). rewrite e3; simpl. tauto.
generalize (partition_lt x pivot a2 H8). rewrite e3; simpl. tauto.
- rewrite e3 in IHp; simpl in IHp. intuition.
+- rewrite e3 in *; simpl in *. intuition.
generalize (partition_lt y pivot a1 H3). rewrite e3; simpl. tauto.
- apply gt_heap_trans with x; auto. red. auto.
+ apply gt_heap_trans with x; auto. red; auto.
Qed.
(** Properties of [insert] *)
@@ -322,11 +319,12 @@ Qed.
Lemma deleteMin_lt:
forall x h, lt_heap h x -> lt_heap (deleteMin h) x.
Proof.
- intros x h0. functional induction (deleteMin h0); simpl; intros.
+Opaque deleteMin.
+ intros x h0. functional induction (deleteMin h0) ; simpl; intros.
auto.
tauto.
- tauto.
- intuition.
+ tauto.
+ intuition. apply IHh. simpl. tauto.
Qed.
Lemma deleteMin_bst:
@@ -337,8 +335,9 @@ Proof.
tauto.
tauto.
intuition.
- apply deleteMin_lt; auto.
- apply gt_heap_trans with y; auto. red; auto.
+ apply IHh. simpl; auto.
+ apply deleteMin_lt; auto. simpl; auto.
+ apply gt_heap_trans with y; auto. red; auto.
Qed.
Lemma In_deleteMin:
@@ -346,11 +345,12 @@ Lemma In_deleteMin:
findMin h = Some x ->
(In y h <-> E.eq y x \/ In y (deleteMin h)).
Proof.
+Transparent deleteMin.
intros y x h0. functional induction (deleteMin h0); simpl; intros.
- congruence.
+ discriminate.
inv H. tauto.
inv H. tauto.
- destruct a. contradiction. tauto.
+ destruct _x. inv H. simpl. tauto. generalize (IHh H). simpl. tauto.
Qed.
Lemma gt_heap_In:
@@ -392,11 +392,12 @@ Qed.
Lemma deleteMax_gt:
forall x h, gt_heap h x -> gt_heap (deleteMax h) x.
Proof.
+Opaque deleteMax.
intros x h0. functional induction (deleteMax h0); simpl; intros.
auto.
tauto.
tauto.
- intuition.
+ intuition. apply IHh. simpl. tauto.
Qed.
Lemma deleteMax_bst:
@@ -407,8 +408,9 @@ Proof.
tauto.
tauto.
intuition.
+ apply IHh. simpl; auto.
apply lt_heap_trans with x; auto. red; auto.
- apply deleteMax_gt; auto.
+ apply deleteMax_gt; auto. simpl; auto.
Qed.
Lemma In_deleteMax:
@@ -416,11 +418,12 @@ Lemma In_deleteMax:
findMax h = Some x ->
(In y h <-> E.eq y x \/ In y (deleteMax h)).
Proof.
+Transparent deleteMax.
intros y x h0. functional induction (deleteMax h0); simpl; intros.
congruence.
inv H. tauto.
inv H. tauto.
- destruct c. contradiction. tauto.
+ destruct _x1. inv H. simpl. tauto. generalize (IHh H). simpl. tauto.
Qed.
Lemma lt_heap_In:
diff --git a/lib/Integers.v b/lib/Integers.v
index 0575436..2c74e80 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -57,6 +57,10 @@ Module Type WORDSIZE.
Axiom wordsize_not_zero: wordsize <> 0%nat.
End WORDSIZE.
+(* To avoid useless definitions of inductors in extracted code. *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
Module Make(WS: WORDSIZE).
Definition wordsize: nat := WS.wordsize.
diff --git a/lib/Lattice.v b/lib/Lattice.v
index 51a7976..fd05b34 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -16,6 +16,10 @@ Require Import Coqlib.
Require Import Maps.
Require Import FSets.
+(* To avoid useless definitions of inductors in extracted code. *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
(** * Signatures of semi-lattices *)
(** A semi-lattice is a type [t] equipped with an equivalence relation [eq],
diff --git a/lib/Maps.v b/lib/Maps.v
index bd5c0e9..0c97ba5 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -34,6 +34,10 @@
Require Import Coqlib.
+(* To avoid useless definitions of inductors in extracted code. *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
Set Implicit Arguments.
(** * The abstract signatures of trees *)
@@ -42,8 +46,6 @@ Module Type TREE.
Variable elt: Type.
Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}.
Variable t: Type -> Type.
- Variable eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) ->
- forall (a b: t A), {a = b} + {a <> b}.
Variable empty: forall (A: Type), t A.
Variable get: forall (A: Type), elt -> t A -> option A.
Variable set: forall (A: Type), elt -> A -> t A -> t A.
@@ -202,18 +204,10 @@ Module PTree <: TREE.
.
Implicit Arguments Leaf [A].
Implicit Arguments Node [A].
+ Scheme tree_ind := Induction for tree Sort Prop.
Definition t := tree.
- Theorem eq : forall (A : Type),
- (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 : Type) := (Leaf : t A).
Fixpoint get (A : Type) (i : positive) (m : t A) {struct i} : option A :=
@@ -1084,14 +1078,6 @@ Module PMap <: MAP.
Definition t (A : Type) : Type := (A * PTree.t A)%type.
- Definition eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) ->
- forall (a b: t A), {a = b} + {a <> b}.
- Proof.
- intros.
- generalize (PTree.eq X). intros.
- decide equality.
- Qed.
-
Definition init (A : Type) (x : A) :=
(x, PTree.empty A).
@@ -1175,8 +1161,6 @@ Module IMap(X: INDEXED_TYPE).
Definition elt := X.t.
Definition elt_eq := X.eq.
Definition t : Type -> Type := PMap.t.
- Definition eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) ->
- forall (a b: t A), {a = b} + {a <> b} := PMap.eq.
Definition init (A: Type) (x: A) := PMap.init x.
Definition get (A: Type) (i: X.t) (m: t A) := PMap.get (X.index i) m.
Definition set (A: Type) (i: X.t) (v: A) (m: t A) := PMap.set (X.index i) v m.
diff --git a/lib/UnionFind.v b/lib/UnionFind.v
index 84d0348..46a886e 100644
--- a/lib/UnionFind.v
+++ b/lib/UnionFind.v
@@ -15,14 +15,16 @@
(** A persistent union-find data structure. *)
-Require Recdef.
-Require Setoid.
Require Coq.Program.Wf.
Require Import Coqlib.
Open Scope nat_scope.
Set Implicit Arguments.
+(* To avoid useless definitions of inductors in extracted code. *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
Module Type MAP.
Variable elt: Type.
Variable elt_eq: forall (x y: elt), {x=y} + {x<>y}.
@@ -151,20 +153,33 @@ Record unionfind : Type := mk { m: M.t elt; mwf: well_founded (order m) }.
Definition t := unionfind.
+Definition getlink (m: M.t elt) (a: elt) : {a' | M.get a m = Some a'} + {M.get a m = None}.
+Proof.
+ destruct (M.get a m). left. exists e; auto. right; auto.
+Defined.
+
(* The canonical representative of an element *)
Section REPR.
Variable uf: t.
-Function repr (a: elt) {wf (order uf.(m)) a} : elt :=
- match M.get a uf.(m) with
- | Some a' => repr a'
- | None => a
+Definition F_repr (a: elt) (rec: forall b, order uf.(m) b a -> elt) : elt :=
+ match getlink uf.(m) a with
+ | inleft (exist a' P) => rec a' P
+ | inright _ => a
end.
+
+Definition repr (a: elt) : elt := Fix uf.(mwf) (fun _ => elt) F_repr a.
+
+Lemma repr_unroll:
+ forall a, repr a = match M.get a uf.(m) with Some a' => repr a' | None => a end.
Proof.
- intros. auto.
- apply mwf.
+ intros. unfold repr at 1. rewrite Fix_eq.
+ unfold F_repr. destruct (getlink uf.(m) a) as [[a' P] | Q].
+ rewrite P; auto.
+ rewrite Q; auto.
+ intros. unfold F_repr. destruct (getlink (m uf) x) as [[a' P] | Q]; auto.
Qed.
Lemma repr_none:
@@ -172,8 +187,7 @@ Lemma repr_none:
M.get a uf.(m) = None ->
repr a = a.
Proof.
- intros.
- functional induction (repr a). congruence. auto.
+ intros. rewrite repr_unroll. rewrite H; auto.
Qed.
Lemma repr_some:
@@ -181,14 +195,14 @@ Lemma repr_some:
M.get a uf.(m) = Some a' ->
repr a = repr a'.
Proof.
- intros.
- functional induction (repr a). congruence. congruence.
+ intros. rewrite repr_unroll. rewrite H; auto.
Qed.
Lemma repr_res_none:
forall (a: elt), M.get (repr a) uf.(m) = None.
Proof.
- intros. functional induction (repr a). auto. auto.
+ apply (well_founded_ind (mwf uf)). intros.
+ rewrite repr_unroll. destruct (M.get x (m uf)) as [y|] eqn:X; auto.
Qed.
Lemma repr_canonical:
@@ -308,25 +322,23 @@ Definition identify := mk (M.set a b uf.(m)) identify_wf.
Lemma repr_identify_1:
forall x, repr uf x <> a -> repr identify x = repr uf x.
Proof.
- intros. functional induction (repr uf x).
-
- rewrite <- IHe; auto. apply repr_some. simpl. rewrite M.gsspec.
- destruct (M.elt_eq a0 a). congruence. auto.
-
- apply repr_none. simpl. rewrite M.gsspec. rewrite dec_eq_false; auto.
+ intros x0; pattern x0. apply (well_founded_ind (mwf uf)); intros.
+ rewrite (repr_unroll uf) in *.
+ destruct (M.get x (m uf)) as [a'|] eqn:X.
+ rewrite <- H; auto.
+ apply repr_some. simpl. rewrite M.gsspec. rewrite dec_eq_false; auto. congruence.
+ apply repr_none. simpl. rewrite M.gsspec. rewrite dec_eq_false; auto.
Qed.
Lemma repr_identify_2:
forall x, repr uf x = a -> repr identify x = repr uf b.
Proof.
- intros. functional induction (repr uf x).
-
- rewrite <- IHe; auto. apply repr_some. simpl. rewrite M.gsspec.
- rewrite dec_eq_false; auto. congruence.
-
- transitivity (repr identify b). apply repr_some. simpl.
- rewrite M.gsspec. apply dec_eq_true.
- apply repr_identify_1. auto.
+ intros x0; pattern x0. apply (well_founded_ind (mwf uf)); intros.
+ rewrite (repr_unroll uf) in H0. destruct (M.get x (m uf)) as [a'|] eqn:X.
+ rewrite <- (H a'); auto.
+ apply repr_some. simpl. rewrite M.gsspec. rewrite dec_eq_false; auto. congruence.
+ subst x. rewrite (repr_unroll identify). simpl. rewrite M.gsspec.
+ rewrite dec_eq_true. apply repr_identify_1. auto.
Qed.
End IDENTIFY.
@@ -474,14 +486,22 @@ Section PATHLEN.
Variable uf: t.
-Function pathlen (a: elt) {wf (order uf.(m)) a} : nat :=
- match M.get a uf.(m) with
- | Some a' => S (pathlen a')
- | None => O
+Definition F_pathlen (a: elt) (rec: forall b, order uf.(m) b a -> nat) : nat :=
+ match getlink uf.(m) a with
+ | inleft (exist a' P) => S (rec a' P)
+ | inright _ => O
end.
+
+Definition pathlen (a: elt) : nat := Fix uf.(mwf) (fun _ => nat) F_pathlen a.
+
+Lemma pathlen_unroll:
+ forall a, pathlen a = match M.get a uf.(m) with Some a' => S(pathlen a') | None => O end.
Proof.
- intros. auto.
- apply mwf.
+ intros. unfold pathlen at 1. rewrite Fix_eq.
+ unfold F_pathlen. destruct (getlink uf.(m) a) as [[a' P] | Q].
+ rewrite P; auto.
+ rewrite Q; auto.
+ intros. unfold F_pathlen. destruct (getlink (m uf) x) as [[a' P] | Q]; auto.
Qed.
Lemma pathlen_none:
@@ -489,8 +509,7 @@ Lemma pathlen_none:
M.get a uf.(m) = None ->
pathlen a = 0.
Proof.
- intros.
- functional induction (pathlen a). congruence. auto.
+ intros. rewrite pathlen_unroll. rewrite H; auto.
Qed.
Lemma pathlen_some:
@@ -498,8 +517,7 @@ Lemma pathlen_some:
M.get a uf.(m) = Some a' ->
pathlen a = S (pathlen a').
Proof.
- intros.
- functional induction (pathlen a). congruence. congruence.
+ intros. rewrite pathlen_unroll. rewrite H; auto.
Qed.
Lemma pathlen_zero:
@@ -507,9 +525,8 @@ Lemma pathlen_zero:
Proof.
intros; split; intros.
apply pathlen_none. rewrite <- H. apply repr_res_none.
- functional induction (pathlen a).
- congruence.
- apply repr_none. auto.
+ apply repr_none. rewrite pathlen_unroll in H.
+ destruct (M.get a (m uf)); congruence.
Qed.
End PATHLEN.
@@ -529,23 +546,19 @@ Proof.
intros. unfold merge.
destruct (M.elt_eq (repr uf a) (repr uf b)).
auto.
- functional induction (pathlen (identify uf (repr uf a) b (repr_res_none uf a) (sym_not_equal n)) x).
- simpl in e. rewrite M.gsspec in e.
- destruct (M.elt_eq a0 (repr uf a)).
- inversion e; subst a'; clear e.
- replace (repr uf a0) with (repr uf a). rewrite dec_eq_true.
- rewrite IHn0. rewrite dec_eq_false; auto.
- rewrite (pathlen_none uf a0). omega. subst a0. apply repr_res_none.
- subst a0. rewrite repr_canonical; auto.
- rewrite (pathlen_some uf a0 a'); auto.
- rewrite IHn0.
- replace (repr uf a0) with (repr uf a').
- destruct (M.elt_eq (repr uf a') (repr uf a)); omega.
- symmetry. apply repr_some; auto.
-
- simpl in e. rewrite M.gsspec in e. destruct (M.elt_eq a0 (repr uf a)).
- congruence. rewrite (repr_none uf a0); auto.
- rewrite dec_eq_false; auto. symmetry. apply pathlen_none; auto.
+ set (uf' := identify uf (repr uf a) b (repr_res_none uf a) (not_eq_sym n)).
+ pattern x. apply (well_founded_ind (mwf uf')); intros.
+ rewrite (pathlen_unroll uf'). destruct (M.get x0 (m uf')) as [x'|] eqn:G.
+ rewrite H; auto. simpl in G. rewrite M.gsspec in G.
+ destruct (M.elt_eq x0 (repr uf a)). rewrite e. rewrite repr_canonical. rewrite dec_eq_true.
+ inversion G. subst x'. rewrite dec_eq_false; auto.
+ replace (pathlen uf (repr uf a)) with 0. omega.
+ symmetry. apply pathlen_none. apply repr_res_none.
+ rewrite (repr_unroll uf x0), (pathlen_unroll uf x0); rewrite G.
+ destruct (M.elt_eq (repr uf x') (repr uf a)); omega.
+ simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x0 (repr uf a)); try discriminate.
+ rewrite (repr_none uf x0) by auto. rewrite dec_eq_false; auto.
+ symmetry. apply pathlen_zero; auto. apply repr_none; auto.
Qed.
Lemma pathlen_gt_merge:
@@ -604,13 +617,16 @@ Definition compress := mk (M.set a b uf.(m)) compress_wf.
Lemma repr_compress:
forall x, repr compress x = repr uf x.
Proof.
- intros. functional induction (repr compress x).
- simpl in e. rewrite M.gsspec in e. destruct (M.elt_eq a0 a).
- subst a0. injection e; intros. subst a'. rewrite IHe. rewrite <- a_repr_b.
- apply repr_canonical.
- rewrite IHe. symmetry. apply repr_some; auto.
- simpl in e. rewrite M.gsspec in e. destruct (M.elt_eq a0 a).
- congruence. symmetry. apply repr_none. auto.
+ apply (well_founded_ind (mwf compress)); intros.
+ rewrite (repr_unroll compress).
+ destruct (M.get x (m compress)) as [y|] eqn:G.
+ rewrite H; auto.
+ simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x a).
+ inversion G. subst x y. rewrite <- a_repr_b. apply repr_canonical.
+ symmetry; apply repr_some; auto.
+ simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x a).
+ congruence.
+ symmetry; apply repr_none; auto.
Qed.
End COMPRESS.