diff options
| -rw-r--r-- | backend/Kildall.v | 4 | ||||
| -rw-r--r-- | common/Globalenvs.v | 29 | ||||
| -rw-r--r-- | common/Memory.v | 4 | ||||
| -rw-r--r-- | common/Switch.v | 97 | ||||
| -rw-r--r-- | lib/Camlcoq.ml | 2 | ||||
| -rw-r--r-- | lib/Heaps.v | 161 | ||||
| -rw-r--r-- | lib/Integers.v | 4 | ||||
| -rw-r--r-- | lib/Lattice.v | 4 | ||||
| -rw-r--r-- | lib/Maps.v | 26 | ||||
| -rw-r--r-- | lib/UnionFind.v | 144 |
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], @@ -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. |