Library FiniteSetLat
Require Import TabTree.
Require Import Lattice.
Require Import ArrayLat.
Require Import BoolLat.
Require Import Omega.
Module FiniteSetLattice <: Lattice.
Module L := ArrayLattice BoolLattice.
Module Pos := L.Pos.
Export Pos.
Definition empty := L.bottom.
Definition inter := L.inter.
Definition inter_bound1 := L.inter_bound1.
Definition inter_bound2 := L.inter_bound2.
Definition inter_greater_bound :=L.inter_greater_bound.
Definition join := L.join.
Definition join_bound1 := L.join_bound1.
Definition join_bound2 := L.join_bound2.
Definition join_least_bound := L.join_least_bound.
Definition order_dec := L.order_dec.
Definition eq_dec := L.eq_dec.
Definition bottom := L.bottom.
Definition bottom_is_a_bottom := L.bottom_is_a_bottom.
Definition top := L.top.
Definition top_is_top := L.top_is_top.
Definition acc_property := L.acc_property.
Definition in_set (p:Word) (s:set) : bool :=
L.apply s p.
Definition singleton (p:Word) : set :=
L.subst L.bottom p true.
Lemma in_set_top : forall p, in_set p top = true.
intros; unfold in_set.
simpl; auto.
Qed.
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 L.applyFunc, L.substFunc, L.Pos.apply_functree, L.Pos.apply_tree; simpl.
rewrite apply_subst_leaf2; intuition.
discriminate H.
Qed.
Lemma in_set_monotone : forall p s1 s2,
order s1 s2 ->
in_set p s1 = true -> in_set p s2 = true.
unfold in_set; intros p s1 s2 H H1.
assert (L.Pos.order s1 s2).
exact H.
clear H; rename H0 into H.
generalize (L.apply_monotone _ _ H p).
rewrite H1.
case (L.apply s2 p); intros.
auto.
inversion_clear H0.
Qed.
Lemma in_set_singleton1 : forall p s,
in_set p s = true -> order (singleton p) s.
unfold in_set, singleton, L.subst, L.bottom; intros.
destruct s; try constructor.
intros x; simpl; unfold apply_tree.
case (positive_dec x (proj1_sig p)); intros.
subst.
rewrite apply_subst_leaf1.
simpl in H; unfold L.applyFunc, L.Pos.apply_functree, L.Pos.apply_tree in H.
rewrite H; auto.
constructor.
auto.
rewrite apply_subst_leaf2; auto.
constructor.
Qed.
Lemma in_set_singleton2 : forall p s,
order (singleton p) s ->
in_set p s = true.
unfold in_set, singleton, L.subst, L.bottom; intros.
destruct s; try constructor.
inversion_clear H.
simpl; unfold L.applyFunc, L.Pos.apply_functree, L.Pos.apply_tree.
generalize (H0 (proj1_sig p)); unfold apply_tree, L.substFunc, L.modifyFunc; simpl.
rewrite apply_subst_leaf1.
intros.
inversion_clear H; auto.
Qed.
Lemma in_set_singleton : forall (p1 p2:Word),
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 (L.apply_subst1 (Some (Fbottom WordSize)) p p true H).
CaseEq
(L.apply (L.subst (Some (Fbottom WordSize)) p true) p); intuition.
inversion H1.
Qed.
Definition add_set (p:Word) (s:set) : set :=
L.subst s p true.
Lemma add_set_monotone : forall p1 p2 s1 s2,
eq_word p1 p2 -> order s1 s2 ->
order (add_set p1 s1) (add_set p2 s2).
Proof.
unfold add_set; intros.
apply L.subst_monotone; auto.
constructor.
Qed.
Lemma add_set_eq : forall p1 p2 s1 s2,
eq_word p1 p2 -> eq s1 s2 -> eq (add_set p1 s1) (add_set p2 s2).
Proof.
unfold add_set; intros.
apply L.subst_eq; auto.
constructor.
Qed.
Hint Resolve add_set_eq : eq_dat.
Lemma order_add_set : forall p s,
order s (add_set p s).
unfold add_set; intros.
apply L.order_subst.
constructor.
Qed.
Lemma in_set_add_set1 : forall p s,
in_set p (add_set p s) = true.
intros; unfold in_set, add_set.
assert (BoolLattice.Pos.order true (L.subst s p true p)).
apply L.apply_subst1; auto.
inversion_clear H; auto.
Qed.
Lemma in_set_add_set2 : forall p a s,
in_set p s = true ->
in_set p (add_set a s) = true.
intros; unfold in_set, add_set.
case (eq_word_dec p a); intros.
assert (BoolLattice.Pos.order true (L.subst s a true p)).
apply L.apply_subst1; auto.
inversion_clear H0; auto.
rewrite L.apply_subst2; auto.
Qed.
Lemma elim_in_set_add_set : forall p a s,
in_set p (add_set a s) = true ->
eq_word p a \/ in_set p s = true.
unfold in_set, add_set; intros.
case (eq_word_dec p a); intros; auto.
right; rewrite L.apply_subst2 in H; auto.
Qed.
Lemma in_set_eq_word : forall x y s,
eq_word x y ->
in_set x s = true ->
in_set y s = true.
unfold in_set; intros.
rewrite <- (L.apply_eq_word s _ _ H); auto.
Qed.
Lemma in_set_eq_word' : forall x y s,
eq_word x y ->
in_set x s = in_set y s.
unfold in_set; intros.
rewrite <- (L.apply_eq_word s _ _ H); auto.
Qed.
Lemma in_set_eq' : forall x y s1 s2,
eq_word x y ->
eq s1 s2 ->
in_set x s1 = in_set y s2.
intros.
rewrite (in_set_eq_word' _ _ s1 H).
apply BoolLattice.Pos.order_antisym.
CaseEq (in_set y s1); intros; try constructor.
rewrite (in_set_monotone y s1 s2); auto.
constructor.
apply order_refl; auto.
CaseEq (in_set y s2); intros; try constructor.
rewrite (in_set_monotone y s2 s1); auto.
constructor.
apply order_refl; apply eq_sym; auto.
Qed.
Fixpoint cardinal_tree (t:tree bool) : nat :=
match t with
leaf => (0)
| node true t1 t2 => S (plus (cardinal_tree t1) (cardinal_tree t2))
| node false t1 t2 => (plus (cardinal_tree t1) (cardinal_tree t2))
end.
Definition cardinal (s:set) : option nat :=
match s with
None => None
| Some f => Some (cardinal_tree (tr _ _ f))
end.
Inductive lt_n_op : option nat -> option nat -> Prop :=
lt_n_op_none : forall n, lt_n_op n None
| lt_n_op_some : forall n m,
lt n m -> lt_n_op (Some n) (Some m).
Lemma lt_n_op_trans: forall p q r,
lt_n_op p q -> lt_n_op q r -> lt_n_op p r.
destruct q; intros.
inversion_clear H.
inversion_clear H0; constructor.
apply lt_trans with n; auto.
inversion_clear H0 in H; auto.
Qed.
Lemma cardinal_tree_bottom : forall s,
is_bottom s -> cardinal_tree s = 0.
induction 1; simpl; auto.
destruct a.
inversion_clear H.
omega.
Qed.
Lemma bottom_cardinal_tree : forall s,
cardinal_tree s = 0 -> is_bottom s.
induction s; simpl; intros.
constructor.
destruct a.
inversion_clear H.
constructor.
constructor.
apply IHs1; omega.
apply IHs2; omega.
Qed.
Lemma cardinal_tree_eq : forall s1 s2,
eq' s1 s2 ->
(cardinal_tree s1) = (cardinal_tree s2).
induction s1; intros.
inversion_clear H; simpl; auto.
destruct b.
inversion_clear H0.
rewrite cardinal_tree_bottom; auto.
rewrite cardinal_tree_bottom; auto.
inversion_clear H; simpl.
destruct a.
inversion_clear H0.
rewrite cardinal_tree_bottom; auto.
rewrite cardinal_tree_bottom; auto.
destruct a.
inversion_clear H0.
rewrite (IHs1_1 _ H1).
rewrite (IHs1_2 _ H2).
auto.
inversion_clear H0.
rewrite (IHs1_1 _ H1).
rewrite (IHs1_2 _ H2).
auto.
Qed.
Lemma cardinal_tree_monotone : forall s1 s2,
order' s1 s2 ->
(cardinal_tree s1) < (cardinal_tree s2)
\/ eq' s1 s2.
induction s1; intros; simpl.
destruct s2; simpl.
right; constructor.
destruct s; simpl.
left; omega.
case (is_bottom_dec s2_1); intros.
case (is_bottom_dec s2_2); intros.
right; constructor 2; auto.
constructor.
left.
CaseEq (cardinal_tree s2_2); intros.
elim n; apply bottom_cardinal_tree; auto.
omega.
left.
CaseEq (cardinal_tree s2_1); intros.
elim n; apply bottom_cardinal_tree; auto.
omega.
inversion_clear H.
destruct a.
inversion_clear H0.
right; constructor 3; auto.
destruct a.
inversion_clear H0; simpl.
elim (IHs1_1 _ H1); intros.
elim (IHs1_2 _ H2); intros.
left; omega.
rewrite (cardinal_tree_eq _ _ H0).
left; omega.
rewrite (cardinal_tree_eq _ _ H).
elim (IHs1_2 _ H2); intros.
left; omega.
right; constructor 4; auto.
constructor.
simpl.
destruct b.
elim (IHs1_1 _ H1); intros.
elim (IHs1_2 _ H2); intros.
left; omega.
rewrite (cardinal_tree_eq _ _ H3).
left; omega.
rewrite (cardinal_tree_eq _ _ H).
elim (IHs1_2 _ H2); intros.
left; omega.
rewrite (cardinal_tree_eq _ _ H3).
left; omega.
elim (IHs1_1 _ H1); intros.
elim (IHs1_2 _ H2); intros.
left; omega.
rewrite (cardinal_tree_eq _ _ H3).
left; omega.
rewrite (cardinal_tree_eq _ _ H).
elim (IHs1_2 _ H2); intros.
left; omega.
right; constructor 4; auto.
constructor.
Qed.
Fixpoint pow2 (n:nat) : nat :=
match n with
0 => 1
| S p => 2 * (pow2 p) +1
end.
Lemma pow2_le1 : forall n, 1 <= pow2 n.
induction n; simpl; omega.
Qed.
Lemma cardinal_tree_inf_pow2 : forall s n,
height_inf s n ->
cardinal_tree s <= pow2 n.
induction 1; simpl; auto.
omega.
destruct a; simpl; omega.
Qed.
Definition CardMax (x:nat) := pow2 (S WordSize).
Lemma cardinal_max : forall s,
s=None \/ exists k, cardinal s = Some k /\ k <= (CardMax 0).
destruct s; auto.
right; simpl.
destruct f; simpl.
exists (cardinal_tree tr); split; auto.
unfold CardMax; apply cardinal_tree_inf_pow2; auto.
Qed.
Lemma cardinal_monotone : forall s1 s2,
order s1 s2 ->
lt_n_op (cardinal s1) (cardinal s2)
\/ eq s1 s2.
destruct s1; intros.
destruct s2.
inversion_clear H.
generalize (Forder_to_order' _ _ H0); clear H0; intros.
elim (cardinal_tree_monotone _ _ H); intros.
left; simpl; constructor; auto.
right; constructor.
apply eq'_to_Feq; auto.
left; simpl; constructor.
inversion_clear H; left; simpl; constructor.
Qed.
Lemma cardinal_0_in_set : forall s p,
cardinal s = Some 0 -> in_set p s = true -> False.
intros.
destruct s; simpl in *.
injection H; clear H; intros.
generalize (bottom_cardinal_tree _ H); intros.
generalize (is_bottom_apply _ H1 p); intros.
assert ((apply_tree (tr _ WordSize f) p)=true).
unfold L.applyFunc,L.Pos.apply_functree in H0.
apply H0.
rewrite H3 in H2; inversion H2.
discriminate H.
Qed.
Require Export List.
Fixpoint height_pos (p:positive) : nat :=
match p with
xH => 0
| xO p => S (height_pos p)
| xI p => S (height_pos p)
end.
Lemma inf_log_height : forall p, inf_log p (height_pos p).
induction p; simpl; intros; auto; constructor; auto.
Qed.
Lemma inf_log_le : forall p n m,
le n m ->
inf_log p n -> inf_log p m.
induction p; intros.
inversion_clear H0 in H.
inversion_clear H; constructor; auto.
apply IHp with n0; auto with arith.
inversion_clear H0 in H.
inversion_clear H; constructor; auto.
apply IHp with n0; auto with arith.
constructor.
Qed.
Definition set2list_rec (max:nat) (t:tree bool) (n:nat) (p:positive) :
height_inf t n -> S max = n + (height_pos p) -> list {p:positive| inf_log p max}.
induction t; intros.
exact nil.
destruct n.
apply False_rec.
inversion H.
destruct a.
refine (cons (exist (fun p => inf_log p max) p _)
((IHt1 n (xO p) _ _) ++ (IHt2 n (xI p) _ _))).
apply inf_log_le with (height_pos p).
omega.
apply inf_log_height.
inversion H; auto.
simpl.
omega.
inversion H; auto.
simpl.
omega.
refine ((IHt1 n (xO p) _ _) ++ (IHt2 n (xI p) _ _)).
inversion H; auto.
simpl.
omega.
inversion H; auto.
simpl.
omega.
Defined.
Definition set2list : set -> list Word.
intros t.
refine (match t with
None => nil
| Some s => set2list_rec WordSize (tr _ _ s) (S WordSize) xH _ _
end).
destruct s; auto.
auto.
Defined.
End FiniteSetLattice.
Module ArraySetLattice (L:Lattice) <: Lattice.
Module M := ArrayLattice L.
Module Pos := M.Pos.
Export Pos.
Definition inter := M.inter.
Definition inter_bound1 := M.inter_bound1.
Definition inter_bound2 := M.inter_bound2.
Definition inter_greater_bound := M.inter_greater_bound.
Definition join := M.join.
Definition join_bound1 := M.join_bound1.
Definition join_bound2 := M.join_bound2.
Definition join_least_bound := M.join_least_bound.
Definition order_dec := M.order_dec.
Definition eq_dec := M.eq_dec.
Definition bottom := M.bottom.
Definition bottom_is_a_bottom := M.bottom_is_a_bottom.
Definition top := M.top.
Definition top_is_top := M.top_is_top.
Definition acc_property := M.acc_property.
Definition apply := M.apply.
Definition subst := M.subst.
Definition modify := M.modify.
Lemma height_inf_modify_set :
forall (a:L.Pos.set) (s:tree bool) (t:tree L.Pos.set) (n:nat) (v:L.Pos.set->L.Pos.set),
(height_inf t n) -> (height_inf s n) ->
(height_inf (modify_set_tree L.Pos.set 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 :
set->FiniteSetLattice.Pos.set->(L.Pos.set->L.Pos.set)->set.
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 _ L.bottom (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,
FiniteSetLattice.in_set p s = true ->
L.Pos.order (f (apply t p)) (apply (modify_set t s f) p).
destruct t.
destruct s; intros.
destruct f; destruct f0; simpl in H|-*.
unfold M.applyFunc, M.Pos.apply_functree, M.Pos.apply_tree; simpl.
rewrite apply_modify_set_tree1; auto.
simpl; auto.
intros; simpl; auto.
Qed.
Lemma apply_modify_set2 :
forall s t f p,
FiniteSetLattice.in_set p s = false ->
(apply (modify_set t s f) p) = (apply t p) .
destruct t.
destruct s; intros.
destruct f; destruct f0; simpl in H|-*.
unfold M.applyFunc, M.Pos.apply_functree, M.Pos.apply_tree; simpl.
rewrite apply_modify_set_tree; auto.
simpl in H; inversion H.
intros; simpl; auto.
Qed.
Definition apply_set :
set -> FiniteSetLattice.Pos.set -> L.Pos.set :=
fun f' s' =>
match f' with
None => L.top
| Some f => match s' with
None => L.top
| Some s =>
apply_set_tree L.Pos.set L.bottom L.join (tr _ _ f) (tr _ _ s)
end
end.
Lemma apply_set_in : forall t s p,
FiniteSetLattice.in_set p s = true ->
L.Pos.order (apply t p) (apply_set t s).
intros.
destruct t; destruct s; simpl.
generalize (apply_set_tree1 L.Pos.set L.bottom L.join L.Pos.order
L.join_bound1 L.join_bound2 L.bottom_is_a_bottom
L.Pos.order_trans); intros H1.
unfold M.applyFunc, M.Pos.apply_functree.
apply H1.
exact H.
auto.
auto.
auto.
Qed.
End ArraySetLattice.
Index
This page has been generated by coqdoc