Library ATBR.DKA_StateSetSets
Properties about sets of sets, and maps over sets
Require Import Utils_WF.
Require Import DisjointSets.
Require Import DKA_Definitions.
Require Import MyFSets.
Require Import MyFSetProperties.
Require Import MyFMapProperties.
Require Import Common.
Module StateSetMap' := FMapAVL.Make StateSet. Module StateSetMap := FMapHide StateSetMap'.
Module StateSetMapProps := MyMapProps StateSetMap.
Notation statesetmap := StateSetMap.t.
Module StateSetSet' := FSetList.Make StateSet. Module StateSetSet := FSetHide StateSetSet'.
Module StateSetSetProps := MySetProps StateSetSet.
Notation statesetset := StateSetSet.t.
map a function f over a set of statesets
Definition statesetset_map f t :=
StateSetSet.fold (fun x acc => StateSetSet.add (f x) acc) t StateSetSet.empty.
StateSetSet.fold (fun x acc => StateSetSet.add (f x) acc) t StateSetSet.empty.
properties of the above function
Section sssm.
Variable t0: StateSetSet.t.
Variable f: stateset -> stateset.
Lemma statesetset_map_in p:
StateSetSet.In p (statesetset_map f t0) -> exists2 q, StateSetSet.In q t0 & StateSet.Equal (f q) p.
Hypothesis Hf: forall p q, StateSetSet.In p t0 -> StateSetSet.In q t0 ->
(StateSet.Equal (f p) (f q) <-> StateSet.Equal p q).
Lemma statesetset_map_cardinal:
StateSetSet.cardinal (statesetset_map f t0) = StateSetSet.cardinal t0.
End sssm.
Variable t0: StateSetSet.t.
Variable f: stateset -> stateset.
Lemma statesetset_map_in p:
StateSetSet.In p (statesetset_map f t0) -> exists2 q, StateSetSet.In q t0 & StateSet.Equal (f q) p.
Hypothesis Hf: forall p q, StateSetSet.In p t0 -> StateSetSet.In q t0 ->
(StateSet.Equal (f p) (f q) <-> StateSet.Equal p q).
Lemma statesetset_map_cardinal:
StateSetSet.cardinal (statesetset_map f t0) = StateSetSet.cardinal t0.
End sssm.
the only set whose all elements are below 0 is the empty set
technical lemmas for using FSet lemmas
Lemma compat_split s: compat_bool StateSet.Equal (fun p => StateSet.mem s p).
Lemma compat_negsplit s: compat_bool StateSet.Equal (fun p => negb (StateSet.mem s p)).
Local Hint Resolve compat_split compat_negsplit.
Ltac solve_p1 := intros ? ? H'; rewrite H'; reflexivity.
Lemma compat_negsplit s: compat_bool StateSet.Equal (fun p => negb (StateSet.mem s p)).
Local Hint Resolve compat_split compat_negsplit.
Ltac solve_p1 := intros ? ? H'; rewrite H'; reflexivity.
bound of the cardinal of a set of bounded sets
Lemma card_pset (s: nat) t: (forall p, StateSetSet.In p t -> setbelow p (state_of_nat s)) ->
(StateSetSet.cardinal t <= power s)%nat.
(StateSetSet.cardinal t <= power s)%nat.
domain of a statesetmap, to apply the above results to maps :
Section domain.
Variable T: Type.
Definition domain t := StateSetMap.fold (fun p (np: T) a => StateSetSet.add p a) t StateSetSet.empty.
Lemma domain_spec: forall x t, StateSetSet.In x (domain t) <-> StateSetMap.In x t.
Lemma cardinal_domain t: StateSetSet.cardinal (domain t) = StateSetMap.cardinal t.
End domain.
Variable T: Type.
Definition domain t := StateSetMap.fold (fun p (np: T) a => StateSetSet.add p a) t StateSetSet.empty.
Lemma domain_spec: forall x t, StateSetSet.In x (domain t) <-> StateSetMap.In x t.
Lemma cardinal_domain t: StateSetSet.cardinal (domain t) = StateSetMap.cardinal t.
End domain.
Results about the number of classes in a partition (for termination of the equivalence check)
Module DS := DisjointSets.PosDisjointSets.
Module DSUtils := DisjointSets.DSUtils Numbers.Positive DS.
Import DSUtils.Notations.
Definition add_classes t := fun i => StateSetSet.add (DS.class_of t (num_of_nat i)).
Fixpoint classes size t :=
match size with
| O => StateSetSet.empty
| Datatypes.S n => add_classes t n (classes n t)
end.
Definition measure size t := StateSetSet.cardinal (classes size t).
Lemma classes_compat: forall size `{DS.WF} {t'} `{DS.WF t'}, t [=T=] t' ->
StateSetSet.Equal (classes size t) (classes size t').
Lemma measure_compat: forall size `{DS.WF} {t'} `{DS.WF t'}, t [=T=] t' -> measure size t = measure size t'.
Section protect.
Lemma measure_union_idem: forall `{DS.WF} size x y, {{t}} x y ->
measure size (DS.union t x y) = measure size t.
Lemma in_classes: forall t size x,
StateSetSet.In x (classes size t) <-> exists2 y, y<size & StateSet.Equal x (DS.class_of t (state_of_nat y)).
Lemma in_classes_empty_below: forall size x,
StateSetSet.In x (classes size DS.empty) -> setbelow x (state_of_nat size).
Lemma add_classes_empty: forall x a,
StateSetSet.Equal (add_classes DS.empty x a) (StateSetSet.add (StateSet.singleton x) a).
Lemma measure_empty: forall size, measure size DS.empty = size.
Lemma classes_union_strict: forall `{DS.WF} size (x y: state),
x < size -> y < size ->
StateSetSet.Equal
(classes size (DS.union t x y))
(StateSetSet.add (StateSet.union (DS.class_of t x) (DS.class_of t y))
(StateSetSet.remove (DS.class_of t x)
(StateSetSet.remove (DS.class_of t y)
(classes size t)))).
Lemma add_cardinal: forall s s' x,
Datatypes.S (StateSetSet.cardinal s) < StateSetSet.cardinal s' ->
StateSetSet.cardinal (StateSetSet.add x s) < StateSetSet.cardinal s'.
Lemma rem_cardinal_lt: forall s x,
StateSetSet.In x s ->
StateSetSet.cardinal (StateSetSet.remove x s) < StateSetSet.cardinal s.
Lemma measure_union_strict: forall `{DS.WF} size t' (x y: state),
x < size -> y < size ->
DS.equiv t x y = (false,t') -> measure size (DS.union t x y) < measure size t.
End protect.