Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 424 insertions, 0 deletions

diff --git a/theories/IntMap/Mapfold.v b/theories/IntMap/Mapfold.v
new file mode 100644
index 00000000..641529ee
--- /dev/null
+++ b/theories/IntMap/Mapfold.v
@@ -0,0 +1,424 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*i   	  $Id: Mapfold.v,v 1.4.2.1 2004/07/16 19:31:04 herbelin Exp $      i*)
+
+Require Import Bool.
+Require Import Sumbool.
+Require Import ZArith.
+Require Import Addr.
+Require Import Adist.
+Require Import Addec.
+Require Import Map.
+Require Import Fset.
+Require Import Mapaxioms.
+Require Import Mapiter.
+Require Import Lsort.
+Require Import Mapsubset.
+Require Import List.
+
+Section MapFoldResults.
+
+  Variable A : Set.
+
+  Variable M : Set.
+  Variable neutral : M.
+  Variable op : M -> M -> M.
+
+  Variable nleft : forall a:M, op neutral a = a.
+  Variable nright : forall a:M, op a neutral = a.
+  Variable assoc : forall a b c:M, op (op a b) c = op a (op b c).
+
+  Lemma MapFold_ext :
+   forall (f:ad -> A -> M) (m m':Map A),
+     eqmap A m m' -> MapFold _ _ neutral op f m = MapFold _ _ neutral op f m'.
+  Proof.
+    intros. rewrite (MapFold_as_fold A M neutral op assoc nleft nright f m).
+    rewrite (MapFold_as_fold A M neutral op assoc nleft nright f m').
+    cut (alist_of_Map A m = alist_of_Map A m'). intro. rewrite H0. reflexivity.
+    apply alist_canonical. unfold eqmap in H. apply eqm_trans with (f' := MapGet A m).
+    apply eqm_sym. apply alist_of_Map_semantics.
+    apply eqm_trans with (f' := MapGet A m'). assumption.
+    apply alist_of_Map_semantics.
+    apply alist_of_Map_sorts2.
+    apply alist_of_Map_sorts2.
+  Qed.
+
+  Lemma MapFold_ext_f_1 :
+   forall (m:Map A) (f g:ad -> A -> M) (pf:ad -> ad),
+     (forall (a:ad) (y:A), MapGet _ m a = SOME _ y -> f (pf a) y = g (pf a) y) ->
+     MapFold1 _ _ neutral op f pf m = MapFold1 _ _ neutral op g pf m.
+  Proof.
+    simple induction m. trivial.
+    simpl in |- *. intros. apply H. rewrite (ad_eq_correct a). reflexivity.
+    intros. simpl in |- *. rewrite (H f g (fun a0:ad => pf (ad_double a0))).
+    rewrite (H0 f g (fun a0:ad => pf (ad_double_plus_un a0))). reflexivity.
+    intros. apply H1. rewrite MapGet_M2_bit_0_1. rewrite ad_double_plus_un_div_2. assumption.
+    apply ad_double_plus_un_bit_0.
+    intros. apply H1. rewrite MapGet_M2_bit_0_0. rewrite ad_double_div_2. assumption.
+    apply ad_double_bit_0.
+  Qed.
+
+  Lemma MapFold_ext_f :
+   forall (f g:ad -> A -> M) (m:Map A),
+     (forall (a:ad) (y:A), MapGet _ m a = SOME _ y -> f a y = g a y) ->
+     MapFold _ _ neutral op f m = MapFold _ _ neutral op g m.
+  Proof.
+    intros. exact (MapFold_ext_f_1 m f g (fun a0:ad => a0) H).
+  Qed.
+
+  Lemma MapFold1_as_Fold_1 :
+   forall (m:Map A) (f f':ad -> A -> M) (pf pf':ad -> ad),
+     (forall (a:ad) (y:A), f (pf a) y = f' (pf' a) y) ->
+     MapFold1 _ _ neutral op f pf m = MapFold1 _ _ neutral op f' pf' m.
+  Proof.
+    simple induction m. trivial.
+    intros. simpl in |- *. apply H.
+    intros. simpl in |- *.
+    rewrite
+     (H f f' (fun a0:ad => pf (ad_double a0))
+        (fun a0:ad => pf' (ad_double a0))).
+    rewrite
+     (H0 f f' (fun a0:ad => pf (ad_double_plus_un a0))
+        (fun a0:ad => pf' (ad_double_plus_un a0))).
+    reflexivity.
+    intros. apply H1.
+    intros. apply H1.
+  Qed.
+
+  Lemma MapFold1_as_Fold :
+   forall (f:ad -> A -> M) (pf:ad -> ad) (m:Map A),
+     MapFold1 _ _ neutral op f pf m =
+     MapFold _ _ neutral op (fun (a:ad) (y:A) => f (pf a) y) m.
+  Proof.
+    intros. unfold MapFold in |- *. apply MapFold1_as_Fold_1. trivial.
+  Qed.
+
+  Lemma MapFold1_ext :
+   forall (f:ad -> A -> M) (m m':Map A),
+     eqmap A m m' ->
+     forall pf:ad -> ad,
+       MapFold1 _ _ neutral op f pf m = MapFold1 _ _ neutral op f pf m'.
+  Proof.
+    intros. rewrite MapFold1_as_Fold. rewrite MapFold1_as_Fold. apply MapFold_ext. assumption.
+  Qed.
+
+  Variable comm : forall a b:M, op a b = op b a.
+
+  Lemma MapFold_Put_disjoint_1 :
+   forall (p:positive) (f:ad -> A -> M) (pf:ad -> ad) 
+     (a1 a2:ad) (y1 y2:A),
+     ad_xor a1 a2 = ad_x p ->
+     MapFold1 A M neutral op f pf (MapPut1 A a1 y1 a2 y2 p) =
+     op (f (pf a1) y1) (f (pf a2) y2).
+  Proof.
+    simple induction p. intros. simpl in |- *. elim (sumbool_of_bool (ad_bit_0 a1)). intro H1. rewrite H1.
+    simpl in |- *. rewrite ad_div_2_double_plus_un. rewrite ad_div_2_double. apply comm.
+    change (ad_bit_0 a2 = negb true) in |- *. rewrite <- H1. rewrite (ad_neg_bit_0_2 _ _ _ H0).
+    rewrite negb_elim. reflexivity.
+    assumption.
+    intro H1. rewrite H1. simpl in |- *. rewrite ad_div_2_double. rewrite ad_div_2_double_plus_un.
+    reflexivity.
+    change (ad_bit_0 a2 = negb false) in |- *. rewrite <- H1. rewrite (ad_neg_bit_0_2 _ _ _ H0).
+    rewrite negb_elim. reflexivity.
+    assumption.
+    simpl in |- *. intros. elim (sumbool_of_bool (ad_bit_0 a1)). intro H1. rewrite H1. simpl in |- *.
+    rewrite nleft.
+    rewrite
+     (H f (fun a0:ad => pf (ad_double_plus_un a0)) (
+        ad_div_2 a1) (ad_div_2 a2) y1 y2).
+    rewrite ad_div_2_double_plus_un. rewrite ad_div_2_double_plus_un. reflexivity.
+    rewrite <- (ad_same_bit_0 _ _ _ H0). assumption.
+    assumption.
+    rewrite <- ad_xor_div_2. rewrite H0. reflexivity.
+    intro H1. rewrite H1. simpl in |- *. rewrite nright.
+    rewrite
+     (H f (fun a0:ad => pf (ad_double a0)) (ad_div_2 a1) (ad_div_2 a2) y1 y2)
+     .
+    rewrite ad_div_2_double. rewrite ad_div_2_double. reflexivity.
+    rewrite <- (ad_same_bit_0 _ _ _ H0). assumption.
+    assumption.
+    rewrite <- ad_xor_div_2. rewrite H0. reflexivity.
+    intros. simpl in |- *. elim (sumbool_of_bool (ad_bit_0 a1)). intro H0. rewrite H0. simpl in |- *.
+    rewrite ad_div_2_double. rewrite ad_div_2_double_plus_un. apply comm.
+    assumption.
+    change (ad_bit_0 a2 = negb true) in |- *. rewrite <- H0. rewrite (ad_neg_bit_0_1 _ _ H).
+    rewrite negb_elim. reflexivity.
+    intro H0. rewrite H0. simpl in |- *. rewrite ad_div_2_double. rewrite ad_div_2_double_plus_un.
+    reflexivity.
+    change (ad_bit_0 a2 = negb false) in |- *. rewrite <- H0. rewrite (ad_neg_bit_0_1 _ _ H).
+    rewrite negb_elim. reflexivity.
+    assumption.
+  Qed.
+
+  Lemma MapFold_Put_disjoint_2 :
+   forall (f:ad -> A -> M) (m:Map A) (a:ad) (y:A) (pf:ad -> ad),
+     MapGet A m a = NONE A ->
+     MapFold1 A M neutral op f pf (MapPut A m a y) =
+     op (f (pf a) y) (MapFold1 A M neutral op f pf m).
+  Proof.
+    simple induction m. intros. simpl in |- *. rewrite (nright (f (pf a) y)). reflexivity.
+    intros a1 y1 a2 y2 pf H. simpl in |- *. elim (ad_sum (ad_xor a1 a2)). intro H0. elim H0.
+    intros p H1. rewrite H1. rewrite comm. exact (MapFold_Put_disjoint_1 p f pf a1 a2 y1 y2 H1).
+    intro H0. rewrite (ad_eq_complete _ _ (ad_xor_eq_true _ _ H0)) in H.
+    rewrite (M1_semantics_1 A a2 y1) in H. discriminate H.
+    intros. elim (sumbool_of_bool (ad_bit_0 a)). intro H2.
+    cut (MapPut A (M2 A m0 m1) a y = M2 A m0 (MapPut A m1 (ad_div_2 a) y)). intro.
+    rewrite H3. simpl in |- *. rewrite (H0 (ad_div_2 a) y (fun a0:ad => pf (ad_double_plus_un a0))).
+    rewrite ad_div_2_double_plus_un. rewrite <- assoc.
+    rewrite
+     (comm (MapFold1 A M neutral op f (fun a0:ad => pf (ad_double a0)) m0)
+        (f (pf a) y)).
+    rewrite assoc. reflexivity.
+    assumption.
+    rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1) in H1. assumption.
+    simpl in |- *. elim (ad_sum a). intro H3. elim H3. intro p. elim p. intros p0 H4 H5. rewrite H5.
+    reflexivity.
+    intros p0 H4 H5. rewrite H5 in H2. discriminate H2.
+    intro H4. rewrite H4. reflexivity.
+    intro H3. rewrite H3 in H2. discriminate H2.
+    intro H2. cut (MapPut A (M2 A m0 m1) a y = M2 A (MapPut A m0 (ad_div_2 a) y) m1).
+    intro. rewrite H3. simpl in |- *. rewrite (H (ad_div_2 a) y (fun a0:ad => pf (ad_double a0))).
+    rewrite ad_div_2_double. rewrite <- assoc. reflexivity.
+    assumption.
+    rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1) in H1. assumption.
+    simpl in |- *. elim (ad_sum a). intro H3. elim H3. intro p. elim p. intros p0 H4 H5. rewrite H5 in H2.
+    discriminate H2.
+    intros p0 H4 H5. rewrite H5. reflexivity.
+    intro H4. rewrite H4 in H2. discriminate H2.
+    intro H3. rewrite H3. reflexivity.
+  Qed.
+
+  Lemma MapFold_Put_disjoint :
+   forall (f:ad -> A -> M) (m:Map A) (a:ad) (y:A),
+     MapGet A m a = NONE A ->
+     MapFold A M neutral op f (MapPut A m a y) =
+     op (f a y) (MapFold A M neutral op f m).
+  Proof.
+    intros. exact (MapFold_Put_disjoint_2 f m a y (fun a0:ad => a0) H).
+  Qed.
+
+  Lemma MapFold_Put_behind_disjoint_2 :
+   forall (f:ad -> A -> M) (m:Map A) (a:ad) (y:A) (pf:ad -> ad),
+     MapGet A m a = NONE A ->
+     MapFold1 A M neutral op f pf (MapPut_behind A m a y) =
+     op (f (pf a) y) (MapFold1 A M neutral op f pf m).
+  Proof.
+    intros. cut (eqmap A (MapPut_behind A m a y) (MapPut A m a y)). intro.
+    rewrite (MapFold1_ext f _ _ H0 pf). apply MapFold_Put_disjoint_2. assumption.
+    apply eqmap_trans with (m' := MapMerge A (M1 A a y) m). apply MapPut_behind_as_Merge.
+    apply eqmap_trans with (m' := MapMerge A m (M1 A a y)).
+    apply eqmap_trans with (m' := MapDelta A (M1 A a y) m). apply eqmap_sym. apply MapDelta_disjoint.
+    unfold MapDisjoint in |- *. unfold in_dom in |- *. simpl in |- *. intros. elim (sumbool_of_bool (ad_eq a a0)).
+    intro H2. rewrite (ad_eq_complete _ _ H2) in H. rewrite H in H1. discriminate H1.
+    intro H2. rewrite H2 in H0. discriminate H0.
+    apply eqmap_trans with (m' := MapDelta A m (M1 A a y)). apply MapDelta_sym.
+    apply MapDelta_disjoint. unfold MapDisjoint in |- *. unfold in_dom in |- *. simpl in |- *. intros.
+    elim (sumbool_of_bool (ad_eq a a0)). intro H2. rewrite (ad_eq_complete _ _ H2) in H.
+    rewrite H in H0. discriminate H0.
+    intro H2. rewrite H2 in H1. discriminate H1.
+    apply eqmap_sym. apply MapPut_as_Merge.
+  Qed.
+
+  Lemma MapFold_Put_behind_disjoint :
+   forall (f:ad -> A -> M) (m:Map A) (a:ad) (y:A),
+     MapGet A m a = NONE A ->
+     MapFold A M neutral op f (MapPut_behind A m a y) =
+     op (f a y) (MapFold A M neutral op f m).
+  Proof.
+    intros. exact (MapFold_Put_behind_disjoint_2 f m a y (fun a0:ad => a0) H).
+  Qed.
+
+  Lemma MapFold_Merge_disjoint_1 :
+   forall (f:ad -> A -> M) (m1 m2:Map A) (pf:ad -> ad),
+     MapDisjoint A A m1 m2 ->
+     MapFold1 A M neutral op f pf (MapMerge A m1 m2) =
+     op (MapFold1 A M neutral op f pf m1) (MapFold1 A M neutral op f pf m2).
+  Proof.
+    simple induction m1. simpl in |- *. intros. rewrite nleft. reflexivity.
+    intros. unfold MapMerge in |- *. apply (MapFold_Put_behind_disjoint_2 f m2 a a0 pf).
+    apply in_dom_none. exact (MapDisjoint_M1_l _ _ m2 a a0 H).
+    simple induction m2. intros. simpl in |- *. rewrite nright. reflexivity.
+    intros. unfold MapMerge in |- *. rewrite (MapFold_Put_disjoint_2 f (M2 A m m0) a a0 pf). apply comm.
+    apply in_dom_none. exact (MapDisjoint_M1_r _ _ (M2 A m m0) a a0 H1).
+    intros. simpl in |- *. rewrite (H m3 (fun a0:ad => pf (ad_double a0))).
+    rewrite (H0 m4 (fun a0:ad => pf (ad_double_plus_un a0))).
+    cut (forall a b c d:M, op (op a b) (op c d) = op (op a c) (op b d)). intro. apply H4.
+    intros. rewrite assoc. rewrite <- (assoc b c d). rewrite (comm b c). rewrite (assoc c b d).
+    rewrite assoc. reflexivity.
+    exact (MapDisjoint_M2_r _ _ _ _ _ _ H3).
+    exact (MapDisjoint_M2_l _ _ _ _ _ _ H3).
+  Qed.
+
+  Lemma MapFold_Merge_disjoint :
+   forall (f:ad -> A -> M) (m1 m2:Map A),
+     MapDisjoint A A m1 m2 ->
+     MapFold A M neutral op f (MapMerge A m1 m2) =
+     op (MapFold A M neutral op f m1) (MapFold A M neutral op f m2).
+  Proof.
+    intros. exact (MapFold_Merge_disjoint_1 f m1 m2 (fun a0:ad => a0) H).
+  Qed.
+ 
+End MapFoldResults.
+
+Section MapFoldDistr.
+
+  Variable A : Set.
+
+  Variable M : Set.
+  Variable neutral : M.
+  Variable op : M -> M -> M.
+
+  Variable M' : Set.
+  Variable neutral' : M'.
+  Variable op' : M' -> M' -> M'.
+
+  Variable N : Set.
+
+  Variable times : M -> N -> M'.
+
+  Variable absorb : forall c:N, times neutral c = neutral'.
+  Variable
+    distr :
+      forall (a b:M) (c:N), times (op a b) c = op' (times a c) (times b c).
+
+  Lemma MapFold_distr_r_1 :
+   forall (f:ad -> A -> M) (m:Map A) (c:N) (pf:ad -> ad),
+     times (MapFold1 A M neutral op f pf m) c =
+     MapFold1 A M' neutral' op' (fun (a:ad) (y:A) => times (f a y) c) pf m.
+  Proof.
+    simple induction m. intros. exact (absorb c).
+    trivial.
+    intros. simpl in |- *. rewrite distr. rewrite H. rewrite H0. reflexivity.
+  Qed.
+
+  Lemma MapFold_distr_r :
+   forall (f:ad -> A -> M) (m:Map A) (c:N),
+     times (MapFold A M neutral op f m) c =
+     MapFold A M' neutral' op' (fun (a:ad) (y:A) => times (f a y) c) m.
+  Proof.
+    intros. exact (MapFold_distr_r_1 f m c (fun a:ad => a)).
+  Qed.
+
+End MapFoldDistr.
+
+Section MapFoldDistrL.
+
+  Variable A : Set.
+
+  Variable M : Set.
+  Variable neutral : M.
+  Variable op : M -> M -> M.
+
+  Variable M' : Set.
+  Variable neutral' : M'.
+  Variable op' : M' -> M' -> M'.
+
+  Variable N : Set.
+
+  Variable times : N -> M -> M'.
+
+  Variable absorb : forall c:N, times c neutral = neutral'.
+  Variable
+    distr :
+      forall (a b:M) (c:N), times c (op a b) = op' (times c a) (times c b).
+
+  Lemma MapFold_distr_l :
+   forall (f:ad -> A -> M) (m:Map A) (c:N),
+     times c (MapFold A M neutral op f m) =
+     MapFold A M' neutral' op' (fun (a:ad) (y:A) => times c (f a y)) m.
+  Proof.
+    intros. apply MapFold_distr_r with (times := fun (a:M) (b:N) => times b a);
+  assumption.
+  Qed.
+
+End MapFoldDistrL.
+
+Section MapFoldExists.
+
+  Variable A : Set.
+
+  Lemma MapFold_orb_1 :
+   forall (f:ad -> A -> bool) (m:Map A) (pf:ad -> ad),
+     MapFold1 A bool false orb f pf m =
+     match MapSweep1 A f pf m with
+     | SOME _ => true
+     | _ => false
+     end.
+  Proof.
+    simple induction m. trivial.
+    intros a y pf. simpl in |- *. unfold MapSweep2 in |- *. case (f (pf a) y); reflexivity.
+    intros. simpl in |- *. rewrite (H (fun a0:ad => pf (ad_double a0))).
+    rewrite (H0 (fun a0:ad => pf (ad_double_plus_un a0))).
+    case (MapSweep1 A f (fun a0:ad => pf (ad_double a0)) m0); reflexivity.
+  Qed.
+
+  Lemma MapFold_orb :
+   forall (f:ad -> A -> bool) (m:Map A),
+     MapFold A bool false orb f m =
+     match MapSweep A f m with
+     | SOME _ => true
+     | _ => false
+     end.
+  Proof.
+    intros. exact (MapFold_orb_1 f m (fun a:ad => a)).
+  Qed.
+
+End MapFoldExists.
+
+Section DMergeDef.
+
+  Variable A : Set.
+
+  Definition DMerge :=
+    MapFold (Map A) (Map A) (M0 A) (MapMerge A) (fun (_:ad) (m:Map A) => m).
+
+  Lemma in_dom_DMerge_1 :
+   forall (m:Map (Map A)) (a:ad),
+     in_dom A a (DMerge m) =
+     match MapSweep _ (fun (_:ad) (m0:Map A) => in_dom A a m0) m with
+     | SOME _ => true
+     | _ => false
+     end.
+  Proof.
+    unfold DMerge in |- *. intros.
+    rewrite
+     (MapFold_distr_l (Map A) (Map A) (M0 A) (MapMerge A) bool false orb ad
+        (in_dom A) (fun c:ad => refl_equal _) (in_dom_merge A))
+     .
+    apply MapFold_orb.
+  Qed.
+
+  Lemma in_dom_DMerge_2 :
+   forall (m:Map (Map A)) (a:ad),
+     in_dom A a (DMerge m) = true ->
+     {b : ad & 
+     {m0 : Map A | MapGet _ m b = SOME _ m0 /\ in_dom A a m0 = true}}.
+  Proof.
+    intros m a. rewrite in_dom_DMerge_1.
+    elim
+     (option_sum _
+        (MapSweep (Map A) (fun (_:ad) (m0:Map A) => in_dom A a m0) m)).
+    intro H. elim H. intro r. elim r. intros b m0 H0. intro. split with b. split with m0.
+    split. exact (MapSweep_semantics_2 _ _ _ _ _ H0).
+    exact (MapSweep_semantics_1 _ _ _ _ _ H0).
+    intro H. rewrite H. intro. discriminate H0.
+  Qed.
+
+  Lemma in_dom_DMerge_3 :
+   forall (m:Map (Map A)) (a b:ad) (m0:Map A),
+     MapGet _ m a = SOME _ m0 ->
+     in_dom A b m0 = true -> in_dom A b (DMerge m) = true.
+  Proof.
+    intros m a b m0 H H0. rewrite in_dom_DMerge_1.
+    elim
+     (MapSweep_semantics_4 _ (fun (_:ad) (m'0:Map A) => in_dom A b m'0) _ _ _
+        H H0).
+    intros a' H1. elim H1. intros m'0 H2. rewrite H2. reflexivity.
+  Qed.
+
+End DMergeDef.
\ No newline at end of file