# semantics.tower.tower

Require Import base ord tower.tarski tower.associated_closure.

Section Tower.
Variable (X : clat) (f : X -> X).
Implicit Types (x y z : X).

## The tower for f

Inductive T : Pred X :=
| T_step x : T x -> T (f x)
| T_lim I (F : I -> X) : (forall i, T (F i)) -> T (inf F).

## The double induction principle

Section DoubleInd.
Variable (R : X -> X -> Prop).
Hypothesis step : forall x y, T x -> T y -> R x y -> R y x -> R x (f y).
Hypothesis limit : forall I (F : I -> X) x, T x ->
(forall i, T (F i)) -> (forall i, R x (F i)) -> R x (inf F).

Lemma T_ind2 x y :
T x -> T y -> R x y.
Proof with eauto.
move=> tx ty; elim: ty x tx => {y} [x tx ih y ty|]...
apply: step... elim: ty...
Qed.
End DoubleInd.

Hypothesis f_mono : monotone f.

Lemma tower_dec x : T x -> f x x.
Proof.
elim=> {x}[x _|I F _ ih]. exact: mono.
focus=> i. rewrite -ih. apply: mono. exact: allE.
Qed.

## The companion for f

Definition t x := y | T y /\ (x y), y.

Lemma T_t x : T (t x).
Proof. apply: T_lim => i. by apply: T_lim => -[]. Qed.

Global Instance t_closure : is_closure t.
Proof.
split=> [<-{y}|le_x_ty]. rewrite/t. by focus=> y [].
apply: allEc le_refl. split=> //. exact: T_t.
Qed.

Global Instance t_monotone : monotone t.
Proof. exact _. Qed.

Lemma t_inc x : x t x.
Proof. exact: closure_inc. Qed.

Lemma t_idem x : t (t x) = t x.
Proof. exact: closure_idem. Qed.

Lemma t_img x : T x <-> t x = x.
Proof.
split=> [tx|<-]; last by exact: T_t.
apply: closure_stable. exact: allEc le_refl.
Qed.

Lemma t_f x : f (t x) = t (f (t x)).
Proof.
apply: le_eq. exact: t_inc. apply: allEc le_refl. split=> //.
apply: T_step. exact: T_t.
Qed.

Theorem tower_induction (P : X -> Prop) :
inf_closed P ->
(forall x, P (t x) -> P (f (t x))) ->
(forall x, P (t x)).
Proof.
move=> h1 h2 x. move: (t x) (T_t x) => {x} x. elim=> {x}[x tx ih|I F _]; last first.
exact: h1. move/t_img: tx => eqn. rewrite -eqn. apply: h2. by rewrite eqn.
Qed.

Lemma t_gfp :
t = gfp f.
Proof.
apply: le_eq.
- apply: gfp_below_coind => //. rewrite t_f. exact: mono.
- apply: tower_induction. move=> I F ih. focus=> i. exact: ih.
move=> x le. rewrite -gfpE. exact: mono.
Qed.

Section UptoLemma.
Variable g : X -> X.
Hypothesis g_mono : monotone g.

Lemma decreasing_is_below_companion :
(forall x, g (t x) t x) -> g t.
Proof.
move=> dec x. rewrite {1}[x]t_inc. exact: dec.
Qed.

Lemma below_companion_to_upto :
g t -> (forall x, g (t x) t x -> g (f (t x)) f (t x)).
Proof. move=> le_g_t x _. by rewrite le_g_t -t_f. Qed.

Lemma upto_lemma :
(forall x, g (t x) t x -> g (f (t x)) f (t x)) ->
forall x, g (t x) t x.
Proof.
move=> h x. apply: (tower_induction (P := fun x => g x x)) => //.
move=> I F ih. focus=> i. rewrite -ih. apply: mono. exact: allE.
Qed.
End UptoLemma.

Lemma t_fdec x :
f (t x) t x.
Proof.
apply: upto_lemma => {x} x. exact: mono.
Qed.

Definition compatible (g : X -> X) :=
monotone g /\ forall x, g (f x) f (g x).

Lemma t_compat x :
t (f x) f (t x).
Proof.
rewrite t_f. apply: mono. apply: mono. exact: t_inc.
Qed.

Lemma t_greatest_compatible :
t = g | compatible g, g.
Proof.
apply: le_eq.
- apply: exIc (t) _ le_refl. split=>[|x]. exact: t_monotone. exact: t_compat.
- focus=> g [g_mono g_compat]. hnf=> x. apply: decreasing_is_below_companion.
apply: upto_lemma => {x} x h. rewrite g_compat. apply: mono. exact: h.
Qed.

Definition respectful (g : X -> X) :=
forall x y, x y -> x f y -> g x f (g y).

Lemma t_greatest_respectful :
t = g | respectful g, g.
Proof.
apply: le_eq.
- apply: exIc (t) _ le_refl => x y le_x_y ->. exact: t_compat.
- focus=> g g_resp. have->: g mceil g. move=> x. exact: exIc (x) _ _.
apply: decreasing_is_below_companion. apply: upto_lemma.
move=> y h /=. focus=> x le_x_fty. rewrite (g_resp x (t y)) //.
+ apply: mono. rewrite -{2}h. exact: exIc (t y) _ _.
+ rewrite le_x_fty. exact: t_fdec.
Qed.

Section UptoLemmaCharacterization.
Variable tt : X -> X.
Hypothesis upto :
forall g : X -> X,
monotone g ->
(forall x, g (tt x) tt x -> g (f (tt x)) f (tt x)) ->
forall x, g (tt x) tt x.

Lemma upto_to_tower_induction (P : Pred X) :
inf_closed P ->
(forall x, P x -> P (f x)) ->
forall x, P (tt x).
Proof.
move=> h1 h2 x. apply/(@closure_of_image X P h1). apply: upto.
- move=> {x} x y le_x_y. rewrite/closure_of. focus => z [pz le_y_z].
apply: allEc (z) _ le_refl. split=> //. by rewrite le_x_y.
- move=> {x} x l1. apply/closure_of_image => //. apply: h2. exact/closure_of_image.
Qed.
End UptoLemmaCharacterization.
End Tower.