From 0507fa6e0a242b58d90037ef0177ec85649e3f11 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Mar 2016 09:31:44 +0100 Subject: Preliminaries: extend the Coqlib and Maps libraries. - Coqlib: option_rel to lift a relation to option type. - Coqlib: more lemmas about list_forall2. - Coqlib: introduce type nlist (nonempty lists) and some operations. - Maps: a variant of PTree.elements_extensional that uses option_rel. --- lib/Maps.v | 167 ++++++++++++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 133 insertions(+), 34 deletions(-) (limited to 'lib/Maps.v') diff --git a/lib/Maps.v b/lib/Maps.v index 39fec9fd..b7825331 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -789,46 +789,42 @@ Module PTree <: TREE. intros. apply (H (xO i0)). Qed. - Theorem elements_canonical_order: + Theorem elements_canonical_order': forall (A B: Type) (R: A -> B -> Prop) (m: t A) (n: t B), - (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) -> + (forall i, option_rel R (get i m) (get i n)) -> list_forall2 (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 R. - assert (forall m n j, + 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)). + Qed. + + Theorem elements_canonical_order: + forall (A B: Type) (R: A -> B -> Prop) (m: t A) (n: t B), (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)) - (xelements m j nil) (xelements n j nil)). - { - 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 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. + (elements m) (elements n). + Proof. + intros. apply elements_canonical_order'. + intros. destruct (get i m) as [x|] eqn:GM. + exploit H; eauto. intros (y & P & Q). rewrite P; constructor; auto. + destruct (get i n) as [y|] eqn:GN. + exploit H0; eauto. intros (x & P & Q). congruence. + constructor. Qed. Theorem elements_extensional: @@ -837,9 +833,8 @@ Module PTree <: TREE. elements m = elements n. Proof. intros. - exploit (elements_canonical_order (fun (x y: A) => x = y) m n). - intros. rewrite H in H0. exists x; auto. - intros. rewrite <- H in H0. exists y; auto. + 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. Qed. @@ -1542,6 +1537,110 @@ Instance Equal_EqDec : EqDec (T.t A) Equal := Equal_dec. End EXTENSIONAL_EQUALITY. +(** Creating a tree from a list of (key, value) pairs. *) + +Section OF_LIST. + +Variable A: Type. + +Let f := fun (m: T.t A) (k_v: T.elt * A) => T.set (fst k_v) (snd k_v) m. + +Definition of_list (l: list (T.elt * A)) : T.t A := + List.fold_left f l (T.empty _). + +Lemma in_of_list: + forall l k v, T.get k (of_list l) = Some v -> In (k, v) l. +Proof. + assert (REC: forall k v l m, + T.get k (fold_left f l m) = Some v -> In (k, v) l \/ T.get k m = Some v). + { induction l as [ | [k1 v1] l]; simpl; intros. + - tauto. + - apply IHl in H. unfold f in H. simpl in H. rewrite T.gsspec in H. + destruct H; auto. + destruct (T.elt_eq k k1). inv H. auto. auto. + } + intros. apply REC in H. rewrite T.gempty in H. intuition congruence. +Qed. + +Lemma of_list_dom: + forall l k, In k (map fst l) -> exists v, T.get k (of_list l) = Some v. +Proof. + assert (REC: forall k l m, + In k (map fst l) \/ (exists v, T.get k m = Some v) -> + exists v, T.get k (fold_left f l m) = Some v). + { induction l as [ | [k1 v1] l]; simpl; intros. + - tauto. + - apply IHl. unfold f; rewrite T.gsspec. simpl. destruct (T.elt_eq k k1). + right; econstructor; eauto. + intuition congruence. + } + intros. apply REC. auto. +Qed. + +Remark of_list_unchanged: + forall k l m, ~In k (map fst l) -> T.get k (List.fold_left f l m) = T.get k m. +Proof. + induction l as [ | [k1 v1] l]; simpl; intros. +- auto. +- rewrite IHl by tauto. unfold f; apply T.gso; intuition auto. +Qed. + +Lemma of_list_unique: + forall k v l1 l2, + ~In k (map fst l2) -> T.get k (of_list (l1 ++ (k, v) :: l2)) = Some v. +Proof. + intros. unfold of_list. rewrite fold_left_app. simpl. + rewrite of_list_unchanged by auto. unfold f; apply T.gss. +Qed. + +Lemma of_list_norepet: + forall l k v, list_norepet (map fst l) -> In (k, v) l -> T.get k (of_list l) = Some v. +Proof. + assert (REC: forall k v l m, + list_norepet (map fst l) -> + In (k, v) l -> + T.get k (fold_left f l m) = Some v). + { induction l as [ | [k1 v1] l]; simpl; intros. + contradiction. + inv H. destruct H0. + inv H. rewrite of_list_unchanged by auto. apply T.gss. + apply IHl; auto. + } + intros; apply REC; auto. +Qed. + +Lemma of_list_elements: + forall m k, T.get k (of_list (T.elements m)) = T.get k m. +Proof. + intros. destruct (T.get k m) as [v|] eqn:M. +- apply of_list_norepet. apply T.elements_keys_norepet. apply T.elements_correct; auto. +- destruct (T.get k (of_list (T.elements m))) as [v|] eqn:M'; auto. + apply in_of_list in M'. apply T.elements_complete in M'. congruence. +Qed. + +End OF_LIST. + +Lemma of_list_related: + forall (A B: Type) (R: A -> B -> Prop) k l1 l2, + list_forall2 (fun ka kb => fst ka = fst kb /\ R (snd ka) (snd kb)) l1 l2 -> + option_rel R (T.get k (of_list l1)) (T.get k (of_list l2)). +Proof. + intros until k. unfold of_list. + set (R' := fun ka kb => fst ka = fst kb /\ R (snd ka) (snd kb)). + set (fa := fun (m : T.t A) (k_v : T.elt * A) => T.set (fst k_v) (snd k_v) m). + set (fb := fun (m : T.t B) (k_v : T.elt * B) => T.set (fst k_v) (snd k_v) m). + assert (REC: forall l1 l2, list_forall2 R' l1 l2 -> + forall m1 m2, option_rel R (T.get k m1) (T.get k m2) -> + option_rel R (T.get k (fold_left fa l1 m1)) (T.get k (fold_left fb l2 m2))). + { induction 1; intros; simpl. + - auto. + - apply IHlist_forall2. unfold fa, fb. rewrite ! T.gsspec. + destruct H as [E F]. rewrite E. destruct (T.elt_eq k (fst b1)). + constructor; auto. + auto. } + intros. apply REC; auto. rewrite ! T.gempty. constructor. +Qed. + End Tree_Properties. Module PTree_Properties := Tree_Properties(PTree). -- cgit