Library CoLoR.Util.Relation.Tarski

CoLoR, a Coq library on rewriting and termination.
• 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.