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.

1 files changed, 133 insertions, 34 deletions

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).