Library FiniteSetLattice
Require Export ArrayLattice.
Require Export BoolLattice.
Section set.
Variable A:Set.
Variable LA : Lattice A.
Variable max:nat.
Definition FiniteSet := funcTree' bool max.
Definition LatticeFiniteSet : Lattice FiniteSet :=
ArrayLattice LatticeBool max.
Definition in_set (p:posInf max) (s:FiniteSet) : bool :=
applyArray LatticeBool s p.
Definition singleton (p:posInf max) : FiniteSet :=
substArray LatticeBool (Some (Fbottom _ _)) p true.
Lemma in_set_singleton' : forall p1 p2,
in_set p1 (singleton p2) = true -> (proj1_sig p1)=(proj1_sig p2).
unfold singleton, in_set.
intros p1 p2.
case (positive_dec (proj1_sig p1) (proj1_sig p2)); intros.
auto.
generalize H; clear H.
simpl.
unfold applyFunc, substFunc, apply_functree; simpl.
rewrite apply_subst_leaf2; intuition.
discriminate H.
Qed.
Lemma in_set_monotone : forall p s1 s2,
order LatticeFiniteSet s1 s2 ->
in_set p s1 = true -> in_set p s2 = true.
unfold in_set; intros p s1 s2 H H1.
generalize (applyArray_monotone _ _ _ _ _ H p).
rewrite H1.
case (applyArray LatticeBool s2 p); intros.
auto.
inversion_clear H0.
Qed.
Lemma height_inf_modify_set :
forall (a:A) (s:tree bool) (t:tree A) (n:nat) (v:A->A),
(height_inf A t n) -> (height_inf bool s n) ->
(height_inf A (modify_set_tree A a t s v) n).
induction s; simpl; intros.
destruct t; auto.
destruct t; auto.
inversion_clear H0.
destruct a0; constructor; auto.
apply IHs1; auto.
constructor.
apply IHs2; auto.
constructor.
apply IHs1; auto.
constructor.
apply IHs2; auto.
constructor.
inversion_clear H in H0.
inversion_clear H0.
destruct a0; try constructor; auto.
Qed.
Definition modify_set :
(funcTree' A max)->FiniteSet->(A->A)->(funcTree' A max).
intros f' s' v.
refine (match f' with
None => None
| Some f => match s' with
None => None | Some s => Some (funcTree_constr _ _
(modify_set_tree A (bottom LA) (tr _ _ f) (tr _ _ s) v) _)
end
end).
destruct f; destruct s; simpl.
apply height_inf_modify_set; auto.
Defined.
Lemma apply_modify_set1 :
forall s t f p,
in_set p s = true ->
order LA (f (applyArray LA t p)) (applyArray LA (modify_set t s f) p).
destruct t.
destruct s; intros.
destruct f; destruct f0; simpl in H|-*.
unfold applyFunc, apply_functree; simpl.
rewrite apply_modify_set_tree1; auto.
simpl; auto.
intros; simpl; auto.
Qed.
Lemma apply_modify_set2 :
forall s t f p,
in_set p s = false ->
(applyArray LA (modify_set t s f) p) = (applyArray LA t p) .
destruct t.
destruct s; intros.
destruct f; destruct f0; simpl in H|-*.
unfold applyFunc, apply_functree; simpl.
rewrite apply_modify_set_tree; auto.
simpl in H; inversion H.
intros; simpl; auto.
Qed.
Definition apply_set :
(funcTree' A max) -> FiniteSet -> A :=
fun f' s' =>
match f' with
None => (top LA)
| Some f => match s' with
None => (top LA)
| Some s =>
apply_set_tree A (bottom LA) (join LA) (tr _ _ f) (tr _ _ s)
end
end.
Lemma apply_set_in : forall t s p,
in_set p s = true ->
order LA (applyArray LA t p) (apply_set t s).
intros.
destruct t; destruct s; simpl.
generalize (apply_set_tree1 A (bottom LA) (join LA) (order LA)
(join_bound1 LA) (join_bound2 LA) (bottom_is_a_bottom LA)
(order_trans LA)); intros H1.
unfold applyFunc,apply_functree.
apply H1.
exact H.
auto.
auto.
auto.
Qed.
End set.
Implicit Arguments modify_set [A max].
Implicit Arguments apply_set [A max].
Implicit Arguments in_set [max].
Implicit Arguments singleton [max].
Lemma in_set_singleton : forall (p1 p2:posInf WordSize),
in_set p1 (singleton p2) = true -> eq_word p1 p2.
intros.
destruct p1; destruct p2; simpl.
apply (in_set_singleton' _ (exist (fun p => (inf_log p WordSize)) x i) (exist (fun p => (inf_log p WordSize)) x0 i0)); auto.
Qed.
Lemma in_singleton : forall (p:Word),
in_set p (singleton p) = true.
intros; unfold in_set, singleton.
assert (eq_word p p).
unfold eq_word; destruct p; auto.
generalize (apply_substArray1 _ LatticeBool (Some (Fbottom bool WordSize)) p p true H).
CaseEq
(applyArray LatticeBool
(substArray LatticeBool (Some (Fbottom bool WordSize)) p true) p); intuition.
inversion H1.
Qed.
Lemma in_singleton_eq : forall (p1 p2:Word),
eq_word p1 p2 -> in_set p1 (singleton p2) = true.
Proof.
intros.
generalize (in_singleton p2); unfold in_set.
rewrite (applyArray_eq_word _ LatticeBool (singleton p2) _ _ H); auto.
Qed.
Lemma in_set_eq : forall p1 p2 s, eq_word p1 p2 ->
in_set p1 s = true -> in_set p2 s = true.
Proof.
unfold in_set; intros.
rewrite <- (applyArray_eq_word _ LatticeBool s _ _ H); auto.
Qed.
Index
This page has been generated by coqdoc