semantics.tower.linear_tower

Require Import base ord tower.tarski tower.associated_closure tower.tower tower.llat.

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.

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.