summaryrefslogtreecommitdiff
path: root/theories/IntMap/Mapfold.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /theories/IntMap/Mapfold.v
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'theories/IntMap/Mapfold.v')
-rw-r--r--theories/IntMap/Mapfold.v425
1 files changed, 0 insertions, 425 deletions
diff --git a/theories/IntMap/Mapfold.v b/theories/IntMap/Mapfold.v
deleted file mode 100644
index eb58cb64..00000000
--- a/theories/IntMap/Mapfold.v
+++ /dev/null
@@ -1,425 +0,0 @@
-(************************************************************************)
-(* 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 8733 2006-04-25 22:52:18Z letouzey $ i*)
-
-Require Import Bool.
-Require Import Sumbool.
-Require Import NArith.
-Require Import Ndigits.
-Require Import Ndec.
-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 (Neqb_correct a). reflexivity.
- intros. simpl in |- *. rewrite (H f g (fun a0:ad => pf (Ndouble a0))).
- rewrite (H0 f g (fun a0:ad => pf (Ndouble_plus_one a0))). reflexivity.
- intros. apply H1. rewrite MapGet_M2_bit_0_1. rewrite Ndouble_plus_one_div2. assumption.
- apply Ndouble_plus_one_bit0.
- intros. apply H1. rewrite MapGet_M2_bit_0_0. rewrite Ndouble_div2. assumption.
- apply Ndouble_bit0.
- 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 (Ndouble a0))
- (fun a0:ad => pf' (Ndouble a0))).
- rewrite
- (H0 f f' (fun a0:ad => pf (Ndouble_plus_one a0))
- (fun a0:ad => pf' (Ndouble_plus_one 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),
- Nxor a1 a2 = Npos 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 (Nbit0 a1)). intro H1. rewrite H1.
- simpl in |- *. rewrite Ndiv2_double_plus_one. rewrite Ndiv2_double. apply comm.
- change (Nbit0 a2 = negb true) in |- *. rewrite <- H1. rewrite (Nneg_bit0_2 _ _ _ H0).
- rewrite negb_elim. reflexivity.
- assumption.
- intro H1. rewrite H1. simpl in |- *. rewrite Ndiv2_double. rewrite Ndiv2_double_plus_one.
- reflexivity.
- change (Nbit0 a2 = negb false) in |- *. rewrite <- H1. rewrite (Nneg_bit0_2 _ _ _ H0).
- rewrite negb_elim. reflexivity.
- assumption.
- simpl in |- *. intros. elim (sumbool_of_bool (Nbit0 a1)). intro H1. rewrite H1. simpl in |- *.
- rewrite nleft.
- rewrite
- (H f (fun a0:ad => pf (Ndouble_plus_one a0)) (
- Ndiv2 a1) (Ndiv2 a2) y1 y2).
- rewrite Ndiv2_double_plus_one. rewrite Ndiv2_double_plus_one. reflexivity.
- unfold Nodd.
- rewrite <- (Nsame_bit0 _ _ _ H0). assumption.
- assumption.
- rewrite <- Nxor_div2. rewrite H0. reflexivity.
- intro H1. rewrite H1. simpl in |- *. rewrite nright.
- rewrite
- (H f (fun a0:ad => pf (Ndouble a0)) (Ndiv2 a1) (Ndiv2 a2) y1 y2)
- .
- rewrite Ndiv2_double. rewrite Ndiv2_double. reflexivity.
- unfold Neven.
- rewrite <- (Nsame_bit0 _ _ _ H0). assumption.
- assumption.
- rewrite <- Nxor_div2. rewrite H0. reflexivity.
- intros. simpl in |- *. elim (sumbool_of_bool (Nbit0 a1)). intro H0. rewrite H0. simpl in |- *.
- rewrite Ndiv2_double. rewrite Ndiv2_double_plus_one. apply comm.
- assumption.
- change (Nbit0 a2 = negb true) in |- *. rewrite <- H0. rewrite (Nneg_bit0_1 _ _ H).
- rewrite negb_elim. reflexivity.
- intro H0. rewrite H0. simpl in |- *. rewrite Ndiv2_double. rewrite Ndiv2_double_plus_one.
- reflexivity.
- change (Nbit0 a2 = negb false) in |- *. rewrite <- H0. rewrite (Nneg_bit0_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 ->
- 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 (Ndiscr (Nxor 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 (Neqb_complete _ _ (Nxor_eq_true _ _ H0)) in H.
- rewrite (M1_semantics_1 A a2 y1) in H. discriminate H.
- intros. elim (sumbool_of_bool (Nbit0 a)). intro H2.
- cut (MapPut A (M2 A m0 m1) a y = M2 A m0 (MapPut A m1 (Ndiv2 a) y)). intro.
- rewrite H3. simpl in |- *. rewrite (H0 (Ndiv2 a) y (fun a0:ad => pf (Ndouble_plus_one a0))).
- rewrite Ndiv2_double_plus_one. rewrite <- assoc.
- rewrite
- (comm (MapFold1 A M neutral op f (fun a0:ad => pf (Ndouble 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 (Ndiscr 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 (Ndiv2 a) y) m1).
- intro. rewrite H3. simpl in |- *. rewrite (H (Ndiv2 a) y (fun a0:ad => pf (Ndouble a0))).
- rewrite Ndiv2_double. rewrite <- assoc. reflexivity.
- assumption.
- rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1) in H1. assumption.
- simpl in |- *. elim (Ndiscr 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 ->
- 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 ->
- 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 (Neqb a a0)).
- intro H2. rewrite (Neqb_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 (Neqb a a0)). intro H2. rewrite (Neqb_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 ->
- 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 (Ndouble a0))).
- rewrite (H0 m4 (fun a0:ad => pf (Ndouble_plus_one 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 (Ndouble a0))).
- rewrite (H0 (fun a0:ad => pf (Ndouble_plus_one a0))).
- case (MapSweep1 A f (fun a0:ad => pf (Ndouble 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