Require TabTree.
Require Lattice.
Require func.
Require BoolLat.
Section set.
Variable max:nat.
Definition FiniteSet := (funcTree bool max).
Definition LatticeFiniteSet : (Lattice.Lattice FiniteSet) :=
(funcTree_Lattice bool LatticeBool max).
Definition singleton : (p:positive) FiniteSet :=
[p] (subst LatticeBool (bottom LatticeFiniteSet) p true).
Definition in_finite : positive -> FiniteSet -> Prop :=
[p,s](apply LatticeBool s p)=true.
Lemma in_finite_dec : (p:positive;s:FiniteSet){(in_finite p s)}+{~(in_finite p s)}.
Unfold in_finite; Intros.
Case (apply LatticeBool s p); Intros.
Left; Reflexivity.
Right; Discriminate.
Qed.
Lemma in_finite_singleton : (p:positive;s:FiniteSet)
(in_finite p s) -> (order LatticeFiniteSet (singleton p) s).
Unfold in_finite singleton; Intros.
Apply (subst_order bool LatticeBool max); Intros.
Rewrite (apply_on_bottom bool LatticeBool max); Auto.
Rewrite H; Auto.
Qed.
Lemma singleton_in_finite : (p:positive;s:FiniteSet)
(inf_log p max) ->
(order LatticeFiniteSet (singleton p) s) -> (in_finite p s).
Unfold singleton in_finite; Intros.
Generalize (apply_monotone ? ? ? ? ? H0 p); Intros.
Rewrite apply_subst1 in H1 ;Auto.
Generalize H1; Case (apply LatticeBool s p); Intros.
Auto.
Unfold LatticeBool in H2.
Inversion H2.
Qed.
Variable A:Set.
Variable PA:(Lattice A).
Definition map : (positive->A) -> FiniteSet -> (funcTree A max) :=
[f,s]let F=[p:positive;b:bool]
Cases b of
| true => (f p)
| false => (bottom PA)
end in
(mapIt F s).
Lemma map_in_finite : (f:positive->A;s:FiniteSet;p:positive)
(in_finite p s) -> (apply PA (map f s) p)=(f p).
Unfold map in_finite; Intros.
Rewrite (mapIt_correct bool A LatticeBool PA).
Rewrite H; Auto.
Intros; Unfold LatticeBool; Simpl; Auto.
Qed.
Lemma map_not_in_finite : (f:positive->A;s:FiniteSet;p:positive)
~(in_finite p s) -> (apply PA (map f s) p)=(bottom PA).
Unfold map in_finite; Intros.
Rewrite (mapIt_correct bool A LatticeBool PA).
Generalize H; Clear H; Case (apply LatticeBool s p); Simpl; Intros.
Elim H; Reflexivity.
Auto.
Intros; Unfold LatticeBool; Simpl; Auto.
Qed.
Lemma in_keep_order : (s1,s2:FiniteSet;p:positive)
(order LatticeFiniteSet s1 s2) ->
(in_finite p s1) -> (in_finite p s2).
Unfold LatticeFiniteSet in_finite; Intros.
Generalize (apply_monotone ? LatticeBool max ? ? H p).
Rewrite H0; Intros.
Inversion H1; Auto.
Qed.
Lemma map_monotone : (f,g:positive->A;s1,s2:FiniteSet)
((p:positive)(order PA (f p) (g p)))->
(order LatticeFiniteSet s1 s2) ->
(order (funcTree_Lattice A PA max) (map f s1) (map g s2)).
Intros.
Apply funcTree_order; Intros.
Case (in_finite_dec p s1); Intros.
Generalize (in_keep_order s1 s2 p H0 i); Intros.
Rewrite map_in_finite; Auto.
Rewrite map_in_finite; Auto.
Rewrite map_not_in_finite; Auto.
Qed.
Section join_on_set.
Variable f:positive->A.
Local F:=[p:positive;b:bool]
Cases b of
| true => (f p)
| false => (bottom PA)
end.
Local join3:=[a1,a2,a3:A](join PA a1 (join PA a2 a3)).
Definition join_on_set : FiniteSet -> A :=
[s]
(join_tabtree bool A F join3 (tr ? ? s)).
Lemma join_on_set_prop : (s:FiniteSet;p:positive)
(in_finite p s) -> (order PA (f p) (join_on_set s)).
Intros; Unfold join_on_set apply.
Unfold in_finite in H.
Replace (f p) with (F p true); [Idtac|Auto].
Rewrite <- H; Clear H.
Unfold apply; Case s; Simpl; Intros.
Apply join_tabtree_prop with P:=(order PA); Unfold join3; Intros.
Auto.
Apply order_trans with b1; Auto.
Apply order_trans with (join PA b1 b2); Auto.
Apply order_trans with b2; Auto.
Apply order_trans with (join PA b1 b2); Auto.
Auto.
Simpl; Auto.
Qed.
Lemma join_on_set_prop2_rec : (tr:(tree bool))
(p:positive; x:A)
((p0:positive)(apply_tree bool false tr p0)=true->(order PA (f (inv_pos p p0)) x))
->(order PA (join_tabtree_rec bool A F join3 p tr) x).
NewInduction tr; Simpl.
Case a; Simpl; Intros.
Apply H; Auto.
Auto.
Unfold join3.
Intros.
Apply join_least_bound.
Generalize H; Clear H.
Case a; Simpl; Intros.
Apply H; Auto.
Auto.
Apply join_least_bound.
Apply IHtr1; Intros.
Generalize (H (xO p0)); Simpl; Auto.
Apply IHtr2; Intros.
Generalize (H (xI p0)); Simpl; Auto.
Qed.
Lemma join_on_set_prop2 : (s:FiniteSet;x:A)
((p:positive)(in_finite p s)->(order PA (f p) x)) ->
(order PA (join_on_set s) x).
Destruct s; Unfold join_on_set in_finite apply join_tabtree; Simpl.
Intros.
Apply join_on_set_prop2_rec; Auto.
Qed.
End join_on_set.
Lemma join_on_set_monotone : (f,g:positive->A;s1,s2:FiniteSet)
((p:positive)(order PA (f p) (g p)))->
(order LatticeFiniteSet s1 s2) ->
(order PA (join_on_set f s1) (join_on_set g s2)).
Intros.
Apply join_on_set_prop2; Intros.
Apply order_trans with (g p); Auto.
Apply join_on_set_prop; Intros.
Apply in_keep_order with s1; Auto.
Qed.
End set.
Implicits singleton [1].
Implicits map [1 2].
Implicits join_on_set [1 2].