Set Implicit Arguments.
Set Contextual Implicit.

Require Import Utf8.
Require Import Setoid.
Require Import Morphisms.
Require Export Relation_Definitions.
Require Import ImpAlg.Ens.
Require Import ImpAlg.Lattices.
Require Import ImpAlg.ImplicativeStructures.
Require Import ImpAlg.Lambda.
Require Import ImpAlg.Adequacy.

Class HeytingAlgebra `{BL:BoundedLattice} :=
{
    imp : X → X → X;
    imp_sup: ∀ a b, sup (fun x => a ⋀ x ≤ b) (imp a b);
}.

Hint Resolve imp_sup.

Class CompleteHeytingAlgebra `{CL:CompleteLattice} `{HA:@HeytingAlgebra _ _ _ CBL}.

Lemma imp_elim `{HA:HeytingAlgebra}:
  ∀ a b x, a ⋀ x ≤ b → x ≤ imp a b.
Proof.
  intros a b x H.
  now apply imp_sup.
Qed.

Lemma imp_self `{HA:HeytingAlgebra}:
  ∀ a b, a ⋀ imp a b ≤ b.
Proof.
  intros a b.
  now apply imp_sup.
Qed.


Lemma imp_intro `{HA:HeytingAlgebra}:
  ∀ a b, (∀ y , (∀ x, a ⋀ x ≤ b → x ≤ y) → imp a b ≤ y).
Proof.
  intros a b x H.
  apply H.
  apply imp_self.
Qed.

Lemma imp_lub `{HA:HeytingAlgebra}:
 ∀ a b, lub (fun x => a ⋀ x ≤ b) (imp a b).
Proof.
  intros a b.
  apply lub_elim_intro.
  split.
  - apply imp_elim.
  - apply imp_intro.
Qed.

Lemma imp_adj `{HA:HeytingAlgebra}:
    ∀a b c, a ⋀ c ≤ b <-> a ≤ imp c b.
Proof.
  intros a b c;split;intro H.
  - apply imp_elim. now rewrite meet_commutative.
  - apply ord_trans with ((imp c b) ⋀ c).
    + now apply meet_mon_l.
    + rewrite meet_commutative. apply imp_self.
Qed.

Lemma imp_mon_l `{HA:HeytingAlgebra}:
  ∀ a a' b, a ≤ a' → (imp a' b) ≤ imp a b.
Proof.
  intros.
  apply imp_intro.
  intros x Hx.
  apply imp_elim.
  apply (@ord_trans _ _ _ (a'⋀x));intuition.
  now apply meet_mon_l.
Qed.

Lemma imp_mon_r `{HA:HeytingAlgebra}:
  ∀ a b b', b ≤ b' → (imp a b) ≤ imp a b'.
Proof.
  intros.
  apply imp_intro.
  intros x Hx.
  apply imp_elim.
  apply (@ord_trans _ _ _ b);intuition.
Qed.

Lemma imp_is_join `{CHA:CompleteHeytingAlgebra}:
   ∀ a b, imp a b = join_set (fun x => a ⋀ x ≤ b).
Proof.
  intros a b.
  apply lub_unique with (λ x : X, a ⋀ x ≤ b);intuition.
  - apply imp_lub.
  - apply join_set_lub.
Qed.

Lemma imp_meet `{CHA:CompleteHeytingAlgebra}:
  ∀ a B, imp a (meet_set B) = meet_set (fun x => ∃b, B b ∧ x = imp a b).
Proof.
  intros a B.
  rewrite imp_is_join.
  apply ord_antisym.
  - apply meet_intro;intros x (b,(Hb,Hx));subst.
    apply join_intro;intros.
    apply imp_elim.
    apply (ord_trans _ (⊓ B));intuition.
  - apply join_elim.
    apply meet_intro. intros.
    rewrite meet_commutative.
    apply imp_adj.
    apply meet_elim.
    now exists x.
Qed.

Hint Resolve imp_elim imp_self imp_intro imp_adj imp_lub imp_mon_l imp_mon_r imp_meet.

Global Instance CHA_IS `{CHA:CompleteHeytingAlgebra}:ImplicativeStructure:={arrow:= imp}.
Proof. apply imp_mon_l. apply imp_mon_r. apply imp_meet. Defined.

Lemma app_CHA `{CHA:CompleteHeytingAlgebra}: ∀ a b, (@app _ _ _ _ CHA_IS a b) = a ⋀ b.
Proof.
intros.
apply ord_antisym.
- apply adjunction. apply imp_adj. reflexivity.
- apply meet_intro. intros x H. now apply imp_adj.
Qed.