Library Lattice
Require Import Wf.
Require Import List.
Require Export Poset.
Module Type Lattice.
Declare Module Pos : PosetSet.
Export Pos.
Parameter join : set -> set -> set.
Parameter join_bound1 : forall x y : set, order x (join x y).
Parameter join_bound2 : forall x y : set, order y (join x y).
Parameter join_least_bound : forall x y z : set, order x z -> order y z -> order (join x y) z.
Parameter inter : set -> set -> set.
Parameter inter_bound1 : forall x y : set, order (inter x y) x.
Parameter inter_bound2 : forall x y : set, order (inter x y) y.
Parameter inter_greater_bound : forall x y z : set, order z x -> order z y -> order z (inter x y).
Parameter order_dec : forall x y : set, {order x y} + {~ order x y}.
Parameter eq_dec : forall x y : set, {eq x y} + {~ eq x y}.
Parameter bottom : set.
Parameter bottom_is_a_bottom : forall x : set, order bottom x.
Parameter top : set.
Parameter top_is_top : forall x : set, order x top.
Parameter acc_property : well_founded (fun x y => ~ eq y x /\ order y x).
Hint Resolve
join_bound1 join_bound2 inter_bound1 inter_bound2 join_least_bound bottom_is_a_bottom top_is_top inter_greater_bound
acc_property.
End Lattice.
Module Pos_dec (P:Poset).
Export P.
Lemma order2eq_dec :
(forall x y : set, {order x y} + {~ order x y}) ->
forall x y : set, {eq x y} + {~ eq x y}.
intros order_dec x y.
case (order_dec x y); intros.
case (order_dec y x); intros.
left; auto.
right; intros H; elim n; auto.
right; intros H; elim n; auto.
Qed.
End Pos_dec.
Module Lattice_prop (L:Lattice).
Import L.
Lemma order_eq_order :
forall x y z : set, order x y -> eq y z -> order x z.
intros x y z H H1; apply order_trans with y; auto.
Qed.
Lemma eq_order_order :
forall x y z : set, eq x y -> order y z -> order x z.
intros x y z H H1; apply order_trans with y; auto.
Qed.
Lemma join_sym : forall x y :set, eq (join x y) (join y x).
auto.
Qed.
Lemma join_eq1 :
forall x y z : set, eq x y -> eq (join x z) (join y z).
intros; apply order_antisym.
apply join_least_bound; auto.
apply eq_order_order with y; auto.
apply join_least_bound; auto.
apply eq_order_order with x; auto.
Qed.
Lemma join_eq2 :
forall x y z : set, eq y z -> eq (join x z) (join x y).
intros; apply order_antisym.
apply join_least_bound; auto.
apply eq_order_order with y; auto.
apply join_least_bound; auto.
apply eq_order_order with z; auto.
Qed.
Lemma join4 :
forall a b c d : set,
order a b -> order c d -> order (join a c) (join b d).
intros.
apply join_least_bound.
apply order_trans with b; auto.
apply order_trans with d; auto.
Qed.
Lemma join_bottom1 : forall x : set, eq (join (bottom) x) x.
intros; apply order_antisym; auto.
Qed.
Lemma join_bottom2 : forall x : set, eq x (join (bottom) x).
intros; apply order_antisym; auto.
Qed.
Fixpoint join_list (l : list set) : set :=
match l with
| nil => bottom
| a :: q => join a (join_list q)
end.
Lemma join_list_greater :
forall (l : list set) (x : set), In x l -> order x (join_list l).
induction l; simpl in |- *; intuition.
subst; auto.
apply order_trans with (join_list l); auto.
Qed.
Lemma join_list_least_greater :
forall (l : list set) (z : set),
(forall x : set, In x l -> order x z) -> order (join_list l) z.
induction l; simpl in |- *; intuition.
Qed.
Inductive list_order : list set -> list set -> Prop :=
| list_order_nil : list_order nil nil
| list_order_cons :
forall (x1 x2 : set) (l1 l2 : list set),
order x1 x2 -> list_order l1 l2 -> list_order (x1 :: l1) (x2 :: l2).
Lemma list_order_join_list :
forall l1 l2 : list set,
list_order l1 l2 -> order (join_list l1) (join_list l2).
induction 1; simpl in |- *; auto.
apply join_least_bound.
apply order_trans with x2; auto.
apply order_trans with (join_list l2); auto.
Qed.
Hint Resolve join_bottom1 join_bottom2 join_list_greater
join_list_least_greater.
End Lattice_prop.
Module Iter_fix (L:Lattice).
Import L.
Module properties := (Lattice_prop L).
Import properties.
Definition monotone (f : set -> set) :=
forall x y : set, order x y -> order (f x) (f y).
Section Fix.
Variable f : set -> set.
Variable f_monotone : monotone f.
Fixpoint iter (n : nat) : set -> set :=
match n with
| O => fun x : set => x
| S p => fun x : set => f (iter p x)
end.
Lemma iter_assoc : forall (n : nat) (x : set), f (iter n x) = iter n (f x).
induction n; simpl in |- *; intros.
reflexivity.
rewrite IHn; reflexivity.
Qed.
Let P (x : set) :=
order x (f x) ->
{a : set | eq a (f a) /\ (exists n : nat, a = iter n x)}.
Let order_acc x y := ~ eq y x /\ order y x.
Definition iter_until_fix_f :
forall x : set, (forall y : set, order_acc y x -> P y) -> P x.
unfold P in |- *; intros.
case (order_dec (f x) x); intros.
exists x; intuition.
exists 0; intuition.
elim (H (f x)); intros.
exists x0; intuition.
elim H2; intros.
exists (S x1).
rewrite H3; simpl in |- *.
apply sym_eq; apply iter_assoc.
unfold order_acc in |- *; intuition.
apply f_monotone; auto.
Defined.
Definition iter_fix (x : set) : P x :=
Fix_F P iter_until_fix_f (acc_property x).
Lemma iter_def : forall (n : nat) (x : set), f (iter n x) = iter (S n) x.
simpl in |- *; auto.
Qed.
Lemma iter_monotone : forall n : nat, monotone (iter n).
induction n; simpl in |- *; unfold monotone in |- *; intros; auto.
Qed.
Lemma fix_implies_fix_iter :
forall x : set, eq x (f x) -> forall n : nat, eq (iter n x) x.
induction n; simpl in |- *; intros.
auto.
apply eq_trans with (f x); auto.
Qed.
Lemma iter_stabilize_implies_lfp :
forall n : nat,
eq (iter n (bottom)) (iter (S n) (bottom)) ->
forall x : set, eq x (f x) -> order (iter n (bottom)) x.
intros.
apply order_trans with (iter n x).
apply iter_monotone; auto.
apply order_refl.
apply fix_implies_fix_iter; auto.
Qed.
Lemma iter_bottom_is_lfp :
forall x : set,
(exists n : nat, x = iter n (bottom)) ->
eq x (f x) -> forall y : set, eq y (f y) -> order x y.
intros.
elim H; intuition.
rewrite H2 in H0; rewrite H2.
apply iter_stabilize_implies_lfp; auto.
Qed.
Lemma ifix_implies_ifix_iter :
forall x : set, order (f x) x -> forall n : nat, order (iter n x) x.
induction n; simpl in |- *; intros.
auto.
apply order_trans with (f x); auto.
Qed.
Lemma iter_stabilize_implies_lifp :
forall n : nat,
eq (iter n (bottom)) (iter (S n) (bottom)) ->
forall x : set, order (f x) x -> order (iter n (bottom)) x.
intros.
apply order_trans with (iter n x).
apply iter_monotone; auto.
apply ifix_implies_ifix_iter; auto.
Qed.
Lemma iter_bottom_is_lifp :
forall x : set,
(exists n : nat, x = iter n (bottom)) ->
eq x (f x) -> forall y : set, order (f y) y -> order x y.
intros.
elim H; intuition.
rewrite H2 in H0; rewrite H2.
apply iter_stabilize_implies_lifp; auto.
Qed.
Definition lfp : set :=
let (x, _) := iter_fix (bottom) (bottom_is_a_bottom _) in x.
Lemma lfp_is_lfp :
eq lfp (f lfp) /\ (forall y : set, eq y (f y) -> order lfp y).
unfold lfp in |- *;
case (iter_fix (bottom) (bottom_is_a_bottom (f (bottom))));
intros.
intuition.
apply iter_bottom_is_lfp; auto.
Qed.
Lemma lfp_is_lifp :
order (f lfp) lfp /\ (forall y : set, order (f y) y -> order lfp y).
unfold lfp in |- *;
case (iter_fix (bottom) (bottom_is_a_bottom (f (bottom))));
intros.
intuition.
apply iter_bottom_is_lifp; auto.
Qed.
End Fix.
Section fix_n.
Fixpoint iter_listf (l : list ( set -> set)) (x:set) {struct l} : set :=
match l with
| nil => x
| f :: q => iter_listf q (join x (f x))
end.
Lemma iter_listf_is_monotone :
forall l : list ( set -> set),
(forall f : set -> set, In f l -> monotone f) -> monotone (iter_listf l).
unfold monotone in |- *; induction l; simpl in |- *; intros.
auto.
apply IHl; auto.
apply join4; auto.
Qed.
Lemma f_in_listf_prop1 :
forall (l : list ( set -> set)) (x : set), order x (iter_listf l x).
induction l; simpl in |- *; intros; auto.
apply order_trans with (join x (a x)); auto.
Qed.
Lemma f_in_listf_prop2 :
forall (l : list ( set -> set)) (f : set -> set),
In f l -> monotone f -> forall x : set, order (f x) (iter_listf l x).
induction l; simpl in |- *; intros; auto.
elim H.
decompose [or] H.
subst.
apply order_trans with (join x (f x)); auto.
apply f_in_listf_prop1.
apply order_trans with (f (join x (a x))); auto.
Qed.
Lemma f_in_listf_prop3 :
forall l : list ( set -> set),
(forall f : set -> set, In f l -> monotone f) ->
forall x : set,
(forall f : set -> set, In f l -> order (f x) x) ->
order (iter_listf l x) x.
induction l; simpl in |- *; intros; auto.
apply order_trans with (join x (a x)); auto.
apply IHl; auto.
intros.
apply order_trans with (f x).
apply H; auto.
apply order_trans with x; auto.
Qed.
Variable listf : list ( set -> set).
Variable
listf_monotone : forall f : set -> set, In f listf -> monotone f.
Definition lfp_list :=
lfp (iter_listf listf)
(iter_listf_is_monotone listf listf_monotone).
Lemma in_rev : forall (A : Set) (l : list A) (x : A), In x l -> In x (rev l).
induction l; intuition.
simpl in |- *.
generalize incl_appr.
unfold incl in |- *; intros.
elim H; intros.
apply H0 with (a :: nil); auto.
subst; auto with datatypes.
generalize incl_appl.
unfold incl in |- *; intros.
apply H2 with (rev l); auto.
Qed.
Lemma lfp_list_is_lifp :
(forall f : set -> set, In f listf -> order (f lfp_list) lfp_list) /\
(forall y : set,
(forall f : set -> set, In f listf -> order (f y) y) ->
order lfp_list y).
split.
intros.
elim
(lfp_is_lfp (iter_listf listf)
(iter_listf_is_monotone listf listf_monotone)).
intros.
unfold lfp_list in |- *.
apply
order_trans
with
(iter_listf listf
(lfp (iter_listf listf)
(iter_listf_is_monotone listf listf_monotone)));
auto.
apply f_in_listf_prop2; auto.
intros.
unfold lfp_list in |- *.
apply
(iter_bottom_is_lifp (iter_listf listf)
(iter_listf_is_monotone listf listf_monotone)).
unfold lfp in |- *.
case
(iter_fix (iter_listf listf)
(iter_listf_is_monotone listf listf_monotone) (
bottom) (bottom_is_a_bottom (iter_listf listf (bottom))));
intros.
intuition.
unfold lfp in |- *.
case
(iter_fix (iter_listf listf)
(iter_listf_is_monotone listf listf_monotone) (
bottom) (bottom_is_a_bottom (iter_listf listf (bottom))));
intros.
intuition.
apply f_in_listf_prop3.
auto.
auto.
Qed.
End fix_n.
End Iter_fix.
Index
This page has been generated by coqdoc