Library CoLoR.Util.Relation.Tarski

CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2013-05-10

Knaster-Tarski theorem


Set Implicit Arguments.


We assume given a set A equipped with a transitive relation <=

and a relation == containing inter_transp <= (reflexivity is not needed).

Section tarski.

  Variables (A : Type) (le eq : relation A).

  Infix "<=" := le (at level 70).
  Infix "==" := eq (at level 70).

  Variable eq_ok : forall x y, x <= y -> y <= x -> x == y.

Definitions of the notions of (least) upper/(greatest) lower bound.

  Definition is_sup a (P : set A) := forall x, P x -> x <= a.

  Definition is_inf a (P : set A) := forall x, P x -> a <= x.

  Definition is_lub a P := is_sup a P /\ forall a', is_sup a' P -> a <= a'.

  Definition is_glb a P := is_inf a P /\ forall a', is_inf a' P -> a' <= a.

lub's and glb's are unique modulo ==.

  Lemma lub_is_uniq : forall P a b, is_lub a P -> is_lub b P -> a == b.

  Lemma glb_is_uniq : forall P a b, is_glb a P -> is_glb b P -> a == b.

Definition of the least and greatest fixpoints of a monotone function f, when one can compute a lub and glb for every subset of A (A is a complete lattice).

  Variables (lub glb : set A -> A)
    (lub_ok : forall P, is_lub (lub P) P)
    (glb_ok : forall P, is_glb (glb P) P).

  Section lfp.

    Variables (le_trans : Transitive le)
              (f : A -> A) (f_mon : Proper (le ==> le) f).

    Definition lfp := glb (fun x => f x <= x).

    Lemma lfp_eq : lfp == f lfp.

    Definition gfp := lub (fun x => x <= f x).

    Lemma gfp_eq : gfp == f gfp.

The least fixpoint can be reached by transfinite iteration.


    Inductive K : set A :=
    | Kf x : K x -> K (f x)
    | Klub S : S [<=] K -> K (lub S).


    Section K_ind.

      Variables (P : A -> Prop) (Pf : forall x, K x -> P x -> P (f x))
                (Plub : forall S, S [<=] K -> S [<=] P -> P (lub S)).

      Fixpoint K_ind y (h : K y) : P y :=
        match h in K y return P y with
        | Kf g => Pf g (K_ind g)
        | Klub QK => Plub QK (fun x g => K_ind (QK x g))
        end.

    End K_ind.

    Lemma lfp_eq_lub : eq (lub K) lfp.

    Lemma lfp_ind (P : A -> Prop) :
      Proper (eq ==> impl) P ->
      (forall x, P x -> P (f x)) -> (forall S, S [<=] P -> P (lub S)) -> P lfp.

  End lfp.

Extensionality of fixpoints: two fixpoints are equivalent modulo == if their functions are pointwise equivalent modulo ==, == is reflexive, <= is compatible with ==, and two glb's (resp. lub's) are equivalent modulo == if their arguments are equivalent modulo SetUtil.equiv.

  Variables (eq_refl : Reflexive eq)
    (le_eq : Proper (eq ==> eq ==> iff) le)
    (glb_equiv : Proper (equiv ==> eq) glb)
    (lub_equiv : Proper (equiv ==> eq) lub).


  Lemma lfp_ext : forall f g, (forall x, f x == g x) -> lfp f == lfp g.

  Lemma gfp_ext : forall f g, (forall x, f x == g x) -> gfp f == gfp g.

End tarski.


Example of complete lattice: the powerset of some set X.


Section powerset.

  Variable X : Type.

  Notation A := (set X).
  Notation set_le := (@subset X).
  Notation set_eq := (@equiv X).

  Global Instance set_le_trans : Transitive set_le.


  Lemma set_eq_ok : forall x y : A, x [<=] y -> y [<=] x -> x [=] y.

  Section lub.

    Variable P : set A.

    Definition set_lub : A := fun x => exists S, P S /\ S x.

    Lemma set_lub_ok : is_lub set_le set_lub P.

    Definition set_glb : A := fun x => forall S, P S -> S x.

    Lemma set_glb_ok : is_glb set_le set_glb P.

  End lub.

  Definition set_lfp := lfp set_le set_glb.
  Definition set_gfp := gfp set_le set_lub.

  Definition set_lfp_eq := lfp_eq set_eq_ok set_glb_ok set_le_trans.
  Definition set_gfp_eq := gfp_eq set_eq_ok set_lub_ok set_le_trans.

  Global Instance set_eq_refl : Reflexive set_eq.


  Global Instance set_le_eq : Proper (set_eq ==> set_eq ==> iff) set_le.


  Global Instance set_glb_equiv : Proper (equiv ==> set_eq) set_glb.


  Global Instance set_lub_equiv : Proper (equiv ==> set_eq) set_lub.


  Definition set_lfp_ext := lfp_ext set_eq_refl set_le_eq set_glb_equiv.
  Definition set_gfp_ext := lfp_ext set_eq_refl set_le_eq set_lub_equiv.

End powerset.


Least fixpoint over a sigma type.


Section sig.

  Variables (A : Type) (le eq : relation A)
            (eq_ok : forall x y, le x y -> le y x -> eq x y)
            (lub glb : set A -> A)
            (lub_ok : forall S, is_lub le (lub S) S)
            (glb_ok : forall S, is_glb le (glb S) S)
            (P : A -> Prop).

  Notation B := (sig P).

  Notation pr1 := (@proj1_sig A P).
  Notation pr2 := (@proj2_sig A P).

  Definition le_sig := Rof le pr1.
  Definition eq_sig := Rof eq pr1.

  Lemma eq_sig_ok x y : le_sig x y -> le_sig y x -> eq_sig x y.

  Definition pr (R : set B) : set A := fun x => exists h : P x, R (exist h).

  Variable glb_prop : forall S : set A, (forall x, S x -> P x) -> P (glb S).

  Definition glb_sig (R : set B) : B.


  Lemma glb_sig_ok R : is_glb le_sig (glb_sig R) R.

  Variable lub_prop : forall S : set A, (forall x, S x -> P x) -> P (lub S).

  Definition lub_sig (R : set B) : B.


  Lemma lub_sig_ok R : is_lub le_sig (lub_sig R) R.

  Variable le_trans : Transitive le.

  Global Instance le_sig_trans : Transitive le_sig.


  Variables (f : A -> A) (f_prop : forall x, P x -> P (f x)).

  Definition lift (x : B) : B := exist (f_prop (pr2 x)).

  Variable f_mon : Proper (le ==> le) f.

  Lemma lift_mon : Proper (le_sig ==> le_sig) lift.

  Definition lfp_lift := pr1 (lfp le_sig glb_sig lift).

  Lemma lfp_lift_prop : P lfp_lift.

  Global Instance proj1_sig_eq : Proper (eq_sig ==> eq) pr1.


  Lemma lfp_lift_eq : eq lfp_lift (f lfp_lift).

End sig.