Set Implicit Arguments.
Unset Strict Implicit.
Require Export Setoid Morphisms.
Require Export Coq.Program.Basics.
From Undecidability.FOL Require Import FullSyntax Heyting.Heyting.

Structure HeytingMorphism (HA1 HA2 : HeytingAlgebra) (F : HA1 -> HA2) : Type :=
  {
    F_inj : forall u v, F u = F v -> u = v ;
    F_mono : forall u v, u <= v -> F u <= F v ;
      
    F_bot : F Bot = Bot ;
    F_meet : forall u v, F (Meet u v) = Meet (F u) (F v) ;
    F_join : forall u v, F (Join u v) = Join (F u) (F v) ;
    F_impl : forall u v, F (Impl u v) = Impl (F u) (F v) ;

    F_inf : forall P u, is_inf P u -> is_inf (fun v => forall z, v = F z -> P z) (F u) ;
    F_sup : forall P u, is_sup P u -> is_sup (fun v => forall z, v = F z -> P z) (F u) ;
  }.

Section MacNeille.

  Context { HA : HeytingAlgebra }.


  Definition hset := HA -> Prop.
  Implicit Type X Y : hset.

  Definition hset_elem x X :=
    X x.

  Notation "x ∈ X" := (hset_elem x X) (at level 70).

  Definition hset_sub X Y :=
    forall x, x ∈ X -> x ∈ Y.

  Notation "X ⊆ Y" := (hset_sub X Y) (at level 70).

  Definition hset_equiv X Y :=
    X ⊆ Y /\ Y ⊆ X.

  Notation "X ≡ Y" := (hset_equiv X Y) (at level 70).

  Global Instance hset_equiv_equiv :
    Equivalence hset_equiv.
  Proof.
    firstorder.
  Qed.

  Global Instance hset_elem_proper x :
    Proper (hset_equiv ==> iff) (hset_elem x).
  Proof.
    firstorder.
  Qed.

  Global Instance hset_sub_proper :
    Proper (hset_equiv ==> hset_equiv ==> iff) hset_sub.
  Proof.
    firstorder.
  Qed.

  Definition lb X :=
    fun y => forall x, x ∈ X -> y <= x.

  Global Instance lb_proper :
    Proper (hset_equiv ==> hset_equiv) lb.
  Proof.
    firstorder.
  Qed.

  Definition ub X :=
    fun y => forall x, x ∈ X -> x <= y.

  Global Instance ub_proper :
    Proper (hset_equiv ==> hset_equiv) ub.
  Proof.
    firstorder.
  Qed.

  Lemma lu_sub X :
    X ⊆ lb (ub X).
  Proof.
    firstorder.
  Qed.

  Lemma lu_idem X :
    lb (ub (lb (ub X))) ≡ lb (ub X).
  Proof.
    split.
    - firstorder.
    - apply lu_sub.
  Qed.

  Definition normal X :=
    lb (ub X) ⊆ X.

  Global Instance normal_proper :
    Proper (hset_equiv ==> iff) normal.
  Proof.
    intros X Y H. unfold normal. now rewrite H.
  Qed.

  Lemma lb_normal X :
    normal (lb X).
  Proof.
    firstorder.
  Qed.

  Definition dclosed X :=
    forall x y, x ∈ X -> y <= x -> X y.

  Lemma normal_dclosed X :
    normal X -> dclosed X.
  Proof.
    intros H x y H1 H2. apply H.
    intros z H3. rewrite H2. now apply H3.
  Qed.

  Lemma normal_bot X :
    normal X -> X Bot.
  Proof.
    intros H. apply H. intros x _. apply Bot1.
  Qed.



  Definition hset_bot : hset :=
    fun x => x <= Bot.

  Lemma hset_bot_normal :
    normal hset_bot.
  Proof.
    intros x H. apply H. intros y H'. apply H'.
  Qed.

  Definition hset_meet X Y : hset :=
    fun x => x ∈ X /\ x ∈ Y.

  Global Instance hset_meet_proper :
    Proper (hset_equiv ==> hset_equiv ==> hset_equiv) hset_meet.
  Proof.
    firstorder.
  Qed.

  Lemma hset_meet_normal X Y :
    normal X -> normal Y -> normal (hset_meet X Y).
  Proof.
    intros H1 H2 x H. split.
    - apply H1. firstorder.
    - apply H2. firstorder.
  Qed.

  Definition hset_join X Y : hset :=
    lb (ub (fun x => x ∈ X \/ x ∈ Y)).

  Global Instance hset_join_proper :
    Proper (hset_equiv ==> hset_equiv ==> hset_equiv) hset_join.
  Proof.
    firstorder.
  Qed.

  Lemma hset_join_normal X Y :
    normal (hset_join X Y).
  Proof.
    firstorder.
  Qed.

  Lemma ub_join X Y :
    ub (hset_join X Y) ≡ hset_meet (ub X) (ub Y).
  Proof.
    firstorder.
  Qed.

  Definition hset_inf P : hset :=
    fun x => forall X, P X -> x ∈ X.

  Lemma hset_inf_normal P :
    (forall X, P X -> normal X) -> normal (hset_inf P).
  Proof.
    intros H x Hx X HX. apply H; firstorder.
  Qed.

  Definition hset_impl X Y : hset :=
    fun x => forall y, y ∈ X -> Meet x y ∈ Y.

  Global Instance hset_impl_proper :
    Proper (hset_equiv ==> hset_equiv ==> hset_equiv) hset_impl.
  Proof.
    firstorder.
  Qed.

  Lemma hset_impl_equiv X Y :
    hset_impl X Y ≡ hset_inf (fun Z => exists x, x ∈ X /\ Z ≡ (fun y => Meet y x ∈ Y)).
  Proof.
    split.
    - intros z Hz Z [x[Hx ->] ]. now apply Hz.
    - intros z H y Hy. apply H.
      exists y. split; trivial. reflexivity.
  Qed.

  Lemma hset_impl_normal X Y :
    normal Y -> normal (hset_impl X Y).
  Proof.
    intros HY. rewrite hset_impl_equiv. apply hset_inf_normal.
    intros Z [x[Hx ->] ]. intros z Hz. unfold hset_elem at 1.
    apply HY. intros y Hy. apply Impl1.
    assert (H : Impl x y ∈ ub (fun y : HA => Meet y x ∈ Y)).
    - intros a. unfold hset_elem at 1. intros H.
      apply Impl1. now apply Hy.
    - firstorder.
  Qed.


  Lemma hset_bot1 X :
    normal X -> hset_bot ⊆ X.
  Proof.
    intros H x Hx. apply H. intros y Hy.
    unfold hset_bot in Hx. rewrite Hx.
    apply Bot1.
  Qed.

  Lemma hset_meet1 X Y Z :
    Z ⊆ X /\ Z ⊆ Y <-> Z ⊆ (hset_meet X Y).
  Proof.
    firstorder.
  Qed.

  Lemma hset_join1 X Y Z :
    normal Z -> X ⊆ Z /\ Y ⊆ Z <-> (hset_join X Y) ⊆ Z.
  Proof.
    intros HZ. split.
    - intros [H1 H2] x Hx. apply HZ. firstorder.
    - firstorder.
  Qed.

  Lemma hset_impl1 X Y Z :
    normal X -> normal Y -> normal Z -> hset_meet Z X ⊆ Y <-> Z ⊆ hset_impl X Y.
  Proof.
    intros HX HY HZ. split.
    - intros H x Hx y Hy. apply H. split.
      + eapply (normal_dclosed HZ); eauto.
      + eapply (normal_dclosed HX); eauto.
    - intros H x [H1 H2]. specialize (H x H1 x H2).
      eapply (normal_dclosed HY); eauto. now apply Meet1.
  Qed.

  Lemma hset_inf1 (P : hset -> Prop) X :
    (forall Y, P Y -> X ⊆ Y) <-> X ⊆ (hset_inf P).
  Proof.
    firstorder.
  Qed.


  Definition completion_algebra : HeytingAlgebra.
  Proof.
    unshelve eapply (@Build_HeytingAlgebra (sig normal)).
    - intros X Y. exact (proj1_sig X ⊆ proj1_sig Y).
    - exists hset_bot. apply hset_bot_normal.
    - intros [X HX] [Y HY]. exists (hset_meet X Y).
      now apply hset_meet_normal.
    - intros [X HX] [Y HY]. exists (hset_join X Y).
      now apply hset_join_normal.
    - intros [X HX] [Y HY]. exists (hset_impl X Y).
      now apply hset_impl_normal.
    - intros [X HX]. firstorder.
    - intros [X HX] [Y HY] [Z HZ]. firstorder.
    - intros [X HX]. now apply hset_bot1.
    - intros [X HX] [Y HY] [Z HZ]. now apply hset_meet1.
    - intros [X HX] [Y HY] [Z HZ]. now apply hset_join1.
    - intros [X HX] [Y HY] [Z HZ]. now apply hset_impl1.
  Defined.

  Definition completion_calgebra : CompleteHeytingAlgebra.
  Proof.
    unshelve eapply (@Build_CompleteHeytingAlgebra completion_algebra).
    - intros P. exists (hset_inf (fun X => exists H : normal X, P (exist _ X H))).
      apply hset_inf_normal. intros X [HX _]. assumption.
    - intros P [X HX]. cbn. rewrite <- hset_inf1. split.
      + intros H Y [HY HP]. now apply H in HP.
      + intros H [Y HY] HP. apply H. now exists HY.
  Defined.


  Definition down x :=
    fun y => y <= x.

  Lemma down_normal x :
    normal (down x).
  Proof.
    intros y H. apply H.
    intros z H'. apply H'.
  Qed.
  #[local]
  Hint Resolve down_normal : core.

  Definition embed x : completion_algebra :=
    exist normal (down x) (@down_normal x).

  Lemma down_inj x y :
    down x ⊆ down y -> x <= y.
  Proof.
    intros H. apply H. unfold down, hset_elem. reflexivity.
  Qed.

  Lemma down_mono x y :
    x <= y -> down x ⊆ down y.
  Proof.
    intros H z Hz. unfold down, hset_elem in *. now rewrite Hz.
  Qed.

  Lemma down_bot :
    down Bot ≡ hset_bot.
  Proof.
    firstorder.
  Qed.

  Lemma down_top :
    down Top ≡ hset_impl hset_bot hset_bot.
  Proof.
    split.
    - apply hset_impl1; eauto using down_normal. firstorder.
    - intros x _. apply Impl1. apply Meet3.
  Qed.

  Lemma down_meet x y :
    down (Meet x y) ≡ hset_meet (down x) (down y).
  Proof.
    split.
    - intros z H. apply Meet1, H.
    - intros z H. apply Meet1, H.
  Qed.

  Lemma down_join x y :
    down (Join x y) ≡ hset_join (down x) (down y).
  Proof.
    split.
    - intros z H. apply hset_join_normal; eauto.
      intros u Hu. apply ub_join in Hu as [H1 H2].
      rewrite H. apply Join1. split.
      + apply H1. apply Rref.
      + apply H2. apply Rref.
    - intros z H. apply H. intros u [Hu|Hu].
      + rewrite Hu. apply Join2.
      + rewrite Hu. apply Join3.
  Qed.

  Lemma down_impl x y :
    down (Impl x y) ≡ hset_impl (down x) (down y).
  Proof.
    split.
    - intros z Hz u Hu. apply Impl1 in Hz.
      unfold down, hset_elem. now rewrite (Meet_left z Hu).
    - intros z Hz. apply Impl1. apply Hz. apply Rref.
  Qed.

  Lemma down_inf (P : HA -> Prop) x x0 :
    is_inf P x -> P x0 -> down x ≡ hset_inf (fun X => exists x, X = down x /\ P x).
  Proof.
    intros H. split.
    - intros y Hy X [z [-> Hz] ]. now apply (H y).
    - intros y Hy. unfold hset_elem, down. rewrite <- (H y).
      intros z Hz. apply Hy. now exists z.
  Qed.

End MacNeille.

Notation "x ∈ X" := (hset_elem x X) (at level 70).
Notation "X ⊆ Y" := (hset_sub X Y) (at level 20).
Notation "X ≡ Y" := (hset_equiv X Y) (at level 70).