Library Lattice


Require Import Wf.

Require Import List.

Require Export Poset.




Record Lattice (A : Set) : Type := lattice_constr

  {poset :> Poset A;

   join : A -> A -> A;

   join_bound1 : forall x y : A, order poset x (join x y);

   join_bound2 : forall x y : A, order poset y (join x y);

   join_least_bound :

    forall x y z : A, order poset x z -> order poset y z -> order poset (join x y) z;

   order_dec : forall x y : A, {order poset x y} + {~ order poset x y};

   bottom : A;

   bottom_is_a_bottom : forall x : A, order poset bottom x;

   top : A;

   top_is_top : forall x : A, order poset x top;

   acc_property : well_founded (fun x y => ~ eq poset y x /\ order poset y x)}.




Implicit Arguments order [A].

Implicit Arguments eq [A].

Implicit Arguments join [A].

Implicit Arguments order_refl [A].

Implicit Arguments order_antisym [A].

Implicit Arguments order_trans [A].

Implicit Arguments eq_refl [A].

Implicit Arguments eq_sym [A].

Implicit Arguments eq_trans [A].

Implicit Arguments join_bound1 [A].

Implicit Arguments join_bound2 [A].

Implicit Arguments join_least_bound [A].

Implicit Arguments order_dec [A].

Implicit Arguments bottom [A].

Implicit Arguments bottom_is_a_bottom [A].

Implicit Arguments top [A].

Implicit Arguments top_is_top [A].

Implicit Arguments acc_property [A].




Hint 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. 




Section Lattice_prop.




Variable A : Set.

Variable PA : Lattice A.




Lemma order_eq_order :

 forall 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 :

 forall 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 : forall x y : A, eq PA (join PA x y) (join PA y x).

auto.

Qed.




Lemma join_eq1 :

 forall 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 :

 forall 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 :

 forall 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 : forall x : A, eq PA (join PA (bottom PA) x) x.

intros; apply order_antisym; auto.

Qed.




Lemma join_bottom2 : forall x : A, eq PA x (join PA (bottom PA) x).

intros; apply order_antisym; auto.

Qed.




Fixpoint join_list (l : list A) : A :=

  match l with

  | nil => bottom PA

  | a :: q => join PA a (join_list q)

  end.




Lemma join_list_greater :

 forall (l : list A) (x : A), In x l -> order PA 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 A) (z : A),

 (forall x : A, In x l -> order PA x z) -> order PA (join_list l) z.

induction l; simpl in |- *; intuition.

Qed.




Inductive list_order : list A -> list A -> Prop :=

  | list_order_nil : list_order nil nil

  | list_order_cons :

      forall (x1 x2 : A) (l1 l2 : list A),

      order PA x1 x2 -> list_order l1 l2 -> list_order (x1 :: l1) (x2 :: l2).




Lemma list_order_join_list :

 forall l1 l2 : list A,

 list_order l1 l2 -> order PA (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.




Definition eq_dec (A:Set) (LA:(Lattice A)) : 

 forall x y : A, {eq LA x y} + {~ eq LA x y}.

intros.

case (order_dec LA x y); intros.

case (order_dec LA y x); intros.

left; auto.

right; red; intros; elim n ;auto.

right; red; intros; elim n ;auto.

Qed.




End Lattice_prop.




Implicit Arguments eq_dec [A].

Hint Resolve join_bottom1 join_bottom2 join_list_greater

  join_list_least_greater.




Section iter_fix.




  Variable set : Set.

  Variable PA : Lattice set.




 Let monotone (f : set -> set) :=

   forall 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 :=

   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 PA x (f x) ->

   {a : set | eq PA a (f a) /\ (exists n : nat, a = iter n x)}.

 Let order_acc x y := ~ eq PA y x /\ order PA 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 PA (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 PA 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 PA x (f x) -> forall n : nat, eq PA (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 PA (iter n (bottom PA)) (iter (S n) (bottom PA)) ->

 forall 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 :

 forall x : set,

 (exists n : nat, x = iter n (bottom PA)) ->

 eq PA x (f x) -> forall 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 :

 forall x : set, order PA (f x) x -> forall n : nat, order PA (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 PA (iter n (bottom PA)) (iter (S n) (bottom PA)) ->

 forall 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 :

 forall x : set,

 (exists n : nat, x = iter n (bottom PA)) ->

 eq PA x (f x) -> forall 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) /\ (forall y : set, eq PA y (f y) -> order PA lfp y).

unfold lfp in |- *;

 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 /\ (forall y : set, order PA (f y) y -> order PA lfp y).

unfold lfp in |- *;

 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 :=

   match l with

   | nil => fun x : set => x

   | f :: q => fun x : set => let y := iter_listf q x in join PA y (f y)

   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 join4; auto.

Qed.




Lemma f_in_listf_prop1 :

 forall (l : list (set -> set)) (x : set), order PA x (iter_listf l x).

induction l; simpl in |- *; intros; auto.

apply order_trans with (iter_listf l 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 PA (f x) (iter_listf l x).

induction l; simpl in |- *; 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 :

 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 PA (f x) x) ->

 order PA (iter_listf l x) x.

induction l; simpl in |- *; 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 : forall 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 : 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 PA (f lfp_list) lfp_list) /\

 (forall y : set,

  (forall 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 in |- *.

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 in |- *.

apply

 (iter_bottom_is_lifp (iter_listf (rev listf))

    (iter_listf_is_monotone (rev listf) listf_monotone)).

unfold lfp in |- *.

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 in |- *.

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 <- (rev_involutive listf).

apply in_rev; auto.

Qed.




End fix_n.




End iter_fix.
Index
This page has been generated by coqdoc