diff options
Diffstat (limited to 'theories7/IntMap/Mapcard.v')
-rw-r--r-- | theories7/IntMap/Mapcard.v | 670 |
1 files changed, 670 insertions, 0 deletions
diff --git a/theories7/IntMap/Mapcard.v b/theories7/IntMap/Mapcard.v new file mode 100644 index 00000000..5c5e2a93 --- /dev/null +++ b/theories7/IntMap/Mapcard.v @@ -0,0 +1,670 @@ +(************************************************************************) +(* 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: Mapcard.v,v 1.1.2.1 2004/07/16 19:31:28 herbelin Exp $ i*) + +Require Bool. +Require Sumbool. +Require Arith. +Require ZArith. +Require Addr. +Require Adist. +Require Addec. +Require Map. +Require Mapaxioms. +Require Mapiter. +Require Fset. +Require Mapsubset. +Require PolyList. +Require Lsort. +Require Peano_dec. + +Section MapCard. + + Variable A, B : Set. + + Lemma MapCard_M0 : (MapCard A (M0 A))=O. + Proof. + Trivial. + Qed. + + Lemma MapCard_M1 : (a:ad) (y:A) (MapCard A (M1 A a y))=(1). + Proof. + Trivial. + Qed. + + Lemma MapCard_is_O : (m:(Map A)) (MapCard A m)=O -> + (a:ad) (MapGet A m a)=(NONE A). + Proof. + Induction m. Trivial. + Intros a y H. Discriminate H. + Intros. Simpl in H1. Elim (plus_is_O ? ? H1). Intros. Rewrite (MapGet_M2_bit_0_if A m0 m1 a). + Case (ad_bit_0 a). Apply H0. Assumption. + Apply H. Assumption. + Qed. + + Lemma MapCard_is_not_O : (m:(Map A)) (a:ad) (y:A) (MapGet A m a)=(SOME A y) -> + {n:nat | (MapCard A m)=(S n)}. + Proof. + Induction m. Intros. Discriminate H. + Intros a y a0 y0 H. Simpl in H. Elim (sumbool_of_bool (ad_eq a a0)). Intro H0. Split with O. + Reflexivity. + Intro H0. Rewrite H0 in H. Discriminate H. + Intros. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H2. + Rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1) in H1. Elim (H0 (ad_div_2 a) y H1). Intros n H3. + Simpl. Rewrite H3. Split with (plus (MapCard A m0) n). + Rewrite <- (plus_Snm_nSm (MapCard A m0) n). Reflexivity. + Intro H2. Rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1) in H1. Elim (H (ad_div_2 a) y H1). + Intros n H3. Simpl. Rewrite H3. Split with (plus n (MapCard A m1)). Reflexivity. + Qed. + + Lemma MapCard_is_one : (m:(Map A)) (MapCard A m)=(1) -> + {a:ad & {y:A | (MapGet A m a)=(SOME A y)}}. + Proof. + Induction m. Intro. Discriminate H. + Intros a y H. Split with a. Split with y. Apply M1_semantics_1. + Intros. Simpl in H1. Elim (plus_is_one (MapCard A m0) (MapCard A m1) H1). + Intro H2. Elim H2. Intros. Elim (H0 H4). Intros a H5. Split with (ad_double_plus_un a). + Rewrite (MapGet_M2_bit_0_1 A ? (ad_double_plus_un_bit_0 a) m0 m1). + Rewrite ad_double_plus_un_div_2. Exact H5. + Intro H2. Elim H2. Intros. Elim (H H3). Intros a H5. Split with (ad_double a). + Rewrite (MapGet_M2_bit_0_0 A ? (ad_double_bit_0 a) m0 m1). + Rewrite ad_double_div_2. Exact H5. + Qed. + + Lemma MapCard_is_one_unique : (m:(Map A)) (MapCard A m)=(1) -> (a,a':ad) (y,y':A) + (MapGet A m a)=(SOME A y) -> (MapGet A m a')=(SOME A y') -> + a=a' /\ y=y'. + Proof. + Induction m. Intro. Discriminate H. + Intros. Elim (sumbool_of_bool (ad_eq a a1)). Intro H2. Rewrite (ad_eq_complete ? ? H2) in H0. + Rewrite (M1_semantics_1 A a1 a0) in H0. Inversion H0. Elim (sumbool_of_bool (ad_eq a a')). + Intro H5. Rewrite (ad_eq_complete ? ? H5) in H1. Rewrite (M1_semantics_1 A a' a0) in H1. + Inversion H1. Rewrite <- (ad_eq_complete ? ? H2). Rewrite <- (ad_eq_complete ? ? H5). + Rewrite <- H4. Rewrite <- H6. (Split; Reflexivity). + Intro H5. Rewrite (M1_semantics_2 A a a' a0 H5) in H1. Discriminate H1. + Intro H2. Rewrite (M1_semantics_2 A a a1 a0 H2) in H0. Discriminate H0. + Intros. Simpl in H1. Elim (plus_is_one ? ? H1). Intro H4. Elim H4. Intros. + Rewrite (MapGet_M2_bit_0_if A m0 m1 a) in H2. Elim (sumbool_of_bool (ad_bit_0 a)). + Intro H7. Rewrite H7 in H2. Rewrite (MapGet_M2_bit_0_if A m0 m1 a') in H3. + Elim (sumbool_of_bool (ad_bit_0 a')). Intro H8. Rewrite H8 in H3. Elim (H0 H6 ? ? ? ? H2 H3). + Intros. Split. Rewrite <- (ad_div_2_double_plus_un a H7). + Rewrite <- (ad_div_2_double_plus_un a' H8). Rewrite H9. Reflexivity. + Assumption. + Intro H8. Rewrite H8 in H3. Rewrite (MapCard_is_O m0 H5 (ad_div_2 a')) in H3. + Discriminate H3. + Intro H7. Rewrite H7 in H2. Rewrite (MapCard_is_O m0 H5 (ad_div_2 a)) in H2. + Discriminate H2. + Intro H4. Elim H4. Intros. Rewrite (MapGet_M2_bit_0_if A m0 m1 a) in H2. + Elim (sumbool_of_bool (ad_bit_0 a)). Intro H7. Rewrite H7 in H2. + Rewrite (MapCard_is_O m1 H6 (ad_div_2 a)) in H2. Discriminate H2. + Intro H7. Rewrite H7 in H2. Rewrite (MapGet_M2_bit_0_if A m0 m1 a') in H3. + Elim (sumbool_of_bool (ad_bit_0 a')). Intro H8. Rewrite H8 in H3. + Rewrite (MapCard_is_O m1 H6 (ad_div_2 a')) in H3. Discriminate H3. + Intro H8. Rewrite H8 in H3. Elim (H H5 ? ? ? ? H2 H3). Intros. Split. + Rewrite <- (ad_div_2_double a H7). Rewrite <- (ad_div_2_double a' H8). + Rewrite H9. Reflexivity. + Assumption. + Qed. + + Lemma length_as_fold : (C:Set) (l:(list C)) + (length l)=(fold_right [_:C][n:nat](S n) O l). + Proof. + Induction l. Reflexivity. + Intros. Simpl. Rewrite H. Reflexivity. + Qed. + + Lemma length_as_fold_2 : (l:(alist A)) + (length l)=(fold_right [r:ad*A][n:nat]let (a,y)=r in (plus (1) n) O l). + Proof. + Induction l. Reflexivity. + Intros. Simpl. Rewrite H. (Elim a; Reflexivity). + Qed. + + Lemma MapCard_as_Fold_1 : (m:(Map A)) (pf:ad->ad) + (MapCard A m)=(MapFold1 A nat O plus [_:ad][_:A](1) pf m). + Proof. + Induction m. Trivial. + Trivial. + Intros. Simpl. Rewrite <- (H [a0:ad](pf (ad_double a0))). + Rewrite <- (H0 [a0:ad](pf (ad_double_plus_un a0))). Reflexivity. + Qed. + + Lemma MapCard_as_Fold : + (m:(Map A)) (MapCard A m)=(MapFold A nat O plus [_:ad][_:A](1) m). + Proof. + Intro. Exact (MapCard_as_Fold_1 m [a0:ad]a0). + Qed. + + Lemma MapCard_as_length : (m:(Map A)) (MapCard A m)=(length (alist_of_Map A m)). + Proof. + Intro. Rewrite MapCard_as_Fold. Rewrite length_as_fold_2. + Apply MapFold_as_fold with op:=plus neutral:=O f:=[_:ad][_:A](1). Exact plus_assoc_r. + Trivial. + Intro. Rewrite <- plus_n_O. Reflexivity. + Qed. + + Lemma MapCard_Put1_equals_2 : (p:positive) (a,a':ad) (y,y':A) + (MapCard A (MapPut1 A a y a' y' p))=(2). + Proof. + Induction p. Intros. Simpl. (Case (ad_bit_0 a); Reflexivity). + Intros. Simpl. Case (ad_bit_0 a). Exact (H (ad_div_2 a) (ad_div_2 a') y y'). + Simpl. Rewrite <- plus_n_O. Exact (H (ad_div_2 a) (ad_div_2 a') y y'). + Intros. Simpl. (Case (ad_bit_0 a); Reflexivity). + Qed. + + Lemma MapCard_Put_sum : (m,m':(Map A)) (a:ad) (y:A) (n,n':nat) + m'=(MapPut A m a y) -> n=(MapCard A m) -> n'=(MapCard A m') -> + {n'=n}+{n'=(S n)}. + Proof. + Induction m. Simpl. Intros. Rewrite H in H1. Simpl in H1. Right . + Rewrite H0. Rewrite H1. Reflexivity. + Intros a y m' a0 y0 n n' H H0 H1. Simpl in H. Elim (ad_sum (ad_xor a a0)). Intro H2. + Elim H2. Intros p H3. Rewrite H3 in H. Rewrite H in H1. + Rewrite (MapCard_Put1_equals_2 p a a0 y y0) in H1. Simpl in H0. Right . + Rewrite H0. Rewrite H1. Reflexivity. + Intro H2. Rewrite H2 in H. Rewrite H in H1. Simpl in H1. Simpl in H0. Left . + Rewrite H0. Rewrite H1. Reflexivity. + Intros. Simpl in H2. Rewrite (MapPut_semantics_3_1 A m0 m1 a y) in H1. + Elim (sumbool_of_bool (ad_bit_0 a)). Intro H4. Rewrite H4 in H1. + Elim (H0 (MapPut A m1 (ad_div_2 a) y) (ad_div_2 a) y (MapCard A m1) + (MapCard A (MapPut A m1 (ad_div_2 a) y)) (refl_equal ? ?) + (refl_equal ? ?) (refl_equal ? ?)). + Intro H5. Rewrite H1 in H3. Simpl in H3. Rewrite H5 in H3. Rewrite <- H2 in H3. Left . + Assumption. + Intro H5. Rewrite H1 in H3. Simpl in H3. Rewrite H5 in H3. + Rewrite <- (plus_Snm_nSm (MapCard A m0) (MapCard A m1)) in H3. + Simpl in H3. Rewrite <- H2 in H3. Right . Assumption. + Intro H4. Rewrite H4 in H1. + Elim (H (MapPut A m0 (ad_div_2 a) y) (ad_div_2 a) y (MapCard A m0) + (MapCard A (MapPut A m0 (ad_div_2 a) y)) (refl_equal ? ?) + (refl_equal ? ?) (refl_equal ? ?)). + Intro H5. Rewrite H1 in H3. Simpl in H3. Rewrite H5 in H3. Rewrite <- H2 in H3. + Left . Assumption. + Intro H5. Rewrite H1 in H3. Simpl in H3. Rewrite H5 in H3. Simpl in H3. Rewrite <- H2 in H3. + Right . Assumption. + Qed. + + Lemma MapCard_Put_lb : (m:(Map A)) (a:ad) (y:A) + (ge (MapCard A (MapPut A m a y)) (MapCard A m)). + Proof. + Unfold ge. Intros. + Elim (MapCard_Put_sum m (MapPut A m a y) a y (MapCard A m) + (MapCard A (MapPut A m a y)) (refl_equal ? ?) (refl_equal ? ?) + (refl_equal ? ?)). + Intro H. Rewrite H. Apply le_n. + Intro H. Rewrite H. Apply le_n_Sn. + Qed. + + Lemma MapCard_Put_ub : (m:(Map A)) (a:ad) (y:A) + (le (MapCard A (MapPut A m a y)) (S (MapCard A m))). + Proof. + Intros. + Elim (MapCard_Put_sum m (MapPut A m a y) a y (MapCard A m) + (MapCard A (MapPut A m a y)) (refl_equal ? ?) (refl_equal ? ?) + (refl_equal ? ?)). + Intro H. Rewrite H. Apply le_n_Sn. + Intro H. Rewrite H. Apply le_n. + Qed. + + Lemma MapCard_Put_1 : (m:(Map A)) (a:ad) (y:A) + (MapCard A (MapPut A m a y))=(MapCard A m) -> + {y:A | (MapGet A m a)=(SOME A y)}. + Proof. + Induction m. Intros. Discriminate H. + Intros a y a0 y0 H. Simpl in H. Elim (ad_sum (ad_xor a a0)). Intro H0. Elim H0. + Intros p H1. Rewrite H1 in H. Rewrite (MapCard_Put1_equals_2 p a a0 y y0) in H. + Discriminate H. + Intro H0. Rewrite H0 in H. Rewrite (ad_xor_eq ? ? H0). Split with y. Apply M1_semantics_1. + Intros. Rewrite (MapPut_semantics_3_1 A m0 m1 a y) in H1. Elim (sumbool_of_bool (ad_bit_0 a)). + Intro H2. Rewrite H2 in H1. Simpl in H1. Elim (H0 (ad_div_2 a) y (simpl_plus_l ? ? ? H1)). + Intros y0 H3. Split with y0. Rewrite <- H3. Exact (MapGet_M2_bit_0_1 A a H2 m0 m1). + Intro H2. Rewrite H2 in H1. Simpl in H1. + Rewrite (plus_sym (MapCard A (MapPut A m0 (ad_div_2 a) y)) (MapCard A m1)) in H1. + Rewrite (plus_sym (MapCard A m0) (MapCard A m1)) in H1. + Elim (H (ad_div_2 a) y (simpl_plus_l ? ? ? H1)). Intros y0 H3. Split with y0. + Rewrite <- H3. Exact (MapGet_M2_bit_0_0 A a H2 m0 m1). + Qed. + + Lemma MapCard_Put_2 : (m:(Map A)) (a:ad) (y:A) + (MapCard A (MapPut A m a y))=(S (MapCard A m)) -> (MapGet A m a)=(NONE A). + Proof. + Induction m. Trivial. + Intros. Simpl in H. Elim (sumbool_of_bool (ad_eq a a1)). Intro H0. + Rewrite (ad_eq_complete ? ? H0) in H. Rewrite (ad_xor_nilpotent a1) in H. Discriminate H. + Intro H0. Exact (M1_semantics_2 A a a1 a0 H0). + Intros. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H2. + Rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1). Apply (H0 (ad_div_2 a) y). + Apply simpl_plus_l with n:=(MapCard A m0). + Rewrite <- (plus_Snm_nSm (MapCard A m0) (MapCard A m1)). Simpl in H1. Simpl. Rewrite <- H1. + Clear H1. + NewInduction a. Discriminate H2. + NewInduction p. Reflexivity. + Discriminate H2. + Reflexivity. + Intro H2. Rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1). Apply (H (ad_div_2 a) y). + Cut (plus (MapCard A (MapPut A m0 (ad_div_2 a) y)) (MapCard A m1)) + =(plus (S (MapCard A m0)) (MapCard A m1)). + Intro. Rewrite (plus_sym (MapCard A (MapPut A m0 (ad_div_2 a) y)) (MapCard A m1)) in H3. + Rewrite (plus_sym (S (MapCard A m0)) (MapCard A m1)) in H3. Exact (simpl_plus_l ? ? ? H3). + Simpl. Simpl in H1. Rewrite <- H1. NewInduction a. Trivial. + NewInduction p. Discriminate H2. + Reflexivity. + Discriminate H2. + Qed. + + Lemma MapCard_Put_1_conv : (m:(Map A)) (a:ad) (y,y':A) + (MapGet A m a)=(SOME A y) -> (MapCard A (MapPut A m a y'))=(MapCard A m). + Proof. + Intros. + Elim (MapCard_Put_sum m (MapPut A m a y') a y' (MapCard A m) + (MapCard A (MapPut A m a y')) (refl_equal ? ?) (refl_equal ? ?) + (refl_equal ? ?)). + Trivial. + Intro H0. Rewrite (MapCard_Put_2 m a y' H0) in H. Discriminate H. + Qed. + + Lemma MapCard_Put_2_conv : (m:(Map A)) (a:ad) (y:A) + (MapGet A m a)=(NONE A) -> (MapCard A (MapPut A m a y))=(S (MapCard A m)). + Proof. + Intros. + Elim (MapCard_Put_sum m (MapPut A m a y) a y (MapCard A m) + (MapCard A (MapPut A m a y)) (refl_equal ? ?) (refl_equal ? ?) + (refl_equal ? ?)). + Intro H0. Elim (MapCard_Put_1 m a y H0). Intros y' H1. Rewrite H1 in H. Discriminate H. + Trivial. + Qed. + + Lemma MapCard_ext : (m,m':(Map A)) + (eqm A (MapGet A m) (MapGet A m')) -> (MapCard A m)=(MapCard A m'). + Proof. + Unfold eqm. Intros. Rewrite (MapCard_as_length m). Rewrite (MapCard_as_length m'). + Rewrite (alist_canonical A (alist_of_Map A m) (alist_of_Map A m')). Reflexivity. + Unfold eqm. Intro. Rewrite (Map_of_alist_semantics A (alist_of_Map A m) a). + Rewrite (Map_of_alist_semantics A (alist_of_Map A m') a). Rewrite (Map_of_alist_of_Map A m' a). + Rewrite (Map_of_alist_of_Map A m a). Exact (H a). + Apply alist_of_Map_sorts2. + Apply alist_of_Map_sorts2. + Qed. + + Lemma MapCard_Dom : (m:(Map A)) (MapCard A m)=(MapCard unit (MapDom A m)). + Proof. + (Induction m; Trivial). Intros. Simpl. Rewrite H. Rewrite H0. Reflexivity. + Qed. + + Lemma MapCard_Dom_Put_behind : (m:(Map A)) (a:ad) (y:A) + (MapDom A (MapPut_behind A m a y))=(MapDom A (MapPut A m a y)). + Proof. + Induction m. Trivial. + Intros a y a0 y0. Simpl. Elim (ad_sum (ad_xor a a0)). Intro H. Elim H. + Intros p H0. Rewrite H0. Reflexivity. + Intro H. Rewrite H. Rewrite (ad_xor_eq ? ? H). Reflexivity. + Intros. Simpl. Elim (ad_sum a). Intro H1. Elim H1. Intros p H2. Rewrite H2. Case p. + Intro p0. Simpl. Rewrite H0. Reflexivity. + Intro p0. Simpl. Rewrite H. Reflexivity. + Simpl. Rewrite H0. Reflexivity. + Intro H1. Rewrite H1. Simpl. Rewrite H. Reflexivity. + Qed. + + Lemma MapCard_Put_behind_Put : (m:(Map A)) (a:ad) (y:A) + (MapCard A (MapPut_behind A m a y))=(MapCard A (MapPut A m a y)). + Proof. + Intros. Rewrite MapCard_Dom. Rewrite MapCard_Dom. Rewrite MapCard_Dom_Put_behind. + Reflexivity. + Qed. + + Lemma MapCard_Put_behind_sum : (m,m':(Map A)) (a:ad) (y:A) (n,n':nat) + m'=(MapPut_behind A m a y) -> n=(MapCard A m) -> n'=(MapCard A m') -> + {n'=n}+{n'=(S n)}. + Proof. + Intros. (Apply (MapCard_Put_sum m (MapPut A m a y) a y n n'); Trivial). + Rewrite <- MapCard_Put_behind_Put. Rewrite <- H. Assumption. + Qed. + + Lemma MapCard_makeM2 : (m,m':(Map A)) + (MapCard A (makeM2 A m m'))=(plus (MapCard A m) (MapCard A m')). + Proof. + Intros. Rewrite (MapCard_ext ? ? (makeM2_M2 A m m')). Reflexivity. + Qed. + + Lemma MapCard_Remove_sum : (m,m':(Map A)) (a:ad) (n,n':nat) + m'=(MapRemove A m a) -> n=(MapCard A m) -> n'=(MapCard A m') -> + {n=n'}+{n=(S n')}. + Proof. + Induction m. Simpl. Intros. Rewrite H in H1. Simpl in H1. Left . Rewrite H1. Assumption. + Simpl. Intros. Elim (sumbool_of_bool (ad_eq a a1)). Intro H2. Rewrite H2 in H. + Rewrite H in H1. Simpl in H1. Right . Rewrite H1. Assumption. + Intro H2. Rewrite H2 in H. Rewrite H in H1. Simpl in H1. Left . Rewrite H1. Assumption. + Intros. Simpl in H1. Simpl in H2. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H4. + Rewrite H4 in H1. Rewrite H1 in H3. + Rewrite (MapCard_makeM2 m0 (MapRemove A m1 (ad_div_2 a))) in H3. + Elim (H0 (MapRemove A m1 (ad_div_2 a)) (ad_div_2 a) (MapCard A m1) + (MapCard A (MapRemove A m1 (ad_div_2 a))) (refl_equal ? ?) + (refl_equal ? ?) (refl_equal ? ?)). + Intro H5. Rewrite H5 in H2. Left . Rewrite H3. Exact H2. + Intro H5. Rewrite H5 in H2. + Rewrite <- (plus_Snm_nSm (MapCard A m0) (MapCard A (MapRemove A m1 (ad_div_2 a)))) in H2. + Right . Rewrite H3. Exact H2. + Intro H4. Rewrite H4 in H1. Rewrite H1 in H3. + Rewrite (MapCard_makeM2 (MapRemove A m0 (ad_div_2 a)) m1) in H3. + Elim (H (MapRemove A m0 (ad_div_2 a)) (ad_div_2 a) (MapCard A m0) + (MapCard A (MapRemove A m0 (ad_div_2 a))) (refl_equal ? ?) + (refl_equal ? ?) (refl_equal ? ?)). + Intro H5. Rewrite H5 in H2. Left . Rewrite H3. Exact H2. + Intro H5. Rewrite H5 in H2. Right . Rewrite H3. Exact H2. + Qed. + + Lemma MapCard_Remove_ub : (m:(Map A)) (a:ad) + (le (MapCard A (MapRemove A m a)) (MapCard A m)). + Proof. + Intros. + Elim (MapCard_Remove_sum m (MapRemove A m a) a (MapCard A m) + (MapCard A (MapRemove A m a)) (refl_equal ? ?) (refl_equal ? ?) + (refl_equal ? ?)). + Intro H. Rewrite H. Apply le_n. + Intro H. Rewrite H. Apply le_n_Sn. + Qed. + + Lemma MapCard_Remove_lb : (m:(Map A)) (a:ad) + (ge (S (MapCard A (MapRemove A m a))) (MapCard A m)). + Proof. + Unfold ge. Intros. + Elim (MapCard_Remove_sum m (MapRemove A m a) a (MapCard A m) + (MapCard A (MapRemove A m a)) (refl_equal ? ?) (refl_equal ? ?) + (refl_equal ? ?)). + Intro H. Rewrite H. Apply le_n_Sn. + Intro H. Rewrite H. Apply le_n. + Qed. + + Lemma MapCard_Remove_1 : (m:(Map A)) (a:ad) + (MapCard A (MapRemove A m a))=(MapCard A m) -> (MapGet A m a)=(NONE A). + Proof. + Induction m. Trivial. + Simpl. Intros a y a0 H. Elim (sumbool_of_bool (ad_eq a a0)). Intro H0. + Rewrite H0 in H. Discriminate H. + Intro H0. Rewrite H0. Reflexivity. + Intros. Simpl in H1. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H2. Rewrite H2 in H1. + Rewrite (MapCard_makeM2 m0 (MapRemove A m1 (ad_div_2 a))) in H1. + Rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1). Apply H0. Exact (simpl_plus_l ? ? ? H1). + Intro H2. Rewrite H2 in H1. + Rewrite (MapCard_makeM2 (MapRemove A m0 (ad_div_2 a)) m1) in H1. + Rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1). Apply H. + Rewrite (plus_sym (MapCard A (MapRemove A m0 (ad_div_2 a))) (MapCard A m1)) in H1. + Rewrite (plus_sym (MapCard A m0) (MapCard A m1)) in H1. Exact (simpl_plus_l ? ? ? H1). + Qed. + + Lemma MapCard_Remove_2 : (m:(Map A)) (a:ad) + (S (MapCard A (MapRemove A m a)))=(MapCard A m) -> + {y:A | (MapGet A m a)=(SOME A y)}. + Proof. + Induction m. Intros. Discriminate H. + Intros a y a0 H. Simpl in H. Elim (sumbool_of_bool (ad_eq a a0)). Intro H0. + Rewrite (ad_eq_complete ? ? H0). Split with y. Exact (M1_semantics_1 A a0 y). + Intro H0. Rewrite H0 in H. Discriminate H. + Intros. Simpl in H1. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H2. Rewrite H2 in H1. + Rewrite (MapCard_makeM2 m0 (MapRemove A m1 (ad_div_2 a))) in H1. + Rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1). Apply H0. + Change (plus (S (MapCard A m0)) (MapCard A (MapRemove A m1 (ad_div_2 a)))) + =(plus (MapCard A m0) (MapCard A m1)) in H1. + Rewrite (plus_Snm_nSm (MapCard A m0) (MapCard A (MapRemove A m1 (ad_div_2 a)))) in H1. + Exact (simpl_plus_l ? ? ? H1). + Intro H2. Rewrite H2 in H1. Rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1). Apply H. + Rewrite (MapCard_makeM2 (MapRemove A m0 (ad_div_2 a)) m1) in H1. + Change (plus (S (MapCard A (MapRemove A m0 (ad_div_2 a)))) (MapCard A m1)) + =(plus (MapCard A m0) (MapCard A m1)) in H1. + Rewrite (plus_sym (S (MapCard A (MapRemove A m0 (ad_div_2 a)))) (MapCard A m1)) in H1. + Rewrite (plus_sym (MapCard A m0) (MapCard A m1)) in H1. Exact (simpl_plus_l ? ? ? H1). + Qed. + + Lemma MapCard_Remove_1_conv : (m:(Map A)) (a:ad) + (MapGet A m a)=(NONE A) -> (MapCard A (MapRemove A m a))=(MapCard A m). + Proof. + Intros. + Elim (MapCard_Remove_sum m (MapRemove A m a) a (MapCard A m) + (MapCard A (MapRemove A m a)) (refl_equal ? ?) (refl_equal ? ?) + (refl_equal ? ?)). + Intro H0. Rewrite H0. Reflexivity. + Intro H0. Elim (MapCard_Remove_2 m a (sym_eq ? ? ? H0)). Intros y H1. Rewrite H1 in H. + Discriminate H. + Qed. + + Lemma MapCard_Remove_2_conv : (m:(Map A)) (a:ad) (y:A) + (MapGet A m a)=(SOME A y) -> + (S (MapCard A (MapRemove A m a)))=(MapCard A m). + Proof. + Intros. + Elim (MapCard_Remove_sum m (MapRemove A m a) a (MapCard A m) + (MapCard A (MapRemove A m a)) (refl_equal ? ?) (refl_equal ? ?) + (refl_equal ? ?)). + Intro H0. Rewrite (MapCard_Remove_1 m a (sym_eq ? ? ? H0)) in H. Discriminate H. + Intro H0. Rewrite H0. Reflexivity. + Qed. + + Lemma MapMerge_Restr_Card : (m,m':(Map A)) + (plus (MapCard A m) (MapCard A m'))= + (plus (MapCard A (MapMerge A m m')) (MapCard A (MapDomRestrTo A A m m'))). + Proof. + Induction m. Simpl. Intro. Apply plus_n_O. + Simpl. Intros a y m'. Elim (option_sum A (MapGet A m' a)). Intro H. Elim H. Intros y0 H0. + Rewrite H0. Rewrite MapCard_Put_behind_Put. Rewrite (MapCard_Put_1_conv m' a y0 y H0). + Simpl. Rewrite <- plus_Snm_nSm. Apply plus_n_O. + Intro H. Rewrite H. Rewrite MapCard_Put_behind_Put. Rewrite (MapCard_Put_2_conv m' a y H). + Apply plus_n_O. + Intros. + Change (plus (plus (MapCard A m0) (MapCard A m1)) (MapCard A m')) + =(plus (MapCard A (MapMerge A (M2 A m0 m1) m')) + (MapCard A (MapDomRestrTo A A (M2 A m0 m1) m'))). + Elim m'. Reflexivity. + Intros a y. Unfold MapMerge. Unfold MapDomRestrTo. + Elim (option_sum A (MapGet A (M2 A m0 m1) a)). Intro H1. Elim H1. Intros y0 H2. Rewrite H2. + Rewrite (MapCard_Put_1_conv (M2 A m0 m1) a y0 y H2). Reflexivity. + Intro H1. Rewrite H1. Rewrite (MapCard_Put_2_conv (M2 A m0 m1) a y H1). Simpl. + Rewrite <- (plus_Snm_nSm (plus (MapCard A m0) (MapCard A m1)) O). Reflexivity. + Intros. Simpl. + Rewrite (plus_permute_2_in_4 (MapCard A m0) (MapCard A m1) (MapCard A m2) (MapCard A m3)). + Rewrite (H m2). Rewrite (H0 m3). + Rewrite (MapCard_makeM2 (MapDomRestrTo A A m0 m2) (MapDomRestrTo A A m1 m3)). + Apply plus_permute_2_in_4. + Qed. + + Lemma MapMerge_disjoint_Card : (m,m':(Map A)) (MapDisjoint A A m m') -> + (MapCard A (MapMerge A m m'))=(plus (MapCard A m) (MapCard A m')). + Proof. + Intros. Rewrite (MapMerge_Restr_Card m m'). + Rewrite (MapCard_ext ? ? (MapDisjoint_imp_2 ? ? ? ? H)). Apply plus_n_O. + Qed. + + Lemma MapSplit_Card : (m:(Map A)) (m':(Map B)) + (MapCard A m)=(plus (MapCard A (MapDomRestrTo A B m m')) + (MapCard A (MapDomRestrBy A B m m'))). + Proof. + Intros. Rewrite (MapCard_ext ? ? (MapDom_Split_1 A B m m')). Apply MapMerge_disjoint_Card. + Apply MapDisjoint_2_imp. Unfold MapDisjoint_2. Apply MapDom_Split_3. + Qed. + + Lemma MapMerge_Card_ub : (m,m':(Map A)) + (le (MapCard A (MapMerge A m m')) (plus (MapCard A m) (MapCard A m'))). + Proof. + Intros. Rewrite MapMerge_Restr_Card. Apply le_plus_l. + Qed. + + Lemma MapDomRestrTo_Card_ub_l : (m:(Map A)) (m':(Map B)) + (le (MapCard A (MapDomRestrTo A B m m')) (MapCard A m)). + Proof. + Intros. Rewrite (MapSplit_Card m m'). Apply le_plus_l. + Qed. + + Lemma MapDomRestrBy_Card_ub_l : (m:(Map A)) (m':(Map B)) + (le (MapCard A (MapDomRestrBy A B m m')) (MapCard A m)). + Proof. + Intros. Rewrite (MapSplit_Card m m'). Apply le_plus_r. + Qed. + + Lemma MapMerge_Card_disjoint : (m,m':(Map A)) + (MapCard A (MapMerge A m m'))=(plus (MapCard A m) (MapCard A m')) -> + (MapDisjoint A A m m'). + Proof. + Induction m. Intros. Apply Map_M0_disjoint. + Simpl. Intros. Rewrite (MapCard_Put_behind_Put m' a a0) in H. Unfold MapDisjoint in_dom. + Simpl. Intros. Elim (sumbool_of_bool (ad_eq a a1)). Intro H2. + Rewrite (ad_eq_complete ? ? H2) in H. Rewrite (MapCard_Put_2 m' a1 a0 H) in H1. + Discriminate H1. + Intro H2. Rewrite H2 in H0. Discriminate H0. + Induction m'. Intros. Apply Map_disjoint_M0. + Intros a y H1. Rewrite <- (MapCard_ext ? ? (MapPut_as_Merge A (M2 A m0 m1) a y)) in H1. + Unfold 3 MapCard in H1. Rewrite <- (plus_Snm_nSm (MapCard A (M2 A m0 m1)) O) in H1. + Rewrite <- (plus_n_O (S (MapCard A (M2 A m0 m1)))) in H1. Unfold MapDisjoint in_dom. + Unfold 2 MapGet. Intros. Elim (sumbool_of_bool (ad_eq a a0)). Intro H4. + Rewrite <- (ad_eq_complete ? ? H4) in H2. Rewrite (MapCard_Put_2 ? ? ? H1) in H2. + Discriminate H2. + Intro H4. Rewrite H4 in H3. Discriminate H3. + Intros. Unfold MapDisjoint. Intros. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H6. + Unfold MapDisjoint in H0. Apply H0 with m':=m3 a:=(ad_div_2 a). Apply le_antisym. + Apply MapMerge_Card_ub. + Apply simpl_le_plus_l with p:=(plus (MapCard A m0) (MapCard A m2)). + Rewrite (plus_permute_2_in_4 (MapCard A m0) (MapCard A m2) (MapCard A m1) (MapCard A m3)). + Change (MapCard A (M2 A (MapMerge A m0 m2) (MapMerge A m1 m3))) + =(plus (plus (MapCard A m0) (MapCard A m1)) (plus (MapCard A m2) (MapCard A m3))) in H3. + Rewrite <- H3. Simpl. Apply le_reg_r. Apply MapMerge_Card_ub. + Elim (in_dom_some ? ? ? H4). Intros y H7. Rewrite (MapGet_M2_bit_0_1 ? a H6 m0 m1) in H7. + Unfold in_dom. Rewrite H7. Reflexivity. + Elim (in_dom_some ? ? ? H5). Intros y H7. Rewrite (MapGet_M2_bit_0_1 ? a H6 m2 m3) in H7. + Unfold in_dom. Rewrite H7. Reflexivity. + Intro H6. Unfold MapDisjoint in H. Apply H with m':=m2 a:=(ad_div_2 a). Apply le_antisym. + Apply MapMerge_Card_ub. + Apply simpl_le_plus_l with p:=(plus (MapCard A m1) (MapCard A m3)). + Rewrite (plus_sym (plus (MapCard A m1) (MapCard A m3)) (plus (MapCard A m0) (MapCard A m2))). + Rewrite (plus_permute_2_in_4 (MapCard A m0) (MapCard A m2) (MapCard A m1) (MapCard A m3)). + Rewrite (plus_sym (plus (MapCard A m1) (MapCard A m3)) (MapCard A (MapMerge A m0 m2))). + Change (plus (MapCard A (MapMerge A m0 m2)) (MapCard A (MapMerge A m1 m3))) + =(plus (plus (MapCard A m0) (MapCard A m1)) (plus (MapCard A m2) (MapCard A m3))) in H3. + Rewrite <- H3. Apply le_reg_l. Apply MapMerge_Card_ub. + Elim (in_dom_some ? ? ? H4). Intros y H7. Rewrite (MapGet_M2_bit_0_0 ? a H6 m0 m1) in H7. + Unfold in_dom. Rewrite H7. Reflexivity. + Elim (in_dom_some ? ? ? H5). Intros y H7. Rewrite (MapGet_M2_bit_0_0 ? a H6 m2 m3) in H7. + Unfold in_dom. Rewrite H7. Reflexivity. + Qed. + + Lemma MapCard_is_Sn : (m:(Map A)) (n:nat) (MapCard ? m)=(S n) -> + {a:ad | (in_dom ? a m)=true}. + Proof. + Induction m. Intros. Discriminate H. + Intros a y n H. Split with a. Unfold in_dom. Rewrite (M1_semantics_1 ? a y). Reflexivity. + Intros. Simpl in H1. Elim (O_or_S (MapCard ? m0)). Intro H2. Elim H2. Intros m2 H3. + Elim (H ? (sym_eq ? ? ? H3)). Intros a H4. Split with (ad_double a). Unfold in_dom. + Rewrite (MapGet_M2_bit_0_0 A (ad_double a) (ad_double_bit_0 a) m0 m1). + Rewrite (ad_double_div_2 a). Elim (in_dom_some ? ? ? H4). Intros y H5. Rewrite H5. Reflexivity. + Intro H2. Rewrite <- H2 in H1. Simpl in H1. Elim (H0 ? H1). Intros a H3. + Split with (ad_double_plus_un a). Unfold in_dom. + Rewrite (MapGet_M2_bit_0_1 A (ad_double_plus_un a) (ad_double_plus_un_bit_0 a) m0 m1). + Rewrite (ad_double_plus_un_div_2 a). Elim (in_dom_some ? ? ? H3). Intros y H4. Rewrite H4. + Reflexivity. + Qed. + +End MapCard. + +Section MapCard2. + + Variable A, B : Set. + + Lemma MapSubset_card_eq_1 : (n:nat) (m:(Map A)) (m':(Map B)) + (MapSubset ? ? m m') -> (MapCard ? m)=n -> (MapCard ? m')=n -> + (MapSubset ? ? m' m). + Proof. + Induction n. Intros. Unfold MapSubset in_dom. Intro. Rewrite (MapCard_is_O ? m H0 a). + Rewrite (MapCard_is_O ? m' H1 a). Intro H2. Discriminate H2. + Intros. Elim (MapCard_is_Sn A m n0 H1). Intros a H3. Elim (in_dom_some ? ? ? H3). + Intros y H4. Elim (in_dom_some ? ? ? (H0 ? H3)). Intros y' H6. + Cut (eqmap ? (MapPut ? (MapRemove ? m a) a y) m). Intro. + Cut (eqmap ? (MapPut ? (MapRemove ? m' a) a y') m'). Intro. + Apply MapSubset_ext with m0:=(MapPut ? (MapRemove ? m' a) a y') + m2:=(MapPut ? (MapRemove ? m a) a y). + Assumption. + Assumption. + Apply MapSubset_Put_mono. Apply H. Apply MapSubset_Remove_mono. Assumption. + Rewrite <- (MapCard_Remove_2_conv ? m a y H4) in H1. Inversion_clear H1. Reflexivity. + Rewrite <- (MapCard_Remove_2_conv ? m' a y' H6) in H2. Inversion_clear H2. Reflexivity. + Unfold eqmap eqm. Intro. Rewrite (MapPut_semantics ? (MapRemove B m' a) a y' a0). + Elim (sumbool_of_bool (ad_eq a a0)). Intro H7. Rewrite H7. Rewrite <- (ad_eq_complete ? ? H7). + Apply sym_eq. Assumption. + Intro H7. Rewrite H7. Rewrite (MapRemove_semantics ? m' a a0). Rewrite H7. Reflexivity. + Unfold eqmap eqm. Intro. Rewrite (MapPut_semantics ? (MapRemove A m a) a y a0). + Elim (sumbool_of_bool (ad_eq a a0)). Intro H7. Rewrite H7. Rewrite <- (ad_eq_complete ? ? H7). + Apply sym_eq. Assumption. + Intro H7. Rewrite H7. Rewrite (MapRemove_semantics A m a a0). Rewrite H7. Reflexivity. + Qed. + + Lemma MapDomRestrTo_Card_ub_r : (m:(Map A)) (m':(Map B)) + (le (MapCard A (MapDomRestrTo A B m m')) (MapCard B m')). + Proof. + Induction m. Intro. Simpl. Apply le_O_n. + Intros a y m'. Simpl. Elim (option_sum B (MapGet B m' a)). Intro H. Elim H. Intros y0 H0. + Rewrite H0. Elim (MapCard_is_not_O B m' a y0 H0). Intros n H1. Rewrite H1. Simpl. + Apply le_n_S. Apply le_O_n. + Intro H. Rewrite H. Simpl. Apply le_O_n. + Induction m'. Simpl. Apply le_O_n. + + Intros a y. Unfold MapDomRestrTo. Case (MapGet A (M2 A m0 m1) a). Simpl. Apply le_O_n. + Intro. Simpl. Apply le_n. + Intros. Simpl. Rewrite (MapCard_makeM2 A (MapDomRestrTo A B m0 m2) (MapDomRestrTo A B m1 m3)). + Apply le_plus_plus. Apply H. + Apply H0. + Qed. + +End MapCard2. + +Section MapCard3. + + Variable A, B : Set. + + Lemma MapMerge_Card_lb_l : (m,m':(Map A)) + (ge (MapCard A (MapMerge A m m')) (MapCard A m)). + Proof. + Unfold ge. Intros. Apply (simpl_le_plus_l (MapCard A m')). + Rewrite (plus_sym (MapCard A m') (MapCard A m)). + Rewrite (plus_sym (MapCard A m') (MapCard A (MapMerge A m m'))). + Rewrite (MapMerge_Restr_Card A m m'). Apply le_reg_l. Apply MapDomRestrTo_Card_ub_r. + Qed. + + Lemma MapMerge_Card_lb_r : (m,m':(Map A)) + (ge (MapCard A (MapMerge A m m')) (MapCard A m')). + Proof. + Unfold ge. Intros. Apply (simpl_le_plus_l (MapCard A m)). Rewrite (MapMerge_Restr_Card A m m'). + Rewrite (plus_sym (MapCard A (MapMerge A m m')) (MapCard A (MapDomRestrTo A A m m'))). + Apply le_reg_r. Apply MapDomRestrTo_Card_ub_l. + Qed. + + Lemma MapDomRestrBy_Card_lb : (m:(Map A)) (m':(Map B)) + (ge (plus (MapCard B m') (MapCard A (MapDomRestrBy A B m m'))) (MapCard A m)). + Proof. + Unfold ge. Intros. Rewrite (MapSplit_Card A B m m'). Apply le_reg_r. + Apply MapDomRestrTo_Card_ub_r. + Qed. + + Lemma MapSubset_Card_le : (m:(Map A)) (m':(Map B)) + (MapSubset A B m m') -> (le (MapCard A m) (MapCard B m')). + Proof. + Intros. Apply le_trans with m:=(plus (MapCard B m') (MapCard A (MapDomRestrBy A B m m'))). + Exact (MapDomRestrBy_Card_lb m m'). + Rewrite (MapCard_ext ? ? ? (MapSubset_imp_2 ? ? ? ? H)). Simpl. Rewrite <- plus_n_O. + Apply le_n. + Qed. + + Lemma MapSubset_card_eq : (m:(Map A)) (m':(Map B)) + (MapSubset ? ? m m') -> (le (MapCard ? m') (MapCard ? m)) -> + (eqmap ? (MapDom ? m) (MapDom ? m')). + Proof. + Intros. Apply MapSubset_antisym. Assumption. + Cut (MapCard B m')=(MapCard A m). Intro. Apply (MapSubset_card_eq_1 A B (MapCard A m)). + Assumption. + Reflexivity. + Assumption. + Apply le_antisym. Assumption. + Apply MapSubset_Card_le. Assumption. + Qed. + +End MapCard3. |