From 795485179071254bfab493dd6733d45b8f272900 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 24 Sep 2014 11:55:10 +0200 Subject: Add theorem "elements_remove". Use "elements_remove" to simplify the proof of "cardinal_remove". Simplify some of the proofs over function "xelements". --- lib/Maps.v | 345 +++++++++++++++++++++++++++++++------------------------------ 1 file changed, 178 insertions(+), 167 deletions(-) (limited to 'lib/Maps.v') diff --git a/lib/Maps.v b/lib/Maps.v index 16e35038..2b6badcb 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -133,6 +133,14 @@ Module Type TREE. Hypothesis elements_keys_norepet: forall (A: Type) (m: t A), list_norepet (List.map (@fst elt A) (elements m)). + Hypothesis elements_extensional: + forall (A: Type) (m n: t A), + (forall i, get i m = get i n) -> + elements m = elements n. + Hypothesis elements_remove: + forall (A: Type) 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. (** Folding a function over all bindings of a tree. *) Variable fold: @@ -634,9 +642,33 @@ Module PTree <: TREE. ((prev i, x) :: xelements r (xI i) k) end. - Definition elements (A: Type) (m : t A) := xelements m xH nil. + 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. + + Remark xelements_leaf: + forall A i, xelements (@Leaf A) i nil = nil. + Proof. + intros; reflexivity. + 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 + ++ match o with None => nil | Some v => (prev i, v) :: nil end + ++ xelements m2 (xI i) nil. + Proof. + intros. simpl. destruct o; 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). @@ -672,112 +704,92 @@ Module PTree <: TREE. Qed. Lemma in_xelements: - forall (A: Type) (m: t A) (i k: positive) (v: A) l, - In (k, v) (xelements m i l) -> - (exists j, k = prev (prev_append j i) /\ get j m = Some v) \/ In (k, v) l. + forall (A: Type) (m: t A) (i k: positive) (v: A) , + In (k, v) (xelements m i nil) -> + exists j, k = prev (prev_append j i) /\ get j m = Some v. Proof. - induction m as [|l IHl o r IHr]; intros i j v k H. - right; exact H. - destruct o as [o|]. - specialize (IHl _ _ _ _ H). destruct IHl as [(j' & -> & Hj')|[IHl|IHl]]. - left. exists (xO j'). split. reflexivity. exact Hj'. - inv IHl. left. exists xH. split. reflexivity. reflexivity. - destruct (IHr _ _ _ _ IHl) as [(j' & -> & Hj') | IH]; clear IHr. - left. exists (xI j'). split. reflexivity. exact Hj'. - right; assumption. - specialize (IHl _ _ _ _ H). destruct IHl as [(j' & -> & Hj' )|IHl]. - left. exists (xO j'). split. reflexivity. exact Hj'. - destruct (IHr _ _ _ _ IHl) as [(j' & -> & Hj') | IH]; clear IHr. - left. exists (xI j'). split. reflexivity. exact Hj'. - right; assumption. + 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. Qed. - Lemma xelements_complete: - forall (A: Type) (m: t A) (i j : positive) (v: A) k, - In (prev_append j i, v) (xelements m j k) -> get i m = Some v \/ In (prev_append j i, v) k. - Proof. - intros A m i j v k H. - apply in_xelements in H. destruct H as [(j' & EQ & Hj')|H]. - rewrite prev_append_prev in EQ. apply prev_append_inj in EQ. left; congruence. - right; assumption. - Qed. - Theorem elements_complete: forall (A: Type) (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. - change i with (prev_append 1 i) in H. - destruct (xelements_complete _ _ _ _ _ H) as [K|()]. exact K. + unfold elements. 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) (l: list (positive * A)) := - List.map (@fst positive A) (xelements m i l). + 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. + + Remark 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. + Qed. Lemma in_xkeys: - forall (A: Type) (m: t A) (i k: positive) l, - In k (xkeys m i l) -> - (exists j, k = prev (prev_append j i)) \/ In k (List.map fst l). + forall (A: Type) (m: t A) (i k: positive), + In k (xkeys m i) -> + (exists j, k = prev (prev_append j i)). Proof. unfold xkeys; intros. apply (list_in_map_inv) in H. destruct H as ((j, v) & -> & H). - change j with (prev_append 1 j) in H. apply in_xelements in H. - destruct H as [(j' & Hj' & _) | H]. simpl in Hj'; subst j. - left. simpl. exists j'. reflexivity. - right. apply in_map. exact H. + exploit in_xelements; eauto. intros (k & P & Q). exists k; auto. Qed. Lemma xelements_keys_norepet: - forall (A: Type) (m: t A) (i: positive) l, - (forall k v, get k m = Some v -> ~In (prev (prev_append k i)) (List.map fst l)) -> - list_norepet (List.map fst l) -> - list_norepet (xkeys m i l). + forall (A: Type) (m: t A) (i: positive), + list_norepet (xkeys m i). Proof. - unfold xkeys. - intros A m. - induction m as [|l Hl o r Hr]; intros i elem H NR. - auto. - destruct o as [o|]. - - apply Hl. - intros k v Hkv IN. - destruct IN as [IN | IN]. - rewrite prev_append_prev in IN. simpl in IN. apply prev_append_inj in IN. discriminate. - apply in_xkeys in IN. destruct IN as [(j & EQ) | IN]. - rewrite !prev_append_prev in EQ. simpl in EQ. apply prev_append_inj in EQ. discriminate. - elim (H (xO k) v); auto; fail. - simpl. constructor. - intros IN. - apply in_xkeys in IN. destruct IN as [(j & EQ) | IN]. - rewrite !prev_append_prev in EQ. simpl in EQ. apply prev_append_inj in EQ. discriminate. - elim (H xH o); auto; fail. - apply Hr; auto. - intros k. - exact (H (xI k)). - - apply Hl. - intros k v Hkv IN. - apply in_xkeys in IN. destruct IN as [(j & EQ) | IN]. - rewrite !prev_append_prev in EQ. simpl in EQ. apply prev_append_inj in EQ. discriminate. - exact (H (xO k) _ Hkv IN). - apply Hr; auto. - intros k. - exact (H (xI k)). + induction m; intros. + - rewrite xkeys_leaf; constructor. + - assert (NOTIN1: ~ In (prev i) (xkeys m1 (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))). + { 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). + 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. + destruct o; simpl; auto. constructor; auto. + red; intros. red; intros; subst y. destruct o; simpl in H0. + destruct H0. subst x. tauto. eauto. eauto. Qed. Theorem elements_keys_norepet: forall (A: Type) (m: t A), list_norepet (List.map (@fst elt A) (elements m)). Proof. - intros. change (list_norepet (xkeys m 1 nil)). apply xelements_keys_norepet. - intros; red; intros. elim H0. constructor. + intros. apply (xelements_keys_norepet m xH). Qed. Remark xelements_empty: - forall (A: Type) (m: t A) i l, (forall i, get i m = None) -> xelements m i l = l. + forall (A: Type) (m: t A) i, (forall i, get i m = None) -> xelements m i nil = nil. Proof. - induction m; simpl; intros. + induction m; intros. auto. - destruct o. generalize (H xH); simpl; congruence. - rewrite IHm1. apply IHm2. + rewrite xelements_node. rewrite IHm1, IHm2. destruct o; auto. + generalize (H xH); simpl; congruence. intros. apply (H (xI i0)). intros. apply (H (xO i0)). Qed. @@ -791,48 +803,37 @@ Module PTree <: TREE. (elements m) (elements n). Proof. intros until R. - assert (forall m n j l1 l2, + assert (forall m n j, (forall i x, get i m = Some x -> exists y, get i n = Some y /\ R x y) -> (forall i y, get i n = Some y -> exists x, get i m = Some x /\ R x y) -> list_forall2 (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y)) - l1 l2 -> - list_forall2 - (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y)) - (xelements m j l1) (xelements n j l2)). + (xelements m j nil) (xelements n j nil)). { - induction m; simpl; intros. - rewrite xelements_empty. auto. + induction m; intros. + - rewrite xelements_leaf. rewrite xelements_empty. constructor. intros. destruct (get i n) eqn:E; auto. exploit H0; eauto. intros [x [P Q]]. rewrite gleaf in P; congruence. - destruct o. - destruct n. exploit (H xH a); auto. simpl. intros [y [P Q]]; congruence. - exploit (H xH a); auto. intros [y [P Q]]. simpl in P. subst o. - simpl. apply IHm1. - intros i x. exact (H (xO i) x). - intros i x. exact (H0 (xO i) x). - constructor. simpl; auto. - apply IHm2. - intros i x. exact (H (xI i) x). - intros i x. exact (H0 (xI i) x). - auto. - destruct n. simpl. - rewrite ! xelements_empty. auto. - intros. destruct (get i m2) eqn:E; auto. exploit (H (xI i)); eauto. - rewrite gleaf. intros [y [P Q]]; congruence. - intros. destruct (get i m1) eqn:E; auto. exploit (H (xO i)); eauto. - rewrite gleaf. intros [y [P Q]]; congruence. - destruct o. - exploit (H0 xH); simpl; eauto. intros [y [P Q]]; congruence. - simpl. apply IHm1. - intros i x. exact (H (xO i) x). - intros i x. exact (H0 (xO i) x). - apply IHm2. - intros i x. exact (H (xI i) x). - intros i x. exact (H0 (xI i) x). - auto. - } - intros. apply H. auto. auto. constructor. + - destruct n as [ | n1 o' n2 ]. + + rewrite xelements_leaf, xelements_empty. constructor. + intros. destruct (get i (Node m1 o m2)) eqn:E; auto. exploit H; eauto. + intros [x [P Q]]. rewrite gleaf in P; congruence. + + rewrite ! xelements_node. apply list_forall2_app. + apply IHm1. + intros. apply (H (xO i) x); auto. + intros. apply (H0 (xO i) y); auto. + apply list_forall2_app. + destruct o, o'. + destruct (H xH a) as [x [P Q]]. auto. simpl in P. inv P. + constructor. auto. constructor. + destruct (H xH a) as [x [P Q]]. auto. simpl in P. inv P. + destruct (H0 xH b) as [x [P Q]]. auto. simpl in P. inv P. + constructor. + apply IHm2. + intros. apply (H (xI i) x); auto. + intros. apply (H0 (xI i) y); auto. + } + intros. apply H with (j := xH); auto. Qed. Theorem elements_extensional: @@ -848,6 +849,57 @@ Module PTree <: TREE. destruct H0. congruence. Qed. + Lemma xelements_remove: + forall (A: Type) 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 ++ + 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'). + exists l1; + exists (l2 ++ + match o with None => nil | Some x => (prev j, x) :: nil end ++ + xelements m2 (xI j) nil); + 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. + Qed. + + Theorem elements_remove: + forall (A: Type) 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. + intros. exploit xelements_remove. eauto. instantiate (1 := xH). + 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 := match m with @@ -1268,64 +1320,23 @@ Variable V: Type. Definition cardinal (x: T.t V) : nat := List.length (T.elements x). -Remark list_incl_length: - forall (A: Type) (l1: list A), list_norepet l1 -> - forall (l2: list A), List.incl l1 l2 -> (List.length l1 <= List.length l2)%nat. -Proof. - induction 1; simpl; intros. - omega. - exploit (List.in_split hd l2). auto with coqlib. intros [l3 [l4 EQ]]. subst l2. - assert (length tl <= length (l3 ++ l4))%nat. - apply IHlist_norepet. red; intros. - exploit (H1 a); auto with coqlib. - repeat rewrite in_app_iff. simpl. intuition. subst. contradiction. - repeat rewrite app_length in *. simpl. omega. -Qed. - -Remark list_length_incl: - forall (A: Type) (l1: list A), list_norepet l1 -> - forall l2, List.incl l1 l2 -> List.length l1 = List.length l2 -> List.incl l2 l1. -Proof. - induction 1; simpl; intros. - destruct l2; simpl in *. auto with coqlib. discriminate. - exploit (List.in_split hd l2). auto with coqlib. intros [l3 [l4 EQ]]. subst l2. - assert (incl (l3 ++ l4) tl). - apply IHlist_norepet. red; intros. - exploit (H1 a); auto with coqlib. - repeat rewrite in_app_iff. simpl. intuition. subst. contradiction. - repeat rewrite app_length in *. simpl in H2. omega. - red; simpl; intros. rewrite in_app_iff in H4; simpl in H4. intuition. -Qed. - -Remark list_strict_incl_length: - forall (A: Type) (l1 l2: list A) (x: A), - list_norepet l1 -> List.incl l1 l2 -> ~In x l1 -> In x l2 -> - (List.length l1 < List.length l2)%nat. -Proof. - intros. exploit list_incl_length; eauto. intros. - assert (length l1 = length l2 \/ length l1 < length l2)%nat by omega. - destruct H4; auto. elim H1. eapply list_length_incl; eauto. -Qed. - -Remark list_norepet_map: - forall (A B: Type) (f: A -> B) (l: list A), - list_norepet (List.map f l) -> list_norepet l. +Theorem cardinal_remove: + forall x m y, T.get x m = Some y -> (cardinal (T.remove x m) < cardinal m)%nat. Proof. - induction l; simpl; intros. - constructor. - inv H. constructor; auto. red; intros; elim H2. apply List.in_map; auto. + unfold cardinal; intros. + exploit T.elements_remove; eauto. intros (l1 & l2 & P & Q). + rewrite P, Q. rewrite ! app_length. simpl. omega. Qed. -Theorem cardinal_remove: - forall x m y, T.get x m = Some y -> (cardinal (T.remove x m) < cardinal m)%nat. +Theorem cardinal_set: + forall x m y, T.get x m = None -> (cardinal m < cardinal (T.set x y m))%nat. Proof. - unfold cardinal; intros. apply list_strict_incl_length with (x := (x, y)). - apply list_norepet_map with (f := @fst T.elt V). apply T.elements_keys_norepet. - red; intros. destruct a as [x' y']. exploit T.elements_complete; eauto. - rewrite T.grspec. destruct (T.elt_eq x' x); intros; try discriminate. - apply T.elements_correct; auto. - red; intros. exploit T.elements_complete; eauto. rewrite T.grspec. rewrite dec_eq_true. congruence. - apply T.elements_correct; auto. + intros. set (m' := T.set x y m). + replace (cardinal m) with (cardinal (T.remove x m')). + apply cardinal_remove with y. unfold m'; apply T.gss. + unfold cardinal. f_equal. apply T.elements_extensional. + intros. unfold m'. rewrite T.grspec, T.gsspec. + destruct (T.elt_eq i x); auto. congruence. Qed. End MEASURE. -- cgit