Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

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