From b9dfe18fb99d9fd0e8918c160ee297755c5fca59 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 16 Nov 2021 09:38:54 +0100 Subject: An improved PTree data structure (#420) This PR replaces the "PTree" data structure used in lib/Maps.v by the canonical binary tries data structure proposed by A. W. Appel and described in the paper "Efficient Extensional Binary Tries", https://arxiv.org/abs/2110.05063 The new implementation is more memory-efficient and a bit faster, resulting in reduced compilation times (-5% on typical C programs, up to -10% on very large C functions). It also enjoys the extensionality property (two tries mapping equal keys to equal data are equal), which simplifies some proofs. --- lib/Lattice.v | 314 ++++++++------- lib/Maps.v | 1226 +++++++++++++++++++++++++++++++++++---------------------- 2 files changed, 902 insertions(+), 638 deletions(-) (limited to 'lib') diff --git a/lib/Lattice.v b/lib/Lattice.v index 6fed3f21..aea331a0 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -3,6 +3,7 @@ (* The Compcert verified compiler *) (* *) (* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Andrew W. Appel, Princeton University *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) @@ -140,7 +141,7 @@ Definition bot : t := PTree.empty _. Lemma get_bot: forall p, get p bot = L.bot. Proof. - unfold bot, get; intros; simpl. rewrite PTree.gempty. auto. + intros; reflexivity. Qed. Lemma ge_bot: forall x, ge x bot. @@ -148,13 +149,7 @@ Proof. unfold ge; intros. rewrite get_bot. apply L.ge_bot. Qed. -(** A [combine] operation over the type [PTree.t L.t] that attempts - to share its result with its arguments. *) - -Section COMBINE. - -Variable f: option L.t -> option L.t -> option L.t. -Hypothesis f_none_none: f None None = None. +(** Equivalence modulo L.eq *) Definition opt_eq (ox oy: option L.t) : Prop := match ox, oy with @@ -194,182 +189,181 @@ Proof. auto. Qed. -Definition tree_eq (m1 m2: PTree.t L.t) : Prop := - forall i, opt_eq (PTree.get i m1) (PTree.get i m2). - -Lemma tree_eq_refl: forall m, tree_eq m m. -Proof. intros; red; intros; apply opt_eq_refl. Qed. - -Lemma tree_eq_sym: forall m1 m2, tree_eq m1 m2 -> tree_eq m2 m1. -Proof. intros; red; intros; apply opt_eq_sym; auto. Qed. +Local Hint Resolve opt_beq_correct opt_eq_refl opt_eq_sym : combine. -Lemma tree_eq_trans: forall m1 m2 m3, tree_eq m1 m2 -> tree_eq m2 m3 -> tree_eq m1 m3. -Proof. intros; red; intros; apply opt_eq_trans with (PTree.get i m2); auto. Qed. - -Lemma tree_eq_node: - forall l1 o1 r1 l2 o2 r2, - tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 -> - tree_eq (PTree.Node l1 o1 r1) (PTree.Node l2 o2 r2). -Proof. - intros; red; intros. destruct i; simpl; auto. -Qed. - -Lemma tree_eq_node': - forall l1 o1 r1 l2 o2 r2, - tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 -> - tree_eq (PTree.Node l1 o1 r1) (PTree.Node' l2 o2 r2). -Proof. - intros; red; intros. rewrite PTree.gnode'. apply tree_eq_node; auto. -Qed. +(** A [combine] operation over the type [PTree.t L.t] that attempts + to share its result with its arguments. *) -Lemma tree_eq_node'': - forall l1 o1 r1 l2 o2 r2, - tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 -> - tree_eq (PTree.Node' l1 o1 r1) (PTree.Node' l2 o2 r2). -Proof. - intros; red; intros. repeat rewrite PTree.gnode'. apply tree_eq_node; auto. -Qed. +Section COMBINE. -Hint Resolve opt_beq_correct opt_eq_refl opt_eq_sym - tree_eq_refl tree_eq_sym - tree_eq_node tree_eq_node' tree_eq_node'' : combine. +Variable f: option L.t -> option L.t -> option L.t. +Hypothesis f_none_none: f None None = None. -Inductive changed: Type := Unchanged | Changed (m: PTree.t L.t). +Inductive changed : Type := + | Same + | Same1 + | Same2 + | Changed (m: PTree.t L.t). + +Let Node_combine_l (l1: PTree.t L.t) (lres: changed) (o1: option L.t) + (r1: PTree.t L.t) (rres: changed) : changed := + let o' := f o1 None in + match lres, rres with + | Same1, Same1 => + if opt_beq o' o1 then Same1 else Changed (PTree.Node l1 o' r1) + | Same1, Changed r' => Changed (PTree.Node l1 o' r') + | Changed l', Same1 => Changed (PTree.Node l' o' r1) + | Changed l', Changed r' => Changed (PTree.Node l' o' r') + | _, _ => Same (**r impossible cases *) + end. -Fixpoint combine_l (m : PTree.t L.t) {struct m} : changed := - match m with - | PTree.Leaf => - Unchanged - | PTree.Node l o r => - let o' := f o None in - match combine_l l, combine_l r with - | Unchanged, Unchanged => if opt_beq o' o then Unchanged else Changed (PTree.Node' l o' r) - | Unchanged, Changed r' => Changed (PTree.Node' l o' r') - | Changed l', Unchanged => Changed (PTree.Node' l' o' r) - | Changed l', Changed r' => Changed (PTree.Node' l' o' r') - end +Let xcombine_l (m: PTree.t L.t) : changed := + PTree.tree_rec Same1 Node_combine_l m. + +Let Node_combine_r (l1: PTree.t L.t) (lres: changed) (o1: option L.t) + (r1: PTree.t L.t) (rres: changed) : changed := + let o' := f None o1 in + match lres, rres with + | Same2, Same2 => + if opt_beq o' o1 then Same2 else Changed (PTree.Node l1 o' r1) + | Same2, Changed r' => Changed (PTree.Node l1 o' r') + | Changed l', Same2 => Changed (PTree.Node l' o' r1) + | Changed l', Changed r' => Changed (PTree.Node l' o' r') + | _, _ => Same (**r impossible cases *) end. -Lemma combine_l_eq: - forall m, - tree_eq (match combine_l m with Unchanged => m | Changed m' => m' end) - (PTree.xcombine_l f m). -Proof. - induction m; simpl. - auto with combine. - destruct (combine_l m1) as [ | l']; destruct (combine_l m2) as [ | r']; - auto with combine. - case_eq (opt_beq (f o None) o); auto with combine. -Qed. - -Fixpoint combine_r (m : PTree.t L.t) {struct m} : changed := - match m with - | PTree.Leaf => - Unchanged - | PTree.Node l o r => - let o' := f None o in - match combine_r l, combine_r r with - | Unchanged, Unchanged => if opt_beq o' o then Unchanged else Changed (PTree.Node' l o' r) - | Unchanged, Changed r' => Changed (PTree.Node' l o' r') - | Changed l', Unchanged => Changed (PTree.Node' l' o' r) - | Changed l', Changed r' => Changed (PTree.Node' l' o' r') +Let xcombine_r (m: PTree.t L.t) : changed := + PTree.tree_rec Same2 Node_combine_r m. + +Let Node_combine_2 + (l1: PTree.t L.t) (o1: option L.t) (r1: PTree.t L.t) + (l2: PTree.t L.t) (o2: option L.t) (r2: PTree.t L.t) + (lres: changed) (rres: changed) : changed := + let o := f o1 o2 in + match lres, rres with + | Same, Same => + match opt_beq o o1, opt_beq o o2 with + | true, true => Same + | true, false => Same1 + | false, true => Same2 + | false, false => Changed (PTree.Node l1 o r1) end + | Same, Same1 + | Same1, Same + | Same1, Same1 => + if opt_beq o o1 then Same1 else Changed (PTree.Node l1 o r1) + | Same, Same2 + | Same2, Same + | Same2, Same2 => + if opt_beq o o2 then Same2 else Changed (PTree.Node l2 o r2) + | Same, Changed m2 => Changed (PTree.Node l1 o m2) + | Same1, Same2 => Changed (PTree.Node l1 o r2) + | Same1, Changed m2 => Changed (PTree.Node l1 o m2) + | Same2, Same1 => Changed (PTree.Node l2 o r1) + | Same2, Changed m2 => Changed (PTree.Node l2 o m2) + | Changed m1, (Same|Same1) => Changed (PTree.Node m1 o r1) + | Changed m1, Same2 => Changed (PTree.Node m1 o r2) + | Changed m1, Changed m2 => Changed (PTree.Node m1 o m2) end. -Lemma combine_r_eq: - forall m, - tree_eq (match combine_r m with Unchanged => m | Changed m' => m' end) - (PTree.xcombine_r f m). +Definition xcombine := + PTree.tree_rec2 + Same + xcombine_r + xcombine_l + Node_combine_2. + +Definition tree_agree (m1 m2 m: PTree.t L.t) : Prop := + forall i, opt_eq m!i (f m1!i m2!i). + +Lemma tree_agree_node: forall l1 o1 r1 l2 o2 r2 l o r, + tree_agree l1 l2 l -> tree_agree r1 r2 r -> opt_eq (f o1 o2) o -> + tree_agree (PTree.Node l1 o1 r1) (PTree.Node l2 o2 r2) (PTree.Node l o r). Proof. - induction m; simpl. - auto with combine. - destruct (combine_r m1) as [ | l']; destruct (combine_r m2) as [ | r']; - auto with combine. - case_eq (opt_beq (f None o) o); auto with combine. + intros; red; intros. rewrite ! PTree.gNode. destruct i; auto using opt_eq_sym. Qed. -Inductive changed2 : Type := - | Same - | Same1 - | Same2 - | CC(m: PTree.t L.t). - -Fixpoint xcombine (m1 m2 : PTree.t L.t) {struct m1} : changed2 := - match m1, m2 with - | PTree.Leaf, PTree.Leaf => - Same - | PTree.Leaf, _ => - match combine_r m2 with - | Unchanged => Same2 - | Changed m => CC m - end - | _, PTree.Leaf => - match combine_l m1 with - | Unchanged => Same1 - | Changed m => CC m - end - | PTree.Node l1 o1 r1, PTree.Node l2 o2 r2 => - let o := f o1 o2 in - match xcombine l1 l2, xcombine r1 r2 with - | Same, Same => - match opt_beq o o1, opt_beq o o2 with - | true, true => Same - | true, false => Same1 - | false, true => Same2 - | false, false => CC(PTree.Node' l1 o r1) - end - | Same1, Same | Same, Same1 | Same1, Same1 => - if opt_beq o o1 then Same1 else CC(PTree.Node' l1 o r1) - | Same2, Same | Same, Same2 | Same2, Same2 => - if opt_beq o o2 then Same2 else CC(PTree.Node' l2 o r2) - | Same1, Same2 => CC(PTree.Node' l1 o r2) - | (Same|Same1), CC r => CC(PTree.Node' l1 o r) - | Same2, Same1 => CC(PTree.Node' l2 o r1) - | Same2, CC r => CC(PTree.Node' l2 o r) - | CC l, (Same|Same1) => CC(PTree.Node' l o r1) - | CC l, Same2 => CC(PTree.Node' l o r2) - | CC l, CC r => CC(PTree.Node' l o r) - end - end. - -Lemma xcombine_eq: - forall m1 m2, - match xcombine m1 m2 with - | Same => tree_eq m1 (PTree.combine f m1 m2) /\ tree_eq m2 (PTree.combine f m1 m2) - | Same1 => tree_eq m1 (PTree.combine f m1 m2) - | Same2 => tree_eq m2 (PTree.combine f m1 m2) - | CC m => tree_eq m (PTree.combine f m1 m2) +Local Hint Resolve tree_agree_node : combine. + +Lemma gxcombine_l: forall m, + match xcombine_l m with + | Same1 => forall i, opt_eq m!i (f m!i None) + | Changed m' => forall i, opt_eq m'!i (f m!i None) + | _ => False end. Proof. -Opaque combine_l combine_r PTree.xcombine_l PTree.xcombine_r. - induction m1; destruct m2; simpl. - split; apply tree_eq_refl. - generalize (combine_r_eq (PTree.Node m2_1 o m2_2)). - destruct (combine_r (PTree.Node m2_1 o m2_2)); auto. - generalize (combine_l_eq (PTree.Node m1_1 o m1_2)). - destruct (combine_l (PTree.Node m1_1 o m1_2)); auto. - generalize (IHm1_1 m2_1) (IHm1_2 m2_2). - destruct (xcombine m1_1 m2_1); - destruct (xcombine m1_2 m2_2); auto with combine; - intuition; case_eq (opt_beq (f o o0) o); case_eq (opt_beq (f o o0) o0); auto with combine. + unfold xcombine_l. induction m using PTree.tree_ind. +- simpl; intros. rewrite PTree.gempty, f_none_none. auto. +- rewrite PTree.unroll_tree_rec by auto. + destruct (PTree.tree_rec Same1 Node_combine_l l); + destruct (PTree.tree_rec Same1 Node_combine_l r); + try contradiction; + unfold Node_combine_l; + try (intros i; rewrite ! PTree.gNode; destruct i; auto with combine). + destruct (opt_beq (f o None) o) eqn:BEQ; intros i; rewrite ! PTree.gNode; destruct i; auto with combine. +Qed. + +Lemma gxcombine_r: forall m, + match xcombine_r m with + | Same2 => forall i, opt_eq m!i (f None m!i) + | Changed m' => forall i, opt_eq m'!i (f None m!i) + | _ => False + end. +Proof. + unfold xcombine_r. induction m using PTree.tree_ind. +- simpl; intros. rewrite PTree.gempty, f_none_none. auto. +- rewrite PTree.unroll_tree_rec by auto. + destruct (PTree.tree_rec Same2 Node_combine_r l); + destruct (PTree.tree_rec Same2 Node_combine_r r); + try contradiction; + unfold Node_combine_r; + try (intros i; rewrite ! PTree.gNode; destruct i; auto with combine). + destruct (opt_beq (f None o) o) eqn:BEQ; intros i; rewrite ! PTree.gNode; destruct i; auto with combine. +Qed. + +Inductive xcombine_spec (m1 m2: PTree.t L.t) : changed -> Prop := + | XCS_Same: + tree_agree m1 m2 m1 -> tree_agree m1 m2 m2 -> xcombine_spec m1 m2 Same + | XCS_Same1: + tree_agree m1 m2 m1 -> xcombine_spec m1 m2 Same1 + | XCS_Same2: + tree_agree m1 m2 m2 -> xcombine_spec m1 m2 Same2 + | XCS_Changed: forall m', + tree_agree m1 m2 m' -> xcombine_spec m1 m2 (Changed m'). + +Local Hint Constructors xcombine_spec : combine. + +Lemma gxcombine: forall m1 m2, xcombine_spec m1 m2 (xcombine m1 m2). +Proof. + Local Opaque opt_eq. + unfold xcombine. + induction m1 using PTree.tree_ind; induction m2 using PTree.tree_ind; intros. +- constructor; red; intros; rewrite ! PTree.gEmpty, f_none_none; auto with combine. +- rewrite PTree.unroll_tree_rec2_EN by auto. set (m2 := PTree.Node l o r). + generalize (gxcombine_r m2); destruct (xcombine_r m2); + try contradiction; constructor; auto. +- rewrite PTree.unroll_tree_rec2_NE by auto. set (m1 := PTree.Node l o r). + generalize (gxcombine_l m1); destruct (xcombine_l m1); + try contradiction; constructor; auto. +- rewrite PTree.unroll_tree_rec2_NN by auto. + clear IHm2 IHm3. specialize (IHm1 l0). specialize (IHm0 r0). + inv IHm1; inv IHm0; unfold Node_combine_2; auto with combine; + destruct (opt_beq (f o o0) o) eqn:E1; destruct (opt_beq (f o o0) o0) eqn:E2; + auto with combine. Qed. Definition combine (m1 m2: PTree.t L.t) : PTree.t L.t := match xcombine m1 m2 with | Same|Same1 => m1 | Same2 => m2 - | CC m => m + | Changed m => m end. -Lemma gcombine: +Theorem gcombine: forall m1 m2 i, opt_eq (PTree.get i (combine m1 m2)) (f (PTree.get i m1) (PTree.get i m2)). Proof. - intros. - assert (tree_eq (combine m1 m2) (PTree.combine f m1 m2)). - unfold combine. - generalize (xcombine_eq m1 m2). - destruct (xcombine m1 m2); tauto. - eapply opt_eq_trans. apply H. rewrite PTree.gcombine; auto. apply opt_eq_refl. + intros. unfold combine. + generalize (gxcombine m1 m2); intros XS; inv XS; auto. Qed. End COMBINE. @@ -526,7 +520,7 @@ Definition top := Top_except (PTree.empty L.t). Lemma get_top: forall p, get p top = L.top. Proof. - unfold top; intros; simpl. rewrite PTree.gempty. auto. + unfold top; intros; auto. Qed. Lemma ge_top: forall x, ge top x. diff --git a/lib/Maps.v b/lib/Maps.v index 3f43d102..f3330776 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -2,7 +2,8 @@ (* *) (* The Compcert verified compiler *) (* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Xavier Leroy and Damien Doligez, INRIA Paris-Rocquencourt *) +(* Andrew W. Appel, Princeton University *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) @@ -33,7 +34,6 @@ inefficient implementation of maps as functions is also provided. *) -Require Import Equivalence EquivDec. Require Import Coqlib. (* To avoid useless definitions of inductors in extracted code. *) @@ -65,14 +65,6 @@ Module Type TREE. Axiom gsspec: forall (A: Type) (i j: elt) (x: A) (m: t A), get i (set j x m) = if elt_eq i j then Some x else get i m. - (* We could implement the following, but it's not needed for the moment. - Hypothesis gsident: - forall (A: Type) (i: elt) (m: t A) (v: A), - get i m = Some v -> set i v m = m. - Hypothesis grident: - forall (A: Type) (i: elt) (m: t A) (v: A), - get i m = None -> remove i m = m. - *) Axiom grs: forall (A: Type) (i: elt) (m: t A), get i (remove i m) = None. Axiom gro: @@ -187,96 +179,208 @@ Module PTree <: TREE. Definition elt := positive. Definition elt_eq := peq. - Inductive tree (A : Type) : Type := - | Leaf : tree A - | Node : tree A -> option A -> tree A -> tree A. +(** ** Representation of trees *) + +(** The type [tree'] of nonempty trees. Each constructor is of the form + [NodeXYZ], where the bit [X] says whether there is a left subtree, + [Y] whether there is a value at this node, and [Z] whether there is + a right subtree. *) + + Inductive tree' (A: Type) : Type := + | Node001: tree' A -> tree' A + | Node010: A -> tree' A + | Node011: A -> tree' A -> tree' A + | Node100: tree' A -> tree' A + | Node101: tree' A -> tree' A ->tree' A + | Node110: tree' A -> A -> tree' A + | Node111: tree' A -> A -> tree' A -> tree' A. + + Inductive tree (A: Type) : Type := + | Empty : tree A + | Nodes: tree' A -> tree A. + + Arguments Node001 {A} _. + Arguments Node010 {A} _. + Arguments Node011 {A} _ _. + Arguments Node100 {A} _. + Arguments Node101 {A} _ _. + Arguments Node110 {A} _ _. + Arguments Node111 {A} _ _ _. - Arguments Leaf {A}. - Arguments Node [A]. - Scheme tree_ind := Induction for tree Sort Prop. + Arguments Empty {A}. + Arguments Nodes {A} _. + + Scheme tree'_ind := Induction for tree' Sort Prop. Definition t := tree. - Definition empty (A : Type) := (Leaf : t A). + (** A smart constructor for type [tree]: given a (possibly empty) + left subtree, a (possibly absent) value, and a (possibly empty) + right subtree, it builds the corresponding tree. *) + + Definition Node {A} (l: tree A) (o: option A) (r: tree A) : tree A := + match l,o,r with + | Empty, None, Empty => Empty + | Empty, None, Nodes r' => Nodes (Node001 r') + | Empty, Some x, Empty => Nodes (Node010 x) + | Empty, Some x, Nodes r' => Nodes (Node011 x r') + | Nodes l', None, Empty => Nodes (Node100 l') + | Nodes l', None, Nodes r' => Nodes (Node101 l' r') + | Nodes l', Some x, Empty => Nodes (Node110 l' x) + | Nodes l', Some x, Nodes r' => Nodes (Node111 l' x r') + end. - Fixpoint get (A : Type) (i : positive) (m : t A) {struct i} : option A := - match m with - | Leaf => None - | Node l o r => - match i with - | xH => o - | xO ii => get ii l - | xI ii => get ii r - end +(** ** Basic operations: [empty], [get], [set], [remove] *) + + Definition empty (A: Type) : t A := Empty. + + Fixpoint get' {A} (p: positive) (m: tree' A) : option A := + match p, m with + | xH, Node001 _ => None + | xH, Node010 x => Some x + | xH, Node011 x _ => Some x + | xH, Node100 _ => None + | xH, Node101 _ _ => None + | xH, Node110 _ x => Some x + | xH, Node111 _ x _ => Some x + | xO q, Node001 _ => None + | xO q, Node010 _ => None + | xO q, Node011 _ _ => None + | xO q, Node100 m' => get' q m' + | xO q, Node101 m' _ => get' q m' + | xO q, Node110 m' _ => get' q m' + | xO q, Node111 m' _ _ => get' q m' + | xI q, Node001 m' => get' q m' + | xI q, Node010 _ => None + | xI q, Node011 _ m' => get' q m' + | xI q, Node100 m' => None + | xI q, Node101 _ m' => get' q m' + | xI q, Node110 _ _ => None + | xI q, Node111 _ _ m' => get' q m' end. - Fixpoint set (A : Type) (i : positive) (v : A) (m : t A) {struct i} : t A := + Definition get {A} (p: positive) (m: tree A) : option A := match m with - | Leaf => - match i with - | xH => Node Leaf (Some v) Leaf - | xO ii => Node (set ii v Leaf) None Leaf - | xI ii => Node Leaf None (set ii v Leaf) - end - | Node l o r => - match i with - | xH => Node l (Some v) r - | xO ii => Node (set ii v l) o r - | xI ii => Node l o (set ii v r) - end + | Empty => None + | Nodes m' => get' p m' end. - Fixpoint remove (A : Type) (i : positive) (m : t A) {struct i} : t A := - match i with - | xH => - match m with - | Leaf => Leaf - | Node Leaf o Leaf => Leaf - | Node l o r => Node l None r - end - | xO ii => - match m with - | Leaf => Leaf - | Node l None Leaf => - match remove ii l with - | Leaf => Leaf - | mm => Node mm None Leaf - end - | Node l o r => Node (remove ii l) o r - end - | xI ii => - match m with - | Leaf => Leaf - | Node Leaf None r => - match remove ii r with - | Leaf => Leaf - | mm => Node Leaf None mm - end - | Node l o r => Node l o (remove ii r) - end - end. + (** [set0 p x] constructs the singleton tree that maps [p] to [x] + and has no other bindings. *) + + Fixpoint set0 {A} (p: positive) (x: A) : tree' A := + match p with + | xH => Node010 x + | xO q => Node100 (set0 q x) + | xI q => Node001 (set0 q x) + end. + + Fixpoint set' {A} (p: positive) (x: A) (m: tree' A) : tree' A := + match p, m with + | xH, Node001 r => Node011 x r + | xH, Node010 _ => Node010 x + | xH, Node011 _ r => Node011 x r + | xH, Node100 l => Node110 l x + | xH, Node101 l r => Node111 l x r + | xH, Node110 l _ => Node110 l x + | xH, Node111 l _ r => Node111 l x r + | xO q, Node001 r => Node101 (set0 q x) r + | xO q, Node010 y => Node110 (set0 q x) y + | xO q, Node011 y r => Node111 (set0 q x) y r + | xO q, Node100 l => Node100 (set' q x l) + | xO q, Node101 l r => Node101 (set' q x l) r + | xO q, Node110 l y => Node110 (set' q x l) y + | xO q, Node111 l y r => Node111 (set' q x l) y r + | xI q, Node001 r => Node001 (set' q x r) + | xI q, Node010 y => Node011 y (set0 q x) + | xI q, Node011 y r => Node011 y (set' q x r) + | xI q, Node100 l => Node101 l (set0 q x) + | xI q, Node101 l r => Node101 l (set' q x r) + | xI q, Node110 l y => Node111 l y (set0 q x) + | xI q, Node111 l y r => Node111 l y (set' q x r) + end. + + Definition set {A} (p: positive) (x: A) (m: tree A) : tree A := + match m with + | Empty => Nodes (set0 p x) + | Nodes m' => Nodes (set' p x m') + end. + + (** Removal in a nonempty tree produces a possibly empty tree. + To simplify the code, we use the [Node] smart constructor in the + cases where the result can be empty or nonempty, depending on the + results of the recursive calls. *) + + Fixpoint rem' {A} (p: positive) (m: tree' A) : tree A := + match p, m with + | xH, Node001 r => Nodes m + | xH, Node010 _ => Empty + | xH, Node011 _ r => Nodes (Node001 r) + | xH, Node100 l => Nodes m + | xH, Node101 l r => Nodes m + | xH, Node110 l _ => Nodes (Node100 l) + | xH, Node111 l _ r => Nodes (Node101 l r) + | xO q, Node001 r => Nodes m + | xO q, Node010 y => Nodes m + | xO q, Node011 y r => Nodes m + | xO q, Node100 l => Node (rem' q l) None Empty + | xO q, Node101 l r => Node (rem' q l) None (Nodes r) + | xO q, Node110 l y => Node (rem' q l) (Some y) Empty + | xO q, Node111 l y r => Node (rem' q l) (Some y) (Nodes r) + | xI q, Node001 r => Node Empty None (rem' q r) + | xI q, Node010 y => Nodes m + | xI q, Node011 y r => Node Empty (Some y) (rem' q r) + | xI q, Node100 l => Nodes m + | xI q, Node101 l r => Node (Nodes l) None (rem' q r) + | xI q, Node110 l y => Nodes m + | xI q, Node111 l y r => Node (Nodes l) (Some y) (rem' q r) + end. + + (** This use of [Node] causes some run-time overhead, which we eliminate + by partial evaluation within Coq. *) + + Definition remove' := Eval cbv [rem' Node] in @rem'. + + Definition remove {A} (p: positive) (m: tree A) : tree A := + match m with + | Empty => Empty + | Nodes m' => remove' p m' + end. + +(** ** Good variable properties for the basic operations *) Theorem gempty: forall (A: Type) (i: positive), get i (empty A) = None. + Proof. reflexivity. Qed. + + Lemma gEmpty: + forall (A: Type) (i: positive), get i (@Empty A) = None. + Proof. reflexivity. Qed. + + Lemma gss0: forall {A} p (x: A), get' p (set0 p x) = Some x. + Proof. induction p; simpl; auto. Qed. + + Lemma gso0: forall {A} p q (x: A), p<>q -> get' p (set0 q x) = None. Proof. - induction i; simpl; auto. + induction p; destruct q; simpl; intros; auto; try apply IHp; congruence. Qed. Theorem gss: - forall (A: Type) (i: positive) (x: A) (m: t A), get i (set i x m) = Some x. + forall (A: Type) (i: positive) (x: A) (m: tree A), get i (set i x m) = Some x. Proof. - induction i; destruct m; simpl; auto. + intros. destruct m as [|m]; simpl. + - apply gss0. + - revert m; induction i; destruct m; simpl; intros; auto using gss0. Qed. - Lemma gleaf : forall (A : Type) (i : positive), get i (Leaf : t A) = None. - Proof. exact gempty. Qed. - Theorem gso: - forall (A: Type) (i j: positive) (x: A) (m: t A), + forall (A: Type) (i j: positive) (x: A) (m: tree A), i <> j -> get i (set j x m) = get i m. Proof. - induction i; intros; destruct j; destruct m; simpl; - try rewrite <- (gleaf A i); auto; try apply IHi; congruence. + intros. destruct m as [|m]; simpl. + - apply gso0; auto. + - revert m j H; induction i; destruct j,m; simpl; intros; auto; + solve [apply IHi; congruence | apply gso0; congruence | congruence]. Qed. Theorem gsspec: @@ -287,72 +391,32 @@ Module PTree <: TREE. destruct (peq i j); [ rewrite e; apply gss | apply gso; auto ]. Qed. - Theorem gsident: - forall (A: Type) (i: positive) (m: t A) (v: A), - get i m = Some v -> set i v m = m. - Proof. - induction i; intros; destruct m; simpl; simpl in H; try congruence. - rewrite (IHi m2 v H); congruence. - rewrite (IHi m1 v H); congruence. - Qed. - - Theorem set2: - forall (A: Type) (i: elt) (m: t A) (v1 v2: A), - set i v2 (set i v1 m) = set i v2 m. + Lemma gNode: + forall {A} (i: positive) (l: tree A) (x: option A) (r: tree A), + get i (Node l x r) = match i with xH => x | xO j => get j l | xI j => get j r end. Proof. - induction i; intros; destruct m; simpl; try (rewrite IHi); auto. + intros. destruct l, x, r; simpl; auto; destruct i; auto. Qed. - Lemma rleaf : forall (A : Type) (i : positive), remove i (Leaf : t A) = Leaf. - Proof. destruct i; simpl; auto. Qed. - Theorem grs: - forall (A: Type) (i: positive) (m: t A), get i (remove i m) = None. - Proof. - induction i; destruct m. - simpl; auto. - destruct m1; destruct o; destruct m2 as [ | ll oo rr]; simpl; auto. - rewrite (rleaf A i); auto. - cut (get i (remove i (Node ll oo rr)) = None). - destruct (remove i (Node ll oo rr)); auto; apply IHi. - apply IHi. - simpl; auto. - destruct m1 as [ | ll oo rr]; destruct o; destruct m2; simpl; auto. - rewrite (rleaf A i); auto. - cut (get i (remove i (Node ll oo rr)) = None). - destruct (remove i (Node ll oo rr)); auto; apply IHi. - apply IHi. - simpl; auto. - destruct m1; destruct m2; simpl; auto. + forall (A: Type) (i: positive) (m: tree A), get i (remove i m) = None. + Proof. + Local Opaque Node. + destruct m as [ |m]; simpl. auto. + change (remove' i m) with (rem' i m). + revert m. induction i; destruct m; simpl; auto; rewrite gNode; auto. Qed. Theorem gro: - forall (A: Type) (i j: positive) (m: t A), + forall (A: Type) (i j: positive) (m: tree A), i <> j -> get i (remove j m) = get i m. Proof. - induction i; intros; destruct j; destruct m; - try rewrite (rleaf A (xI j)); - try rewrite (rleaf A (xO j)); - try rewrite (rleaf A 1); auto; - destruct m1; destruct o; destruct m2; - simpl; - try apply IHi; try congruence; - try rewrite (rleaf A j); auto; - try rewrite (gleaf A i); auto. - cut (get i (remove j (Node m2_1 o m2_2)) = get i (Node m2_1 o m2_2)); - [ destruct (remove j (Node m2_1 o m2_2)); try rewrite (gleaf A i); auto - | apply IHi; congruence ]. - destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf A i); - auto. - destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf A i); - auto. - cut (get i (remove j (Node m1_1 o0 m1_2)) = get i (Node m1_1 o0 m1_2)); - [ destruct (remove j (Node m1_1 o0 m1_2)); try rewrite (gleaf A i); auto - | apply IHi; congruence ]. - destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf A i); - auto. - destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf A i); - auto. + Local Opaque Node. + destruct m as [ |m]; simpl. auto. + change (remove' j m) with (rem' j m). + revert j m. induction i; destruct j, m; simpl; intros; auto; + solve [ congruence + | rewrite gNode; auto; apply IHi; congruence ]. Qed. Theorem grspec: @@ -362,47 +426,304 @@ Module PTree <: TREE. intros. destruct (elt_eq i j). subst j. apply grs. apply gro; auto. Qed. +(** ** Custom case analysis principles and induction principles *) + +(** We can view trees as being of one of two (non-exclusive) + cases: either [Empty] for an empty tree, or [Node l o r] for a + nonempty tree, with [l] and [r] the left and right subtrees + and [o] an optional value. The [Empty] constructor and the [Node] + smart function defined above provide one half of the view: the one + that lets us construct values of type [tree A]. + + We now define the other half of the view: the one that lets us + inspect and recurse over values of type [tree A]. This is achieved + by defining appropriate principles for case analysis and induction. *) + + Definition not_trivially_empty {A} (l: tree A) (o: option A) (r: tree A) := + match l, o, r with + | Empty, None, Empty => False + | _, _, _ => True + end. + + (** A case analysis principle *) + + Section TREE_CASE. + + Context {A B: Type} + (empty: B) + (node: tree A -> option A -> tree A -> B). + + Definition tree_case (m: tree A) : B := + match m with + | Empty => empty + | Nodes (Node001 r) => node Empty None (Nodes r) + | Nodes (Node010 x) => node Empty (Some x) Empty + | Nodes (Node011 x r) => node Empty (Some x) (Nodes r) + | Nodes (Node100 l) => node (Nodes l) None Empty + | Nodes (Node101 l r) => node (Nodes l) None (Nodes r) + | Nodes (Node110 l x) => node (Nodes l) (Some x) Empty + | Nodes (Node111 l x r) => node (Nodes l) (Some x) (Nodes r) + end. + + Lemma unroll_tree_case: forall l o r, + not_trivially_empty l o r -> + tree_case (Node l o r) = node l o r. + Proof. + destruct l, o, r; simpl; intros; auto. contradiction. + Qed. + + End TREE_CASE. + + (** A recursion principle *) + + Section TREE_REC. + + Context {A B: Type} + (empty: B) + (node: tree A -> B -> option A -> tree A -> B -> B). + + Fixpoint tree_rec' (m: tree' A) : B := + match m with + | Node001 r => node Empty empty None (Nodes r) (tree_rec' r) + | Node010 x => node Empty empty (Some x) Empty empty + | Node011 x r => node Empty empty (Some x) (Nodes r) (tree_rec' r) + | Node100 l => node (Nodes l) (tree_rec' l) None Empty empty + | Node101 l r => node (Nodes l) (tree_rec' l) None (Nodes r) (tree_rec' r) + | Node110 l x => node (Nodes l) (tree_rec' l) (Some x) Empty empty + | Node111 l x r => node (Nodes l) (tree_rec' l) (Some x) (Nodes r) (tree_rec' r) + end. + + Definition tree_rec (m: tree A) : B := + match m with + | Empty => empty + | Nodes m' => tree_rec' m' + end. + + Lemma unroll_tree_rec: forall l o r, + not_trivially_empty l o r -> + tree_rec (Node l o r) = node l (tree_rec l) o r (tree_rec r). + Proof. + destruct l, o, r; simpl; intros; auto. contradiction. + Qed. + + End TREE_REC. + + (** A double recursion principle *) + + Section TREE_REC2. + + Context {A B C: Type} + (base: C) + (base1: tree B -> C) + (base2: tree A -> C) + (nodes: forall (l1: tree A) (o1: option A) (r1: tree A) + (l2: tree B) (o2: option B) (r2: tree B) + (lrec: C) (rrec: C), C). + + Fixpoint tree_rec2' (m1: tree' A) (m2: tree' B) : C. + Proof. + destruct m1 as [ r1 | x1 | x1 r1 | l1 | l1 r1 | l1 x1 | l1 x1 r1 ]; + destruct m2 as [ r2 | x2 | x2 r2 | l2 | l2 r2 | l2 x2 | l2 x2 r2 ]; + (apply nodes; + [ solve [ exact (Nodes l1) | exact Empty ] + | solve [ exact (Some x1) | exact None ] + | solve [ exact (Nodes r1) | exact Empty ] + | solve [ exact (Nodes l2) | exact Empty ] + | solve [ exact (Some x2) | exact None ] + | solve [ exact (Nodes r2) | exact Empty ] + | solve [ exact (tree_rec2' l1 l2) | exact (base2 (Nodes l1)) | exact (base1 (Nodes l2)) | exact base ] + | solve [ exact (tree_rec2' r1 r2) | exact (base2 (Nodes r1)) | exact (base1 (Nodes r2)) | exact base ] + ]). + Defined. + + Definition tree_rec2 (a: tree A) (b: tree B) : C := + match a, b with + | Empty, Empty => base + | Empty, _ => base1 b + | _, Empty => base2 a + | Nodes a', Nodes b' => tree_rec2' a' b' + end. + + Lemma unroll_tree_rec2_NE: + forall l1 o1 r1, + not_trivially_empty l1 o1 r1 -> + tree_rec2 (Node l1 o1 r1) Empty = base2 (Node l1 o1 r1). + Proof. + intros. destruct l1, o1, r1; try contradiction; reflexivity. + Qed. + + Lemma unroll_tree_rec2_EN: + forall l2 o2 r2, + not_trivially_empty l2 o2 r2 -> + tree_rec2 Empty (Node l2 o2 r2) = base1 (Node l2 o2 r2). + Proof. + intros. destruct l2, o2, r2; try contradiction; reflexivity. + Qed. + + Lemma unroll_tree_rec2_NN: + forall l1 o1 r1 l2 o2 r2, + not_trivially_empty l1 o1 r1 -> not_trivially_empty l2 o2 r2 -> + tree_rec2 (Node l1 o1 r1) (Node l2 o2 r2) = + nodes l1 o1 r1 l2 o2 r2 (tree_rec2 l1 l2) (tree_rec2 r1 r2). + Proof. + intros. + destruct l1, o1, r1; try contradiction; destruct l2, o2, r2; try contradiction; reflexivity. + Qed. + + End TREE_REC2. + +(** An induction principle *) + + Section TREE_IND. + + Context {A: Type} (P: tree A -> Type) + (empty: P Empty) + (node: forall l, P l -> forall o r, P r -> not_trivially_empty l o r -> + P (Node l o r)). + + Program Fixpoint tree_ind' (m: tree' A) : P (Nodes m) := + match m with + | Node001 r => @node Empty empty None (Nodes r) (tree_ind' r) _ + | Node010 x => @node Empty empty (Some x) Empty empty _ + | Node011 x r => @node Empty empty (Some x) (Nodes r) (tree_ind' r) _ + | Node100 l => @node (Nodes l) (tree_ind' l) None Empty empty _ + | Node101 l r => @node (Nodes l) (tree_ind' l) None (Nodes r) (tree_ind' r) _ + | Node110 l x => @node (Nodes l) (tree_ind' l) (Some x) Empty empty _ + | Node111 l x r => @node (Nodes l) (tree_ind' l) (Some x) (Nodes r) (tree_ind' r) _ + end. + + Definition tree_ind (m: tree A) : P m := + match m with + | Empty => empty + | Nodes m' => tree_ind' m' + end. + + End TREE_IND. + +(** ** Extensionality property *) + + Lemma tree'_not_empty: + forall {A} (m: tree' A), exists i, get' i m <> None. + Proof. + induction m; simpl; try destruct IHm as [p H]. + - exists (xI p); auto. + - exists xH; simpl; congruence. + - exists xH; simpl; congruence. + - exists (xO p); auto. + - destruct IHm1 as [p H]; exists (xO p); auto. + - exists xH; simpl; congruence. + - exists xH; simpl; congruence. + Qed. + + Corollary extensionality_empty: + forall {A} (m: tree A), + (forall i, get i m = None) -> m = Empty. + Proof. + intros. destruct m as [ | m]; auto. destruct (tree'_not_empty m) as [i GET]. + elim GET. apply H. + Qed. + + Theorem extensionality: + forall (A: Type) (m1 m2: tree A), + (forall i, get i m1 = get i m2) -> m1 = m2. + Proof. + intros A. induction m1 using tree_ind; induction m2 using tree_ind; intros. + - auto. + - symmetry. apply extensionality_empty. intros; symmetry; apply H0. + - apply extensionality_empty. apply H0. + - f_equal. + + apply IHm1_1. intros. specialize (H1 (xO i)); rewrite ! gNode in H1. auto. + + specialize (H1 xH); rewrite ! gNode in H1. auto. + + apply IHm1_2. intros. specialize (H1 (xI i)); rewrite ! gNode in H1. auto. + Qed. + + (** Some consequences of extensionality *) + + Theorem gsident: + forall {A} (i: positive) (m: t A) (v: A), + get i m = Some v -> set i v m = m. + Proof. + intros; apply extensionality; intros j. + rewrite gsspec. destruct (peq j i); congruence. + Qed. + + Theorem set2: + forall {A} (i: elt) (m: t A) (v1 v2: A), + set i v2 (set i v1 m) = set i v2 m. + Proof. + intros; apply extensionality; intros j. + rewrite ! gsspec. destruct (peq j i); auto. + Qed. + +(** ** Boolean equality *) + Section BOOLEAN_EQUALITY. Variable A: Type. Variable beqA: A -> A -> bool. - Fixpoint bempty (m: t A) : bool := - match m with - | Leaf => true - | Node l None r => bempty l && bempty r - | Node l (Some _) r => false - end. + Fixpoint beq' (m1 m2: tree' A) {struct m1} : bool := + match m1, m2 with + | Node001 r1, Node001 r2 => beq' r1 r2 + | Node010 x1, Node010 x2 => beqA x1 x2 + | Node011 x1 r1, Node011 x2 r2 => beqA x1 x2 && beq' r1 r2 + | Node100 l1, Node100 l2 => beq' l1 l2 + | Node101 l1 r1, Node101 l2 r2 => beq' l1 l2 && beq' r1 r2 + | Node110 l1 x1, Node110 l2 x2 => beqA x1 x2 && beq' l1 l2 + | Node111 l1 x1 r1, Node111 l2 x2 r2 => beqA x1 x2 && beq' l1 l2 && beq' r1 r2 + | _, _ => false + end. - Fixpoint beq (m1 m2: t A) {struct m1} : bool := - match m1, m2 with - | Leaf, _ => bempty m2 - | _, Leaf => bempty m1 - | Node l1 o1 r1, Node l2 o2 r2 => - match o1, o2 with - | None, None => true - | Some y1, Some y2 => beqA y1 y2 - | _, _ => false - end - && beq l1 l2 && beq r1 r2 + Definition beq (m1 m2: t A) : bool := + match m1, m2 with + | Empty, Empty => true + | Nodes m1', Nodes m2' => beq' m1' m2' + | _, _ => false + end. + + Let beq_optA (o1 o2: option A) : bool := + match o1, o2 with + | None, None => true + | Some a1, Some a2 => beqA a1 a2 + | _, _ => false end. - Lemma bempty_correct: - forall m, bempty m = true <-> (forall x, get x m = None). + Lemma beq_correct_bool: + forall m1 m2, + beq m1 m2 = true <-> (forall x, beq_optA (get x m1) (get x m2) = true). Proof. - induction m; simpl. - split; intros. apply gleaf. auto. - destruct o; split; intros. - congruence. - generalize (H xH); simpl; congruence. - destruct (andb_prop _ _ H). rewrite IHm1 in H0. rewrite IHm2 in H1. - destruct x; simpl; auto. - apply andb_true_intro; split. - apply IHm1. intros; apply (H (xO x)). - apply IHm2. intros; apply (H (xI x)). +Local Transparent Node. + assert (beq_NN: forall l1 o1 r1 l2 o2 r2, + not_trivially_empty l1 o1 r1 -> + not_trivially_empty l2 o2 r2 -> + beq (Node l1 o1 r1) (Node l2 o2 r2) = + beq l1 l2 && beq_optA o1 o2 && beq r1 r2). + { intros. + destruct l1, o1, r1; try contradiction; destruct l2, o2, r2; try contradiction; + simpl; rewrite ? andb_true_r, ? andb_false_r; auto. + rewrite andb_comm; auto. + f_equal; rewrite andb_comm; auto. } + induction m1 using tree_ind; [|induction m2 using tree_ind]. + - intros. simpl; split; intros. + + destruct m2; try discriminate. simpl; auto. + + replace m2 with (@Empty A); auto. apply extensionality; intros x. + specialize (H x). destruct (get x m2); simpl; congruence. + - split; intros. + + destruct (Node l o r); try discriminate. simpl; auto. + + replace (Node l o r) with (@Empty A); auto. apply extensionality; intros x. + specialize (H0 x). destruct (get x (Node l o r)); simpl in *; congruence. + - rewrite beq_NN by auto. split; intros. + + InvBooleans. rewrite ! gNode. destruct x. + * apply IHm0; auto. + * apply IHm1; auto. + * auto. + + apply andb_true_intro; split; [apply andb_true_intro; split|]. + * apply IHm1. intros. specialize (H1 (xO x)); rewrite ! gNode in H1; auto. + * specialize (H1 xH); rewrite ! gNode in H1; auto. + * apply IHm0. intros. specialize (H1 (xI x)); rewrite ! gNode in H1; auto. Qed. - Lemma beq_correct: + Theorem beq_correct: forall m1 m2, beq m1 m2 = true <-> (forall (x: elt), @@ -412,27 +733,15 @@ Module PTree <: TREE. | _, _ => False end). Proof. - induction m1; intros. - - simpl. rewrite bempty_correct. split; intros. - rewrite gleaf. rewrite H. auto. - generalize (H x). rewrite gleaf. destruct (get x m2); tauto. - - destruct m2. - + unfold beq. rewrite bempty_correct. split; intros. - rewrite H. rewrite gleaf. auto. - generalize (H x). rewrite gleaf. destruct (get x (Node m1_1 o m1_2)); tauto. - + simpl. split; intros. - * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). - rewrite IHm1_1 in H3. rewrite IHm1_2 in H1. - destruct x; simpl. apply H1. apply H3. - destruct o; destruct o0; auto || congruence. - * apply andb_true_intro. split. apply andb_true_intro. split. - generalize (H xH); simpl. destruct o; destruct o0; tauto. - apply IHm1_1. intros; apply (H (xO x)). - apply IHm1_2. intros; apply (H (xI x)). + intros. rewrite beq_correct_bool. unfold beq_optA. split; intros. + - specialize (H x). destruct (get x m1), (get x m2); intuition congruence. + - specialize (H x). destruct (get x m1), (get x m2); intuition auto. Qed. End BOOLEAN_EQUALITY. +(** ** Collective operations *) + Fixpoint prev_append (i j: positive) {struct i} : positive := match i with | xH => j @@ -464,78 +773,92 @@ Module PTree <: TREE. specialize (Hi _ _ H); congruence. Qed. - Fixpoint xmap (A B : Type) (f : positive -> A -> B) (m : t A) (i : positive) - {struct m} : t B := - match m with - | Leaf => Leaf - | Node l o r => Node (xmap f l (xO i)) - (match o with None => None | Some x => Some (f (prev i) x) end) - (xmap f r (xI i)) - end. + Fixpoint map' {A B} (f: positive -> A -> B) (m: tree' A) (i: positive) + {struct m} : tree' B := + match m with + | Node001 r => Node001 (map' f r (xI i)) + | Node010 x => Node010 (f (prev i) x) + | Node011 x r => Node011 (f (prev i) x) (map' f r (xI i)) + | Node100 l => Node100 (map' f l (xO i)) + | Node101 l r => Node101 (map' f l (xO i)) (map' f r (xI i)) + | Node110 l x => Node110 (map' f l (xO i)) (f (prev i) x) + | Node111 l x r => Node111 (map' f l (xO i)) (f (prev i) x) (map' f r (xI i)) + end. - Definition map (A B : Type) (f : positive -> A -> B) m := xmap f m xH. + Definition map {A B} (f: positive -> A -> B) (m: tree A) := + match m with + | Empty => Empty + | Nodes m => Nodes (map' f m xH) + end. - Lemma xgmap: - forall (A B: Type) (f: positive -> A -> B) (i j : positive) (m: t A), - get i (xmap f m j) = option_map (f (prev (prev_append i j))) (get i m). - Proof. - induction i; intros; destruct m; simpl; auto. - Qed. + Lemma gmap': + forall {A B} (f: positive -> A -> B) (i j : positive) (m: tree' A), + get' i (map' f m j) = option_map (f (prev (prev_append i j))) (get' i m). + Proof. + induction i; intros; destruct m; simpl; auto. + Qed. Theorem gmap: - forall (A B: Type) (f: positive -> A -> B) (i: positive) (m: t A), + forall {A B} (f: positive -> A -> B) (i: positive) (m: t A), get i (map f m) = option_map (f i) (get i m). Proof. - intros A B f i m. - unfold map. - rewrite xgmap. repeat f_equal. exact (prev_involutive i). + intros; destruct m as [|m]; simpl. auto. rewrite gmap'. repeat f_equal. exact (prev_involutive i). Qed. - Fixpoint map1 (A B: Type) (f: A -> B) (m: t A) {struct m} : t B := + Fixpoint map1' {A B} (f: A -> B) (m: tree' A) {struct m} : tree' B := + match m with + | Node001 r => Node001 (map1' f r) + | Node010 x => Node010 (f x) + | Node011 x r => Node011 (f x) (map1' f r) + | Node100 l => Node100 (map1' f l) + | Node101 l r => Node101 (map1' f l) (map1' f r) + | Node110 l x => Node110 (map1' f l) (f x) + | Node111 l x r => Node111 (map1' f l) (f x) (map1' f r) + end. + + Definition map1 {A B} (f: A -> B) (m: t A) : t B := match m with - | Leaf => Leaf - | Node l o r => Node (map1 f l) (option_map f o) (map1 f r) + | Empty => Empty + | Nodes m => Nodes (map1' f m) end. Theorem gmap1: - forall (A B: Type) (f: A -> B) (i: elt) (m: t A), + forall {A B} (f: A -> B) (i: elt) (m: t A), get i (map1 f m) = option_map f (get i m). Proof. - induction i; intros; destruct m; simpl; auto. + intros. destruct m as [|m]; simpl. auto. + revert i; induction m; destruct i; simpl; auto. Qed. - Definition Node' (A: Type) (l: t A) (x: option A) (r: t A): t A := - match l, x, r with - | Leaf, None, Leaf => Leaf - | _, _, _ => Node l x r - end. + Definition map_filter1_nonopt {A B} (f: A -> option B) (m: tree A) : tree B := + tree_rec + Empty + (fun l lrec o r rrec => Node lrec (match o with None => None | Some a => f a end) rrec) + m. + + Definition map_filter1 := + Eval cbv [map_filter1_nonopt tree_rec tree_rec' Node] in @map_filter1_nonopt. - Lemma gnode': - forall (A: Type) (l r: t A) (x: option A) (i: positive), - get i (Node' l x r) = get i (Node l x r). + Lemma gmap_filter1: + forall {A B} (f: A -> option B) (m: tree A) (i: positive), + get i (map_filter1 f m) = match get i m with None => None | Some a => f a end. Proof. - intros. unfold Node'. - destruct l; destruct x; destruct r; auto. - destruct i; simpl; auto; rewrite gleaf; auto. + change @map_filter1 with @map_filter1_nonopt. unfold map_filter1_nonopt. + intros until f. induction m using tree_ind; intros. + - auto. + - rewrite unroll_tree_rec by auto. rewrite ! gNode; destruct i; auto. Qed. - Fixpoint filter1 (A: Type) (pred: A -> bool) (m: t A) {struct m} : t A := - match m with - | Leaf => Leaf - | Node l o r => - let o' := match o with None => None | Some x => if pred x then o else None end in - Node' (filter1 pred l) o' (filter1 pred r) - end. + Definition filter1 {A} (pred: A -> bool) (m: t A) : t A := + map_filter1 (fun a => if pred a then Some a else None) m. Theorem gfilter1: - forall (A: Type) (pred: A -> bool) (i: elt) (m: t A), + forall {A} (pred: A -> bool) (i: elt) (m: t A), get i (filter1 pred m) = match get i m with None => None | Some x => if pred x then Some x else None end. Proof. - intros until m. revert m i. induction m; simpl; intros. - rewrite gleaf; auto. - rewrite gnode'. destruct i; simpl; auto. destruct o; auto. - Qed. + intros. apply gmap_filter1. + Qed. Section COMBINE. @@ -543,201 +866,152 @@ Module PTree <: TREE. Variable f: option A -> option B -> option C. Hypothesis f_none_none: f None None = None. - Fixpoint xcombine_l (m : t A) {struct m} : t C := - match m with - | Leaf => Leaf - | Node l o r => Node' (xcombine_l l) (f o None) (xcombine_l r) - end. + Let combine_l := map_filter1 (fun a => f (Some a) None). + Let combine_r := map_filter1 (fun b => f None (Some b)). - Lemma xgcombine_l : - forall (m: t A) (i : positive), - get i (xcombine_l m) = f (get i m) None. - Proof. - induction m; intros; simpl. - repeat rewrite gleaf. auto. - rewrite gnode'. destruct i; simpl; auto. - Qed. + Let combine_nonopt (m1: tree A) (m2: tree B) : tree C := + tree_rec2 + Empty + combine_r + combine_l + (fun l1 o1 r1 l2 o2 r2 lrec rrec => + Node lrec + (match o1, o2 with None, None => None | _, _ => f o1 o2 end) + rrec) + m1 m2. - Fixpoint xcombine_r (m : t B) {struct m} : t C := - match m with - | Leaf => Leaf - | Node l o r => Node' (xcombine_r l) (f None o) (xcombine_r r) - end. + Definition combine := + Eval cbv [combine_nonopt tree_rec2 tree_rec2'] in combine_nonopt. - Lemma xgcombine_r : - forall (m: t B) (i : positive), - get i (xcombine_r m) = f None (get i m). - Proof. - induction m; intros; simpl. - repeat rewrite gleaf. auto. - rewrite gnode'. destruct i; simpl; auto. - Qed. + Lemma gcombine_l: forall m i, get i (combine_l m) = f (get i m) None. + Proof. + intros; unfold combine_l; rewrite gmap_filter1. destruct (get i m); auto. + Qed. - Fixpoint combine (m1: t A) (m2: t B) {struct m1} : t C := - match m1 with - | Leaf => xcombine_r m2 - | Node l1 o1 r1 => - match m2 with - | Leaf => xcombine_l m1 - | Node l2 o2 r2 => Node' (combine l1 l2) (f o1 o2) (combine r1 r2) - end - end. + Lemma gcombine_r: forall m i, get i (combine_r m) = f None (get i m). + Proof. + intros; unfold combine_r; rewrite gmap_filter1. destruct (get i m); auto. + Qed. Theorem gcombine: forall (m1: t A) (m2: t B) (i: positive), get i (combine m1 m2) = f (get i m1) (get i m2). Proof. - induction m1; intros; simpl. - rewrite gleaf. apply xgcombine_r. - destruct m2; simpl. - rewrite gleaf. rewrite <- xgcombine_l. auto. - repeat rewrite gnode'. destruct i; simpl; auto. + change combine with combine_nonopt. + induction m1 using tree_ind; induction m2 using tree_ind; intros. + - auto. + - unfold combine_nonopt; rewrite unroll_tree_rec2_EN by auto. apply gcombine_r. + - unfold combine_nonopt; rewrite unroll_tree_rec2_NE by auto. apply gcombine_l. + - unfold combine_nonopt; rewrite unroll_tree_rec2_NN by auto. + rewrite ! gNode; destruct i; auto. destruct o, o0; auto. Qed. End COMBINE. - Lemma xcombine_lr : - forall (A B: Type) (f g : option A -> option A -> option B) (m : t A), - (forall (i j : option A), f i j = g j i) -> - xcombine_l f m = xcombine_r g m. - Proof. - induction m; intros; simpl; auto. - rewrite IHm1; auto. - rewrite IHm2; auto. - rewrite H; auto. - Qed. - Theorem combine_commut: forall (A B: Type) (f g: option A -> option A -> option B), + f None None = None -> g None None = None -> (forall (i j: option A), f i j = g j i) -> forall (m1 m2: t A), combine f m1 m2 = combine g m2 m1. Proof. - intros A B f g EQ1. - assert (EQ2: forall (i j: option A), g i j = f j i). - intros; auto. - induction m1; intros; destruct m2; simpl; - try rewrite EQ1; - repeat rewrite (xcombine_lr f g); - repeat rewrite (xcombine_lr g f); - auto. - rewrite IHm1_1. - rewrite IHm1_2. - auto. - Qed. - - Fixpoint xelements (A : Type) (m : t A) (i : positive) - (k: list (positive * A)) {struct m} - : list (positive * A) := - match m with - | Leaf => k - | Node l None r => - xelements l (xO i) (xelements r (xI i) k) - | Node l (Some x) r => - xelements l (xO i) - ((prev i, x) :: xelements r (xI i) k) - end. + intros. apply extensionality; intros i. rewrite ! gcombine by auto. auto. + Qed. - Definition elements (A: Type) (m : t A) := xelements m xH nil. +(** ** List of all bindings *) - Remark xelements_append: - forall A (m: t A) i k1 k2, - xelements m i (k1 ++ k2) = xelements m i k1 ++ k2. - Proof. - induction m; intros; simpl. - - auto. - - destruct o; rewrite IHm2; rewrite <- IHm1; auto. - Qed. + Fixpoint xelements' {A} (m : tree' A) (i: positive) (k: list (positive * A)) + {struct m} : list (positive * A) := + match m with + | Node001 r => xelements' r (xI i) k + | Node010 x => (prev i, x) :: k + | Node011 x r => (prev i, x) :: xelements' r (xI i) k + | Node100 l => xelements' l (xO i) k + | Node101 l r => xelements' l (xO i) (xelements' r (xI i) k) + | Node110 l x => xelements' l (xO i) ((prev i, x)::k) + | Node111 l x r => xelements' l (xO i) ((prev i, x):: (xelements' r (xI i) k)) + end. - Remark xelements_leaf: - forall A i, xelements (@Leaf A) i nil = nil. + Definition elements {A} (m : t A) : list (positive * A) := + match m with Empty => nil | Nodes m' => xelements' m' xH nil end. + + Definition xelements {A} (m : t A) (i: positive) : list (positive * A) := + match m with Empty => nil | Nodes m' => xelements' m' i nil end. + + Lemma xelements'_append: + forall A (m: tree' A) i k1 k2, + xelements' m i (k1 ++ k2) = xelements' m i k1 ++ k2. Proof. - intros; reflexivity. + induction m; intros; simpl; auto. + - f_equal; auto. + - rewrite IHm2, IHm1. auto. + - rewrite <- IHm. auto. + - rewrite IHm2, <- IHm1. auto. Qed. - Remark xelements_node: - forall A (m1: t A) o (m2: t A) i, - xelements (Node m1 o m2) i nil = - xelements m1 (xO i) nil + Lemma xelements_Node: + forall A (l: tree A) (o: option A) (r: tree A) i, + xelements (Node l o r) i = + xelements l (xO i) ++ match o with None => nil | Some v => (prev i, v) :: nil end - ++ xelements m2 (xI i) nil. + ++ xelements r (xI i). Proof. - intros. simpl. destruct o; simpl; rewrite <- xelements_append; auto. + Local Transparent Node. + intros; destruct l, o, r; simpl; rewrite <- ? xelements'_append; auto. Qed. - Lemma xelements_incl: - forall (A: Type) (m: t A) (i : positive) k x, - In x k -> In x (xelements m i k). - Proof. - induction m; intros; simpl. - auto. - destruct o. - apply IHm1. simpl; right; auto. - auto. - Qed. - - Lemma xelements_correct: - forall (A: Type) (m: t A) (i j : positive) (v: A) k, - get i m = Some v -> In (prev (prev_append i j), v) (xelements m j k). - Proof. - induction m; intros. - rewrite (gleaf A i) in H; congruence. - destruct o; destruct i; simpl; simpl in H. - apply xelements_incl. right. auto. - auto. - inv H. apply xelements_incl. left. reflexivity. - apply xelements_incl. auto. - auto. - inv H. - Qed. + Lemma xelements_correct: + forall A (m: tree A) i j v, + get i m = Some v -> In (prev (prev_append i j), v) (xelements m j). + Proof. + intros A. induction m using tree_ind; intros. + - discriminate. + - rewrite xelements_Node, ! in_app. rewrite gNode in H0. destruct i. + + right; right. apply (IHm2 i (xI j)); auto. + + left. apply (IHm1 i (xO j)); auto. + + right; left. subst o. rewrite prev_append_prev. auto with coqlib. + Qed. Theorem elements_correct: - forall (A: Type) (m: t A) (i: positive) (v: A), + forall A (m: t A) (i: positive) (v: A), get i m = Some v -> In (i, v) (elements m). Proof. intros A m i v H. - generalize (xelements_correct m i xH nil H). rewrite prev_append_prev. exact id. + generalize (xelements_correct m i xH H). rewrite prev_append_prev. auto. Qed. Lemma in_xelements: - forall (A: Type) (m: t A) (i k: positive) (v: A) , - In (k, v) (xelements m i nil) -> + forall A (m: tree A) (i k: positive) (v: A) , + In (k, v) (xelements m i) -> exists j, k = prev (prev_append j i) /\ get j m = Some v. Proof. - induction m; intros. - - rewrite xelements_leaf in H. contradiction. - - rewrite xelements_node in H. rewrite ! in_app_iff in H. destruct H as [P | [P | P]]. - + exploit IHm1; eauto. intros (j & Q & R). exists (xO j); auto. - + destruct o; simpl in P; intuition auto. inv H. exists xH; auto. - + exploit IHm2; eauto. intros (j & Q & R). exists (xI j); auto. + intros A. induction m using tree_ind; intros. + - elim H. + - rewrite xelements_Node, ! in_app in H0. destruct H0 as [P | [P | P]]. + + exploit IHm1; eauto. intros (j & Q & R). exists (xO j); rewrite gNode; auto. + + destruct o; simpl in P; intuition auto. inv H0. exists xH; rewrite gNode; auto. + + exploit IHm2; eauto. intros (j & Q & R). exists (xI j); rewrite gNode; auto. Qed. Theorem elements_complete: - forall (A: Type) (m: t A) (i: positive) (v: A), + forall A (m: t A) (i: positive) (v: A), In (i, v) (elements m) -> get i m = Some v. Proof. - unfold elements. intros A m i v H. exploit in_xelements; eauto. intros (j & P & Q). + intros A m i v H. exploit in_xelements; eauto. intros (j & P & Q). rewrite prev_append_prev in P. change i with (prev_append 1 i) in P. exploit prev_append_inj; eauto. intros; congruence. Qed. - Definition xkeys (A: Type) (m: t A) (i: positive) := - List.map (@fst positive A) (xelements m i nil). - - Remark xkeys_leaf: - forall A i, xkeys (@Leaf A) i = nil. - Proof. - intros; reflexivity. - Qed. + Definition xkeys {A} (m: t A) (i: positive) := List.map fst (xelements m i). - Remark xkeys_node: + Lemma xkeys_Node: forall A (m1: t A) o (m2: t A) i, xkeys (Node m1 o m2) i = xkeys m1 (xO i) ++ match o with None => nil | Some v => prev i :: nil end ++ xkeys m2 (xI i). Proof. - intros. unfold xkeys. rewrite xelements_node. rewrite ! map_app. destruct o; auto. + intros. unfold xkeys. rewrite xelements_Node, ! map_app. destruct o; auto. Qed. Lemma in_xkeys: @@ -754,40 +1028,36 @@ Module PTree <: TREE. forall (A: Type) (m: t A) (i: positive), list_norepet (xkeys m i). Proof. - induction m; intros. - - rewrite xkeys_leaf; constructor. - - assert (NOTIN1: ~ In (prev i) (xkeys m1 (xO i))). + intros A; induction m using tree_ind; intros. + - constructor. + - assert (NOTIN1: ~ In (prev i) (xkeys l (xO i))). { red; intros. exploit in_xkeys; eauto. intros (j & EQ). rewrite prev_append_prev in EQ. simpl in EQ. apply prev_append_inj in EQ. discriminate. } - assert (NOTIN2: ~ In (prev i) (xkeys m2 (xI i))). + assert (NOTIN2: ~ In (prev i) (xkeys r (xI i))). { red; intros. exploit in_xkeys; eauto. intros (j & EQ). rewrite prev_append_prev in EQ. simpl in EQ. apply prev_append_inj in EQ. discriminate. } - assert (DISJ: forall x, In x (xkeys m1 (xO i)) -> In x (xkeys m2 (xI i)) -> False). - { intros. exploit in_xkeys. eexact H. intros (j1 & EQ1). - exploit in_xkeys. eexact H0. intros (j2 & EQ2). + assert (DISJ: forall x, In x (xkeys l (xO i)) -> In x (xkeys r (xI i)) -> False). + { intros. exploit in_xkeys. eexact H0. intros (j1 & EQ1). + exploit in_xkeys. eexact H1. intros (j2 & EQ2). rewrite prev_append_prev in *. simpl in *. rewrite EQ2 in EQ1. apply prev_append_inj in EQ1. discriminate. } - rewrite xkeys_node. apply list_norepet_append. auto. + rewrite xkeys_Node. apply list_norepet_append. auto. destruct o; simpl; auto. constructor; auto. - red; intros. red; intros; subst y. destruct o; simpl in H0. - destruct H0. subst x. tauto. eauto. eauto. + red; intros. red; intros; subst y. destruct o; simpl in H1. + destruct H1. subst x. tauto. eauto. eauto. Qed. Theorem elements_keys_norepet: - forall (A: Type) (m: t A), + forall A (m: t A), list_norepet (List.map (@fst elt A) (elements m)). Proof. intros. apply (xelements_keys_norepet m xH). Qed. Remark xelements_empty: - forall (A: Type) (m: t A) i, (forall i, get i m = None) -> xelements m i nil = nil. + forall A (m: t A) i, (forall i, get i m = None) -> xelements m i = nil. Proof. - induction m; intros. - auto. - rewrite xelements_node. rewrite IHm1, IHm2. destruct o; auto. - generalize (H xH); simpl; congruence. - intros. apply (H (xI i0)). - intros. apply (H (xO i0)). + intros. replace m with (@Empty A). auto. + apply extensionality; intros. symmetry; auto. Qed. Theorem elements_canonical_order': @@ -797,19 +1067,18 @@ Module PTree <: TREE. (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y)) (elements m) (elements n). Proof. - intros until n. unfold elements. generalize 1%positive. revert m n. - induction m; intros. - - simpl. rewrite xelements_empty. constructor. - intros. specialize (H i). rewrite gempty in H. inv H; auto. - - destruct n as [ | n1 o' n2 ]. - + rewrite (xelements_empty (Node m1 o m2)). simpl; constructor. - intros. specialize (H i). rewrite gempty in H. inv H; auto. - + rewrite ! xelements_node. repeat apply list_forall2_app. - apply IHm1. intros. apply (H (xO i)). - generalize (H xH); simpl; intros OR; inv OR. - constructor. - constructor. auto. constructor. - apply IHm2. intros. apply (H (xI i)). + intros until n. + change (elements m) with (xelements m xH). change (elements n) with (xelements n xH). + generalize 1%positive. revert m n. + induction m using tree_ind; [ | induction n using tree_ind]; intros until p; intros REL. + - replace n with (@Empty B). constructor. + apply extensionality; intros. specialize (REL i). simpl in *. inv REL; auto. + - replace (Node l o r) with (@Empty A). constructor. + apply extensionality; intros. specialize (REL i). simpl in *. inv REL; auto. + - rewrite ! xelements_Node. repeat apply list_forall2_app. + + apply IHm. intros. specialize (REL (xO i)). rewrite ! gNode in REL; auto. + + specialize (REL xH). rewrite ! gNode in REL. inv REL; constructor; auto using list_forall2_nil. + + apply IHm0. intros. specialize (REL (xI i)). rewrite ! gNode in REL; auto. Qed. Theorem elements_canonical_order: @@ -833,57 +1102,48 @@ Module PTree <: TREE. (forall i, get i m = get i n) -> elements m = elements n. Proof. - intros. - exploit (@elements_canonical_order' _ _ (fun (x y: A) => x = y) m n). - intros. rewrite H. destruct (get i n); constructor; auto. - induction 1. auto. destruct a1 as [a2 a3]; destruct b1 as [b2 b3]; simpl in *. - destruct H0. congruence. + intros. replace n with m; auto. apply extensionality; auto. Qed. Lemma xelements_remove: - forall (A: Type) v (m: t A) i j, + forall A v (m: t A) i j, get i m = Some v -> exists l1 l2, - xelements m j nil = l1 ++ (prev (prev_append i j), v) :: l2 - /\ xelements (remove i m) j nil = l1 ++ l2. - Proof. - induction m; intros. - - rewrite gleaf in H; discriminate. - - assert (REMOVE: xelements (remove i (Node m1 o m2)) j nil = - xelements (match i with - | xH => Node m1 None m2 - | xO ii => Node (remove ii m1) o m2 - | xI ii => Node m1 o (remove ii m2) end) - j nil). - { - destruct i; simpl remove. - destruct m1; auto. destruct o; auto. destruct (remove i m2); auto. - destruct o; auto. destruct m2; auto. destruct (remove i m1); auto. - destruct m1; auto. destruct m2; auto. - } - rewrite REMOVE. destruct i; simpl in H. - + destruct (IHm2 i (xI j) H) as (l1 & l2 & EQ & EQ'). - exists (xelements m1 (xO j) nil ++ + xelements m j = l1 ++ (prev (prev_append i j), v) :: l2 + /\ xelements (remove i m) j = l1 ++ l2. + Proof. + intros A; induction m using tree_ind; intros. + - discriminate. + - assert (REMOVE: remove i (Node l o r) = + match i with + | xH => Node l None r + | xO ii => Node (remove ii l) o r + | xI ii => Node l o (remove ii r) + end). + { destruct l, o, r, i; reflexivity. } + rewrite gNode in H0. rewrite REMOVE. destruct i; rewrite ! xelements_Node. + + destruct (IHm0 i (xI j) H0) as (l1 & l2 & EQ & EQ'). + exists (xelements l (xO j) ++ match o with None => nil | Some x => (prev j, x) :: nil end ++ l1); exists l2; split. - rewrite xelements_node, EQ, ! app_ass. auto. - rewrite xelements_node, EQ', ! app_ass. auto. - + destruct (IHm1 i (xO j) H) as (l1 & l2 & EQ & EQ'). + rewrite EQ, ! app_ass. auto. + rewrite EQ', ! app_ass. auto. + + destruct (IHm i (xO j) H0) as (l1 & l2 & EQ & EQ'). exists l1; exists (l2 ++ match o with None => nil | Some x => (prev j, x) :: nil end ++ - xelements m2 (xI j) nil); + xelements r (xI j)); split. - rewrite xelements_node, EQ, ! app_ass. auto. - rewrite xelements_node, EQ', ! app_ass. auto. - + subst o. exists (xelements m1 (xO j) nil); exists (xelements m2 (xI j) nil); split. - rewrite xelements_node. rewrite prev_append_prev. auto. - rewrite xelements_node; auto. + rewrite EQ, ! app_ass. auto. + rewrite EQ', ! app_ass. auto. + + subst o. exists (xelements l (xO j)); exists (xelements r (xI j)); split. + rewrite prev_append_prev. auto. + auto. Qed. Theorem elements_remove: - forall (A: Type) i v (m: t A), + forall A i v (m: t A), get i m = Some v -> exists l1 l2, elements m = l1 ++ (i,v) :: l2 /\ elements (remove i m) = l1 ++ l2. Proof. @@ -891,74 +1151,82 @@ Module PTree <: TREE. rewrite prev_append_prev. auto. Qed. - Fixpoint xfold (A B: Type) (f: B -> positive -> A -> B) - (i: positive) (m: t A) (v: B) {struct m} : B := +(** ** Folding over a tree *) + + Fixpoint fold' {A B} (f: B -> positive -> A -> B) + (i: positive) (m: tree' A) (v: B) {struct m} : B := match m with - | Leaf => v - | Node l None r => - let v1 := xfold f (xO i) l v in - xfold f (xI i) r v1 - | Node l (Some x) r => - let v1 := xfold f (xO i) l v in - let v2 := f v1 (prev i) x in - xfold f (xI i) r v2 + | Node001 r => fold' f (xI i) r v + | Node010 x => f v (prev i) x + | Node011 x r => fold' f (xI i) r (f v (prev i) x) + | Node100 l => fold' f (xO i) l v + | Node101 l r => fold' f (xI i) r (fold' f (xO i) l v) + | Node110 l x => f (fold' f (xO i) l v) (prev i) x + | Node111 l x r => fold' f (xI i) r (f (fold' f (xO i) l v) (prev i) x) end. - Definition fold (A B : Type) (f: B -> positive -> A -> B) (m: t A) (v: B) := - xfold f xH m v. + Definition fold {A B} (f: B -> positive -> A -> B) (m: t A) (v: B) := + match m with Empty => v | Nodes m' => fold' f xH m' v end. - Lemma xfold_xelements: - forall (A B: Type) (f: B -> positive -> A -> B) m i v l, - List.fold_left (fun a p => f a (fst p) (snd p)) l (xfold f i m v) = - List.fold_left (fun a p => f a (fst p) (snd p)) (xelements m i l) v. + Lemma fold'_xelements': + forall A B (f: B -> positive -> A -> B) m i v l, + List.fold_left (fun a p => f a (fst p) (snd p)) l (fold' f i m v) = + List.fold_left (fun a p => f a (fst p) (snd p)) (xelements' m i l) v. Proof. - induction m; intros. - simpl. auto. - destruct o; simpl. - rewrite <- IHm1. simpl. rewrite <- IHm2. auto. - rewrite <- IHm1. rewrite <- IHm2. auto. + induction m; intros; simpl; auto. + rewrite <- IHm1, <- IHm2; auto. + rewrite <- IHm; auto. + rewrite <- IHm1. simpl. rewrite <- IHm2; auto. Qed. Theorem fold_spec: - forall (A B: Type) (f: B -> positive -> A -> B) (v: B) (m: t A), + forall A B (f: B -> positive -> A -> B) (v: B) (m: t A), fold f m v = List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v. Proof. - intros. unfold fold, elements. rewrite <- xfold_xelements. auto. + intros. unfold fold, elements. destruct m; auto. rewrite <- fold'_xelements'. auto. Qed. - Fixpoint fold1 (A B: Type) (f: B -> A -> B) (m: t A) (v: B) {struct m} : B := + Fixpoint fold1' {A B} (f: B -> A -> B) (m: tree' A) (v: B) {struct m} : B := match m with - | Leaf => v - | Node l None r => - let v1 := fold1 f l v in - fold1 f r v1 - | Node l (Some x) r => - let v1 := fold1 f l v in - let v2 := f v1 x in - fold1 f r v2 + | Node001 r => fold1' f r v + | Node010 x => f v x + | Node011 x r => fold1' f r (f v x) + | Node100 l => fold1' f l v + | Node101 l r => fold1' f r (fold1' f l v) + | Node110 l x => f (fold1' f l v) x + | Node111 l x r => fold1' f r (f (fold1' f l v) x) end. - Lemma fold1_xelements: - forall (A B: Type) (f: B -> A -> B) m i v l, - List.fold_left (fun a p => f a (snd p)) l (fold1 f m v) = - List.fold_left (fun a p => f a (snd p)) (xelements m i l) v. + + Definition fold1 {A B} (f: B -> A -> B) (m: t A) (v: B) : B := + match m with Empty => v | Nodes m' => fold1' f m' v end. + + Lemma fold1'_xelements': + forall A B (f: B -> A -> B) m i v l, + List.fold_left (fun a p => f a (snd p)) l (fold1' f m v) = + List.fold_left (fun a p => f a (snd p)) (xelements' m i l) v. Proof. - induction m; intros. - simpl. auto. - destruct o; simpl. - rewrite <- IHm1. simpl. rewrite <- IHm2. auto. + induction m; simpl; intros; auto. rewrite <- IHm1. rewrite <- IHm2. auto. + rewrite <- IHm. auto. + rewrite <- IHm1. simpl. rewrite <- IHm2. auto. Qed. Theorem fold1_spec: - forall (A B: Type) (f: B -> A -> B) (v: B) (m: t A), + forall A B (f: B -> A -> B) (v: B) (m: t A), fold1 f m v = List.fold_left (fun a p => f a (snd p)) (elements m) v. Proof. - intros. apply fold1_xelements with (l := @nil (positive * A)). + intros. destruct m as [|m]. reflexivity. + apply fold1'_xelements' with (l := @nil (positive * A)). Qed. + Arguments empty A : simpl never. + Arguments get {A} p m : simpl never. + Arguments set {A} p x m : simpl never. + Arguments remove {A} p m : simpl never. + End PTree. (** * An implementation of maps over type [positive] *) @@ -984,7 +1252,7 @@ Module PMap <: MAP. Theorem gi: forall (A: Type) (i: positive) (x: A), get i (init x) = x. Proof. - intros. unfold init. unfold get. simpl. rewrite PTree.gempty. auto. + intros. reflexivity. Qed. Theorem gss: @@ -1284,6 +1552,8 @@ Module ZTree := ITree(ZIndexed). (** * Additional properties over trees *) +Require Import Equivalence EquivDec. + Module Tree_Properties(T: TREE). (** Two induction principles over [fold]. *) -- cgit