diff options
Diffstat (limited to 'theories/IntMap/Fset.v')
| -rw-r--r-- | theories/IntMap/Fset.v | 481 |
1 files changed, 257 insertions, 224 deletions
diff --git a/theories/IntMap/Fset.v b/theories/IntMap/Fset.v index 3c00c21e09..8a2ab00c35 100644 --- a/theories/IntMap/Fset.v +++ b/theories/IntMap/Fset.v @@ -9,330 +9,363 @@ (*s Sets operations on maps *) -Require Bool. -Require Sumbool. -Require ZArith. -Require Addr. -Require Adist. -Require Addec. -Require Map. +Require Import Bool. +Require Import Sumbool. +Require Import ZArith. +Require Import Addr. +Require Import Adist. +Require Import Addec. +Require Import Map. Section Dom. - Variable A, B : Set. - - Fixpoint MapDomRestrTo [m:(Map A)] : (Map B) -> (Map A) := - Cases m of - M0 => [_:(Map B)] (M0 A) - | (M1 a y) => [m':(Map B)] Cases (MapGet B m' a) of - NONE => (M0 A) - | _ => m - end - | (M2 m1 m2) => [m':(Map B)] Cases m' of - M0 => (M0 A) - | (M1 a' y') => Cases (MapGet A m a') of - NONE => (M0 A) - | (SOME y) => (M1 A a' y) - end - | (M2 m'1 m'2) => (makeM2 A (MapDomRestrTo m1 m'1) - (MapDomRestrTo m2 m'2)) - end + Variables A B : Set. + + Fixpoint MapDomRestrTo (m:Map A) : Map B -> Map A := + match m with + | M0 => fun _:Map B => M0 A + | M1 a y => + fun m':Map B => match MapGet B m' a with + | NONE => M0 A + | _ => m + end + | M2 m1 m2 => + fun m':Map B => + match m' with + | M0 => M0 A + | M1 a' y' => + match MapGet A m a' with + | NONE => M0 A + | SOME y => M1 A a' y + end + | M2 m'1 m'2 => + makeM2 A (MapDomRestrTo m1 m'1) (MapDomRestrTo m2 m'2) + end end. - Lemma MapDomRestrTo_semantics : (m:(Map A)) (m':(Map B)) - (eqm A (MapGet A (MapDomRestrTo m m')) - [a0:ad] Cases (MapGet B m' a0) of - NONE => (NONE A) - | _ => (MapGet A m a0) - end). - Proof. - Unfold eqm. Induction m. Simpl. Intros. Case (MapGet B m' a); Trivial. - Intros. Simpl. Elim (sumbool_of_bool (ad_eq a a1)). Intro H. Rewrite H. - Rewrite <- (ad_eq_complete ? ? H). Case (MapGet B m' a). Reflexivity. - Intro. Apply M1_semantics_1. - Intro H. Rewrite H. Case (MapGet B m' a). - Case (MapGet B m' a1); Reflexivity. - Case (MapGet B m' a1); Intros; Exact (M1_semantics_2 A a a1 a0 H). - Induction m'. Trivial. - Unfold MapDomRestrTo. Intros. Elim (sumbool_of_bool (ad_eq a a1)). - Intro H1. - Rewrite (ad_eq_complete ? ? H1). Rewrite (M1_semantics_1 B a1 a0). - Case (MapGet A (M2 A m0 m1) a1). Reflexivity. - Intro. Apply M1_semantics_1. - Intro H1. Rewrite (M1_semantics_2 B a a1 a0 H1). Case (MapGet A (M2 A m0 m1) a). Reflexivity. - Intro. Exact (M1_semantics_2 A a a1 a2 H1). - Intros. Change (MapGet A (makeM2 A (MapDomRestrTo m0 m2) (MapDomRestrTo m1 m3)) a) - =(Cases (MapGet B (M2 B m2 m3) a) of - NONE => (NONE A) - | (SOME _) => (MapGet A (M2 A m0 m1) a) + Lemma MapDomRestrTo_semantics : + forall (m:Map A) (m':Map B), + eqm A (MapGet A (MapDomRestrTo m m')) + (fun a0:ad => + match MapGet B m' a0 with + | NONE => NONE A + | _ => MapGet A m a0 end). - Rewrite (makeM2_M2 A (MapDomRestrTo m0 m2) (MapDomRestrTo m1 m3) a). - Rewrite MapGet_M2_bit_0_if. Rewrite (H0 m3 (ad_div_2 a)). Rewrite (H m2 (ad_div_2 a)). - Rewrite (MapGet_M2_bit_0_if B m2 m3 a). Rewrite (MapGet_M2_bit_0_if A m0 m1 a). - Case (ad_bit_0 a); Reflexivity. + Proof. + unfold eqm in |- *. simple induction m. simpl in |- *. intros. case (MapGet B m' a); trivial. + intros. simpl in |- *. elim (sumbool_of_bool (ad_eq a a1)). intro H. rewrite H. + rewrite <- (ad_eq_complete _ _ H). case (MapGet B m' a). reflexivity. + intro. apply M1_semantics_1. + intro H. rewrite H. case (MapGet B m' a). + case (MapGet B m' a1); reflexivity. + case (MapGet B m' a1); intros; exact (M1_semantics_2 A a a1 a0 H). + simple induction m'. trivial. + unfold MapDomRestrTo in |- *. intros. elim (sumbool_of_bool (ad_eq a a1)). + intro H1. + rewrite (ad_eq_complete _ _ H1). rewrite (M1_semantics_1 B a1 a0). + case (MapGet A (M2 A m0 m1) a1). reflexivity. + intro. apply M1_semantics_1. + intro H1. rewrite (M1_semantics_2 B a a1 a0 H1). case (MapGet A (M2 A m0 m1) a). reflexivity. + intro. exact (M1_semantics_2 A a a1 a2 H1). + intros. change + (MapGet A (makeM2 A (MapDomRestrTo m0 m2) (MapDomRestrTo m1 m3)) a = + match MapGet B (M2 B m2 m3) a with + | NONE => NONE A + | SOME _ => MapGet A (M2 A m0 m1) a + end) in |- *. + rewrite (makeM2_M2 A (MapDomRestrTo m0 m2) (MapDomRestrTo m1 m3) a). + rewrite MapGet_M2_bit_0_if. rewrite (H0 m3 (ad_div_2 a)). rewrite (H m2 (ad_div_2 a)). + rewrite (MapGet_M2_bit_0_if B m2 m3 a). rewrite (MapGet_M2_bit_0_if A m0 m1 a). + case (ad_bit_0 a); reflexivity. Qed. - Fixpoint MapDomRestrBy [m:(Map A)] : (Map B) -> (Map A) := - Cases m of - M0 => [_:(Map B)] (M0 A) - | (M1 a y) => [m':(Map B)] Cases (MapGet B m' a) of - NONE => m - | _ => (M0 A) - end - | (M2 m1 m2) => [m':(Map B)] Cases m' of - M0 => m - | (M1 a' y') => (MapRemove A m a') - | (M2 m'1 m'2) => (makeM2 A (MapDomRestrBy m1 m'1) - (MapDomRestrBy m2 m'2)) - end + Fixpoint MapDomRestrBy (m:Map A) : Map B -> Map A := + match m with + | M0 => fun _:Map B => M0 A + | M1 a y => + fun m':Map B => match MapGet B m' a with + | NONE => m + | _ => M0 A + end + | M2 m1 m2 => + fun m':Map B => + match m' with + | M0 => m + | M1 a' y' => MapRemove A m a' + | M2 m'1 m'2 => + makeM2 A (MapDomRestrBy m1 m'1) (MapDomRestrBy m2 m'2) + end end. - Lemma MapDomRestrBy_semantics : (m:(Map A)) (m':(Map B)) - (eqm A (MapGet A (MapDomRestrBy m m')) - [a0:ad] Cases (MapGet B m' a0) of - NONE => (MapGet A m a0) - | _ => (NONE A) - end). - Proof. - Unfold eqm. Induction m. Simpl. Intros. Case (MapGet B m' a); Trivial. - Intros. Simpl. Elim (sumbool_of_bool (ad_eq a a1)). Intro H. Rewrite H. - Rewrite (ad_eq_complete ? ? H). Case (MapGet B m' a1). Apply M1_semantics_1. - Trivial. - Intro H. Rewrite H. Case (MapGet B m' a). Rewrite (M1_semantics_2 A a a1 a0 H). - Case (MapGet B m' a1); Trivial. - Case (MapGet B m' a1); Trivial. - Induction m'. Trivial. - Unfold MapDomRestrBy. Intros. Rewrite (MapRemove_semantics A (M2 A m0 m1) a a1). - Elim (sumbool_of_bool (ad_eq a a1)). Intro H1. Rewrite H1. Rewrite (ad_eq_complete ? ? H1). - Rewrite (M1_semantics_1 B a1 a0). Reflexivity. - Intro H1. Rewrite H1. Rewrite (M1_semantics_2 B a a1 a0 H1). Reflexivity. - Intros. Change (MapGet A (makeM2 A (MapDomRestrBy m0 m2) (MapDomRestrBy m1 m3)) a) - =(Cases (MapGet B (M2 B m2 m3) a) of - NONE => (MapGet A (M2 A m0 m1) a) - | (SOME _) => (NONE A) + Lemma MapDomRestrBy_semantics : + forall (m:Map A) (m':Map B), + eqm A (MapGet A (MapDomRestrBy m m')) + (fun a0:ad => + match MapGet B m' a0 with + | NONE => MapGet A m a0 + | _ => NONE A end). - Rewrite (makeM2_M2 A (MapDomRestrBy m0 m2) (MapDomRestrBy m1 m3) a). - Rewrite MapGet_M2_bit_0_if. Rewrite (H0 m3 (ad_div_2 a)). Rewrite (H m2 (ad_div_2 a)). - Rewrite (MapGet_M2_bit_0_if B m2 m3 a). Rewrite (MapGet_M2_bit_0_if A m0 m1 a). - Case (ad_bit_0 a); Reflexivity. + Proof. + unfold eqm in |- *. simple induction m. simpl in |- *. intros. case (MapGet B m' a); trivial. + intros. simpl in |- *. elim (sumbool_of_bool (ad_eq a a1)). intro H. rewrite H. + rewrite (ad_eq_complete _ _ H). case (MapGet B m' a1). apply M1_semantics_1. + trivial. + intro H. rewrite H. case (MapGet B m' a). rewrite (M1_semantics_2 A a a1 a0 H). + case (MapGet B m' a1); trivial. + case (MapGet B m' a1); trivial. + simple induction m'. trivial. + unfold MapDomRestrBy in |- *. intros. rewrite (MapRemove_semantics A (M2 A m0 m1) a a1). + elim (sumbool_of_bool (ad_eq a a1)). intro H1. rewrite H1. rewrite (ad_eq_complete _ _ H1). + rewrite (M1_semantics_1 B a1 a0). reflexivity. + intro H1. rewrite H1. rewrite (M1_semantics_2 B a a1 a0 H1). reflexivity. + intros. change + (MapGet A (makeM2 A (MapDomRestrBy m0 m2) (MapDomRestrBy m1 m3)) a = + match MapGet B (M2 B m2 m3) a with + | NONE => MapGet A (M2 A m0 m1) a + | SOME _ => NONE A + end) in |- *. + rewrite (makeM2_M2 A (MapDomRestrBy m0 m2) (MapDomRestrBy m1 m3) a). + rewrite MapGet_M2_bit_0_if. rewrite (H0 m3 (ad_div_2 a)). rewrite (H m2 (ad_div_2 a)). + rewrite (MapGet_M2_bit_0_if B m2 m3 a). rewrite (MapGet_M2_bit_0_if A m0 m1 a). + case (ad_bit_0 a); reflexivity. Qed. - Definition in_dom := [a:ad; m:(Map A)] - Cases (MapGet A m a) of - NONE => false - | _ => true + Definition in_dom (a:ad) (m:Map A) := + match MapGet A m a with + | NONE => false + | _ => true end. - Lemma in_dom_M0 : (a:ad) (in_dom a (M0 A))=false. + Lemma in_dom_M0 : forall a:ad, in_dom a (M0 A) = false. Proof. - Trivial. + trivial. Qed. - Lemma in_dom_M1 : (a,a0:ad) (y:A) (in_dom a0 (M1 A a y))=(ad_eq a a0). + Lemma in_dom_M1 : forall (a a0:ad) (y:A), in_dom a0 (M1 A a y) = ad_eq a a0. Proof. - Unfold in_dom. Intros. Simpl. Case (ad_eq a a0); Reflexivity. + unfold in_dom in |- *. intros. simpl in |- *. case (ad_eq a a0); reflexivity. Qed. - Lemma in_dom_M1_1 : (a:ad) (y:A) (in_dom a (M1 A a y))=true. + Lemma in_dom_M1_1 : forall (a:ad) (y:A), in_dom a (M1 A a y) = true. Proof. - Intros. Rewrite in_dom_M1. Apply ad_eq_correct. + intros. rewrite in_dom_M1. apply ad_eq_correct. Qed. - Lemma in_dom_M1_2 : (a,a0:ad) (y:A) (in_dom a0 (M1 A a y))=true -> a=a0. + Lemma in_dom_M1_2 : + forall (a a0:ad) (y:A), in_dom a0 (M1 A a y) = true -> a = a0. Proof. - Intros. Apply (ad_eq_complete a a0). Rewrite (in_dom_M1 a a0 y) in H. Assumption. + intros. apply (ad_eq_complete a a0). rewrite (in_dom_M1 a a0 y) in H. assumption. Qed. - Lemma in_dom_some : (m:(Map A)) (a:ad) (in_dom a m)=true -> - {y:A | (MapGet A m a)=(SOME A y)}. + Lemma in_dom_some : + forall (m:Map A) (a:ad), + in_dom a m = true -> {y : A | MapGet A m a = SOME A y}. Proof. - Unfold in_dom. Intros. Elim (option_sum ? (MapGet A m a)). Trivial. - Intro H0. Rewrite H0 in H. Discriminate H. + unfold in_dom in |- *. intros. elim (option_sum _ (MapGet A m a)). trivial. + intro H0. rewrite H0 in H. discriminate H. Qed. - Lemma in_dom_none : (m:(Map A)) (a:ad) (in_dom a m)=false -> - (MapGet A m a)=(NONE A). + Lemma in_dom_none : + forall (m:Map A) (a:ad), in_dom a m = false -> MapGet A m a = NONE A. Proof. - Unfold in_dom. Intros. Elim (option_sum ? (MapGet A m a)). Intro H0. Elim H0. - Intros y H1. Rewrite H1 in H. Discriminate H. - Trivial. + unfold in_dom in |- *. intros. elim (option_sum _ (MapGet A m a)). intro H0. elim H0. + intros y H1. rewrite H1 in H. discriminate H. + trivial. Qed. - Lemma in_dom_put : (m:(Map A)) (a0:ad) (y0:A) (a:ad) - (in_dom a (MapPut A m a0 y0))=(orb (ad_eq a a0) (in_dom a m)). + Lemma in_dom_put : + forall (m:Map A) (a0:ad) (y0:A) (a:ad), + in_dom a (MapPut A m a0 y0) = orb (ad_eq a a0) (in_dom a m). Proof. - Unfold in_dom. Intros. Rewrite (MapPut_semantics A m a0 y0 a). - Elim (sumbool_of_bool (ad_eq a a0)). Intro H. Rewrite H. Rewrite (ad_eq_comm a a0) in H. - Rewrite H. Rewrite orb_true_b. Reflexivity. - Intro H. Rewrite H. Rewrite (ad_eq_comm a a0) in H. Rewrite H. Rewrite orb_false_b. - Reflexivity. + unfold in_dom in |- *. intros. rewrite (MapPut_semantics A m a0 y0 a). + elim (sumbool_of_bool (ad_eq a a0)). intro H. rewrite H. rewrite (ad_eq_comm a a0) in H. + rewrite H. rewrite orb_true_b. reflexivity. + intro H. rewrite H. rewrite (ad_eq_comm a a0) in H. rewrite H. rewrite orb_false_b. + reflexivity. Qed. - Lemma in_dom_put_behind : (m:(Map A)) (a0:ad) (y0:A) (a:ad) - (in_dom a (MapPut_behind A m a0 y0))=(orb (ad_eq a a0) (in_dom a m)). + Lemma in_dom_put_behind : + forall (m:Map A) (a0:ad) (y0:A) (a:ad), + in_dom a (MapPut_behind A m a0 y0) = orb (ad_eq a a0) (in_dom a m). Proof. - Unfold in_dom. Intros. Rewrite (MapPut_behind_semantics A m a0 y0 a). - Elim (sumbool_of_bool (ad_eq a a0)). Intro H. Rewrite H. Rewrite (ad_eq_comm a a0) in H. - Rewrite H. Case (MapGet A m a); Reflexivity. - Intro H. Rewrite H. Rewrite (ad_eq_comm a a0) in H. Rewrite H. Case (MapGet A m a); Trivial. + unfold in_dom in |- *. intros. rewrite (MapPut_behind_semantics A m a0 y0 a). + elim (sumbool_of_bool (ad_eq a a0)). intro H. rewrite H. rewrite (ad_eq_comm a a0) in H. + rewrite H. case (MapGet A m a); reflexivity. + intro H. rewrite H. rewrite (ad_eq_comm a a0) in H. rewrite H. case (MapGet A m a); trivial. Qed. - Lemma in_dom_remove : (m:(Map A)) (a0:ad) (a:ad) - (in_dom a (MapRemove A m a0))=(andb (negb (ad_eq a a0)) (in_dom a m)). + Lemma in_dom_remove : + forall (m:Map A) (a0 a:ad), + in_dom a (MapRemove A m a0) = andb (negb (ad_eq a a0)) (in_dom a m). Proof. - Unfold in_dom. Intros. Rewrite (MapRemove_semantics A m a0 a). - Elim (sumbool_of_bool (ad_eq a a0)). Intro H. Rewrite H. Rewrite (ad_eq_comm a a0) in H. - Rewrite H. Reflexivity. - Intro H. Rewrite H. Rewrite (ad_eq_comm a a0) in H. Rewrite H. - Case (MapGet A m a); Reflexivity. + unfold in_dom in |- *. intros. rewrite (MapRemove_semantics A m a0 a). + elim (sumbool_of_bool (ad_eq a a0)). intro H. rewrite H. rewrite (ad_eq_comm a a0) in H. + rewrite H. reflexivity. + intro H. rewrite H. rewrite (ad_eq_comm a a0) in H. rewrite H. + case (MapGet A m a); reflexivity. Qed. - Lemma in_dom_merge : (m,m':(Map A)) (a:ad) - (in_dom a (MapMerge A m m'))=(orb (in_dom a m) (in_dom a m')). + Lemma in_dom_merge : + forall (m m':Map A) (a:ad), + in_dom a (MapMerge A m m') = orb (in_dom a m) (in_dom a m'). Proof. - Unfold in_dom. Intros. Rewrite (MapMerge_semantics A m m' a). - Elim (option_sum A (MapGet A m' a)). Intro H. Elim H. Intros y H0. Rewrite H0. - Case (MapGet A m a); Reflexivity. - Intro H. Rewrite H. Rewrite orb_b_false. Reflexivity. + unfold in_dom in |- *. intros. rewrite (MapMerge_semantics A m m' a). + elim (option_sum A (MapGet A m' a)). intro H. elim H. intros y H0. rewrite H0. + case (MapGet A m a); reflexivity. + intro H. rewrite H. rewrite orb_b_false. reflexivity. Qed. - Lemma in_dom_delta : (m,m':(Map A)) (a:ad) - (in_dom a (MapDelta A m m'))=(xorb (in_dom a m) (in_dom a m')). + Lemma in_dom_delta : + forall (m m':Map A) (a:ad), + in_dom a (MapDelta A m m') = xorb (in_dom a m) (in_dom a m'). Proof. - Unfold in_dom. Intros. Rewrite (MapDelta_semantics A m m' a). - Elim (option_sum A (MapGet A m' a)). Intro H. Elim H. Intros y H0. Rewrite H0. - Case (MapGet A m a); Reflexivity. - Intro H. Rewrite H. Case (MapGet A m a); Reflexivity. + unfold in_dom in |- *. intros. rewrite (MapDelta_semantics A m m' a). + elim (option_sum A (MapGet A m' a)). intro H. elim H. intros y H0. rewrite H0. + case (MapGet A m a); reflexivity. + intro H. rewrite H. case (MapGet A m a); reflexivity. Qed. End Dom. Section InDom. - Variable A, B : Set. + Variables A B : Set. - Lemma in_dom_restrto : (m:(Map A)) (m':(Map B)) (a:ad) - (in_dom A a (MapDomRestrTo A B m m'))=(andb (in_dom A a m) (in_dom B a m')). + Lemma in_dom_restrto : + forall (m:Map A) (m':Map B) (a:ad), + in_dom A a (MapDomRestrTo A B m m') = + andb (in_dom A a m) (in_dom B a m'). Proof. - Unfold in_dom. Intros. Rewrite (MapDomRestrTo_semantics A B m m' a). - Elim (option_sum B (MapGet B m' a)). Intro H. Elim H. Intros y H0. Rewrite H0. - Rewrite andb_b_true. Reflexivity. - Intro H. Rewrite H. Rewrite andb_b_false. Reflexivity. + unfold in_dom in |- *. intros. rewrite (MapDomRestrTo_semantics A B m m' a). + elim (option_sum B (MapGet B m' a)). intro H. elim H. intros y H0. rewrite H0. + rewrite andb_b_true. reflexivity. + intro H. rewrite H. rewrite andb_b_false. reflexivity. Qed. - Lemma in_dom_restrby : (m:(Map A)) (m':(Map B)) (a:ad) - (in_dom A a (MapDomRestrBy A B m m'))=(andb (in_dom A a m) (negb (in_dom B a m'))). + Lemma in_dom_restrby : + forall (m:Map A) (m':Map B) (a:ad), + in_dom A a (MapDomRestrBy A B m m') = + andb (in_dom A a m) (negb (in_dom B a m')). Proof. - Unfold in_dom. Intros. Rewrite (MapDomRestrBy_semantics A B m m' a). - Elim (option_sum B (MapGet B m' a)). Intro H. Elim H. Intros y H0. Rewrite H0. - Unfold negb. Rewrite andb_b_false. Reflexivity. - Intro H. Rewrite H. Unfold negb. Rewrite andb_b_true. Reflexivity. + unfold in_dom in |- *. intros. rewrite (MapDomRestrBy_semantics A B m m' a). + elim (option_sum B (MapGet B m' a)). intro H. elim H. intros y H0. rewrite H0. + unfold negb in |- *. rewrite andb_b_false. reflexivity. + intro H. rewrite H. unfold negb in |- *. rewrite andb_b_true. reflexivity. Qed. End InDom. -Definition FSet := (Map unit). +Definition FSet := Map unit. Section FSetDefs. Variable A : Set. - Definition in_FSet : ad -> FSet -> bool := (in_dom unit). + Definition in_FSet : ad -> FSet -> bool := in_dom unit. - Fixpoint MapDom [m:(Map A)] : FSet := - Cases m of - M0 => (M0 unit) - | (M1 a _) => (M1 unit a tt) - | (M2 m m') => (M2 unit (MapDom m) (MapDom m')) + Fixpoint MapDom (m:Map A) : FSet := + match m with + | M0 => M0 unit + | M1 a _ => M1 unit a tt + | M2 m m' => M2 unit (MapDom m) (MapDom m') end. - Lemma MapDom_semantics_1 : (m:(Map A)) (a:ad) - (y:A) (MapGet A m a)=(SOME A y) -> (in_FSet a (MapDom m))=true. + Lemma MapDom_semantics_1 : + forall (m:Map A) (a:ad) (y:A), + MapGet A m a = SOME A y -> in_FSet a (MapDom m) = true. Proof. - Induction m. Intros. Discriminate H. - Unfold MapDom. Unfold in_FSet. Unfold in_dom. Unfold MapGet. Intros a y a0 y0. - Case (ad_eq a a0). Trivial. - Intro. Discriminate H. - Intros m0 H m1 H0 a y. Rewrite (MapGet_M2_bit_0_if A m0 m1 a). Simpl. Unfold in_FSet. - Unfold in_dom. Rewrite (MapGet_M2_bit_0_if unit (MapDom m0) (MapDom m1) a). - Case (ad_bit_0 a). Unfold in_FSet in_dom in H0. Intro. Apply H0 with y:=y. Assumption. - Unfold in_FSet in_dom in H. Intro. Apply H with y:=y. Assumption. + simple induction m. intros. discriminate H. + unfold MapDom in |- *. unfold in_FSet in |- *. unfold in_dom in |- *. unfold MapGet in |- *. intros a y a0 y0. + case (ad_eq a a0). trivial. + intro. discriminate H. + intros m0 H m1 H0 a y. rewrite (MapGet_M2_bit_0_if A m0 m1 a). simpl in |- *. unfold in_FSet in |- *. + unfold in_dom in |- *. rewrite (MapGet_M2_bit_0_if unit (MapDom m0) (MapDom m1) a). + case (ad_bit_0 a). unfold in_FSet, in_dom in H0. intro. apply H0 with (y := y). assumption. + unfold in_FSet, in_dom in H. intro. apply H with (y := y). assumption. Qed. - Lemma MapDom_semantics_2 : (m:(Map A)) (a:ad) - (in_FSet a (MapDom m))=true -> {y:A | (MapGet A m a)=(SOME A y)}. + Lemma MapDom_semantics_2 : + forall (m:Map A) (a:ad), + in_FSet a (MapDom m) = true -> {y : A | MapGet A m a = SOME A y}. Proof. - Induction m. Intros. Discriminate H. - Unfold MapDom. Unfold in_FSet. Unfold in_dom. Unfold MapGet. Intros a y a0. Case (ad_eq a a0). - Intro. Split with y. Reflexivity. - Intro. Discriminate H. - Intros m0 H m1 H0 a. Rewrite (MapGet_M2_bit_0_if A m0 m1 a). Simpl. Unfold in_FSet. - Unfold in_dom. Rewrite (MapGet_M2_bit_0_if unit (MapDom m0) (MapDom m1) a). - Case (ad_bit_0 a). Unfold in_FSet in_dom in H0. Intro. Apply H0. Assumption. - Unfold in_FSet in_dom in H. Intro. Apply H. Assumption. + simple induction m. intros. discriminate H. + unfold MapDom in |- *. unfold in_FSet in |- *. unfold in_dom in |- *. unfold MapGet in |- *. intros a y a0. case (ad_eq a a0). + intro. split with y. reflexivity. + intro. discriminate H. + intros m0 H m1 H0 a. rewrite (MapGet_M2_bit_0_if A m0 m1 a). simpl in |- *. unfold in_FSet in |- *. + unfold in_dom in |- *. rewrite (MapGet_M2_bit_0_if unit (MapDom m0) (MapDom m1) a). + case (ad_bit_0 a). unfold in_FSet, in_dom in H0. intro. apply H0. assumption. + unfold in_FSet, in_dom in H. intro. apply H. assumption. Qed. - Lemma MapDom_semantics_3 : (m:(Map A)) (a:ad) - (MapGet A m a)=(NONE A) -> (in_FSet a (MapDom m))=false. + Lemma MapDom_semantics_3 : + forall (m:Map A) (a:ad), + MapGet A m a = NONE A -> in_FSet a (MapDom m) = false. Proof. - Intros. Elim (sumbool_of_bool (in_FSet a (MapDom m))). Intro H0. - Elim (MapDom_semantics_2 m a H0). Intros y H1. Rewrite H in H1. Discriminate H1. - Trivial. + intros. elim (sumbool_of_bool (in_FSet a (MapDom m))). intro H0. + elim (MapDom_semantics_2 m a H0). intros y H1. rewrite H in H1. discriminate H1. + trivial. Qed. - Lemma MapDom_semantics_4 : (m:(Map A)) (a:ad) - (in_FSet a (MapDom m))=false -> (MapGet A m a)=(NONE A). + Lemma MapDom_semantics_4 : + forall (m:Map A) (a:ad), + in_FSet a (MapDom m) = false -> MapGet A m a = NONE A. Proof. - Intros. Elim (option_sum A (MapGet A m a)). Intro H0. Elim H0. Intros y H1. - Rewrite (MapDom_semantics_1 m a y H1) in H. Discriminate H. - Trivial. + intros. elim (option_sum A (MapGet A m a)). intro H0. elim H0. intros y H1. + rewrite (MapDom_semantics_1 m a y H1) in H. discriminate H. + trivial. Qed. - Lemma MapDom_Dom : (m:(Map A)) (a:ad) (in_dom A a m)=(in_FSet a (MapDom m)). + Lemma MapDom_Dom : + forall (m:Map A) (a:ad), in_dom A a m = in_FSet a (MapDom m). Proof. - Intros. Elim (sumbool_of_bool (in_FSet a (MapDom m))). Intro H. - Elim (MapDom_semantics_2 m a H). Intros y H0. Rewrite H. Unfold in_dom. Rewrite H0. - Reflexivity. - Intro H. Rewrite H. Unfold in_dom. Rewrite (MapDom_semantics_4 m a H). Reflexivity. + intros. elim (sumbool_of_bool (in_FSet a (MapDom m))). intro H. + elim (MapDom_semantics_2 m a H). intros y H0. rewrite H. unfold in_dom in |- *. rewrite H0. + reflexivity. + intro H. rewrite H. unfold in_dom in |- *. rewrite (MapDom_semantics_4 m a H). reflexivity. Qed. - Definition FSetUnion : FSet -> FSet -> FSet := [s,s':FSet] (MapMerge unit s s'). + Definition FSetUnion (s s':FSet) : FSet := MapMerge unit s s'. - Lemma in_FSet_union : (s,s':FSet) (a:ad) - (in_FSet a (FSetUnion s s'))=(orb (in_FSet a s) (in_FSet a s')). + Lemma in_FSet_union : + forall (s s':FSet) (a:ad), + in_FSet a (FSetUnion s s') = orb (in_FSet a s) (in_FSet a s'). Proof. - Exact (in_dom_merge unit). + exact (in_dom_merge unit). Qed. - Definition FSetInter : FSet -> FSet -> FSet := [s,s':FSet] (MapDomRestrTo unit unit s s'). + Definition FSetInter (s s':FSet) : FSet := MapDomRestrTo unit unit s s'. - Lemma in_FSet_inter : (s,s':FSet) (a:ad) - (in_FSet a (FSetInter s s'))=(andb (in_FSet a s) (in_FSet a s')). + Lemma in_FSet_inter : + forall (s s':FSet) (a:ad), + in_FSet a (FSetInter s s') = andb (in_FSet a s) (in_FSet a s'). Proof. - Exact (in_dom_restrto unit unit). + exact (in_dom_restrto unit unit). Qed. - Definition FSetDiff : FSet -> FSet -> FSet := [s,s':FSet] (MapDomRestrBy unit unit s s'). + Definition FSetDiff (s s':FSet) : FSet := MapDomRestrBy unit unit s s'. - Lemma in_FSet_diff : (s,s':FSet) (a:ad) - (in_FSet a (FSetDiff s s'))=(andb (in_FSet a s) (negb (in_FSet a s'))). + Lemma in_FSet_diff : + forall (s s':FSet) (a:ad), + in_FSet a (FSetDiff s s') = andb (in_FSet a s) (negb (in_FSet a s')). Proof. - Exact (in_dom_restrby unit unit). + exact (in_dom_restrby unit unit). Qed. - Definition FSetDelta : FSet -> FSet -> FSet := [s,s':FSet] (MapDelta unit s s'). + Definition FSetDelta (s s':FSet) : FSet := MapDelta unit s s'. - Lemma in_FSet_delta : (s,s':FSet) (a:ad) - (in_FSet a (FSetDelta s s'))=(xorb (in_FSet a s) (in_FSet a s')). + Lemma in_FSet_delta : + forall (s s':FSet) (a:ad), + in_FSet a (FSetDelta s s') = xorb (in_FSet a s) (in_FSet a s'). Proof. - Exact (in_dom_delta unit). + exact (in_dom_delta unit). Qed. End FSetDefs. -Lemma FSet_Dom : (s:FSet) (MapDom unit s)=s. +Lemma FSet_Dom : forall s:FSet, MapDom unit s = s. Proof. - Induction s. Trivial. - Simpl. Intros a t. Elim t. Reflexivity. - Intros. Simpl. Rewrite H. Rewrite H0. Reflexivity. -Qed. + simple induction s. trivial. + simpl in |- *. intros a t. elim t. reflexivity. + intros. simpl in |- *. rewrite H. rewrite H0. reflexivity. +Qed.
\ No newline at end of file |