Lvc.Equiv.Tower2

Require Import Util Option AllInRel Get Setoid.
Require Export paco2.
Require Import Coq.Logic.FunctionalExtensionality ClassicalFacts.

Axiom propositional_extensionality : prop_extensionality.

Notation "p =2= q" :=
  (∀ x0 x1, p x0 x1 ↔ (q x0 x1:Prop))
    (at level 50, no associativity).

Lemma pred2_extensionality A B (R R' : A → B → Prop)
  : R =2= R' → R = R'.
Proof.
  intros.
  do 2 (eapply functional_extensionality; intros).
  eapply propositional_extensionality. eauto.
Qed.

Set Implicit Arguments.

Section Tower2.
  Variables A B : Type.
  Variable f : (A → B → Prop) → (A → B → Prop).

  Definition inf2 I (F: I → A → B → Prop) : A → B → Prop :=
    fun a b ⇒ ∀ i:I, F i a b.

  Inductive T2 : (A → B → Prop) → Prop :=
  | T2_step R : T2 R → T2 (f R)
  | T2_lim I (F : I → A → B → Prop)
    : (∀ i, T2 (F i)) → T2 (inf2 F).

  Definition companion2 (R : A → B → Prop) : A → B → Prop :=
    fun a b ⇒ ∀ S, T2 S → R <2= S → S a b.

  Notation "'㚘'" := companion2 (at level 0).

  Lemma T_companion2 x : T2 (companion2 x).
    repeat (eapply T2_lim; intros).
    eauto.
  Qed.

  Lemma companion2_monotone : monotone2 companion2.
    hnf; intros. hnf; intros.
    eapply IN; eauto.
  Qed.

  Lemma companion2_inc R : R <2= companion2 R.
    intros; hnf; eauto.
  Qed.

  Lemma companion2_idem x : companion2 (companion2 x) = companion2 x.
    eapply pred2_extensionality; split.
    - intros H; eapply H; eauto using T_companion2.
    - eapply companion2_inc.
  Qed.

  Lemma companion2_img x : T2 x → companion2 x = x.
    intros. eapply pred2_extensionality.
    split; intros; eauto using companion2_inc.
    - eapply H0; eauto.
  Qed.

  Definition inf2_closed (P: (A → B → Prop) → Prop) :=
    ∀ I (F : I → A → B → Prop),
      (∀ i, P (F i)) → P (inf2 F).

  Theorem tower_ind2 P
    : inf2_closed P →
      (∀ x, P (companion2 x) → P (f (companion2 x))) →
      ∀ x, P (companion2 x).
  Proof.
    intros.
    do 3 (eapply H; intros).
    clear x i1.
    induction i0; eauto.
    rewrite <- (companion2_img i0).
    eapply H0. rewrite companion2_img; eauto.
  Qed.

  Lemma companion2_fold R
    : monotone2 f → f (companion2 R) <2= companion2 R.
  Proof.
    intro.
    eapply tower_ind2.
    - hnf; intros. hnf; intros. eauto.
    - intros. eapply H; eauto.
  Qed.

  Lemma companion2_unfold
    : companion2 bot2 <2= f (companion2 bot2).
  Proof.
    intros. eapply PR; intros.
    - econstructor 1. eapply T_companion2.
    - isabsurd.
  Qed.

  Section UptoLemma2.
    Variable g : (A → B → Prop) → (A → B → Prop).
    Hypothesis gP : monotone2 g.

    Lemma upto2 :
      (∀ x, g (companion2 x) <2= companion2 x → g (f (companion2 x)) <2= f (companion2 x)) →
      (∀ x, g (companion2 x) <2= companion2 x).
    Proof.
      intros H1 H2.
      eapply tower_ind2.
      - intros; hnf; intros; eauto.
        hnf; eauto.
      - intros; eauto.
    Qed.

    Lemma upto_below2 :
      (∀ x, g (companion2 x) <2= companion2 x) → g <3= companion2.
    Proof.
      intros H1 r; intros.
      eapply H1. eapply gP; eauto.
      eapply companion2_inc.
    Qed.

    Lemma upto_char2 :
      monotone2 f →
      g <3= companion2 →
      ∀ x, g (companion2 x) <2= companion2 x → g (f (companion2 x)) <2= f (companion2 x).
    Proof.
      intros gM H1 r H2; intros.
      eapply H1; eauto.
      econstructor 1. eapply T_companion2.
    Qed.
  End UptoLemma2.
End Tower2.