summaryrefslogtreecommitdiff
path: root/theories/IntMap/Mapfold.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /theories/IntMap/Mapfold.v
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'theories/IntMap/Mapfold.v')
-rw-r--r--theories/IntMap/Mapfold.v424
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