diff options
Diffstat (limited to 'theories/IntMap/Mapiter.v')
| -rw-r--r-- | theories/IntMap/Mapiter.v | 865 |
1 files changed, 479 insertions, 386 deletions
diff --git a/theories/IntMap/Mapiter.v b/theories/IntMap/Mapiter.v index 216a07c630..3c0aad8028 100644 --- a/theories/IntMap/Mapiter.v +++ b/theories/IntMap/Mapiter.v @@ -7,16 +7,16 @@ (***********************************************************************) (*i $Id$ i*) -Require Bool. -Require Sumbool. -Require ZArith. -Require Addr. -Require Adist. -Require Addec. -Require Map. -Require Mapaxioms. -Require Fset. -Require PolyList. +Require Import Bool. +Require Import Sumbool. +Require Import ZArith. +Require Import Addr. +Require Import Adist. +Require Import Addec. +Require Import Map. +Require Import Mapaxioms. +Require Import Fset. +Require Import List. Section MapIter. @@ -24,172 +24,200 @@ Section MapIter. Section MapSweepDef. - Variable f:ad->A->bool. - - Definition MapSweep2 := [a0:ad; y:A] if (f a0 y) then (SOME ? (a0, y)) else (NONE ?). - - Fixpoint MapSweep1 [pf:ad->ad; m:(Map A)] : (option (ad * A)) := - Cases m of - M0 => (NONE ?) - | (M1 a y) => (MapSweep2 (pf a) y) - | (M2 m m') => Cases (MapSweep1 ([a:ad] (pf (ad_double a))) m) of - (SOME r) => (SOME ? r) - | NONE => (MapSweep1 ([a:ad] (pf (ad_double_plus_un a))) m') - end + Variable f : ad -> A -> bool. + + Definition MapSweep2 (a0:ad) (y:A) := + if f a0 y then SOME _ (a0, y) else NONE _. + + Fixpoint MapSweep1 (pf:ad -> ad) (m:Map A) {struct m} : + option (ad * A) := + match m with + | M0 => NONE _ + | M1 a y => MapSweep2 (pf a) y + | M2 m m' => + match MapSweep1 (fun a:ad => pf (ad_double a)) m with + | SOME r => SOME _ r + | NONE => MapSweep1 (fun a:ad => pf (ad_double_plus_un a)) m' + end end. - Definition MapSweep := [m:(Map A)] (MapSweep1 ([a:ad] a) m). + Definition MapSweep (m:Map A) := MapSweep1 (fun a:ad => a) m. - Lemma MapSweep_semantics_1_1 : (m:(Map A)) (pf:ad->ad) (a:ad) (y:A) - (MapSweep1 pf m)=(SOME ? (a, y)) -> (f a y)=true. + Lemma MapSweep_semantics_1_1 : + forall (m:Map A) (pf:ad -> ad) (a:ad) (y:A), + MapSweep1 pf m = SOME _ (a, y) -> f a y = true. Proof. - Induction m. Intros. Discriminate H. - Simpl. Intros a y pf a0 y0. Elim (sumbool_of_bool (f (pf a) y)). Intro H. Unfold MapSweep2. - Rewrite H. Intro H0. Inversion H0. Rewrite <- H3. Assumption. - Intro H. Unfold MapSweep2. Rewrite H. Intro H0. Discriminate H0. - Simpl. Intros. Elim (option_sum ad*A (MapSweep1 [a0:ad](pf (ad_double a0)) m0)). - Intro H2. Elim H2. Intros r H3. Rewrite H3 in H1. Inversion H1. Rewrite H5 in H3. - Exact (H [a0:ad](pf (ad_double a0)) a y H3). - Intro H2. Rewrite H2 in H1. Exact (H0 [a0:ad](pf (ad_double_plus_un a0)) a y H1). + simple induction m. intros. discriminate H. + simpl in |- *. intros a y pf a0 y0. elim (sumbool_of_bool (f (pf a) y)). intro H. unfold MapSweep2 in |- *. + rewrite H. intro H0. inversion H0. rewrite <- H3. assumption. + intro H. unfold MapSweep2 in |- *. rewrite H. intro H0. discriminate H0. + simpl in |- *. intros. elim (option_sum (ad * A) (MapSweep1 (fun a0:ad => pf (ad_double a0)) m0)). + intro H2. elim H2. intros r H3. rewrite H3 in H1. inversion H1. rewrite H5 in H3. + exact (H (fun a0:ad => pf (ad_double a0)) a y H3). + intro H2. rewrite H2 in H1. exact (H0 (fun a0:ad => pf (ad_double_plus_un a0)) a y H1). Qed. - Lemma MapSweep_semantics_1 : (m:(Map A)) (a:ad) (y:A) - (MapSweep m)=(SOME ? (a, y)) -> (f a y)=true. + Lemma MapSweep_semantics_1 : + forall (m:Map A) (a:ad) (y:A), MapSweep m = SOME _ (a, y) -> f a y = true. Proof. - Intros. Exact (MapSweep_semantics_1_1 m [a:ad]a a y H). + intros. exact (MapSweep_semantics_1_1 m (fun a:ad => a) a y H). Qed. - Lemma MapSweep_semantics_2_1 : (m:(Map A)) (pf:ad->ad) (a:ad) (y:A) - (MapSweep1 pf m)=(SOME ? (a, y)) -> {a':ad | a=(pf a')}. + Lemma MapSweep_semantics_2_1 : + forall (m:Map A) (pf:ad -> ad) (a:ad) (y:A), + MapSweep1 pf m = SOME _ (a, y) -> {a' : ad | a = pf a'}. Proof. - Induction m. Intros. Discriminate H. - Simpl. Unfold MapSweep2. Intros a y pf a0 y0. Case (f (pf a) y). Intros. Split with a. - Inversion H. Reflexivity. - Intro. Discriminate H. - Intros m0 H m1 H0 pf a y. Simpl. - Elim (option_sum ad*A (MapSweep1 [a0:ad](pf (ad_double a0)) m0)). Intro H1. Elim H1. - Intros r H2. Rewrite H2. Intro H3. Inversion H3. Rewrite H5 in H2. - Elim (H [a0:ad](pf (ad_double a0)) a y H2). Intros a0 H6. Split with (ad_double a0). - Assumption. - Intro H1. Rewrite H1. Intro H2. Elim (H0 [a0:ad](pf (ad_double_plus_un a0)) a y H2). - Intros a0 H3. Split with (ad_double_plus_un a0). Assumption. + simple induction m. intros. discriminate H. + simpl in |- *. unfold MapSweep2 in |- *. intros a y pf a0 y0. case (f (pf a) y). intros. split with a. + inversion H. reflexivity. + intro. discriminate H. + intros m0 H m1 H0 pf a y. simpl in |- *. + elim + (option_sum (ad * A) (MapSweep1 (fun a0:ad => pf (ad_double a0)) m0)). intro H1. elim H1. + intros r H2. rewrite H2. intro H3. inversion H3. rewrite H5 in H2. + elim (H (fun a0:ad => pf (ad_double a0)) a y H2). intros a0 H6. split with (ad_double a0). + assumption. + intro H1. rewrite H1. intro H2. elim (H0 (fun a0:ad => pf (ad_double_plus_un a0)) a y H2). + intros a0 H3. split with (ad_double_plus_un a0). assumption. Qed. - Lemma MapSweep_semantics_2_2 : (m:(Map A)) - (pf,fp:ad->ad) ((a0:ad) (fp (pf a0))=a0) -> (a:ad) (y:A) - (MapSweep1 pf m)=(SOME ? (a, y)) -> (MapGet A m (fp a))=(SOME ? y). + Lemma MapSweep_semantics_2_2 : + forall (m:Map A) (pf fp:ad -> ad), + (forall a0:ad, fp (pf a0) = a0) -> + forall (a:ad) (y:A), + MapSweep1 pf m = SOME _ (a, y) -> MapGet A m (fp a) = SOME _ y. Proof. - Induction m. Intros. Discriminate H0. - Simpl. Intros a y pf fp H a0 y0. Unfold MapSweep2. Elim (sumbool_of_bool (f (pf a) y)). - Intro H0. Rewrite H0. Intro H1. Inversion H1. Rewrite (H a). Rewrite (ad_eq_correct a). - Reflexivity. - Intro H0. Rewrite H0. Intro H1. Discriminate H1. - Intros. Rewrite (MapGet_M2_bit_0_if A m0 m1 (fp a)). Elim (sumbool_of_bool (ad_bit_0 (fp a))). - Intro H3. Rewrite H3. Elim (option_sum ad*A (MapSweep1 [a0:ad](pf (ad_double a0)) m0)). - Intro H4. Simpl in H2. Apply (H0 [a0:ad](pf (ad_double_plus_un a0)) [a0:ad](ad_div_2 (fp a0))). - Intro. Rewrite H1. Apply ad_double_plus_un_div_2. - Elim (option_sum ad*A (MapSweep1 [a0:ad](pf (ad_double a0)) m0)). Intro H5. Elim H5. - Intros r H6. Rewrite H6 in H2. Inversion H2. Rewrite H8 in H6. - Elim (MapSweep_semantics_2_1 m0 [a0:ad](pf (ad_double a0)) a y H6). Intros a0 H9. - Rewrite H9 in H3. Rewrite (H1 (ad_double a0)) in H3. Rewrite (ad_double_bit_0 a0) in H3. - Discriminate H3. - Intro H5. Rewrite H5 in H2. Assumption. - Intro H4. Simpl in H2. Rewrite H4 in H2. - Apply (H0 [a0:ad](pf (ad_double_plus_un a0)) [a0:ad](ad_div_2 (fp a0))). Intro. - Rewrite H1. Apply ad_double_plus_un_div_2. - Assumption. - Intro H3. Rewrite H3. Simpl in H2. - Elim (option_sum ad*A (MapSweep1 [a0:ad](pf (ad_double a0)) m0)). Intro H4. Elim H4. - Intros r H5. Rewrite H5 in H2. Inversion H2. Rewrite H7 in H5. - Apply (H [a0:ad](pf (ad_double a0)) [a0:ad](ad_div_2 (fp a0))). Intro. Rewrite H1. - Apply ad_double_div_2. - Assumption. - Intro H4. Rewrite H4 in H2. - Elim (MapSweep_semantics_2_1 m1 [a0:ad](pf (ad_double_plus_un a0)) a y H2). - Intros a0 H5. Rewrite H5 in H3. Rewrite (H1 (ad_double_plus_un a0)) in H3. - Rewrite (ad_double_plus_un_bit_0 a0) in H3. Discriminate H3. + simple induction m. intros. discriminate H0. + simpl in |- *. intros a y pf fp H a0 y0. unfold MapSweep2 in |- *. elim (sumbool_of_bool (f (pf a) y)). + intro H0. rewrite H0. intro H1. inversion H1. rewrite (H a). rewrite (ad_eq_correct a). + reflexivity. + intro H0. rewrite H0. intro H1. discriminate H1. + intros. rewrite (MapGet_M2_bit_0_if A m0 m1 (fp a)). elim (sumbool_of_bool (ad_bit_0 (fp a))). + intro H3. rewrite H3. elim (option_sum (ad * A) (MapSweep1 (fun a0:ad => pf (ad_double a0)) m0)). + intro H4. simpl in H2. apply + (H0 (fun a0:ad => pf (ad_double_plus_un a0)) + (fun a0:ad => ad_div_2 (fp a0))). + intro. rewrite H1. apply ad_double_plus_un_div_2. + elim + (option_sum (ad * A) (MapSweep1 (fun a0:ad => pf (ad_double a0)) m0)). intro H5. elim H5. + intros r H6. rewrite H6 in H2. inversion H2. rewrite H8 in H6. + elim (MapSweep_semantics_2_1 m0 (fun a0:ad => pf (ad_double a0)) a y H6). intros a0 H9. + rewrite H9 in H3. rewrite (H1 (ad_double a0)) in H3. rewrite (ad_double_bit_0 a0) in H3. + discriminate H3. + intro H5. rewrite H5 in H2. assumption. + intro H4. simpl in H2. rewrite H4 in H2. + apply + (H0 (fun a0:ad => pf (ad_double_plus_un a0)) + (fun a0:ad => ad_div_2 (fp a0))). intro. + rewrite H1. apply ad_double_plus_un_div_2. + assumption. + intro H3. rewrite H3. simpl in H2. + elim + (option_sum (ad * A) (MapSweep1 (fun a0:ad => pf (ad_double a0)) m0)). intro H4. elim H4. + intros r H5. rewrite H5 in H2. inversion H2. rewrite H7 in H5. + apply + (H (fun a0:ad => pf (ad_double a0)) (fun a0:ad => ad_div_2 (fp a0))). intro. rewrite H1. + apply ad_double_div_2. + assumption. + intro H4. rewrite H4 in H2. + elim + (MapSweep_semantics_2_1 m1 (fun a0:ad => pf (ad_double_plus_un a0)) a y + H2). + intros a0 H5. rewrite H5 in H3. rewrite (H1 (ad_double_plus_un a0)) in H3. + rewrite (ad_double_plus_un_bit_0 a0) in H3. discriminate H3. Qed. - Lemma MapSweep_semantics_2 : (m:(Map A)) (a:ad) (y:A) - (MapSweep m)=(SOME ? (a, y)) -> (MapGet A m a)=(SOME ? y). + Lemma MapSweep_semantics_2 : + forall (m:Map A) (a:ad) (y:A), + MapSweep m = SOME _ (a, y) -> MapGet A m a = SOME _ y. Proof. - Intros. - Exact (MapSweep_semantics_2_2 m [a0:ad]a0 [a0:ad]a0 [a0:ad](refl_equal ad a0) a y H). + intros. + exact + (MapSweep_semantics_2_2 m (fun a0:ad => a0) (fun a0:ad => a0) + (fun a0:ad => refl_equal a0) a y H). Qed. - Lemma MapSweep_semantics_3_1 : (m:(Map A)) (pf:ad->ad) - (MapSweep1 pf m)=(NONE ?) -> - (a:ad) (y:A) (MapGet A m a)=(SOME ? y) -> (f (pf a) y)=false. + Lemma MapSweep_semantics_3_1 : + forall (m:Map A) (pf:ad -> ad), + MapSweep1 pf m = NONE _ -> + forall (a:ad) (y:A), MapGet A m a = SOME _ y -> f (pf a) y = false. Proof. - Induction m. Intros. Discriminate H0. - Simpl. Unfold MapSweep2. Intros a y pf. Elim (sumbool_of_bool (f (pf a) y)). Intro H. - Rewrite H. Intro. Discriminate H0. - Intro H. Rewrite H. Intros H0 a0 y0. Elim (sumbool_of_bool (ad_eq a a0)). Intro H1. Rewrite H1. - Intro H2. Inversion H2. Rewrite <- H4. Rewrite <- (ad_eq_complete ? ? H1). Assumption. - Intro H1. Rewrite H1. Intro. Discriminate H2. - Intros. Simpl in H1. Elim (option_sum ad*A (MapSweep1 [a:ad](pf (ad_double a)) m0)). - Intro H3. Elim H3. Intros r H4. Rewrite H4 in H1. Discriminate H1. - Intro H3. Rewrite H3 in H1. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H4. - Rewrite (MapGet_M2_bit_0_1 A a H4 m0 m1) in H2. Rewrite <- (ad_div_2_double_plus_un a H4). - Exact (H0 [a:ad](pf (ad_double_plus_un a)) H1 (ad_div_2 a) y H2). - Intro H4. Rewrite (MapGet_M2_bit_0_0 A a H4 m0 m1) in H2. Rewrite <- (ad_div_2_double a H4). - Exact (H [a:ad](pf (ad_double a)) H3 (ad_div_2 a) y H2). + simple induction m. intros. discriminate H0. + simpl in |- *. unfold MapSweep2 in |- *. intros a y pf. elim (sumbool_of_bool (f (pf a) y)). intro H. + rewrite H. intro. discriminate H0. + intro H. rewrite H. intros H0 a0 y0. elim (sumbool_of_bool (ad_eq a a0)). intro H1. rewrite H1. + intro H2. inversion H2. rewrite <- H4. rewrite <- (ad_eq_complete _ _ H1). assumption. + intro H1. rewrite H1. intro. discriminate H2. + intros. simpl in H1. elim (option_sum (ad * A) (MapSweep1 (fun a:ad => pf (ad_double a)) m0)). + intro H3. elim H3. intros r H4. rewrite H4 in H1. discriminate H1. + intro H3. rewrite H3 in H1. elim (sumbool_of_bool (ad_bit_0 a)). intro H4. + rewrite (MapGet_M2_bit_0_1 A a H4 m0 m1) in H2. rewrite <- (ad_div_2_double_plus_un a H4). + exact (H0 (fun a:ad => pf (ad_double_plus_un a)) H1 (ad_div_2 a) y H2). + intro H4. rewrite (MapGet_M2_bit_0_0 A a H4 m0 m1) in H2. rewrite <- (ad_div_2_double a H4). + exact (H (fun a:ad => pf (ad_double a)) H3 (ad_div_2 a) y H2). Qed. - Lemma MapSweep_semantics_3 : (m:(Map A)) - (MapSweep m)=(NONE ?) -> (a:ad) (y:A) (MapGet A m a)=(SOME ? y) -> - (f a y)=false. + Lemma MapSweep_semantics_3 : + forall m:Map A, + MapSweep m = NONE _ -> + forall (a:ad) (y:A), MapGet A m a = SOME _ y -> f a y = false. Proof. - Intros. - Exact (MapSweep_semantics_3_1 m [a0:ad]a0 H a y H0). + intros. + exact (MapSweep_semantics_3_1 m (fun a0:ad => a0) H a y H0). Qed. - Lemma MapSweep_semantics_4_1 : (m:(Map A)) (pf:ad->ad) (a:ad) (y:A) - (MapGet A m a)=(SOME A y) -> (f (pf a) y)=true -> - {a':ad & {y':A | (MapSweep1 pf m)=(SOME ? (a', y'))}}. + Lemma MapSweep_semantics_4_1 : + forall (m:Map A) (pf:ad -> ad) (a:ad) (y:A), + MapGet A m a = SOME A y -> + f (pf a) y = true -> + {a' : ad & {y' : A | MapSweep1 pf m = SOME _ (a', y')}}. Proof. - Induction m. Intros. Discriminate H. - Intros. Elim (sumbool_of_bool (ad_eq a a1)). Intro H1. Split with (pf a1). Split with y. - Rewrite (ad_eq_complete ? ? H1). Unfold MapSweep1 MapSweep2. - Rewrite (ad_eq_complete ? ? H1) in H. Rewrite (M1_semantics_1 ? a1 a0) in H. - Inversion H. Rewrite H0. Reflexivity. - - Intro H1. Rewrite (M1_semantics_2 ? a a1 a0 H1) in H. Discriminate H. - - Intros. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H3. - Rewrite (MapGet_M2_bit_0_1 ? ? H3 m0 m1) in H1. - Rewrite <- (ad_div_2_double_plus_un a H3) in H2. - Elim (H0 [a0:ad](pf (ad_double_plus_un a0)) (ad_div_2 a) y H1 H2). Intros a'' H4. Elim H4. - Intros y'' H5. Simpl. Elim (option_sum ? (MapSweep1 [a:ad](pf (ad_double a)) m0)). - Intro H6. Elim H6. Intro r. Elim r. Intros a''' y''' H7. Rewrite H7. Split with a'''. - Split with y'''. Reflexivity. - Intro H6. Rewrite H6. Split with a''. Split with y''. Assumption. - Intro H3. Rewrite (MapGet_M2_bit_0_0 ? ? H3 m0 m1) in H1. - Rewrite <- (ad_div_2_double a H3) in H2. - Elim (H [a0:ad](pf (ad_double a0)) (ad_div_2 a) y H1 H2). Intros a'' H4. Elim H4. - Intros y'' H5. Split with a''. Split with y''. Simpl. Rewrite H5. Reflexivity. + simple induction m. intros. discriminate H. + intros. elim (sumbool_of_bool (ad_eq a a1)). intro H1. split with (pf a1). split with y. + rewrite (ad_eq_complete _ _ H1). unfold MapSweep1, MapSweep2 in |- *. + rewrite (ad_eq_complete _ _ H1) in H. rewrite (M1_semantics_1 _ a1 a0) in H. + inversion H. rewrite H0. reflexivity. + + intro H1. rewrite (M1_semantics_2 _ a a1 a0 H1) in H. discriminate H. + + intros. elim (sumbool_of_bool (ad_bit_0 a)). intro H3. + rewrite (MapGet_M2_bit_0_1 _ _ H3 m0 m1) in H1. + rewrite <- (ad_div_2_double_plus_un a H3) in H2. + elim (H0 (fun a0:ad => pf (ad_double_plus_un a0)) (ad_div_2 a) y H1 H2). intros a'' H4. elim H4. + intros y'' H5. simpl in |- *. elim (option_sum _ (MapSweep1 (fun a:ad => pf (ad_double a)) m0)). + intro H6. elim H6. intro r. elim r. intros a''' y''' H7. rewrite H7. split with a'''. + split with y'''. reflexivity. + intro H6. rewrite H6. split with a''. split with y''. assumption. + intro H3. rewrite (MapGet_M2_bit_0_0 _ _ H3 m0 m1) in H1. + rewrite <- (ad_div_2_double a H3) in H2. + elim (H (fun a0:ad => pf (ad_double a0)) (ad_div_2 a) y H1 H2). intros a'' H4. elim H4. + intros y'' H5. split with a''. split with y''. simpl in |- *. rewrite H5. reflexivity. Qed. - Lemma MapSweep_semantics_4 : (m:(Map A)) (a:ad) (y:A) - (MapGet A m a)=(SOME A y) -> (f a y)=true -> - {a':ad & {y':A | (MapSweep m)=(SOME ? (a', y'))}}. + Lemma MapSweep_semantics_4 : + forall (m:Map A) (a:ad) (y:A), + MapGet A m a = SOME A y -> + f a y = true -> {a' : ad & {y' : A | MapSweep m = SOME _ (a', y')}}. Proof. - Intros. Exact (MapSweep_semantics_4_1 m [a0:ad]a0 a y H H0). + intros. exact (MapSweep_semantics_4_1 m (fun a0:ad => a0) a y H H0). Qed. End MapSweepDef. Variable B : Set. - Fixpoint MapCollect1 [f:ad->A->(Map B); pf:ad->ad; m:(Map A)] : (Map B) := - Cases m of - M0 => (M0 B) - | (M1 a y) => (f (pf a) y) - | (M2 m1 m2) => (MapMerge B (MapCollect1 f [a0:ad] (pf (ad_double a0)) m1) - (MapCollect1 f [a0:ad] (pf (ad_double_plus_un a0)) m2)) + Fixpoint MapCollect1 (f:ad -> A -> Map B) (pf:ad -> ad) + (m:Map A) {struct m} : Map B := + match m with + | M0 => M0 B + | M1 a y => f (pf a) y + | M2 m1 m2 => + MapMerge B (MapCollect1 f (fun a0:ad => pf (ad_double a0)) m1) + (MapCollect1 f (fun a0:ad => pf (ad_double_plus_un a0)) m2) end. - Definition MapCollect := [f:ad->A->(Map B); m:(Map A)] (MapCollect1 f [a:ad]a m). + Definition MapCollect (f:ad -> A -> Map B) (m:Map A) := + MapCollect1 f (fun a:ad => a) m. Section MapFoldDef. @@ -197,331 +225,396 @@ Section MapIter. Variable neutral : M. Variable op : M -> M -> M. - Fixpoint MapFold1 [f:ad->A->M; pf:ad->ad; m:(Map A)] : M := - Cases m of - M0 => neutral - | (M1 a y) => (f (pf a) y) - | (M2 m1 m2) => (op (MapFold1 f [a0:ad] (pf (ad_double a0)) m1) - (MapFold1 f [a0:ad] (pf (ad_double_plus_un a0)) m2)) + Fixpoint MapFold1 (f:ad -> A -> M) (pf:ad -> ad) + (m:Map A) {struct m} : M := + match m with + | M0 => neutral + | M1 a y => f (pf a) y + | M2 m1 m2 => + op (MapFold1 f (fun a0:ad => pf (ad_double a0)) m1) + (MapFold1 f (fun a0:ad => pf (ad_double_plus_un a0)) m2) end. - Definition MapFold := [f:ad->A->M; m:(Map A)] (MapFold1 f [a:ad]a m). + Definition MapFold (f:ad -> A -> M) (m:Map A) := + MapFold1 f (fun a:ad => a) m. - Lemma MapFold_empty : (f:ad->A->M) (MapFold f (M0 A))=neutral. + Lemma MapFold_empty : forall f:ad -> A -> M, MapFold f (M0 A) = neutral. Proof. - Trivial. + trivial. Qed. - Lemma MapFold_M1 : (f:ad->A->M) (a:ad) (y:A) (MapFold f (M1 A a y)) = (f a y). + Lemma MapFold_M1 : + forall (f:ad -> A -> M) (a:ad) (y:A), MapFold f (M1 A a y) = f a y. Proof. - Trivial. + trivial. Qed. Variable State : Set. - Variable f:State -> ad -> A -> State * M. - - Fixpoint MapFold1_state [state:State; pf:ad->ad; m:(Map A)] - : State * M := - Cases m of - M0 => (state, neutral) - | (M1 a y) => (f state (pf a) y) - | (M2 m1 m2) => - Cases (MapFold1_state state [a0:ad] (pf (ad_double a0)) m1) of - (state1, x1) => - Cases (MapFold1_state state1 [a0:ad] (pf (ad_double_plus_un a0)) m2) of - (state2, x2) => (state2, (op x1 x2)) - end + Variable f : State -> ad -> A -> State * M. + + Fixpoint MapFold1_state (state:State) (pf:ad -> ad) + (m:Map A) {struct m} : State * M := + match m with + | M0 => (state, neutral) + | M1 a y => f state (pf a) y + | M2 m1 m2 => + match MapFold1_state state (fun a0:ad => pf (ad_double a0)) m1 with + | (state1, x1) => + match + MapFold1_state state1 + (fun a0:ad => pf (ad_double_plus_un a0)) m2 + with + | (state2, x2) => (state2, op x1 x2) + end end end. - Definition MapFold_state := [state:State] (MapFold1_state state [a:ad]a). + Definition MapFold_state (state:State) := + MapFold1_state state (fun a:ad => a). - Lemma pair_sp : (B,C:Set) (x:B*C) x=(Fst x, Snd x). + Lemma pair_sp : forall (B C:Set) (x:B * C), x = (fst x, snd x). Proof. - Induction x. Trivial. + simple induction x. trivial. Qed. - Lemma MapFold_state_stateless_1 : (m:(Map A)) (g:ad->A->M) (pf:ad->ad) - ((state:State) (a:ad) (y:A) (Snd (f state a y))=(g a y)) -> - (state:State) - (Snd (MapFold1_state state pf m))=(MapFold1 g pf m). + Lemma MapFold_state_stateless_1 : + forall (m:Map A) (g:ad -> A -> M) (pf:ad -> ad), + (forall (state:State) (a:ad) (y:A), snd (f state a y) = g a y) -> + forall state:State, snd (MapFold1_state state pf m) = MapFold1 g pf m. Proof. - Induction m. Trivial. - Intros. Simpl. Apply H. - Intros. Simpl. Rewrite (pair_sp ? ? - (MapFold1_state state [a0:ad](pf (ad_double a0)) m0)). - Rewrite (H g [a0:ad](pf (ad_double a0)) H1 state). - Rewrite (pair_sp ? ? + simple induction m. trivial. + intros. simpl in |- *. apply H. + intros. simpl in |- *. rewrite + (pair_sp _ _ (MapFold1_state state (fun a0:ad => pf (ad_double a0)) m0)) + . + rewrite (H g (fun a0:ad => pf (ad_double a0)) H1 state). + rewrite + (pair_sp _ _ (MapFold1_state - (Fst (MapFold1_state state [a0:ad](pf (ad_double a0)) m0)) - [a0:ad](pf (ad_double_plus_un a0)) m1)). - Simpl. - Rewrite (H0 g [a0:ad](pf (ad_double_plus_un a0)) H1 - (Fst (MapFold1_state state [a0:ad](pf (ad_double a0)) m0))). - Reflexivity. + (fst (MapFold1_state state (fun a0:ad => pf (ad_double a0)) m0)) + (fun a0:ad => pf (ad_double_plus_un a0)) m1)) + . + simpl in |- *. + rewrite + (H0 g (fun a0:ad => pf (ad_double_plus_un a0)) H1 + (fst (MapFold1_state state (fun a0:ad => pf (ad_double a0)) m0))) + . + reflexivity. Qed. - Lemma MapFold_state_stateless : (g:ad->A->M) - ((state:State) (a:ad) (y:A) (Snd (f state a y))=(g a y)) -> - (state:State) (m:(Map A)) - (Snd (MapFold_state state m))=(MapFold g m). + Lemma MapFold_state_stateless : + forall g:ad -> A -> M, + (forall (state:State) (a:ad) (y:A), snd (f state a y) = g a y) -> + forall (state:State) (m:Map A), + snd (MapFold_state state m) = MapFold g m. Proof. - Intros. Exact (MapFold_state_stateless_1 m g [a0:ad]a0 H state). + intros. exact (MapFold_state_stateless_1 m g (fun a0:ad => a0) H state). Qed. End MapFoldDef. - Lemma MapCollect_as_Fold : (f:ad->A->(Map B)) (m:(Map A)) - (MapCollect f m)=(MapFold (Map B) (M0 B) (MapMerge B) f m). + Lemma MapCollect_as_Fold : + forall (f:ad -> A -> Map B) (m:Map A), + MapCollect f m = MapFold (Map B) (M0 B) (MapMerge B) f m. Proof. - Induction m;Trivial. + simple induction m; trivial. Qed. - Definition alist := (list (ad*A)). - Definition anil := (nil (ad*A)). - Definition acons := (!cons (ad*A)). - Definition aapp := (!app (ad*A)). + Definition alist := list (ad * A). + Definition anil := nil (A:=(ad * A)). + Definition acons := cons (A:=(ad * A)). + Definition aapp := app (A:=(ad * A)). - Definition alist_of_Map := (MapFold alist anil aapp [a:ad;y:A] (acons (pair ? ? a y) anil)). + Definition alist_of_Map := + MapFold alist anil aapp (fun (a:ad) (y:A) => acons (a, y) anil). - Fixpoint alist_semantics [l:alist] : ad -> (option A) := - Cases l of - nil => [_:ad] (NONE A) - | (cons (a, y) l') => [a0:ad] if (ad_eq a a0) then (SOME A y) else (alist_semantics l' a0) + Fixpoint alist_semantics (l:alist) : ad -> option A := + match l with + | nil => fun _:ad => NONE A + | (a, y) :: l' => + fun a0:ad => if ad_eq a a0 then SOME A y else alist_semantics l' a0 end. - Lemma alist_semantics_app : (l,l':alist) (a:ad) - (alist_semantics (aapp l l') a)= - (Cases (alist_semantics l a) of - NONE => (alist_semantics l' a) - | (SOME y) => (SOME A y) - end). + Lemma alist_semantics_app : + forall (l l':alist) (a:ad), + alist_semantics (aapp l l') a = + match alist_semantics l a with + | NONE => alist_semantics l' a + | SOME y => SOME A y + end. Proof. - Unfold aapp. Induction l. Trivial. - Intros. Elim a. Intros a1 y1. Simpl. Case (ad_eq a1 a0). Reflexivity. - Apply H. + unfold aapp in |- *. simple induction l. trivial. + intros. elim a. intros a1 y1. simpl in |- *. case (ad_eq a1 a0). reflexivity. + apply H. Qed. - Lemma alist_of_Map_semantics_1_1 : (m:(Map A)) (pf:ad->ad) (a:ad) (y:A) - (alist_semantics (MapFold1 alist anil aapp [a0:ad][y:A](acons (a0,y) anil) pf m) a) - =(SOME A y) -> {a':ad | a=(pf a')}. + Lemma alist_of_Map_semantics_1_1 : + forall (m:Map A) (pf:ad -> ad) (a:ad) (y:A), + alist_semantics + (MapFold1 alist anil aapp (fun (a0:ad) (y:A) => acons (a0, y) anil) pf + m) a = SOME A y -> {a' : ad | a = pf a'}. Proof. - Induction m. Simpl. Intros. Discriminate H. - Simpl. Intros a y pf a0 y0. Elim (sumbool_of_bool (ad_eq (pf a) a0)). Intro H. Rewrite H. - Intro H0. Split with a. Rewrite (ad_eq_complete ? ? H). Reflexivity. - Intro H. Rewrite H. Intro H0. Discriminate H0. - Intros. Change (alist_semantics - (aapp - (MapFold1 alist anil aapp [a0:ad][y:A](acons (a0,y) anil) - [a0:ad](pf (ad_double a0)) m0) - (MapFold1 alist anil aapp [a0:ad][y:A](acons (a0,y) anil) - [a0:ad](pf (ad_double_plus_un a0)) m1)) a)=(SOME A y) in H1. - Rewrite (alist_semantics_app - (MapFold1 alist anil aapp [a0:ad][y0:A](acons (a0,y0) anil) - [a0:ad](pf (ad_double a0)) m0) - (MapFold1 alist anil aapp [a0:ad][y0:A](acons (a0,y0) anil) - [a0:ad](pf (ad_double_plus_un a0)) m1) a) in H1. - Elim (option_sum A - (alist_semantics - (MapFold1 alist anil aapp [a0:ad][y0:A](acons (a0,y0) anil) - [a0:ad](pf (ad_double a0)) m0) a)). - Intro H2. Elim H2. Intros y0 H3. Elim (H [a0:ad](pf (ad_double a0)) a y0 H3). Intros a0 H4. - Split with (ad_double a0). Assumption. - Intro H2. Rewrite H2 in H1. Elim (H0 [a0:ad](pf (ad_double_plus_un a0)) a y H1). - Intros a0 H3. Split with (ad_double_plus_un a0). Assumption. + simple induction m. simpl in |- *. intros. discriminate H. + simpl in |- *. intros a y pf a0 y0. elim (sumbool_of_bool (ad_eq (pf a) a0)). intro H. rewrite H. + intro H0. split with a. rewrite (ad_eq_complete _ _ H). reflexivity. + intro H. rewrite H. intro H0. discriminate H0. + intros. change + (alist_semantics + (aapp + (MapFold1 alist anil aapp (fun (a0:ad) (y:A) => acons (a0, y) anil) + (fun a0:ad => pf (ad_double a0)) m0) + (MapFold1 alist anil aapp (fun (a0:ad) (y:A) => acons (a0, y) anil) + (fun a0:ad => pf (ad_double_plus_un a0)) m1)) a = + SOME A y) in H1. + rewrite + (alist_semantics_app + (MapFold1 alist anil aapp (fun (a0:ad) (y0:A) => acons (a0, y0) anil) + (fun a0:ad => pf (ad_double a0)) m0) + (MapFold1 alist anil aapp (fun (a0:ad) (y0:A) => acons (a0, y0) anil) + (fun a0:ad => pf (ad_double_plus_un a0)) m1) a) + in H1. + elim + (option_sum A + (alist_semantics + (MapFold1 alist anil aapp + (fun (a0:ad) (y0:A) => acons (a0, y0) anil) + (fun a0:ad => pf (ad_double a0)) m0) a)). + intro H2. elim H2. intros y0 H3. elim (H (fun a0:ad => pf (ad_double a0)) a y0 H3). intros a0 H4. + split with (ad_double a0). assumption. + intro H2. rewrite H2 in H1. elim (H0 (fun a0:ad => pf (ad_double_plus_un a0)) a y H1). + intros a0 H3. split with (ad_double_plus_un a0). assumption. Qed. - Definition ad_inj := [pf:ad->ad] (a0,a1:ad) (pf a0)=(pf a1) -> a0=a1. + Definition ad_inj (pf:ad -> ad) := + forall a0 a1:ad, pf a0 = pf a1 -> a0 = a1. - Lemma ad_comp_double_inj : - (pf:ad->ad) (ad_inj pf) -> (ad_inj [a0:ad] (pf (ad_double a0))). + Lemma ad_comp_double_inj : + forall pf:ad -> ad, ad_inj pf -> ad_inj (fun a0:ad => pf (ad_double a0)). Proof. - Unfold ad_inj. Intros. Apply ad_double_inj. Exact (H ? ? H0). + unfold ad_inj in |- *. intros. apply ad_double_inj. exact (H _ _ H0). Qed. - Lemma ad_comp_double_plus_un_inj : (pf:ad->ad) (ad_inj pf) -> - (ad_inj [a0:ad] (pf (ad_double_plus_un a0))). + Lemma ad_comp_double_plus_un_inj : + forall pf:ad -> ad, + ad_inj pf -> ad_inj (fun a0:ad => pf (ad_double_plus_un a0)). Proof. - Unfold ad_inj. Intros. Apply ad_double_plus_un_inj. Exact (H ? ? H0). + unfold ad_inj in |- *. intros. apply ad_double_plus_un_inj. exact (H _ _ H0). Qed. - Lemma alist_of_Map_semantics_1 : (m:(Map A)) (pf:ad->ad) (ad_inj pf) -> - (a:ad) (MapGet A m a)=(alist_semantics (MapFold1 alist anil aapp - [a0:ad;y:A] (acons (pair ? ? a0 y) anil) pf m) - (pf a)). + Lemma alist_of_Map_semantics_1 : + forall (m:Map A) (pf:ad -> ad), + ad_inj pf -> + forall a:ad, + MapGet A m a = + alist_semantics + (MapFold1 alist anil aapp (fun (a0:ad) (y:A) => acons (a0, y) anil) + pf m) (pf a). Proof. - Induction m. Trivial. - Simpl. Intros. Elim (sumbool_of_bool (ad_eq a a1)). Intro H0. Rewrite H0. - Rewrite (ad_eq_complete ? ? H0). Rewrite (ad_eq_correct (pf a1)). Reflexivity. - Intro H0. Rewrite H0. Elim (sumbool_of_bool (ad_eq (pf a) (pf a1))). Intro H1. - Rewrite (H a a1 (ad_eq_complete ? ? H1)) in H0. Rewrite (ad_eq_correct a1) in H0. - Discriminate H0. - Intro H1. Rewrite H1. Reflexivity. - Intros. Change (MapGet A (M2 A m0 m1) a) - =(alist_semantics - (aapp - (MapFold1 alist anil aapp [a0:ad][y:A](acons (a0,y) anil) - [a0:ad](pf (ad_double a0)) m0) - (MapFold1 alist anil aapp [a0:ad][y:A](acons (a0,y) anil) - [a0:ad](pf (ad_double_plus_un a0)) m1)) (pf a)). - Rewrite alist_semantics_app. Rewrite (MapGet_M2_bit_0_if A m0 m1 a). - Elim (ad_double_or_double_plus_un a). Intro H2. Elim H2. Intros a0 H3. Rewrite H3. - Rewrite (ad_double_bit_0 a0). - Rewrite <- (H [a1:ad](pf (ad_double a1)) (ad_comp_double_inj pf H1) a0). - Rewrite ad_double_div_2. Case (MapGet A m0 a0). - Elim (option_sum A - (alist_semantics - (MapFold1 alist anil aapp [a1:ad][y:A](acons (a1,y) anil) - [a1:ad](pf (ad_double_plus_un a1)) m1) (pf (ad_double a0)))). - Intro H4. Elim H4. Intros y H5. - Elim (alist_of_Map_semantics_1_1 m1 [a1:ad](pf (ad_double_plus_un a1)) - (pf (ad_double a0)) y H5). - Intros a1 H6. Cut (ad_bit_0 (ad_double a0))=(ad_bit_0 (ad_double_plus_un a1)). - Intro. Rewrite (ad_double_bit_0 a0) in H7. Rewrite (ad_double_plus_un_bit_0 a1) in H7. - Discriminate H7. - Rewrite (H1 (ad_double a0) (ad_double_plus_un a1) H6). Reflexivity. - Intro H4. Rewrite H4. Reflexivity. - Trivial. - Intro H2. Elim H2. Intros a0 H3. Rewrite H3. Rewrite (ad_double_plus_un_bit_0 a0). - Rewrite <- (H0 [a1:ad](pf (ad_double_plus_un a1)) (ad_comp_double_plus_un_inj pf H1) a0). - Rewrite ad_double_plus_un_div_2. - Elim (option_sum A - (alist_semantics - (MapFold1 alist anil aapp [a1:ad][y:A](acons (a1,y) anil) - [a1:ad](pf (ad_double a1)) m0) (pf (ad_double_plus_un a0)))). - Intro H4. Elim H4. Intros y H5. - Elim (alist_of_Map_semantics_1_1 m0 [a1:ad](pf (ad_double a1)) - (pf (ad_double_plus_un a0)) y H5). - Intros a1 H6. Cut (ad_bit_0 (ad_double_plus_un a0))=(ad_bit_0 (ad_double a1)). - Intro H7. Rewrite (ad_double_plus_un_bit_0 a0) in H7. Rewrite (ad_double_bit_0 a1) in H7. - Discriminate H7. - Rewrite (H1 (ad_double_plus_un a0) (ad_double a1) H6). Reflexivity. - Intro H4. Rewrite H4. Reflexivity. + simple induction m. trivial. + simpl in |- *. intros. elim (sumbool_of_bool (ad_eq a a1)). intro H0. rewrite H0. + rewrite (ad_eq_complete _ _ H0). rewrite (ad_eq_correct (pf a1)). reflexivity. + intro H0. rewrite H0. elim (sumbool_of_bool (ad_eq (pf a) (pf a1))). intro H1. + rewrite (H a a1 (ad_eq_complete _ _ H1)) in H0. rewrite (ad_eq_correct a1) in H0. + discriminate H0. + intro H1. rewrite H1. reflexivity. + intros. change + (MapGet A (M2 A m0 m1) a = + alist_semantics + (aapp + (MapFold1 alist anil aapp (fun (a0:ad) (y:A) => acons (a0, y) anil) + (fun a0:ad => pf (ad_double a0)) m0) + (MapFold1 alist anil aapp (fun (a0:ad) (y:A) => acons (a0, y) anil) + (fun a0:ad => pf (ad_double_plus_un a0)) m1)) ( + pf a)) in |- *. + rewrite alist_semantics_app. rewrite (MapGet_M2_bit_0_if A m0 m1 a). + elim (ad_double_or_double_plus_un a). intro H2. elim H2. intros a0 H3. rewrite H3. + rewrite (ad_double_bit_0 a0). + rewrite <- + (H (fun a1:ad => pf (ad_double a1)) (ad_comp_double_inj pf H1) a0) + . + rewrite ad_double_div_2. case (MapGet A m0 a0). + elim + (option_sum A + (alist_semantics + (MapFold1 alist anil aapp + (fun (a1:ad) (y:A) => acons (a1, y) anil) + (fun a1:ad => pf (ad_double_plus_un a1)) m1) + (pf (ad_double a0)))). + intro H4. elim H4. intros y H5. + elim + (alist_of_Map_semantics_1_1 m1 (fun a1:ad => pf (ad_double_plus_un a1)) + (pf (ad_double a0)) y H5). + intros a1 H6. cut (ad_bit_0 (ad_double a0) = ad_bit_0 (ad_double_plus_un a1)). + intro. rewrite (ad_double_bit_0 a0) in H7. rewrite (ad_double_plus_un_bit_0 a1) in H7. + discriminate H7. + rewrite (H1 (ad_double a0) (ad_double_plus_un a1) H6). reflexivity. + intro H4. rewrite H4. reflexivity. + trivial. + intro H2. elim H2. intros a0 H3. rewrite H3. rewrite (ad_double_plus_un_bit_0 a0). + rewrite <- + (H0 (fun a1:ad => pf (ad_double_plus_un a1)) + (ad_comp_double_plus_un_inj pf H1) a0). + rewrite ad_double_plus_un_div_2. + elim + (option_sum A + (alist_semantics + (MapFold1 alist anil aapp + (fun (a1:ad) (y:A) => acons (a1, y) anil) + (fun a1:ad => pf (ad_double a1)) m0) + (pf (ad_double_plus_un a0)))). + intro H4. elim H4. intros y H5. + elim + (alist_of_Map_semantics_1_1 m0 (fun a1:ad => pf (ad_double a1)) + (pf (ad_double_plus_un a0)) y H5). + intros a1 H6. cut (ad_bit_0 (ad_double_plus_un a0) = ad_bit_0 (ad_double a1)). + intro H7. rewrite (ad_double_plus_un_bit_0 a0) in H7. rewrite (ad_double_bit_0 a1) in H7. + discriminate H7. + rewrite (H1 (ad_double_plus_un a0) (ad_double a1) H6). reflexivity. + intro H4. rewrite H4. reflexivity. Qed. - Lemma alist_of_Map_semantics : (m:(Map A)) - (eqm A (MapGet A m) (alist_semantics (alist_of_Map m))). + Lemma alist_of_Map_semantics : + forall m:Map A, eqm A (MapGet A m) (alist_semantics (alist_of_Map m)). Proof. - Unfold eqm. Intros. Exact (alist_of_Map_semantics_1 m [a0:ad]a0 [a0,a1:ad][p:a0=a1]p a). + unfold eqm in |- *. intros. exact + (alist_of_Map_semantics_1 m (fun a0:ad => a0) + (fun (a0 a1:ad) (p:a0 = a1) => p) a). Qed. - Fixpoint Map_of_alist [l:alist] : (Map A) := - Cases l of - nil => (M0 A) - | (cons (a, y) l') => (MapPut A (Map_of_alist l') a y) + Fixpoint Map_of_alist (l:alist) : Map A := + match l with + | nil => M0 A + | (a, y) :: l' => MapPut A (Map_of_alist l') a y end. - Lemma Map_of_alist_semantics : (l:alist) - (eqm A (alist_semantics l) (MapGet A (Map_of_alist l))). + Lemma Map_of_alist_semantics : + forall l:alist, eqm A (alist_semantics l) (MapGet A (Map_of_alist l)). Proof. - Unfold eqm. Induction l. Trivial. - Intros r l0 H a. Elim r. Intros a0 y0. Simpl. Elim (sumbool_of_bool (ad_eq a0 a)). - Intro H0. Rewrite H0. Rewrite (ad_eq_complete ? ? H0). - Rewrite (MapPut_semantics A (Map_of_alist l0) a y0 a). Rewrite (ad_eq_correct a). - Reflexivity. - Intro H0. Rewrite H0. Rewrite (MapPut_semantics A (Map_of_alist l0) a0 y0 a). - Rewrite H0. Apply H. + unfold eqm in |- *. simple induction l. trivial. + intros r l0 H a. elim r. intros a0 y0. simpl in |- *. elim (sumbool_of_bool (ad_eq a0 a)). + intro H0. rewrite H0. rewrite (ad_eq_complete _ _ H0). + rewrite (MapPut_semantics A (Map_of_alist l0) a y0 a). rewrite (ad_eq_correct a). + reflexivity. + intro H0. rewrite H0. rewrite (MapPut_semantics A (Map_of_alist l0) a0 y0 a). + rewrite H0. apply H. Qed. - Lemma Map_of_alist_of_Map : (m:(Map A)) (eqmap A (Map_of_alist (alist_of_Map m)) m). + Lemma Map_of_alist_of_Map : + forall m:Map A, eqmap A (Map_of_alist (alist_of_Map m)) m. Proof. - Unfold eqmap. Intro. Apply eqm_trans with f':=(alist_semantics (alist_of_Map m)). - Apply eqm_sym. Apply Map_of_alist_semantics. - Apply eqm_sym. Apply alist_of_Map_semantics. + unfold eqmap in |- *. intro. apply eqm_trans with (f' := alist_semantics (alist_of_Map m)). + apply eqm_sym. apply Map_of_alist_semantics. + apply eqm_sym. apply alist_of_Map_semantics. Qed. - Lemma alist_of_Map_of_alist : (l:alist) - (eqm A (alist_semantics (alist_of_Map (Map_of_alist l))) (alist_semantics l)). + Lemma alist_of_Map_of_alist : + forall l:alist, + eqm A (alist_semantics (alist_of_Map (Map_of_alist l))) + (alist_semantics l). Proof. - Intro. Apply eqm_trans with f':=(MapGet A (Map_of_alist l)). - Apply eqm_sym. Apply alist_of_Map_semantics. - Apply eqm_sym. Apply Map_of_alist_semantics. + intro. apply eqm_trans with (f' := MapGet A (Map_of_alist l)). + apply eqm_sym. apply alist_of_Map_semantics. + apply eqm_sym. apply Map_of_alist_semantics. Qed. - Lemma fold_right_aapp : (M:Set) (neutral:M) (op:M->M->M) - ((a,b,c:M) (op (op a b) c)=(op a (op b c))) -> - ((a:M) (op neutral a)=a) -> - (f:ad->A->M) (l,l':alist) - (fold_right [r:ad*A][m:M] let (a,y)=r in (op (f a y) m) neutral - (aapp l l'))= - (op (fold_right [r:ad*A][m:M] let (a,y)=r in (op (f a y) m) neutral l) - (fold_right [r:ad*A][m:M] let (a,y)=r in (op (f a y) m) neutral l')) -. + Lemma fold_right_aapp : + forall (M:Set) (neutral:M) (op:M -> M -> M), + (forall a b c:M, op (op a b) c = op a (op b c)) -> + (forall a:M, op neutral a = a) -> + forall (f:ad -> A -> M) (l l':alist), + fold_right (fun (r:ad * A) (m:M) => let (a, y) := r in op (f a y) m) + neutral (aapp l l') = + op + (fold_right + (fun (r:ad * A) (m:M) => let (a, y) := r in op (f a y) m) neutral + l) + (fold_right + (fun (r:ad * A) (m:M) => let (a, y) := r in op (f a y) m) neutral + l'). Proof. - Induction l. Simpl. Intro. Rewrite H0. Reflexivity. - Intros r l0 H1 l'. Elim r. Intros a y. Simpl. Rewrite H. Rewrite (H1 l'). Reflexivity. + simple induction l. simpl in |- *. intro. rewrite H0. reflexivity. + intros r l0 H1 l'. elim r. intros a y. simpl in |- *. rewrite H. rewrite (H1 l'). reflexivity. Qed. - Lemma MapFold_as_fold_1 : (M:Set) (neutral:M) (op:M->M->M) - ((a,b,c:M) (op (op a b) c)=(op a (op b c))) -> - ((a:M) (op neutral a)=a) -> - ((a:M) (op a neutral)=a) -> - (f:ad->A->M) (m:(Map A)) (pf:ad->ad) - (MapFold1 M neutral op f pf m)= - (fold_right [r:(ad*A)][m:M] let (a,y)=r in (op (f a y) m) neutral - (MapFold1 alist anil aapp [a:ad;y:A] (acons (pair ? ? -a y) anil) pf m)). + Lemma MapFold_as_fold_1 : + forall (M:Set) (neutral:M) (op:M -> M -> M), + (forall a b c:M, op (op a b) c = op a (op b c)) -> + (forall a:M, op neutral a = a) -> + (forall a:M, op a neutral = a) -> + forall (f:ad -> A -> M) (m:Map A) (pf:ad -> ad), + MapFold1 M neutral op f pf m = + fold_right (fun (r:ad * A) (m:M) => let (a, y) := r in op (f a y) m) + neutral + (MapFold1 alist anil aapp (fun (a:ad) (y:A) => acons (a, y) anil) pf + m). Proof. - Induction m. Trivial. - Intros. Simpl. Rewrite H1. Reflexivity. - Intros. Simpl. Rewrite (fold_right_aapp M neutral op H H0 f). - Rewrite (H2 [a0:ad](pf (ad_double a0))). Rewrite (H3 [a0:ad](pf (ad_double_plus_un a0))). - Reflexivity. + simple induction m. trivial. + intros. simpl in |- *. rewrite H1. reflexivity. + intros. simpl in |- *. rewrite (fold_right_aapp M neutral op H H0 f). + rewrite (H2 (fun a0:ad => pf (ad_double a0))). rewrite (H3 (fun a0:ad => pf (ad_double_plus_un a0))). + reflexivity. Qed. - Lemma MapFold_as_fold : (M:Set) (neutral:M) (op:M->M->M) - ((a,b,c:M) (op (op a b) c)=(op a (op b c))) -> - ((a:M) (op neutral a)=a) -> - ((a:M) (op a neutral)=a) -> - (f:ad->A->M) (m:(Map A)) - (MapFold M neutral op f m)= - (fold_right [r:(ad*A)][m:M] let (a,y)=r in (op (f a y) m) neutral - (alist_of_Map m)). + Lemma MapFold_as_fold : + forall (M:Set) (neutral:M) (op:M -> M -> M), + (forall a b c:M, op (op a b) c = op a (op b c)) -> + (forall a:M, op neutral a = a) -> + (forall a:M, op a neutral = a) -> + forall (f:ad -> A -> M) (m:Map A), + MapFold M neutral op f m = + fold_right (fun (r:ad * A) (m:M) => let (a, y) := r in op (f a y) m) + neutral (alist_of_Map m). Proof. - Intros. Exact (MapFold_as_fold_1 M neutral op H H0 H1 f m [a0:ad]a0). + intros. exact (MapFold_as_fold_1 M neutral op H H0 H1 f m (fun a0:ad => a0)). Qed. - Lemma alist_MapMerge_semantics : (m,m':(Map A)) - (eqm A (alist_semantics (aapp (alist_of_Map m') (alist_of_Map m))) - (alist_semantics (alist_of_Map (MapMerge A m m')))). + Lemma alist_MapMerge_semantics : + forall m m':Map A, + eqm A (alist_semantics (aapp (alist_of_Map m') (alist_of_Map m))) + (alist_semantics (alist_of_Map (MapMerge A m m'))). Proof. - Unfold eqm. Intros. Rewrite alist_semantics_app. Rewrite <- (alist_of_Map_semantics m a). - Rewrite <- (alist_of_Map_semantics m' a). - Rewrite <- (alist_of_Map_semantics (MapMerge A m m') a). - Rewrite (MapMerge_semantics A m m' a). Reflexivity. + unfold eqm in |- *. intros. rewrite alist_semantics_app. rewrite <- (alist_of_Map_semantics m a). + rewrite <- (alist_of_Map_semantics m' a). + rewrite <- (alist_of_Map_semantics (MapMerge A m m') a). + rewrite (MapMerge_semantics A m m' a). reflexivity. Qed. - Lemma alist_MapMerge_semantics_disjoint : (m,m':(Map A)) - (eqmap A (MapDomRestrTo A A m m') (M0 A)) -> - (eqm A (alist_semantics (aapp (alist_of_Map m) (alist_of_Map m'))) - (alist_semantics (alist_of_Map (MapMerge A m m')))). + Lemma alist_MapMerge_semantics_disjoint : + forall m m':Map A, + eqmap A (MapDomRestrTo A A m m') (M0 A) -> + eqm A (alist_semantics (aapp (alist_of_Map m) (alist_of_Map m'))) + (alist_semantics (alist_of_Map (MapMerge A m m'))). Proof. - Unfold eqm. Intros. Rewrite alist_semantics_app. Rewrite <- (alist_of_Map_semantics m a). - Rewrite <- (alist_of_Map_semantics m' a). - Rewrite <- (alist_of_Map_semantics (MapMerge A m m') a). Rewrite (MapMerge_semantics A m m' a). - Elim (option_sum ? (MapGet A m a)). Intro H0. Elim H0. Intros y H1. Rewrite H1. - Elim (option_sum ? (MapGet A m' a)). Intro H2. Elim H2. Intros y' H3. - Cut (MapGet A (MapDomRestrTo A A m m') a)=(NONE A). - Rewrite (MapDomRestrTo_semantics A A m m' a). Rewrite H3. Rewrite H1. Intro. Discriminate H4. - Exact (H a). - Intro H2. Rewrite H2. Reflexivity. - Intro H0. Rewrite H0. Case (MapGet A m' a); Trivial. + unfold eqm in |- *. intros. rewrite alist_semantics_app. rewrite <- (alist_of_Map_semantics m a). + rewrite <- (alist_of_Map_semantics m' a). + rewrite <- (alist_of_Map_semantics (MapMerge A m m') a). rewrite (MapMerge_semantics A m m' a). + elim (option_sum _ (MapGet A m a)). intro H0. elim H0. intros y H1. rewrite H1. + elim (option_sum _ (MapGet A m' a)). intro H2. elim H2. intros y' H3. + cut (MapGet A (MapDomRestrTo A A m m') a = NONE A). + rewrite (MapDomRestrTo_semantics A A m m' a). rewrite H3. rewrite H1. intro. discriminate H4. + exact (H a). + intro H2. rewrite H2. reflexivity. + intro H0. rewrite H0. case (MapGet A m' a); trivial. Qed. - Lemma alist_semantics_disjoint_comm : (l,l':alist) - (eqmap A (MapDomRestrTo A A (Map_of_alist l) (Map_of_alist l')) (M0 A)) -> - (eqm A (alist_semantics (aapp l l')) (alist_semantics (aapp l' l))). + Lemma alist_semantics_disjoint_comm : + forall l l':alist, + eqmap A (MapDomRestrTo A A (Map_of_alist l) (Map_of_alist l')) (M0 A) -> + eqm A (alist_semantics (aapp l l')) (alist_semantics (aapp l' l)). Proof. - Unfold eqm. Intros. Rewrite (alist_semantics_app l l' a). Rewrite (alist_semantics_app l' l a). - Rewrite <- (alist_of_Map_of_alist l a). Rewrite <- (alist_of_Map_of_alist l' a). - Rewrite <- (alist_semantics_app (alist_of_Map (Map_of_alist l)) - (alist_of_Map (Map_of_alist l')) a). - Rewrite <- (alist_semantics_app (alist_of_Map (Map_of_alist l')) - (alist_of_Map (Map_of_alist l)) a). - Rewrite (alist_MapMerge_semantics (Map_of_alist l) (Map_of_alist l') a). - Rewrite (alist_MapMerge_semantics_disjoint (Map_of_alist l) (Map_of_alist l') H a). - Reflexivity. + unfold eqm in |- *. intros. rewrite (alist_semantics_app l l' a). rewrite (alist_semantics_app l' l a). + rewrite <- (alist_of_Map_of_alist l a). rewrite <- (alist_of_Map_of_alist l' a). + rewrite <- + (alist_semantics_app (alist_of_Map (Map_of_alist l)) + (alist_of_Map (Map_of_alist l')) a). + rewrite <- + (alist_semantics_app (alist_of_Map (Map_of_alist l')) + (alist_of_Map (Map_of_alist l)) a). + rewrite (alist_MapMerge_semantics (Map_of_alist l) (Map_of_alist l') a). + rewrite + (alist_MapMerge_semantics_disjoint (Map_of_alist l) ( + Map_of_alist l') H a). + reflexivity. Qed. End MapIter. - |