diff options
Diffstat (limited to 'theories/IntMap/Mapcanon.v')
| -rw-r--r-- | theories/IntMap/Mapcanon.v | 569 |
1 files changed, 296 insertions, 273 deletions
diff --git a/theories/IntMap/Mapcanon.v b/theories/IntMap/Mapcanon.v index b98e9b233a..70966c60db 100644 --- a/theories/IntMap/Mapcanon.v +++ b/theories/IntMap/Mapcanon.v @@ -7,316 +7,328 @@ (***********************************************************************) (*i $Id$ i*) -Require Bool. -Require Sumbool. -Require Arith. -Require ZArith. -Require Addr. -Require Adist. -Require Addec. -Require Map. -Require Mapaxioms. -Require Mapiter. -Require Fset. -Require PolyList. -Require Lsort. -Require Mapsubset. -Require Mapcard. +Require Import Bool. +Require Import Sumbool. +Require Import Arith. +Require Import ZArith. +Require Import Addr. +Require Import Adist. +Require Import Addec. +Require Import Map. +Require Import Mapaxioms. +Require Import Mapiter. +Require Import Fset. +Require Import List. +Require Import Lsort. +Require Import Mapsubset. +Require Import Mapcard. Section MapCanon. Variable A : Set. - Inductive mapcanon : (Map A) -> Prop := - M0_canon : (mapcanon (M0 A)) - | M1_canon : (a:ad) (y:A) (mapcanon (M1 A a y)) - | M2_canon : (m1,m2:(Map A)) (mapcanon m1) -> (mapcanon m2) -> - (le (2) (MapCard A (M2 A m1 m2))) -> (mapcanon (M2 A m1 m2)). + Inductive mapcanon : Map A -> Prop := + | M0_canon : mapcanon (M0 A) + | M1_canon : forall (a:ad) (y:A), mapcanon (M1 A a y) + | M2_canon : + forall m1 m2:Map A, + mapcanon m1 -> + mapcanon m2 -> 2 <= MapCard A (M2 A m1 m2) -> mapcanon (M2 A m1 m2). - Lemma mapcanon_M2 : - (m1,m2:(Map A)) (mapcanon (M2 A m1 m2)) -> (le (2) (MapCard A (M2 A m1 m2))). + Lemma mapcanon_M2 : + forall m1 m2:Map A, mapcanon (M2 A m1 m2) -> 2 <= MapCard A (M2 A m1 m2). Proof. - Intros. Inversion H. Assumption. + intros. inversion H. assumption. Qed. - Lemma mapcanon_M2_1 : (m1,m2:(Map A)) (mapcanon (M2 A m1 m2)) -> (mapcanon m1). + Lemma mapcanon_M2_1 : + forall m1 m2:Map A, mapcanon (M2 A m1 m2) -> mapcanon m1. Proof. - Intros. Inversion H. Assumption. + intros. inversion H. assumption. Qed. - Lemma mapcanon_M2_2 : (m1,m2:(Map A)) (mapcanon (M2 A m1 m2)) -> (mapcanon m2). + Lemma mapcanon_M2_2 : + forall m1 m2:Map A, mapcanon (M2 A m1 m2) -> mapcanon m2. Proof. - Intros. Inversion H. Assumption. + intros. inversion H. assumption. Qed. - Lemma M2_eqmap_1 : (m0,m1,m2,m3:(Map A)) - (eqmap A (M2 A m0 m1) (M2 A m2 m3)) -> (eqmap A m0 m2). + Lemma M2_eqmap_1 : + forall m0 m1 m2 m3:Map A, + eqmap A (M2 A m0 m1) (M2 A m2 m3) -> eqmap A m0 m2. Proof. - Unfold eqmap eqm. Intros. Rewrite <- (ad_double_div_2 a). - Rewrite <- (MapGet_M2_bit_0_0 A ? (ad_double_bit_0 a) m0 m1). - Rewrite <- (MapGet_M2_bit_0_0 A ? (ad_double_bit_0 a) m2 m3). - Exact (H (ad_double a)). + unfold eqmap, eqm in |- *. intros. rewrite <- (ad_double_div_2 a). + rewrite <- (MapGet_M2_bit_0_0 A _ (ad_double_bit_0 a) m0 m1). + rewrite <- (MapGet_M2_bit_0_0 A _ (ad_double_bit_0 a) m2 m3). + exact (H (ad_double a)). Qed. - Lemma M2_eqmap_2 : (m0,m1,m2,m3:(Map A)) - (eqmap A (M2 A m0 m1) (M2 A m2 m3)) -> (eqmap A m1 m3). + Lemma M2_eqmap_2 : + forall m0 m1 m2 m3:Map A, + eqmap A (M2 A m0 m1) (M2 A m2 m3) -> eqmap A m1 m3. Proof. - Unfold eqmap eqm. Intros. Rewrite <- (ad_double_plus_un_div_2 a). - Rewrite <- (MapGet_M2_bit_0_1 A ? (ad_double_plus_un_bit_0 a) m0 m1). - Rewrite <- (MapGet_M2_bit_0_1 A ? (ad_double_plus_un_bit_0 a) m2 m3). - Exact (H (ad_double_plus_un a)). + unfold eqmap, eqm in |- *. intros. rewrite <- (ad_double_plus_un_div_2 a). + rewrite <- (MapGet_M2_bit_0_1 A _ (ad_double_plus_un_bit_0 a) m0 m1). + rewrite <- (MapGet_M2_bit_0_1 A _ (ad_double_plus_un_bit_0 a) m2 m3). + exact (H (ad_double_plus_un a)). Qed. - Lemma mapcanon_unique : (m,m':(Map A)) (mapcanon m) -> (mapcanon m') -> - (eqmap A m m') -> m=m'. + Lemma mapcanon_unique : + forall m m':Map A, mapcanon m -> mapcanon m' -> eqmap A m m' -> m = m'. Proof. - Induction m. Induction m'. Trivial. - Intros a y H H0 H1. Cut (NONE A)=(MapGet A (M1 A a y) a). Simpl. Rewrite (ad_eq_correct a). - Intro. Discriminate H2. - Exact (H1 a). - Intros. Cut (le (2) (MapCard A (M0 A))). Intro. Elim (le_Sn_O ? H4). - Rewrite (MapCard_ext A ? ? H3). Exact (mapcanon_M2 ? ? H2). - Intros a y. Induction m'. Intros. Cut (MapGet A (M1 A a y) a)=(NONE A). Simpl. - Rewrite (ad_eq_correct a). Intro. Discriminate H2. - Exact (H1 a). - Intros a0 y0 H H0 H1. Cut (MapGet A (M1 A a y) a)=(MapGet A (M1 A a0 y0) a). Simpl. - Rewrite (ad_eq_correct a). Intro. Elim (sumbool_of_bool (ad_eq a0 a)). Intro H3. - Rewrite H3 in H2. Inversion H2. Rewrite (ad_eq_complete ? ? H3). Reflexivity. - Intro H3. Rewrite H3 in H2. Discriminate H2. - Exact (H1 a). - Intros. Cut (le (2) (MapCard A (M1 A a y))). Intro. Elim (le_Sn_O ? (le_S_n ? ? H4)). - Rewrite (MapCard_ext A ? ? H3). Exact (mapcanon_M2 ? ? H2). - Induction m'. Intros. Cut (le (2) (MapCard A (M0 A))). Intro. Elim (le_Sn_O ? H4). - Rewrite <- (MapCard_ext A ? ? H3). Exact (mapcanon_M2 ? ? H1). - Intros a y H1 H2 H3. Cut (le (2) (MapCard A (M1 A a y))). Intro. - Elim (le_Sn_O ? (le_S_n ? ? H4)). - Rewrite <- (MapCard_ext A ? ? H3). Exact (mapcanon_M2 ? ? H1). - Intros. Rewrite (H m2). Rewrite (H0 m3). Reflexivity. - Exact (mapcanon_M2_2 ? ? H3). - Exact (mapcanon_M2_2 ? ? H4). - Exact (M2_eqmap_2 ? ? ? ? H5). - Exact (mapcanon_M2_1 ? ? H3). - Exact (mapcanon_M2_1 ? ? H4). - Exact (M2_eqmap_1 ? ? ? ? H5). + simple induction m. simple induction m'. trivial. + intros a y H H0 H1. cut (NONE A = MapGet A (M1 A a y) a). simpl in |- *. rewrite (ad_eq_correct a). + intro. discriminate H2. + exact (H1 a). + intros. cut (2 <= MapCard A (M0 A)). intro. elim (le_Sn_O _ H4). + rewrite (MapCard_ext A _ _ H3). exact (mapcanon_M2 _ _ H2). + intros a y. simple induction m'. intros. cut (MapGet A (M1 A a y) a = NONE A). simpl in |- *. + rewrite (ad_eq_correct a). intro. discriminate H2. + exact (H1 a). + intros a0 y0 H H0 H1. cut (MapGet A (M1 A a y) a = MapGet A (M1 A a0 y0) a). simpl in |- *. + rewrite (ad_eq_correct a). intro. elim (sumbool_of_bool (ad_eq a0 a)). intro H3. + rewrite H3 in H2. inversion H2. rewrite (ad_eq_complete _ _ H3). reflexivity. + intro H3. rewrite H3 in H2. discriminate H2. + exact (H1 a). + intros. cut (2 <= MapCard A (M1 A a y)). intro. elim (le_Sn_O _ (le_S_n _ _ H4)). + rewrite (MapCard_ext A _ _ H3). exact (mapcanon_M2 _ _ H2). + simple induction m'. intros. cut (2 <= MapCard A (M0 A)). intro. elim (le_Sn_O _ H4). + rewrite <- (MapCard_ext A _ _ H3). exact (mapcanon_M2 _ _ H1). + intros a y H1 H2 H3. cut (2 <= MapCard A (M1 A a y)). intro. + elim (le_Sn_O _ (le_S_n _ _ H4)). + rewrite <- (MapCard_ext A _ _ H3). exact (mapcanon_M2 _ _ H1). + intros. rewrite (H m2). rewrite (H0 m3). reflexivity. + exact (mapcanon_M2_2 _ _ H3). + exact (mapcanon_M2_2 _ _ H4). + exact (M2_eqmap_2 _ _ _ _ H5). + exact (mapcanon_M2_1 _ _ H3). + exact (mapcanon_M2_1 _ _ H4). + exact (M2_eqmap_1 _ _ _ _ H5). Qed. - Lemma MapPut1_canon : - (p:positive) (a,a':ad) (y,y':A) (mapcanon (MapPut1 A a y a' y' p)). + Lemma MapPut1_canon : + forall (p:positive) (a a':ad) (y y':A), mapcanon (MapPut1 A a y a' y' p). Proof. - Induction p. Simpl. Intros. Case (ad_bit_0 a). Apply M2_canon. Apply M1_canon. - Apply M1_canon. - Apply le_n. - Apply M2_canon. Apply M1_canon. - Apply M1_canon. - Apply le_n. - Simpl. Intros. Case (ad_bit_0 a). Apply M2_canon. Apply M0_canon. - Apply H. - Simpl. Rewrite MapCard_Put1_equals_2. Apply le_n. - Apply M2_canon. Apply H. - Apply M0_canon. - Simpl. Rewrite MapCard_Put1_equals_2. Apply le_n. - Simpl. Simpl. Intros. Case (ad_bit_0 a). Apply M2_canon. Apply M1_canon. - Apply M1_canon. - Simpl. Apply le_n. - Apply M2_canon. Apply M1_canon. - Apply M1_canon. - Simpl. Apply le_n. + simple induction p. simpl in |- *. intros. case (ad_bit_0 a). apply M2_canon. apply M1_canon. + apply M1_canon. + apply le_n. + apply M2_canon. apply M1_canon. + apply M1_canon. + apply le_n. + simpl in |- *. intros. case (ad_bit_0 a). apply M2_canon. apply M0_canon. + apply H. + simpl in |- *. rewrite MapCard_Put1_equals_2. apply le_n. + apply M2_canon. apply H. + apply M0_canon. + simpl in |- *. rewrite MapCard_Put1_equals_2. apply le_n. + simpl in |- *. simpl in |- *. intros. case (ad_bit_0 a). apply M2_canon. apply M1_canon. + apply M1_canon. + simpl in |- *. apply le_n. + apply M2_canon. apply M1_canon. + apply M1_canon. + simpl in |- *. apply le_n. Qed. - Lemma MapPut_canon : - (m:(Map A)) (mapcanon m) -> (a:ad) (y:A) (mapcanon (MapPut A m a y)). + Lemma MapPut_canon : + forall m:Map A, + mapcanon m -> forall (a:ad) (y:A), mapcanon (MapPut A m a y). Proof. - Induction m. Intros. Simpl. Apply M1_canon. - Intros a0 y0 H a y. Simpl. Case (ad_xor a0 a). Apply M1_canon. - Intro. Apply MapPut1_canon. - Intros. Simpl. Elim a. Apply M2_canon. Apply H. Exact (mapcanon_M2_1 m0 m1 H1). - Exact (mapcanon_M2_2 m0 m1 H1). - Simpl. Apply le_trans with m:=(plus (MapCard A m0) (MapCard A m1)). Exact (mapcanon_M2 ? ? H1). - Apply le_plus_plus. Exact (MapCard_Put_lb A m0 ad_z y). - Apply le_n. - Intro. Case p. Intro. Apply M2_canon. Exact (mapcanon_M2_1 m0 m1 H1). - Apply H0. Exact (mapcanon_M2_2 m0 m1 H1). - Simpl. Apply le_trans with m:=(plus (MapCard A m0) (MapCard A m1)). - Exact (mapcanon_M2 m0 m1 H1). - Apply le_reg_l. Exact (MapCard_Put_lb A m1 (ad_x p0) y). - Intro. Apply M2_canon. Apply H. Exact (mapcanon_M2_1 m0 m1 H1). - Exact (mapcanon_M2_2 m0 m1 H1). - Simpl. Apply le_trans with m:=(plus (MapCard A m0) (MapCard A m1)). - Exact (mapcanon_M2 m0 m1 H1). - Apply le_reg_r. Exact (MapCard_Put_lb A m0 (ad_x p0) y). - Apply M2_canon. Apply (mapcanon_M2_1 m0 m1 H1). - Apply H0. Apply (mapcanon_M2_2 m0 m1 H1). - Simpl. Apply le_trans with m:=(plus (MapCard A m0) (MapCard A m1)). - Exact (mapcanon_M2 m0 m1 H1). - Apply le_reg_l. Exact (MapCard_Put_lb A m1 ad_z y). + simple induction m. intros. simpl in |- *. apply M1_canon. + intros a0 y0 H a y. simpl in |- *. case (ad_xor a0 a). apply M1_canon. + intro. apply MapPut1_canon. + intros. simpl in |- *. elim a. apply M2_canon. apply H. exact (mapcanon_M2_1 m0 m1 H1). + exact (mapcanon_M2_2 m0 m1 H1). + simpl in |- *. apply le_trans with (m := MapCard A m0 + MapCard A m1). exact (mapcanon_M2 _ _ H1). + apply plus_le_compat. exact (MapCard_Put_lb A m0 ad_z y). + apply le_n. + intro. case p. intro. apply M2_canon. exact (mapcanon_M2_1 m0 m1 H1). + apply H0. exact (mapcanon_M2_2 m0 m1 H1). + simpl in |- *. apply le_trans with (m := MapCard A m0 + MapCard A m1). + exact (mapcanon_M2 m0 m1 H1). + apply plus_le_compat_l. exact (MapCard_Put_lb A m1 (ad_x p0) y). + intro. apply M2_canon. apply H. exact (mapcanon_M2_1 m0 m1 H1). + exact (mapcanon_M2_2 m0 m1 H1). + simpl in |- *. apply le_trans with (m := MapCard A m0 + MapCard A m1). + exact (mapcanon_M2 m0 m1 H1). + apply plus_le_compat_r. exact (MapCard_Put_lb A m0 (ad_x p0) y). + apply M2_canon. apply (mapcanon_M2_1 m0 m1 H1). + apply H0. apply (mapcanon_M2_2 m0 m1 H1). + simpl in |- *. apply le_trans with (m := MapCard A m0 + MapCard A m1). + exact (mapcanon_M2 m0 m1 H1). + apply plus_le_compat_l. exact (MapCard_Put_lb A m1 ad_z y). Qed. - Lemma MapPut_behind_canon : (m:(Map A)) (mapcanon m) -> - (a:ad) (y:A) (mapcanon (MapPut_behind A m a y)). + Lemma MapPut_behind_canon : + forall m:Map A, + mapcanon m -> forall (a:ad) (y:A), mapcanon (MapPut_behind A m a y). Proof. - Induction m. Intros. Simpl. Apply M1_canon. - Intros a0 y0 H a y. Simpl. Case (ad_xor a0 a). Apply M1_canon. - Intro. Apply MapPut1_canon. - Intros. Simpl. Elim a. Apply M2_canon. Apply H. Exact (mapcanon_M2_1 m0 m1 H1). - Exact (mapcanon_M2_2 m0 m1 H1). - Simpl. Apply le_trans with m:=(plus (MapCard A m0) (MapCard A m1)). Exact (mapcanon_M2 ? ? H1). - Apply le_plus_plus. Rewrite MapCard_Put_behind_Put. Exact (MapCard_Put_lb A m0 ad_z y). - Apply le_n. - Intro. Case p. Intro. Apply M2_canon. Exact (mapcanon_M2_1 m0 m1 H1). - Apply H0. Exact (mapcanon_M2_2 m0 m1 H1). - Simpl. Apply le_trans with m:=(plus (MapCard A m0) (MapCard A m1)). - Exact (mapcanon_M2 m0 m1 H1). - Apply le_reg_l. Rewrite MapCard_Put_behind_Put. Exact (MapCard_Put_lb A m1 (ad_x p0) y). - Intro. Apply M2_canon. Apply H. Exact (mapcanon_M2_1 m0 m1 H1). - Exact (mapcanon_M2_2 m0 m1 H1). - Simpl. Apply le_trans with m:=(plus (MapCard A m0) (MapCard A m1)). - Exact (mapcanon_M2 m0 m1 H1). - Apply le_reg_r. Rewrite MapCard_Put_behind_Put. Exact (MapCard_Put_lb A m0 (ad_x p0) y). - Apply M2_canon. Apply (mapcanon_M2_1 m0 m1 H1). - Apply H0. Apply (mapcanon_M2_2 m0 m1 H1). - Simpl. Apply le_trans with m:=(plus (MapCard A m0) (MapCard A m1)). - Exact (mapcanon_M2 m0 m1 H1). - Apply le_reg_l. Rewrite MapCard_Put_behind_Put. Exact (MapCard_Put_lb A m1 ad_z y). + simple induction m. intros. simpl in |- *. apply M1_canon. + intros a0 y0 H a y. simpl in |- *. case (ad_xor a0 a). apply M1_canon. + intro. apply MapPut1_canon. + intros. simpl in |- *. elim a. apply M2_canon. apply H. exact (mapcanon_M2_1 m0 m1 H1). + exact (mapcanon_M2_2 m0 m1 H1). + simpl in |- *. apply le_trans with (m := MapCard A m0 + MapCard A m1). exact (mapcanon_M2 _ _ H1). + apply plus_le_compat. rewrite MapCard_Put_behind_Put. exact (MapCard_Put_lb A m0 ad_z y). + apply le_n. + intro. case p. intro. apply M2_canon. exact (mapcanon_M2_1 m0 m1 H1). + apply H0. exact (mapcanon_M2_2 m0 m1 H1). + simpl in |- *. apply le_trans with (m := MapCard A m0 + MapCard A m1). + exact (mapcanon_M2 m0 m1 H1). + apply plus_le_compat_l. rewrite MapCard_Put_behind_Put. exact (MapCard_Put_lb A m1 (ad_x p0) y). + intro. apply M2_canon. apply H. exact (mapcanon_M2_1 m0 m1 H1). + exact (mapcanon_M2_2 m0 m1 H1). + simpl in |- *. apply le_trans with (m := MapCard A m0 + MapCard A m1). + exact (mapcanon_M2 m0 m1 H1). + apply plus_le_compat_r. rewrite MapCard_Put_behind_Put. exact (MapCard_Put_lb A m0 (ad_x p0) y). + apply M2_canon. apply (mapcanon_M2_1 m0 m1 H1). + apply H0. apply (mapcanon_M2_2 m0 m1 H1). + simpl in |- *. apply le_trans with (m := MapCard A m0 + MapCard A m1). + exact (mapcanon_M2 m0 m1 H1). + apply plus_le_compat_l. rewrite MapCard_Put_behind_Put. exact (MapCard_Put_lb A m1 ad_z y). Qed. - Lemma makeM2_canon : - (m,m':(Map A)) (mapcanon m) -> (mapcanon m') -> (mapcanon (makeM2 A m m')). + Lemma makeM2_canon : + forall m m':Map A, mapcanon m -> mapcanon m' -> mapcanon (makeM2 A m m'). Proof. - Intro. Case m. Intro. Case m'. Intros. Exact M0_canon. - Intros a y H H0. Exact (M1_canon (ad_double_plus_un a) y). - Intros. Simpl. (Apply M2_canon; Try Assumption). Exact (mapcanon_M2 m0 m1 H0). - Intros a y m'. Case m'. Intros. Exact (M1_canon (ad_double a) y). - Intros a0 y0 H H0. Simpl. (Apply M2_canon; Try Assumption). Apply le_n. - Intros. Simpl. (Apply M2_canon; Try Assumption). - Apply le_trans with m:=(MapCard A (M2 A m0 m1)). Exact (mapcanon_M2 ? ? H0). - Exact (le_plus_r (MapCard A (M1 A a y)) (MapCard A (M2 A m0 m1))). - Simpl. Intros. (Apply M2_canon; Try Assumption). - Apply le_trans with m:=(MapCard A (M2 A m0 m1)). Exact (mapcanon_M2 ? ? H). - Exact (le_plus_l (MapCard A (M2 A m0 m1)) (MapCard A m')). + intro. case m. intro. case m'. intros. exact M0_canon. + intros a y H H0. exact (M1_canon (ad_double_plus_un a) y). + intros. simpl in |- *. apply M2_canon; try assumption. exact (mapcanon_M2 m0 m1 H0). + intros a y m'. case m'. intros. exact (M1_canon (ad_double a) y). + intros a0 y0 H H0. simpl in |- *. apply M2_canon; try assumption. apply le_n. + intros. simpl in |- *. apply M2_canon; try assumption. + apply le_trans with (m := MapCard A (M2 A m0 m1)). exact (mapcanon_M2 _ _ H0). + exact (le_plus_r (MapCard A (M1 A a y)) (MapCard A (M2 A m0 m1))). + simpl in |- *. intros. apply M2_canon; try assumption. + apply le_trans with (m := MapCard A (M2 A m0 m1)). exact (mapcanon_M2 _ _ H). + exact (le_plus_l (MapCard A (M2 A m0 m1)) (MapCard A m')). Qed. - Fixpoint MapCanonicalize [m:(Map A)] : (Map A) := - Cases m of - (M2 m0 m1) => (makeM2 A (MapCanonicalize m0) (MapCanonicalize m1)) - | _ => m - end. + Fixpoint MapCanonicalize (m:Map A) : Map A := + match m with + | M2 m0 m1 => makeM2 A (MapCanonicalize m0) (MapCanonicalize m1) + | _ => m + end. - Lemma mapcanon_exists_1 : (m:(Map A)) (eqmap A m (MapCanonicalize m)). + Lemma mapcanon_exists_1 : forall m:Map A, eqmap A m (MapCanonicalize m). Proof. - Induction m. Apply eqmap_refl. - Intros. Apply eqmap_refl. - Intros. Simpl. Unfold eqmap eqm. Intro. - Rewrite (makeM2_M2 A (MapCanonicalize m0) (MapCanonicalize m1) a). - Rewrite MapGet_M2_bit_0_if. Rewrite MapGet_M2_bit_0_if. - Rewrite <- (H (ad_div_2 a)). Rewrite <- (H0 (ad_div_2 a)). Reflexivity. + simple induction m. apply eqmap_refl. + intros. apply eqmap_refl. + intros. simpl in |- *. unfold eqmap, eqm in |- *. intro. + rewrite (makeM2_M2 A (MapCanonicalize m0) (MapCanonicalize m1) a). + rewrite MapGet_M2_bit_0_if. rewrite MapGet_M2_bit_0_if. + rewrite <- (H (ad_div_2 a)). rewrite <- (H0 (ad_div_2 a)). reflexivity. Qed. - Lemma mapcanon_exists_2 : (m:(Map A)) (mapcanon (MapCanonicalize m)). + Lemma mapcanon_exists_2 : forall m:Map A, mapcanon (MapCanonicalize m). Proof. - Induction m. Apply M0_canon. - Intros. Simpl. Apply M1_canon. - Intros. Simpl. (Apply makeM2_canon; Assumption). + simple induction m. apply M0_canon. + intros. simpl in |- *. apply M1_canon. + intros. simpl in |- *. apply makeM2_canon; assumption. Qed. - Lemma mapcanon_exists : - (m:(Map A)) {m':(Map A) | (eqmap A m m') /\ (mapcanon m')}. + Lemma mapcanon_exists : + forall m:Map A, {m' : Map A | eqmap A m m' /\ mapcanon m'}. Proof. - Intro. Split with (MapCanonicalize m). Split. Apply mapcanon_exists_1. - Apply mapcanon_exists_2. + intro. split with (MapCanonicalize m). split. apply mapcanon_exists_1. + apply mapcanon_exists_2. Qed. - Lemma MapRemove_canon : - (m:(Map A)) (mapcanon m) -> (a:ad) (mapcanon (MapRemove A m a)). + Lemma MapRemove_canon : + forall m:Map A, mapcanon m -> forall a:ad, mapcanon (MapRemove A m a). Proof. - Induction m. Intros. Exact M0_canon. - Intros a y H a0. Simpl. Case (ad_eq a a0). Exact M0_canon. - Assumption. - Intros. Simpl. Case (ad_bit_0 a). Apply makeM2_canon. Exact (mapcanon_M2_1 ? ? H1). - Apply H0. Exact (mapcanon_M2_2 ? ? H1). - Apply makeM2_canon. Apply H. Exact (mapcanon_M2_1 ? ? H1). - Exact (mapcanon_M2_2 ? ? H1). + simple induction m. intros. exact M0_canon. + intros a y H a0. simpl in |- *. case (ad_eq a a0). exact M0_canon. + assumption. + intros. simpl in |- *. case (ad_bit_0 a). apply makeM2_canon. exact (mapcanon_M2_1 _ _ H1). + apply H0. exact (mapcanon_M2_2 _ _ H1). + apply makeM2_canon. apply H. exact (mapcanon_M2_1 _ _ H1). + exact (mapcanon_M2_2 _ _ H1). Qed. - Lemma MapMerge_canon : (m,m':(Map A)) (mapcanon m) -> (mapcanon m') -> - (mapcanon (MapMerge A m m')). + Lemma MapMerge_canon : + forall m m':Map A, mapcanon m -> mapcanon m' -> mapcanon (MapMerge A m m'). Proof. - Induction m. Intros. Exact H0. - Simpl. Intros a y m' H H0. Exact (MapPut_behind_canon m' H0 a y). - Induction m'. Intros. Exact H1. - Intros a y H1 H2. Unfold MapMerge. Exact (MapPut_canon ? H1 a y). - Intros. Simpl. Apply M2_canon. Apply H. Exact (mapcanon_M2_1 ? ? H3). - Exact (mapcanon_M2_1 ? ? H4). - Apply H0. Exact (mapcanon_M2_2 ? ? H3). - Exact (mapcanon_M2_2 ? ? H4). - Change (le (2) (MapCard A (MapMerge A (M2 A m0 m1) (M2 A m2 m3)))). - Apply le_trans with m:=(MapCard A (M2 A m0 m1)). Exact (mapcanon_M2 ? ? H3). - Exact (MapMerge_Card_lb_l A (M2 A m0 m1) (M2 A m2 m3)). + simple induction m. intros. exact H0. + simpl in |- *. intros a y m' H H0. exact (MapPut_behind_canon m' H0 a y). + simple induction m'. intros. exact H1. + intros a y H1 H2. unfold MapMerge in |- *. exact (MapPut_canon _ H1 a y). + intros. simpl in |- *. apply M2_canon. apply H. exact (mapcanon_M2_1 _ _ H3). + exact (mapcanon_M2_1 _ _ H4). + apply H0. exact (mapcanon_M2_2 _ _ H3). + exact (mapcanon_M2_2 _ _ H4). + change (2 <= MapCard A (MapMerge A (M2 A m0 m1) (M2 A m2 m3))) in |- *. + apply le_trans with (m := MapCard A (M2 A m0 m1)). exact (mapcanon_M2 _ _ H3). + exact (MapMerge_Card_lb_l A (M2 A m0 m1) (M2 A m2 m3)). Qed. - Lemma MapDelta_canon : (m,m':(Map A)) (mapcanon m) -> (mapcanon m') -> - (mapcanon (MapDelta A m m')). + Lemma MapDelta_canon : + forall m m':Map A, mapcanon m -> mapcanon m' -> mapcanon (MapDelta A m m'). Proof. - Induction m. Intros. Exact H0. - Simpl. Intros a y m' H H0. Case (MapGet A m' a). Exact (MapPut_canon m' H0 a y). - Intro. Exact (MapRemove_canon m' H0 a). - Induction m'. Intros. Exact H1. - Unfold MapDelta. Intros a y H1 H2. Case (MapGet A (M2 A m0 m1) a). - Exact (MapPut_canon ? H1 a y). - Intro. Exact (MapRemove_canon ? H1 a). - Intros. Simpl. Apply makeM2_canon. Apply H. Exact (mapcanon_M2_1 ? ? H3). - Exact (mapcanon_M2_1 ? ? H4). - Apply H0. Exact (mapcanon_M2_2 ? ? H3). - Exact (mapcanon_M2_2 ? ? H4). + simple induction m. intros. exact H0. + simpl in |- *. intros a y m' H H0. case (MapGet A m' a). exact (MapPut_canon m' H0 a y). + intro. exact (MapRemove_canon m' H0 a). + simple induction m'. intros. exact H1. + unfold MapDelta in |- *. intros a y H1 H2. case (MapGet A (M2 A m0 m1) a). + exact (MapPut_canon _ H1 a y). + intro. exact (MapRemove_canon _ H1 a). + intros. simpl in |- *. apply makeM2_canon. apply H. exact (mapcanon_M2_1 _ _ H3). + exact (mapcanon_M2_1 _ _ H4). + apply H0. exact (mapcanon_M2_2 _ _ H3). + exact (mapcanon_M2_2 _ _ H4). Qed. Variable B : Set. - Lemma MapDomRestrTo_canon : (m:(Map A)) (mapcanon m) -> - (m':(Map B)) (mapcanon (MapDomRestrTo A B m m')). + Lemma MapDomRestrTo_canon : + forall m:Map A, + mapcanon m -> forall m':Map B, mapcanon (MapDomRestrTo A B m m'). Proof. - Induction m. Intros. Exact M0_canon. - Simpl. Intros a y H m'. Case (MapGet B m' a). Exact M0_canon. - Intro. Apply M1_canon. - Induction m'. Exact M0_canon. - Unfold MapDomRestrTo. Intros a y. Case (MapGet A (M2 A m0 m1) a). Exact M0_canon. - Intro. Apply M1_canon. - Intros. Simpl. Apply makeM2_canon. Apply H. Exact (mapcanon_M2_1 m0 m1 H1). - Apply H0. Exact (mapcanon_M2_2 m0 m1 H1). + simple induction m. intros. exact M0_canon. + simpl in |- *. intros a y H m'. case (MapGet B m' a). exact M0_canon. + intro. apply M1_canon. + simple induction m'. exact M0_canon. + unfold MapDomRestrTo in |- *. intros a y. case (MapGet A (M2 A m0 m1) a). exact M0_canon. + intro. apply M1_canon. + intros. simpl in |- *. apply makeM2_canon. apply H. exact (mapcanon_M2_1 m0 m1 H1). + apply H0. exact (mapcanon_M2_2 m0 m1 H1). Qed. - Lemma MapDomRestrBy_canon : (m:(Map A)) (mapcanon m) -> - (m':(Map B)) (mapcanon (MapDomRestrBy A B m m')). + Lemma MapDomRestrBy_canon : + forall m:Map A, + mapcanon m -> forall m':Map B, mapcanon (MapDomRestrBy A B m m'). Proof. - Induction m. Intros. Exact M0_canon. - Simpl. Intros a y H m'. Case (MapGet B m' a). Assumption. - Intro. Exact M0_canon. - Induction m'. Exact H1. - Intros a y. Simpl. Case (ad_bit_0 a). Apply makeM2_canon. Exact (mapcanon_M2_1 ? ? H1). - Apply MapRemove_canon. Exact (mapcanon_M2_2 ? ? H1). - Apply makeM2_canon. Apply MapRemove_canon. Exact (mapcanon_M2_1 ? ? H1). - Exact (mapcanon_M2_2 ? ? H1). - Intros. Simpl. Apply makeM2_canon. Apply H. Exact (mapcanon_M2_1 ? ? H1). - Apply H0. Exact (mapcanon_M2_2 ? ? H1). + simple induction m. intros. exact M0_canon. + simpl in |- *. intros a y H m'. case (MapGet B m' a). assumption. + intro. exact M0_canon. + simple induction m'. exact H1. + intros a y. simpl in |- *. case (ad_bit_0 a). apply makeM2_canon. exact (mapcanon_M2_1 _ _ H1). + apply MapRemove_canon. exact (mapcanon_M2_2 _ _ H1). + apply makeM2_canon. apply MapRemove_canon. exact (mapcanon_M2_1 _ _ H1). + exact (mapcanon_M2_2 _ _ H1). + intros. simpl in |- *. apply makeM2_canon. apply H. exact (mapcanon_M2_1 _ _ H1). + apply H0. exact (mapcanon_M2_2 _ _ H1). Qed. - Lemma Map_of_alist_canon : (l:(alist A)) (mapcanon (Map_of_alist A l)). + Lemma Map_of_alist_canon : forall l:alist A, mapcanon (Map_of_alist A l). Proof. - Induction l. Exact M0_canon. - Intro r. Elim r. Intros a y l0 H. Simpl. Apply MapPut_canon. Assumption. + simple induction l. exact M0_canon. + intro r. elim r. intros a y l0 H. simpl in |- *. apply MapPut_canon. assumption. Qed. - Lemma MapSubset_c_1 : (m:(Map A)) (m':(Map B)) (mapcanon m) -> - (MapSubset A B m m') -> (MapDomRestrBy A B m m')=(M0 A). + Lemma MapSubset_c_1 : + forall (m:Map A) (m':Map B), + mapcanon m -> MapSubset A B m m' -> MapDomRestrBy A B m m' = M0 A. Proof. - Intros. Apply mapcanon_unique. Apply MapDomRestrBy_canon. Assumption. - Apply M0_canon. - Exact (MapSubset_imp_2 ? ? m m' H0). + intros. apply mapcanon_unique. apply MapDomRestrBy_canon. assumption. + apply M0_canon. + exact (MapSubset_imp_2 _ _ m m' H0). Qed. - Lemma MapSubset_c_2 : (m:(Map A)) (m':(Map B)) - (MapDomRestrBy A B m m')=(M0 A) -> (MapSubset A B m m'). + Lemma MapSubset_c_2 : + forall (m:Map A) (m':Map B), + MapDomRestrBy A B m m' = M0 A -> MapSubset A B m m'. Proof. - Intros. Apply MapSubset_2_imp. Unfold MapSubset_2. Rewrite H. Apply eqmap_refl. + intros. apply MapSubset_2_imp. unfold MapSubset_2 in |- *. rewrite H. apply eqmap_refl. Qed. End MapCanon. @@ -325,52 +337,63 @@ Section FSetCanon. Variable A : Set. - Lemma MapDom_canon : (m:(Map A)) (mapcanon A m) -> (mapcanon unit (MapDom A m)). + Lemma MapDom_canon : + forall m:Map A, mapcanon A m -> mapcanon unit (MapDom A m). Proof. - Induction m. Intro. Exact (M0_canon unit). - Intros a y H. Exact (M1_canon unit a ?). - Intros. Simpl. Apply M2_canon. Apply H. Exact (mapcanon_M2_1 A ? ? H1). - Apply H0. Exact (mapcanon_M2_2 A ? ? H1). - Change (le (2) (MapCard unit (MapDom A (M2 A m0 m1)))). Rewrite <- MapCard_Dom. - Exact (mapcanon_M2 A ? ? H1). + simple induction m. intro. exact (M0_canon unit). + intros a y H. exact (M1_canon unit a _). + intros. simpl in |- *. apply M2_canon. apply H. exact (mapcanon_M2_1 A _ _ H1). + apply H0. exact (mapcanon_M2_2 A _ _ H1). + change (2 <= MapCard unit (MapDom A (M2 A m0 m1))) in |- *. rewrite <- MapCard_Dom. + exact (mapcanon_M2 A _ _ H1). Qed. End FSetCanon. Section MapFoldCanon. - Variable A, B : Set. - - Lemma MapFold_canon_1 : (m0:(Map B)) (mapcanon B m0) -> - (op : (Map B) -> (Map B) -> (Map B)) - ((m1:(Map B)) (mapcanon B m1) -> (m2:(Map B)) (mapcanon B m2) -> - (mapcanon B (op m1 m2))) -> - (f : ad->A->(Map B)) ((a:ad) (y:A) (mapcanon B (f a y))) -> - (m:(Map A)) (pf : ad->ad) (mapcanon B (MapFold1 A (Map B) m0 op f pf m)). + Variables A B : Set. + + Lemma MapFold_canon_1 : + forall m0:Map B, + mapcanon B m0 -> + forall op:Map B -> Map B -> Map B, + (forall m1:Map B, + mapcanon B m1 -> + forall m2:Map B, mapcanon B m2 -> mapcanon B (op m1 m2)) -> + forall f:ad -> A -> Map B, + (forall (a:ad) (y:A), mapcanon B (f a y)) -> + forall (m:Map A) (pf:ad -> ad), + mapcanon B (MapFold1 A (Map B) m0 op f pf m). Proof. - Induction m. Intro. Exact H. - Intros a y pf. Simpl. Apply H1. - Intros. Simpl. Apply H0. Apply H2. - Apply H3. + simple induction m. intro. exact H. + intros a y pf. simpl in |- *. apply H1. + intros. simpl in |- *. apply H0. apply H2. + apply H3. Qed. - Lemma MapFold_canon : (m0:(Map B)) (mapcanon B m0) -> - (op : (Map B) -> (Map B) -> (Map B)) - ((m1:(Map B)) (mapcanon B m1) -> (m2:(Map B)) (mapcanon B m2) -> - (mapcanon B (op m1 m2))) -> - (f : ad->A->(Map B)) ((a:ad) (y:A) (mapcanon B (f a y))) -> - (m:(Map A)) (mapcanon B (MapFold A (Map B) m0 op f m)). + Lemma MapFold_canon : + forall m0:Map B, + mapcanon B m0 -> + forall op:Map B -> Map B -> Map B, + (forall m1:Map B, + mapcanon B m1 -> + forall m2:Map B, mapcanon B m2 -> mapcanon B (op m1 m2)) -> + forall f:ad -> A -> Map B, + (forall (a:ad) (y:A), mapcanon B (f a y)) -> + forall m:Map A, mapcanon B (MapFold A (Map B) m0 op f m). Proof. - Intros. Exact (MapFold_canon_1 m0 H op H0 f H1 m [a:ad]a). + intros. exact (MapFold_canon_1 m0 H op H0 f H1 m (fun a:ad => a)). Qed. - Lemma MapCollect_canon : - (f : ad->A->(Map B)) ((a:ad) (y:A) (mapcanon B (f a y))) -> - (m:(Map A)) (mapcanon B (MapCollect A B f m)). + Lemma MapCollect_canon : + forall f:ad -> A -> Map B, + (forall (a:ad) (y:A), mapcanon B (f a y)) -> + forall m:Map A, mapcanon B (MapCollect A B f m). Proof. - Intros. Rewrite MapCollect_as_Fold. Apply MapFold_canon. Apply M0_canon. - Intros. Exact (MapMerge_canon B m1 m2 H0 H1). - Assumption. + intros. rewrite MapCollect_as_Fold. apply MapFold_canon. apply M0_canon. + intros. exact (MapMerge_canon B m1 m2 H0 H1). + assumption. Qed. -End MapFoldCanon. +End MapFoldCanon.
\ No newline at end of file |