diff options
Diffstat (limited to 'theories7/IntMap/Maplists.v')
| -rw-r--r-- | theories7/IntMap/Maplists.v | 399 |
1 files changed, 399 insertions, 0 deletions
diff --git a/theories7/IntMap/Maplists.v b/theories7/IntMap/Maplists.v new file mode 100644 index 00000000..f01ee3d8 --- /dev/null +++ b/theories7/IntMap/Maplists.v @@ -0,0 +1,399 @@ +(************************************************************************) +(* 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: Maplists.v,v 1.1.2.1 2004/07/16 19:31:28 herbelin Exp $ i*) + +Require Addr. +Require Addec. +Require Map. +Require Fset. +Require Mapaxioms. +Require Mapsubset. +Require Mapcard. +Require Mapcanon. +Require Mapc. +Require Bool. +Require Sumbool. +Require PolyList. +Require Arith. +Require Mapiter. +Require Mapfold. + +Section MapLists. + + Fixpoint ad_in_list [a:ad;l:(list ad)] : bool := + Cases l of + nil => false + | (cons a' l') => (orb (ad_eq a a') (ad_in_list a l')) + end. + + Fixpoint ad_list_stutters [l:(list ad)] : bool := + Cases l of + nil => false + | (cons a l') => (orb (ad_in_list a l') (ad_list_stutters l')) + end. + + Lemma ad_in_list_forms_circuit : (x:ad) (l:(list ad)) (ad_in_list x l)=true -> + {l1 : (list ad) & {l2 : (list ad) | l=(app l1 (cons x l2))}}. + Proof. + Induction l. Intro. Discriminate H. + Intros. Elim (sumbool_of_bool (ad_eq x a)). Intro H1. Simpl in H0. Split with (nil ad). + Split with l0. Rewrite (ad_eq_complete ? ? H1). Reflexivity. + Intro H2. Simpl in H0. Rewrite H2 in H0. Simpl in H0. Elim (H H0). Intros l'1 H3. + Split with (cons a l'1). Elim H3. Intros l2 H4. Split with l2. Rewrite H4. Reflexivity. + Qed. + + Lemma ad_list_stutters_has_circuit : (l:(list ad)) (ad_list_stutters l)=true -> + {x:ad & {l0 : (list ad) & {l1 : (list ad) & {l2 : (list ad) | + l=(app l0 (cons x (app l1 (cons x l2))))}}}}. + Proof. + Induction l. Intro. Discriminate H. + Intros. Simpl in H0. Elim (orb_true_elim ? ? H0). Intro H1. Split with a. + Split with (nil ad). Simpl. Elim (ad_in_list_forms_circuit a l0 H1). Intros l1 H2. + Split with l1. Elim H2. Intros l2 H3. Split with l2. Rewrite H3. Reflexivity. + Intro H1. Elim (H H1). Intros x H2. Split with x. Elim H2. Intros l1 H3. + Split with (cons a l1). Elim H3. Intros l2 H4. Split with l2. Elim H4. Intros l3 H5. + Split with l3. Rewrite H5. Reflexivity. + Qed. + + Fixpoint Elems [l:(list ad)] : FSet := + Cases l of + nil => (M0 unit) + | (cons a l') => (MapPut ? (Elems l') a tt) + end. + + Lemma Elems_canon : (l:(list ad)) (mapcanon ? (Elems l)). + Proof. + Induction l. Exact (M0_canon unit). + Intros. Simpl. Apply MapPut_canon. Assumption. + Qed. + + Lemma Elems_app : (l,l':(list ad)) (Elems (app l l'))=(FSetUnion (Elems l) (Elems l')). + Proof. + Induction l. Trivial. + Intros. Simpl. Rewrite (MapPut_as_Merge_c unit (Elems l0)). + Rewrite (MapPut_as_Merge_c unit (Elems (app l0 l'))). + Change (FSetUnion (Elems (app l0 l')) (M1 unit a tt)) + =(FSetUnion (FSetUnion (Elems l0) (M1 unit a tt)) (Elems l')). + Rewrite FSetUnion_comm_c. Rewrite (FSetUnion_comm_c (Elems l0) (M1 unit a tt)). + Rewrite FSetUnion_assoc_c. Rewrite (H l'). Reflexivity. + Apply M1_canon. + Apply Elems_canon. + Apply Elems_canon. + Apply Elems_canon. + Apply M1_canon. + Apply Elems_canon. + Apply M1_canon. + Apply Elems_canon. + Apply Elems_canon. + Qed. + + Lemma Elems_rev : (l:(list ad)) (Elems (rev l))=(Elems l). + Proof. + Induction l. Trivial. + Intros. Simpl. Rewrite Elems_app. Simpl. Rewrite (MapPut_as_Merge_c unit (Elems l0)). + Rewrite H. Reflexivity. + Apply Elems_canon. + Qed. + + Lemma ad_in_elems_in_list : (l:(list ad)) (a:ad) (in_FSet a (Elems l))=(ad_in_list a l). + Proof. + Induction l. Trivial. + Simpl. Unfold in_FSet. Intros. Rewrite (in_dom_put ? (Elems l0) a tt a0). + Rewrite (H a0). Reflexivity. + Qed. + + Lemma ad_list_not_stutters_card : (l:(list ad)) (ad_list_stutters l)=false -> + (length l)=(MapCard ? (Elems l)). + Proof. + Induction l. Trivial. + Simpl. Intros. Rewrite MapCard_Put_2_conv. Rewrite H. Reflexivity. + Elim (orb_false_elim ? ? H0). Trivial. + Elim (sumbool_of_bool (in_FSet a (Elems l0))). Rewrite ad_in_elems_in_list. + Intro H1. Rewrite H1 in H0. Discriminate H0. + Exact (in_dom_none unit (Elems l0) a). + Qed. + + Lemma ad_list_card : (l:(list ad)) (le (MapCard ? (Elems l)) (length l)). + Proof. + Induction l. Trivial. + Intros. Simpl. Apply le_trans with m:=(S (MapCard ? (Elems l0))). Apply MapCard_Put_ub. + Apply le_n_S. Assumption. + Qed. + + Lemma ad_list_stutters_card : (l:(list ad)) (ad_list_stutters l)=true -> + (lt (MapCard ? (Elems l)) (length l)). + Proof. + Induction l. Intro. Discriminate H. + Intros. Simpl. Simpl in H0. Elim (orb_true_elim ? ? H0). Intro H1. + Rewrite <- (ad_in_elems_in_list l0 a) in H1. Elim (in_dom_some ? ? ? H1). Intros y H2. + Rewrite (MapCard_Put_1_conv ? ? ? ? tt H2). Apply le_lt_trans with m:=(length l0). + Apply ad_list_card. + Apply lt_n_Sn. + Intro H1. Apply le_lt_trans with m:=(S (MapCard ? (Elems l0))). Apply MapCard_Put_ub. + Apply lt_n_S. Apply H. Assumption. + Qed. + + Lemma ad_list_not_stutters_card_conv : (l:(list ad)) (length l)=(MapCard ? (Elems l)) -> + (ad_list_stutters l)=false. + Proof. + Intros. Elim (sumbool_of_bool (ad_list_stutters l)). Intro H0. + Cut (lt (MapCard ? (Elems l)) (length l)). Intro. Rewrite H in H1. Elim (lt_n_n ? H1). + Exact (ad_list_stutters_card ? H0). + Trivial. + Qed. + + Lemma ad_list_stutters_card_conv : (l:(list ad)) (lt (MapCard ? (Elems l)) (length l)) -> + (ad_list_stutters l)=true. + Proof. + Intros. Elim (sumbool_of_bool (ad_list_stutters l)). Trivial. + Intro H0. Rewrite (ad_list_not_stutters_card ? H0) in H. Elim (lt_n_n ? H). + Qed. + + Lemma ad_in_list_l : (l,l':(list ad)) (a:ad) (ad_in_list a l)=true -> + (ad_in_list a (app l l'))=true. + Proof. + Induction l. Intros. Discriminate H. + Intros. Simpl. Simpl in H0. Elim (orb_true_elim ? ? H0). Intro H1. Rewrite H1. Reflexivity. + Intro H1. Rewrite (H l' a0 H1). Apply orb_b_true. + Qed. + + Lemma ad_list_stutters_app_l : (l,l':(list ad)) (ad_list_stutters l)=true -> + (ad_list_stutters (app l l'))=true. + Proof. + Induction l. Intros. Discriminate H. + Intros. Simpl. Simpl in H0. Elim (orb_true_elim ? ? H0). Intro H1. + Rewrite (ad_in_list_l l0 l' a H1). Reflexivity. + Intro H1. Rewrite (H l' H1). Apply orb_b_true. + Qed. + + Lemma ad_in_list_r : (l,l':(list ad)) (a:ad) (ad_in_list a l')=true -> + (ad_in_list a (app l l'))=true. + Proof. + Induction l. Trivial. + Intros. Simpl. Rewrite (H l' a0 H0). Apply orb_b_true. + Qed. + + Lemma ad_list_stutters_app_r : (l,l':(list ad)) (ad_list_stutters l')=true -> + (ad_list_stutters (app l l'))=true. + Proof. + Induction l. Trivial. + Intros. Simpl. Rewrite (H l' H0). Apply orb_b_true. + Qed. + + Lemma ad_list_stutters_app_conv_l : (l,l':(list ad)) (ad_list_stutters (app l l'))=false -> + (ad_list_stutters l)=false. + Proof. + Intros. Elim (sumbool_of_bool (ad_list_stutters l)). Intro H0. + Rewrite (ad_list_stutters_app_l l l' H0) in H. Discriminate H. + Trivial. + Qed. + + Lemma ad_list_stutters_app_conv_r : (l,l':(list ad)) (ad_list_stutters (app l l'))=false -> + (ad_list_stutters l')=false. + Proof. + Intros. Elim (sumbool_of_bool (ad_list_stutters l')). Intro H0. + Rewrite (ad_list_stutters_app_r l l' H0) in H. Discriminate H. + Trivial. + Qed. + + Lemma ad_in_list_app_1 : (l,l':(list ad)) (x:ad) (ad_in_list x (app l (cons x l')))=true. + Proof. + Induction l. Simpl. Intros. Rewrite (ad_eq_correct x). Reflexivity. + Intros. Simpl. Rewrite (H l' x). Apply orb_b_true. + Qed. + + Lemma ad_in_list_app : (l,l':(list ad)) (x:ad) + (ad_in_list x (app l l'))=(orb (ad_in_list x l) (ad_in_list x l')). + Proof. + Induction l. Trivial. + Intros. Simpl. Rewrite <- orb_assoc. Rewrite (H l' x). Reflexivity. + Qed. + + Lemma ad_in_list_rev : (l:(list ad)) (x:ad) + (ad_in_list x (rev l))=(ad_in_list x l). + Proof. + Induction l. Trivial. + Intros. Simpl. Rewrite ad_in_list_app. Rewrite (H x). Simpl. Rewrite orb_b_false. + Apply orb_sym. + Qed. + + Lemma ad_list_has_circuit_stutters : (l0,l1,l2:(list ad)) (x:ad) + (ad_list_stutters (app l0 (cons x (app l1 (cons x l2)))))=true. + Proof. + Induction l0. Simpl. Intros. Rewrite (ad_in_list_app_1 l1 l2 x). Reflexivity. + Intros. Simpl. Rewrite (H l1 l2 x). Apply orb_b_true. + Qed. + + Lemma ad_list_stutters_prev_l : (l,l':(list ad)) (x:ad) (ad_in_list x l)=true -> + (ad_list_stutters (app l (cons x l')))=true. + Proof. + Intros. Elim (ad_in_list_forms_circuit ? ? H). Intros l0 H0. Elim H0. Intros l1 H1. + Rewrite H1. Rewrite app_ass. Simpl. Apply ad_list_has_circuit_stutters. + Qed. + + Lemma ad_list_stutters_prev_conv_l : (l,l':(list ad)) (x:ad) + (ad_list_stutters (app l (cons x l')))=false -> (ad_in_list x l)=false. + Proof. + Intros. Elim (sumbool_of_bool (ad_in_list x l)). Intro H0. + Rewrite (ad_list_stutters_prev_l l l' x H0) in H. Discriminate H. + Trivial. + Qed. + + Lemma ad_list_stutters_prev_r : (l,l':(list ad)) (x:ad) (ad_in_list x l')=true -> + (ad_list_stutters (app l (cons x l')))=true. + Proof. + Intros. Elim (ad_in_list_forms_circuit ? ? H). Intros l0 H0. Elim H0. Intros l1 H1. + Rewrite H1. Apply ad_list_has_circuit_stutters. + Qed. + + Lemma ad_list_stutters_prev_conv_r : (l,l':(list ad)) (x:ad) + (ad_list_stutters (app l (cons x l')))=false -> (ad_in_list x l')=false. + Proof. + Intros. Elim (sumbool_of_bool (ad_in_list x l')). Intro H0. + Rewrite (ad_list_stutters_prev_r l l' x H0) in H. Discriminate H. + Trivial. + Qed. + + Lemma ad_list_Elems : (l,l':(list ad)) (MapCard ? (Elems l))=(MapCard ? (Elems l')) -> + (length l)=(length l') -> + (ad_list_stutters l)=(ad_list_stutters l'). + Proof. + Intros. Elim (sumbool_of_bool (ad_list_stutters l)). Intro H1. Rewrite H1. Apply sym_eq. + Apply ad_list_stutters_card_conv. Rewrite <- H. Rewrite <- H0. Apply ad_list_stutters_card. + Assumption. + Intro H1. Rewrite H1. Apply sym_eq. Apply ad_list_not_stutters_card_conv. Rewrite <- H. + Rewrite <- H0. Apply ad_list_not_stutters_card. Assumption. + Qed. + + Lemma ad_list_app_length : (l,l':(list ad)) (length (app l l'))=(plus (length l) (length l')). + Proof. + Induction l. Trivial. + Intros. Simpl. Rewrite (H l'). Reflexivity. + Qed. + + Lemma ad_list_stutters_permute : (l,l':(list ad)) + (ad_list_stutters (app l l'))=(ad_list_stutters (app l' l)). + Proof. + Intros. Apply ad_list_Elems. Rewrite Elems_app. Rewrite Elems_app. + Rewrite (FSetUnion_comm_c ? ? (Elems_canon l) (Elems_canon l')). Reflexivity. + Rewrite ad_list_app_length. Rewrite ad_list_app_length. Apply plus_sym. + Qed. + + Lemma ad_list_rev_length : (l:(list ad)) (length (rev l))=(length l). + Proof. + Induction l. Trivial. + Intros. Simpl. Rewrite ad_list_app_length. Simpl. Rewrite H. Rewrite <- plus_Snm_nSm. + Rewrite <- plus_n_O. Reflexivity. + Qed. + + Lemma ad_list_stutters_rev : (l:(list ad)) (ad_list_stutters (rev l))=(ad_list_stutters l). + Proof. + Intros. Apply ad_list_Elems. Rewrite Elems_rev. Reflexivity. + Apply ad_list_rev_length. + Qed. + + Lemma ad_list_app_rev : (l,l':(list ad)) (x:ad) + (app (rev l) (cons x l'))=(app (rev (cons x l)) l'). + Proof. + Induction l. Trivial. + Intros. Simpl. Rewrite (app_ass (rev l0) (cons a (nil ad)) (cons x l')). Simpl. + Rewrite (H (cons x l') a). Simpl. + Rewrite (app_ass (rev l0) (cons a (nil ad)) (cons x (nil ad))). Simpl. + Rewrite app_ass. Simpl. Rewrite app_ass. Reflexivity. + Qed. + + Section ListOfDomDef. + + Variable A : Set. + + Definition ad_list_of_dom := + (MapFold A (list ad) (nil ad) (!app ad) [a:ad][_:A] (cons a (nil ad))). + + Lemma ad_in_list_of_dom_in_dom : (m:(Map A)) (a:ad) + (ad_in_list a (ad_list_of_dom m))=(in_dom A a m). + Proof. + Unfold ad_list_of_dom. Intros. + Rewrite (MapFold_distr_l A (list ad) (nil ad) (!app ad) bool false orb + ad [a:ad][l:(list ad)](ad_in_list a l) [c:ad](refl_equal ? ?) + ad_in_list_app [a0:ad][_:A](cons a0 (nil ad)) m a). + Simpl. Rewrite (MapFold_orb A [a0:ad][_:A](orb (ad_eq a a0) false) m). + Elim (option_sum ? (MapSweep A [a0:ad][_:A](orb (ad_eq a a0) false) m)). Intro H. Elim H. + Intro r. Elim r. Intros a0 y H0. Rewrite H0. Unfold in_dom. + Elim (orb_prop ? ? (MapSweep_semantics_1 ? ? ? ? ? H0)). Intro H1. + Rewrite (ad_eq_complete ? ? H1). Rewrite (MapSweep_semantics_2 A ? ? ? ? H0). Reflexivity. + Intro H1. Discriminate H1. + Intro H. Rewrite H. Elim (sumbool_of_bool (in_dom A a m)). Intro H0. + Elim (in_dom_some A m a H0). Intros y H1. + Elim (orb_false_elim ? ? (MapSweep_semantics_3 ? ? ? H ? ? H1)). Intro H2. + Rewrite (ad_eq_correct a) in H2. Discriminate H2. + Exact (sym_eq ? ? ?). + Qed. + + Lemma Elems_of_list_of_dom : + (m:(Map A)) (eqmap unit (Elems (ad_list_of_dom m)) (MapDom A m)). + Proof. + Unfold eqmap eqm. Intros. Elim (sumbool_of_bool (in_FSet a (Elems (ad_list_of_dom m)))). + Intro H. Elim (in_dom_some ? ? ? H). Intro t. Elim t. Intro H0. + Rewrite (ad_in_elems_in_list (ad_list_of_dom m) a) in H. + Rewrite (ad_in_list_of_dom_in_dom m a) in H. Rewrite (MapDom_Dom A m a) in H. + Elim (in_dom_some ? ? ? H). Intro t'. Elim t'. Intro H1. Rewrite H1. Assumption. + Intro H. Rewrite (in_dom_none ? ? ? H). + Rewrite (ad_in_elems_in_list (ad_list_of_dom m) a) in H. + Rewrite (ad_in_list_of_dom_in_dom m a) in H. Rewrite (MapDom_Dom A m a) in H. + Rewrite (in_dom_none ? ? ? H). Reflexivity. + Qed. + + Lemma Elems_of_list_of_dom_c : (m:(Map A)) (mapcanon A m) -> + (Elems (ad_list_of_dom m))=(MapDom A m). + Proof. + Intros. Apply (mapcanon_unique unit). Apply Elems_canon. + Apply MapDom_canon. Assumption. + Apply Elems_of_list_of_dom. + Qed. + + Lemma ad_list_of_dom_card_1 : (m:(Map A)) (pf:ad->ad) + (length (MapFold1 A (list ad) (nil ad) (app 1!ad) [a:ad][_:A](cons a (nil ad)) pf m))= + (MapCard A m). + Proof. + Induction m; Try Trivial. Simpl. Intros. Rewrite ad_list_app_length. + Rewrite (H [a0:ad](pf (ad_double a0))). Rewrite (H0 [a0:ad](pf (ad_double_plus_un a0))). + Reflexivity. + Qed. + + Lemma ad_list_of_dom_card : (m:(Map A)) (length (ad_list_of_dom m))=(MapCard A m). + Proof. + Exact [m:(Map A)](ad_list_of_dom_card_1 m [a:ad]a). + Qed. + + Lemma ad_list_of_dom_not_stutters : + (m:(Map A)) (ad_list_stutters (ad_list_of_dom m))=false. + Proof. + Intro. Apply ad_list_not_stutters_card_conv. Rewrite ad_list_of_dom_card. Apply sym_eq. + Rewrite (MapCard_Dom A m). Apply MapCard_ext. Exact (Elems_of_list_of_dom m). + Qed. + + End ListOfDomDef. + + Lemma ad_list_of_dom_Dom_1 : (A:Set) + (m:(Map A)) (pf:ad->ad) + (MapFold1 A (list ad) (nil ad) (app 1!ad) + [a:ad][_:A](cons a (nil ad)) pf m)= + (MapFold1 unit (list ad) (nil ad) (app 1!ad) + [a:ad][_:unit](cons a (nil ad)) pf (MapDom A m)). + Proof. + Induction m; Try Trivial. Simpl. Intros. Rewrite (H [a0:ad](pf (ad_double a0))). + Rewrite (H0 [a0:ad](pf (ad_double_plus_un a0))). Reflexivity. + Qed. + + Lemma ad_list_of_dom_Dom : (A:Set) (m:(Map A)) + (ad_list_of_dom A m)=(ad_list_of_dom unit (MapDom A m)). + Proof. + Intros. Exact (ad_list_of_dom_Dom_1 A m [a0:ad]a0). + Qed. + +End MapLists. |