Require Wf.
Require PolyList.
Record Lattice [A:Set]: Type := poset_constr {
order : A -> A -> Prop;
eq : A -> A -> Prop;
join : A -> A -> A;
order_refl : (x,y:A) (eq x y) -> (order x y);
order_antisym : (x,y:A) (order x y) -> (order y x) -> (eq x y);
order_trans : (x,y,z:A) (order x y) -> (order y z) -> (order x z);
eq_refl : (x:A) (eq x x);
eq_sym : (x,y:A) (eq x y) -> (eq y x);
eq_trans : (x,y,z:A) (eq x y) -> (eq y z) -> (eq x z);
join_bound1 : (x,y:A) (order x (join x y));
join_bound2 : (x,y:A) (order y (join x y));
join_least_bound : (x,y,z:A)
(order x z) -> (order y z) -> (order (join x y) z);
eq_dec : (x,y:A){(eq x y)}+{~(eq x y)};
bottom : A;
bottom_is_a_bottom : (x:A) (order bottom x);
top : A;
top_is_top : (x:A)(order x top);
acc_property : (well_founded A ([x,y] ~(eq y x)/\(order y x)))
}.
Implicits order [1].
Implicits eq [1].
Implicits join [1].
Implicits order_refl [1].
Implicits order_antisym [1].
Implicits order_trans [1].
Implicits eq_refl [1].
Implicits eq_sym [1].
Implicits eq_trans [1].
Implicits join_bound1 [1].
Implicits join_bound2 [1].
Implicits join_least_bound [1].
Implicits eq_dec [1].
Implicits bottom [1].
Implicits bottom_is_a_bottom [1].
Implicits top [1].
Implicits top_is_top [1].
Implicits acc_property [1].
Hints Resolve order_refl order_antisym eq_trans
eq_refl eq_sym order_trans
join_bound1 join_bound2 join_least_bound
bottom_is_a_bottom top_is_top acc_property.
Definition prod_Lattice : (A,B:Set) (Lattice A) -> (Lattice B) -> (Lattice A*B).
Intros A B PA PB.
Refine (poset_constr
A*B
[x,y]((order PA (Fst x) (Fst y)) /\(order PB (Snd x) (Snd y)))
[x,y](eq PA (Fst x) (Fst y)) /\ (eq PB (Snd x) (Snd y))
[x,y](join PA (Fst x) (Fst y),join PB (Snd x) (Snd y))
? ? ? ? ? ? ? ? ?
? (bottom PA,bottom PB) ? (top PA,top PB) ? ?).
Intuition; Apply order_refl; Auto.
Intuition; Apply order_antisym; Auto.
Intros Latticex Latticey Latticez; Case Latticex; Case Latticey; Case Latticez; Simpl; Intuition; EApply order_trans; EAuto.
Intuition; Apply eq_refl; Auto.
Intuition; Apply eq_sym; Auto.
Intros Latticex Latticey Latticez; Case Latticex; Case Latticey; Case Latticez; Simpl; Intuition; EApply eq_trans; EAuto.
Intuition; Simpl; Apply join_bound1.
Intuition; Simpl; Apply join_bound2.
Intuition; Simpl; Apply join_least_bound; Auto.
Destruct x; Intros x1 x2.
Destruct y; Intros y1 y2.
Case (eq_dec PA x1 y1); Intros.
Case (eq_dec PB x2 y2); Intros.
Left; Simpl; Auto.
Right; Simpl; Red; Intros; Elim n; Intuition.
Right; Simpl; Red; Intros; Elim n; Intuition.
Simpl; Intuition.
Simpl; Intuition.
Unfold well_founded.
Destruct a; Intros x.
NewInduction (acc_property PA x).
Intro Hx; Intros y.
Generalize x Hx; Clear H Hx x a.
NewInduction (acc_property PB y).
Intro Hy; Constructor.
Destruct y; Intros x' y'.
Intros H'; Intuition.
Case (eq_dec PA x0 x'); Intros.
Apply Hy; Intuition.
Apply Hx; Split.
Intros; Elim H4.
Apply eq_trans with x0; Auto.
Apply order_trans with x'; Auto.
Apply Hx; Split; Auto.
Defined.
Section monotone.
Variable A,B:Set.
Variable PA:(Lattice A).
Variable PB:(Lattice B).
Lemma pair_monotone : (a1,a2:A;b1,b2:B)
(order PA a1 a2) -> (order PB b1 b2) ->
(order (prod_Lattice A B PA PB) (a1,b1) (a2,b2)).
Intros; Unfold prod_Lattice; Simpl.
Split; Auto.
Qed.
Lemma Fst_monotone : (p1,p2:A*B)
(order (prod_Lattice A B PA PB) p1 p2) ->
(order PA (Fst p1) (Fst p2)).
Unfold prod_Lattice; Simpl; Intuition.
Qed.
Lemma Snd_monotone : (p1,p2:A*B)
(order (prod_Lattice A B PA PB) p1 p2) ->
(order PB (Snd p1) (Snd p2)).
Unfold prod_Lattice; Simpl; Intuition.
Qed.
End monotone.
Section Lattice_prop.
Variable A:Set.
Variable PA:(Lattice A).
Lemma order_eq_order : (x,y,z:A)
(order PA x y) -> (eq PA y z) -> (order PA x z).
Intros x y z H H1; Apply order_trans with y; Auto.
Qed.
Lemma eq_order_order : (x,y,z:A)
(eq PA x y) -> (order PA y z) -> (order PA x z).
Intros x y z H H1; Apply order_trans with y; Auto.
Qed.
Lemma join_sym : (x,y:A) (eq PA (join PA x y) (join PA y x)).
Auto.
Qed.
Lemma join_eq1 : (x,y,z:A)
(eq PA x y) -> (eq PA (join PA x z) (join PA 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 : (x,y,z:A)
(eq PA y z) -> (eq PA (join PA x z) (join PA 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 : (a,b,c,d:A)
(order PA a b) -> (order PA c d) ->
(order PA (join PA a c) (join PA b d)).
Intros.
Apply join_least_bound.
Apply order_trans with b; Auto.
Apply order_trans with d; Auto.
Qed.
Lemma join_bottom1 : (x:A) (eq PA (join PA (bottom PA) x) x).
Intros; Apply order_antisym; Auto.
Qed.
Lemma join_bottom2 : (x:A) (eq PA x (join PA (bottom PA) x)).
Intros; Apply order_antisym; Auto.
Qed.
Fixpoint join_list [l:(list A)] : A :=
Cases l of
| nil => (bottom PA)
| (cons a q) => (join PA a (join_list q))
end.
Lemma join_list_greater : (l:(list A);x:A) (In x l) ->
(order PA x (join_list l)).
NewInduction l; Simpl; Intuition.
Subst; Auto.
Apply order_trans with (join_list l); Auto.
Qed.
Lemma join_list_least_greater : (l:(list A);z:A)
((x:A)(In x l) -> (order PA x z)) ->
(order PA (join_list l) z).
NewInduction l; Simpl; Intuition.
Qed.
Inductive list_order : (list A) -> (list A) -> Prop :=
list_order_nil : (list_order (nil ?) (nil ?))
| list_order_cons : (x1,x2:A;l1,l2:(list A))
(order PA x1 x2) -> (list_order l1 l2) ->
(list_order (cons x1 l1) (cons x2 l2)).
Lemma list_order_join_list : (l1,l2:(list A))
(list_order l1 l2) -> (order PA (join_list l1) (join_list l2)).
NewInduction 1; Simpl; Auto.
Apply join_least_bound.
Apply order_trans with x2; Auto.
Apply order_trans with (join_list l2); Auto.
Qed.
End Lattice_prop.
Hints Resolve join_bottom1 join_bottom2 join_list_greater join_list_least_greater.
Section iter_fix.
Variable set:Set.
Variable PA:(Lattice set).
Local monotone := [f:set->set]
(x,y:set) (order PA x y) -> (order PA (f x) (f y)).
Section fix.
Variable f:set->set.
Variable f_monotone : (monotone f).
Fixpoint iter [n:nat] : set->set :=
Cases n of
| O => [x:set]x
| (S p) => [x:set](f (iter p x))
end.
Lemma iter_assoc : (n:nat;x:set) (f (iter n x))=(iter n (f x)).
NewInduction n; Simpl; Intros.
Reflexivity.
Rewrite IHn; Reflexivity.
Qed.
Local P := [x:set] (order PA x (f x)) -> {a:set | (eq PA a (f a))/\(EX n:nat | a=(iter n x))}.
Local order_acc := ([x,y] ~(eq PA y x)/\(order PA y x)).
Definition iter_until_fix_f : (x:set)((y:set)(order_acc y x)->(P y)) ->(P x).
Unfold P; Intros.
Case (eq_dec PA x (f x)); Intros.
Exists x; Intuition.
Exists O; Intuition.
Elim (H (f x)); Intros.
Exists x0; Intuition.
Elim H2; Intros.
Exists (S x1).
Rewrite H3; Simpl.
Apply sym_eq; Apply iter_assoc.
Unfold order_acc; Intuition.
Apply f_monotone; Auto.
Defined.
Definition iter_fix: (x:set) (P x):=
[x:set]
(Fix_F set order_acc P iter_until_fix_f x (acc_property PA x)).
Lemma iter_def : (n:nat;x:set) (f (iter n x))=(iter (S n) x).
Simpl; Auto.
Qed.
Lemma iter_monotone : (n:nat) (monotone (iter n)).
NewInduction n; Simpl; Unfold monotone; Intros; Auto.
Qed.
Lemma fix_implies_fix_iter : (x:set) (eq PA x (f x)) ->
(n:nat) (eq PA (iter n x) x).
NewInduction n; Simpl; Intros.
Auto.
Apply eq_trans with (f x); Auto.
Qed.
Lemma iter_stabilize_implies_lfp : (n:nat)
(eq PA (iter n(bottom PA)) (iter (S n) (bottom PA))) ->
(x:set) (eq PA x (f x)) -> (order PA (iter n (bottom PA)) 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 : (x:set)
(EX n:nat | x=(iter n (bottom PA))) -> (eq PA x (f x)) ->
(y:set) (eq PA y (f y)) -> (order PA x y).
Intros.
Elim H; Intuition.
Rewrite H2 in H0; Rewrite H2.
Apply iter_stabilize_implies_lfp; Auto.
Qed.
Lemma ifix_implies_ifix_iter : (x:set) (order PA (f x) x) ->
(n:nat) (order PA (iter n x) x).
NewInduction n; Simpl; Intros.
Auto.
Apply order_trans with (f x); Auto.
Qed.
Lemma iter_stabilize_implies_lifp : (n:nat)
(eq PA (iter n(bottom PA)) (iter (S n) (bottom PA))) ->
(x:set) (order PA (f x) x) -> (order PA (iter n (bottom PA)) 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 : (x:set)
(EX n:nat | x=(iter n (bottom PA))) -> (eq PA x (f x)) ->
(y:set) (order PA (f y) y) -> (order PA 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 PA) (bottom_is_a_bottom PA ?)) in x.
Lemma lfp_is_lfp :
(eq PA lfp (f lfp))/\
(y:set) (eq PA y (f y)) -> (order PA lfp y).
Unfold lfp;
Case (iter_fix (bottom PA) (bottom_is_a_bottom PA (f (bottom PA)))); Intros.
Intuition.
Apply iter_bottom_is_lfp; Auto.
Qed.
Lemma lfp_is_lifp :
(order PA (f lfp) lfp)/\
(y:set) (order PA (f y) y) -> (order PA lfp y).
Unfold lfp;
Case (iter_fix (bottom PA) (bottom_is_a_bottom PA (f (bottom PA)))); Intros.
Intuition.
Apply iter_bottom_is_lifp; Auto.
Qed.
End fix.
Section fix_n.
Fixpoint iter_listf [l:(list (set->set))] : set->set :=
Cases l of
| nil => [x:set]x
| (cons f q) => [x:set]let y=(iter_listf q x) in
(join PA y (f y))
end.
Lemma iter_listf_is_monotone : (l:(list (set->set)))
((f:set->set)(In f l) -> (monotone f)) ->
(monotone (iter_listf l)).
Unfold monotone; NewInduction l; Simpl; Intros.
Auto.
Apply join4; Auto.
Qed.
Lemma f_in_listf_prop1 : (l:(list (set->set)))
(x:set) (order PA x (iter_listf l x)).
NewInduction l; Simpl; Intros; Auto.
Apply order_trans with (iter_listf l x); Auto.
Qed.
Lemma f_in_listf_prop2 : (l:(list (set->set)))
(f:set->set) (In f l) -> (monotone f) ->
(x:set) (order PA (f x) (iter_listf l x)).
NewInduction l; Simpl; Intros; Auto.
Elim H.
Decompose [or] H.
Subst.
Apply order_trans with (f (iter_listf l x)); Auto.
Apply H0.
Apply f_in_listf_prop1.
Apply order_trans with (iter_listf l x); Auto.
Qed.
Lemma f_in_listf_prop3 : (l:(list (set->set)))
((f:set->set) (In f l) -> (monotone f)) ->
(x:set)
((f:set->set) (In f l) -> (order PA (f x) x)) ->
(order PA (iter_listf l x) x).
NewInduction l; Simpl; Intros; Auto.
Apply join_least_bound.
Auto.
Apply order_trans with (a x); Auto.
Apply (H a); Auto.
Qed.
Variable listf:(list (set->set)).
Variable listf_monotone : (f:set->set)(In f (rev listf)) -> (monotone f).
Definition lfp_list := (lfp (iter_listf (rev listf))
(iter_listf_is_monotone (rev listf) listf_monotone)).
Lemma in_rev : (A:Set)(l:(list A))(x:A)
(In x l) -> (In x (rev l)).
NewInduction l; Intuition.
Simpl.
Generalize incl_appr.
Unfold incl; Intros.
Elim H; Intros.
Apply H0 with (cons a (nil A)); Auto.
Subst; Auto with datatypes.
Generalize incl_appl.
Unfold incl; Intros.
Apply H2 with (rev l); Auto.
Qed.
Lemma lfp_list_is_lifp :
((f:set->set) (In f listf) -> (order PA (f lfp_list) lfp_list))
/\
( (y:set) ((f:set->set) (In f listf) -> (order PA (f y) y))
-> (order PA lfp_list y)).
Split.
Intros.
Elim (lfp_is_lfp (iter_listf (rev listf))(iter_listf_is_monotone (rev listf) listf_monotone) ).
Intros.
Unfold lfp_list.
Apply order_trans with (iter_listf (rev listf)
(lfp (iter_listf (rev listf))
(iter_listf_is_monotone (rev listf) listf_monotone))); Auto.
Apply f_in_listf_prop2; Auto.
Apply in_rev; Auto.
Apply listf_monotone.
Apply in_rev; Auto.
Intros.
Unfold lfp_list.
Apply (iter_bottom_is_lifp (iter_listf (rev listf))
(iter_listf_is_monotone (rev listf) listf_monotone)).
Unfold lfp.
Case (iter_fix (iter_listf (rev listf))
(iter_listf_is_monotone (rev listf) listf_monotone)
(bottom PA)
(bottom_is_a_bottom PA
(iter_listf (rev listf) (bottom PA)))); Intros.
Intuition.
Unfold lfp.
Case (iter_fix (iter_listf (rev listf))
(iter_listf_is_monotone (rev listf) listf_monotone)
(bottom PA)
(bottom_is_a_bottom PA
(iter_listf (rev listf) (bottom PA)))); Intros.
Intuition.
Apply f_in_listf_prop3.
Auto.
Intros.
Apply H.
Rewrite <- (idempot_rev listf).
Apply in_rev; Auto.
Qed.
End fix_n.
End iter_fix.