# semantics.tower.linear_tower

## Constructive linearity and well-foundedness

Section LinearTower.
Variable (X : llat) (f : X -> X).
Hypothesis f_mono : lmonotone f.

Local Notation T := (T f).

Lemma tower_f_linear x y :
T x -> T y -> ((y x) -> y f x) /\ ((f x y) -> x y).
Proof with eauto.
move: x y. apply: T_ind2.
- move=> x y tx ty _ [ih2L ih2R]; split=> lt_fy_x.
+ apply: mono. exact: ih2R.
+ apply: ih2L. exact: lmonoP.
- intros I F x _ _ ih; split.
+ case/lt_inf=> i lt_fi_x. case: (ih i) => /(_ lt_fi_x) h _. exact: allE h.
+ move=> lt_fx_F. focus=> i. case: (ih i) => ihL ihR.
apply: ihR. apply: lt_left lt_fx_F _. exact: allE.
Qed.

Lemma tower_linear_left x y :
T x -> T y -> (x y) -> x f y.
Proof.
move=> tx ty. by case: (tower_f_linear ty tx).
Qed.

Lemma tower_linear_right x y :
T x -> T y -> (f x y) -> x y.
Proof.
move=> tx ty. by case: (tower_f_linear tx ty).
Qed.

Lemma tower_linear x y :
T x -> T y -> (x y) -> x y.
Proof.
move=> tx ty lt_x_y. rewrite (tower_linear_left tx ty) //.
exact: tower_dec.
Qed.

(* no infinite ascending chain *)
Inductive acc_on {T} (P : T -> Prop) (R : T -> T -> Prop) (x : T) : Prop :=
| acc_on_i : (forall y, P y -> R x y -> acc_on P R y) -> acc_on P R x.

Lemma tower_wf x :
acc_on T (@ord_l_op X) x.
Proof.
constructor=> y ty _ {x}; move: y ty => x tx.
suff H: forall y, (x y) -> acc_on T (@ord_l_op X) y by exact: H le_refl.
elim: tx => {x}.
- move=> x tx ih y le_fx_y. constructor=> z tz lt_y_z.
apply: ih. case: (tower_f_linear tx tz) => _. apply.
exact: lt_right lt_y_z.
- move=> I F tF ih y le_x_y. constructor=> z tz lt_y_z.
have: inf F z by exact: lt_right lt_y_z.
case/lt_inf=> i /tower_linear le_Fi_z.
apply: (ih i). exact: le_Fi_z.
Qed.
End LinearTower.

## Classical well-orderedness

Section ClassicalTower.
Variable (X : clat) (f : X -> X).
Hypothesis f_mono : monotone f.
Variable xm : forall P : Prop, P \/ ~P.

Definition classic := [clat of X].
Implicit Types (x y z : classic).

Definition classical_lt x y := ~(y x).

Lemma classical_lt_left x y z :
classical_lt x y -> (y z) -> classical_lt x z.
Proof.
move=> h1 h2 h3. apply: h1. by rewrite h2.
Qed.

Lemma classical_lt_right x y z :
(x y) -> classical_lt y z -> classical_lt x z.
Proof.
move=> h1 h2 h3. apply: h2. by rewrite h3.
Qed.

Lemma classical_lt_inf I (F : I -> X) x :
classical_lt (inf F) x -> exists i, classical_lt (F i) x.
Proof.
move=> h. case: (xm (exists i, classical_lt (F i) x)) => // H.
case: h. focus=> i. case: (xm (x F i)) => // HH. case: H. by exists i.
Qed.

Canonical classical_llatMixin := LLatMixin classical_lt_left classical_lt_right classical_lt_inf.
Canonical classical_llat := Eval hnf in LLat classic classical_llatMixin.

Lemma classic_mono_to_lmono :
lmonotone (f : classic -> classic).
Proof.
constructor=> //= x y nle h. apply: nle. exact: mono.
Qed.

Lemma classical_tower_glue (x : X) : @T X f x -> @T classic f x.
Proof. elim; eauto using @T => *; exact: T_lim. Qed.
Hint Resolve classical_tower_glue.

Lemma classical_tower_linear x y :
T f x -> T f y -> (x y) \/ (y x).
Proof.
move=> tx ty. case: (xm (x y)). by left. right.
apply: (@tower_linear classical_llat f classic_mono_to_lmono y x); eauto.
Qed.

Lemma classical_tower_max I (F : I -> X) :
(forall i, T f (F i)) -> I -> exists k, is_ub F (F k).
Proof.
move=> h i0. move: (@tower_wf classical_llat f classic_mono_to_lmono (F i0)).
move eqn: (F i0) => j ac. elim: ac i0 eqn =>{j} /=x _ ih i eqn. subst.
case: (xm (exists j, ~(F j F i))) => H; last first.
- exists i => j. case: (xm (F j F i)) => // nle. case: H. by exists j.
- case: H => j ltj. apply: (ih (F j)). apply: classical_tower_glue. exact: h.
exact: ltj. reflexivity.
Qed.
End ClassicalTower.