# The Dual Companion Construction

Require Import prelim companion.

## Least Fixed Points

Section TarskiMu.
Variables (A : clat) (f : A -> A).
Hypothesis (fP : monotone f).

Let B := Eval hnf in reverse_clat A.

Definition mu := \inf_(x | f x <= x) x.

Lemma mu_tarski x : f x <= x -> mu <= x.
Proof. exact: (@nu_tarski B). Qed.

Lemma mu_fp : f mu = mu.
Proof. exact: (@nu_fp B). Qed.

End TarskiMu.

## Dual Companions (Corollary 35)

Definition sup_closed {X : clat} (P : Pred X) :=
forall T (F : T -> X), (forall i, P (F i)) -> P (sup F).

Section TowerMu.
Variable (A : clat) (f : A -> A).
Implicit Types (x y z : A).
Context {fP : monotone f}.
Let B := Eval hnf in reverse_clat A.

Definition l (x : A) : A := @t B f x.

### Corollary 35 (a)

Global Instance l_kernel : is_kernel l.
Proof. move=>??; exact: (@t_closure B). Qed.

Global Instance l_monotone : monotone l. exact _. Qed.

Lemma l_dec x : l x <= x. exact: (@t_inc B). Qed.
Lemma l_idem x : l (l x) = l x. exact: (@t_idem B). Qed.

### Corollary 35 (b)

Lemma l_f x : f (l x) = l (f (l x)). exact: (@t_f B). Qed.

### Corollary 35 (c)

Lemma ind (P : Pred A) :
sup_closed P ->
(forall x, P (l x) -> P (f (l x))) ->
forall x, P (l x).
Proof. exact: (@tower_ind B). Qed.

### Corollary 35 (d)

Section UptoLemma.
Variable g : A -> A.
Hypothesis gP : monotone g.

Lemma ind_upto :
(forall x, l x <= g (l x) -> f (l x) <= g (f (l x))) ->
(forall x, l x <= g (l x)).
Proof. exact: (@upto B). Qed.

Lemma ind_upto_above :
(forall x, l x <= g (l x)) -> l <= g.
Proof. exact: (@upto_below B). Qed.

Lemma ind_upto_char :
l <= g ->
forall x, l x <= g (l x) -> f (l x) <= g (f (l x)).
Proof. exact: (@upto_char B). Qed.
End UptoLemma.

### Corollary 35 (e)

Lemma mu_l : mu f = l top.
Proof. exact: (@nu_t B). Qed.

### Corollary 35 (f)

Lemma l_unfold x : l x <= f (l x).
Proof. exact: (@t_fold B). Qed.

End TowerMu.