diff options
Diffstat (limited to 'theories/IntMap/Maplists.v')
| -rw-r--r-- | theories/IntMap/Maplists.v | 562 |
1 files changed, 300 insertions, 262 deletions
diff --git a/theories/IntMap/Maplists.v b/theories/IntMap/Maplists.v index 6e5e40814b..bcb87179c4 100644 --- a/theories/IntMap/Maplists.v +++ b/theories/IntMap/Maplists.v @@ -7,304 +7,334 @@ (***********************************************************************) (*i $Id$ 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. +Require Import Addr. +Require Import Addec. +Require Import Map. +Require Import Fset. +Require Import Mapaxioms. +Require Import Mapsubset. +Require Import Mapcard. +Require Import Mapcanon. +Require Import Mapc. +Require Import Bool. +Require Import Sumbool. +Require Import List. +Require Import Arith. +Require Import Mapiter. +Require Import 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')) + Fixpoint ad_in_list (a:ad) (l:list ad) {struct l} : bool := + match l with + | nil => false + | 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')) + Fixpoint ad_list_stutters (l:list ad) : bool := + match l with + | nil => false + | 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) + Lemma ad_in_list_forms_circuit : + forall (x:ad) (l:list ad), + ad_in_list x l = true -> + {l1 : list ad & {l2 : list ad | l = l1 ++ x :: l2}}. + Proof. + simple induction l. intro. discriminate H. + intros. elim (sumbool_of_bool (ad_eq x a)). intro H1. simpl in H0. split with (nil (A:=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 (a :: l'1). elim H3. intros l2 H4. split with l2. rewrite H4. reflexivity. + Qed. + + Lemma ad_list_stutters_has_circuit : + forall l:list ad, + ad_list_stutters l = true -> + {x : ad & + {l0 : list ad & + {l1 : list ad & {l2 : list ad | l = l0 ++ x :: l1 ++ x :: l2}}}}. + Proof. + simple induction l. intro. discriminate H. + intros. simpl in H0. elim (orb_true_elim _ _ H0). intro H1. split with a. + split with (nil (A:=ad)). simpl in |- *. 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 (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 := + match l with + | nil => M0 unit + | a :: l' => MapPut _ (Elems l') a tt end. - Lemma Elems_canon : (l:(list ad)) (mapcanon ? (Elems l)). + Lemma Elems_canon : forall l:list ad, mapcanon _ (Elems l). Proof. - Induction l. Exact (M0_canon unit). - Intros. Simpl. Apply MapPut_canon. Assumption. + simple induction l. exact (M0_canon unit). + intros. simpl in |- *. apply MapPut_canon. assumption. Qed. - Lemma Elems_app : (l,l':(list ad)) (Elems (app l l'))=(FSetUnion (Elems l) (Elems l')). + Lemma Elems_app : + forall l l':list ad, Elems (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. + simple induction l. trivial. + intros. simpl in |- *. rewrite (MapPut_as_Merge_c unit (Elems l0)). + rewrite (MapPut_as_Merge_c unit (Elems (l0 ++ l'))). + change + (FSetUnion (Elems (l0 ++ l')) (M1 unit a tt) = + FSetUnion (FSetUnion (Elems l0) (M1 unit a tt)) (Elems l')) + in |- *. + 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). + Lemma Elems_rev : forall 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. + simple induction l. trivial. + intros. simpl in |- *. rewrite Elems_app. simpl in |- *. 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). + Lemma ad_in_elems_in_list : + forall (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. + simple induction l. trivial. + simpl in |- *. unfold in_FSet in |- *. 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)). + Lemma ad_list_not_stutters_card : + forall 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). + simple induction l. trivial. + simpl in |- *. 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)). + Lemma ad_list_card : forall l:list ad, 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. + simple induction l. trivial. + intros. simpl in |- *. 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)). + Lemma ad_list_stutters_card : + forall l:list ad, + ad_list_stutters l = true -> 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. + simple induction l. intro. discriminate H. + intros. simpl in |- *. 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. + Lemma ad_list_not_stutters_card_conv : + forall 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. + intros. elim (sumbool_of_bool (ad_list_stutters l)). intro H0. + cut (MapCard _ (Elems l) < length l). intro. rewrite H in H1. elim (lt_irrefl _ 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. + Lemma ad_list_stutters_card_conv : + forall l:list ad, + 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). + intros. elim (sumbool_of_bool (ad_list_stutters l)). trivial. + intro H0. rewrite (ad_list_not_stutters_card _ H0) in H. elim (lt_irrefl _ 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. + Lemma ad_in_list_l : + forall (l l':list ad) (a:ad), + ad_in_list a l = true -> ad_in_list a (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. + simple induction l. intros. discriminate H. + intros. simpl in |- *. 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. + Lemma ad_list_stutters_app_l : + forall l l':list ad, + ad_list_stutters l = true -> ad_list_stutters (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. + simple induction l. intros. discriminate H. + intros. simpl in |- *. 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. + Lemma ad_in_list_r : + forall (l l':list ad) (a:ad), + ad_in_list a l' = true -> ad_in_list a (l ++ l') = true. Proof. - Induction l. Trivial. - Intros. Simpl. Rewrite (H l' a0 H0). Apply orb_b_true. + simple induction l. trivial. + intros. simpl in |- *. 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. + Lemma ad_list_stutters_app_r : + forall l l':list ad, + ad_list_stutters l' = true -> ad_list_stutters (l ++ l') = true. Proof. - Induction l. Trivial. - Intros. Simpl. Rewrite (H l' H0). Apply orb_b_true. + simple induction l. trivial. + intros. simpl in |- *. 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. + Lemma ad_list_stutters_app_conv_l : + forall l l':list ad, + ad_list_stutters (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. + 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. + Lemma ad_list_stutters_app_conv_r : + forall l l':list ad, + ad_list_stutters (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. + 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. + Lemma ad_in_list_app_1 : + forall (l l':list ad) (x:ad), ad_in_list x (l ++ x :: l') = true. Proof. - Induction l. Simpl. Intros. Rewrite (ad_eq_correct x). Reflexivity. - Intros. Simpl. Rewrite (H l' x). Apply orb_b_true. + simple induction l. simpl in |- *. intros. rewrite (ad_eq_correct x). reflexivity. + intros. simpl in |- *. 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')). + Lemma ad_in_list_app : + forall (l l':list ad) (x:ad), + ad_in_list x (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. + simple induction l. trivial. + intros. simpl in |- *. 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). + Lemma ad_in_list_rev : + forall (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. + simple induction l. trivial. + intros. simpl in |- *. rewrite ad_in_list_app. rewrite (H x). simpl in |- *. rewrite orb_b_false. + apply orb_comm. 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. + Lemma ad_list_has_circuit_stutters : + forall (l0 l1 l2:list ad) (x:ad), + ad_list_stutters (l0 ++ x :: l1 ++ 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. + simple induction l0. simpl in |- *. intros. rewrite (ad_in_list_app_1 l1 l2 x). reflexivity. + intros. simpl in |- *. 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. + Lemma ad_list_stutters_prev_l : + forall (l l':list ad) (x:ad), + ad_in_list x l = true -> ad_list_stutters (l ++ 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. + intros. elim (ad_in_list_forms_circuit _ _ H). intros l0 H0. elim H0. intros l1 H1. + rewrite H1. rewrite app_ass. simpl in |- *. 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. + Lemma ad_list_stutters_prev_conv_l : + forall (l l':list ad) (x:ad), + ad_list_stutters (l ++ 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. + 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. + Lemma ad_list_stutters_prev_r : + forall (l l':list ad) (x:ad), + ad_in_list x l' = true -> ad_list_stutters (l ++ 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. + 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. + Lemma ad_list_stutters_prev_conv_r : + forall (l l':list ad) (x:ad), + ad_list_stutters (l ++ 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. + 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'). + Lemma ad_list_Elems : + forall 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. + 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')). + Lemma ad_list_app_length : + forall l l':list ad, length (l ++ l') = length l + length l'. Proof. - Induction l. Trivial. - Intros. Simpl. Rewrite (H l'). Reflexivity. + simple induction l. trivial. + intros. simpl in |- *. 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)). + Lemma ad_list_stutters_permute : + forall l l':list ad, + ad_list_stutters (l ++ l') = ad_list_stutters (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. + 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_comm. Qed. - Lemma ad_list_rev_length : (l:(list ad)) (length (rev l))=(length l). + Lemma ad_list_rev_length : forall 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. + simple induction l. trivial. + intros. simpl in |- *. rewrite ad_list_app_length. simpl in |- *. 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). + Lemma ad_list_stutters_rev : + forall 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. + 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'). + Lemma ad_list_app_rev : + forall (l l':list ad) (x:ad), rev l ++ x :: l' = rev (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. + simple induction l. trivial. + intros. simpl in |- *. rewrite (app_ass (rev l0) (a :: nil) (x :: l')). simpl in |- *. + rewrite (H (x :: l') a). simpl in |- *. + rewrite (app_ass (rev l0) (a :: nil) (x :: nil)). simpl in |- *. + rewrite app_ass. simpl in |- *. rewrite app_ass. reflexivity. Qed. Section ListOfDomDef. @@ -312,88 +342,96 @@ Section MapLists. Variable A : Set. Definition ad_list_of_dom := - (MapFold A (list ad) (nil ad) (!app ad) [a:ad][_:A] (cons a (nil ad))). + MapFold A (list ad) nil (app (A:=ad)) (fun (a:ad) (_:A) => a :: nil). - 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). + Lemma ad_in_list_of_dom_in_dom : + forall (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 ? ? ?). + unfold ad_list_of_dom in |- *. intros. + rewrite + (MapFold_distr_l A (list ad) nil (app (A:=ad)) bool false orb ad + (fun (a:ad) (l:list ad) => ad_in_list a l) ( + fun c:ad => refl_equal _) ad_in_list_app + (fun (a0:ad) (_:A) => a0 :: nil) m a). + simpl in |- *. rewrite (MapFold_orb A (fun (a0:ad) (_:A) => orb (ad_eq a a0) false) m). + elim + (option_sum _ + (MapSweep A (fun (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 in |- *. + 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 (y:=_)). Qed. - Lemma Elems_of_list_of_dom : - (m:(Map A)) (eqmap unit (Elems (ad_list_of_dom m)) (MapDom A m)). + Lemma Elems_of_list_of_dom : + forall 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. + unfold eqmap, eqm in |- *. 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). + Lemma Elems_of_list_of_dom_c : + forall 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. + 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). + Lemma ad_list_of_dom_card_1 : + forall (m:Map A) (pf:ad -> ad), + length + (MapFold1 A (list ad) nil (app (A:=ad)) (fun (a:ad) (_:A) => a :: nil) + 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. + simple induction m; try trivial. simpl in |- *. intros. rewrite ad_list_app_length. + rewrite (H (fun a0:ad => pf (ad_double a0))). rewrite (H0 (fun 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). + Lemma ad_list_of_dom_card : + forall 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). + exact (fun m:Map A => ad_list_of_dom_card_1 m (fun a:ad => a)). Qed. - Lemma ad_list_of_dom_not_stutters : - (m:(Map A)) (ad_list_stutters (ad_list_of_dom m))=false. + Lemma ad_list_of_dom_not_stutters : + forall 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). + 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)). + Lemma ad_list_of_dom_Dom_1 : + forall (A:Set) (m:Map A) (pf:ad -> ad), + MapFold1 A (list ad) nil (app (A:=ad)) (fun (a:ad) (_:A) => a :: nil) pf + m = + MapFold1 unit (list ad) nil (app (A:=ad)) + (fun (a:ad) (_:unit) => a :: nil) 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. + simple induction m; try trivial. simpl in |- *. intros. rewrite (H (fun a0:ad => pf (ad_double a0))). + rewrite (H0 (fun 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)). + Lemma ad_list_of_dom_Dom : + forall (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). + intros. exact (ad_list_of_dom_Dom_1 A m (fun a0:ad => a0)). Qed. -End MapLists. +End MapLists.
\ No newline at end of file |