Set Implicit Arguments.
Set Contextual Implicit.

Require Import Utf8.
Require Import Setoid.
Require Import Morphisms.
Require Export Relation_Definitions.
Require Import Sets.Ensembles.
Require Import ImpAlg.Lattices.
Require Import ImpAlg.HeytingAlgebras.
Require Import ImpAlg.ImplicativeStructures.
Require Import ImpAlg.ImplicativeAlgebras.
Require Import ImpAlg.Adequacy.
Require Import ImpAlg.Combinators.

Class BooleanAlgebra `{BL:BoundedLattice} :=
{
    neg : X → X;

    meet_distributive: ∀ (a b c:X), meet a (join b c) = join (meet a b) (meet a c);
    join_distributive: ∀ (a b c:X), join a (meet b c) = meet (join a b) (join a c);
    meet_neg: ∀ a:X, meet a (neg a) = bot;
    join_neg: ∀ a:X, join a (neg a) = top;
}.

Hint Resolve top_max bot_min meet_distributive join_distributive join_neg meet_neg.
Notation "¬ a":=(neg a).

Class CompleteBooleanAlgebra `{CL:CompleteLattice} `{BA:@BooleanAlgebra _ _ _ CBL}.

Definition RevBooleanAlgebra `{BA:BooleanAlgebra}:=
    @Build_BooleanAlgebra _ _ _ RevBoundedLattice neg join_distributive meet_distributive join_neg meet_neg.

Definition RevCompleteBooleanAlgebra `{CBA:CompleteBooleanAlgebra}:=
    @Build_CompleteBooleanAlgebra _ _ _ RevCompleteLattice RevBooleanAlgebra.

Ltac dualityBA t:= apply (t _ _ _ _ RevBooleanAlgebra).
Ltac dualityCBA t:= apply (t _ _ _ _ _ RevCompleteBooleanAlgebra).

Lemma neg_complement `{BA:BooleanAlgebra}:
   ∀ (a b:X), (b = ¬ a) <-> (a ⋁ b = ⊤) /\ (a ⋀ b = ⊥).
Proof.
  intros a b;split.
  - intro H;subst;auto.
  - intros (Ha,Hb).
    rewrite <- (@meet_top_l _ _ _ BL).
    rewrite <- Ha.
    rewrite meet_commutative,meet_distributive.
    rewrite meet_commutative,meet_neg,join_bot_l.
    rewrite <- (@meet_top_r _ _ _ BL b) at 1.
    rewrite <- (join_neg a).
    rewrite meet_distributive.
    rewrite meet_commutative,Hb,join_bot_l,meet_commutative.
    reflexivity.
Qed.

Lemma neg_top `{BA:BooleanAlgebra}: (¬ ⊤) = ⊥.
Proof.
symmetry;apply neg_complement. split;auto.
Qed.

Lemma neg_bot `{BA:BooleanAlgebra}: (¬ ⊥) = ⊤.
Proof.
symmetry;apply neg_complement. split;auto.
Qed.

Lemma top_join `{CBA:CompleteBooleanAlgebra}: ⊤ = ⊔ (λ x:X, True).
Proof.
apply ord_antisym; auto.
Qed.

Lemma bot_meet `{CBA:CompleteBooleanAlgebra}: ⊥ = ⊓ (λ x:X, True).
Proof.
apply ord_antisym; auto.
Qed.

Lemma double_neg `{BA:BooleanAlgebra}:
  ∀a, (¬(¬a)) = a.
Proof.
intro a.
symmetry; apply neg_complement.
rewrite join_commutative,meet_commutative;intuition.
Qed.

Lemma neg_join `{BA:BooleanAlgebra}:
   ∀a b:X, (¬(a ⋁ b)) = (¬a) ⋀ (¬b).
Proof.
intros a b.
symmetry; apply neg_complement.
split.
- rewrite join_distributive.
  rewrite join_commutative at 1.
  rewrite <- join_associative, (join_commutative (¬a)), join_neg, join_top_l,meet_top_l.
  rewrite join_associative, join_neg,join_top_r.
  reflexivity.
- rewrite meet_commutative,meet_distributive.
  rewrite meet_commutative at 1.
  rewrite <- meet_associative, meet_neg, meet_bot_l, join_bot_l.
  rewrite meet_associative, (meet_commutative _ b), meet_neg, meet_bot_r.
  reflexivity.
Qed.

Lemma neg_meet `{BA:BooleanAlgebra}:
   ∀ a b,(¬(a ⋀ b)) = (¬a) ⋁ (¬b).
Proof.
dualityBA @neg_join.
Qed.

Lemma neg_mon `{BA:BooleanAlgebra}:
  ∀a b, a ≤ b → (¬b) ≤ ¬ a.
Proof.
  intros a b H.
  rewrite <- (@meet_top_r _ _ _ _ b).
  rewrite <- (join_neg a).
  rewrite meet_distributive, neg_join.
  apply consistent in H.
  rewrite meet_commutative in H.
  rewrite <- H.
  rewrite neg_meet, double_neg.
  rewrite meet_distributive.
  rewrite (meet_commutative (¬a) a), meet_neg,join_bot_r.
  apply meet_lb_l.
Qed.

Theorem meet_join_set `{CBA:CompleteBooleanAlgebra}:
  ∀ A b, (⊔ A) ⋀ b = ⊔ (fun x => ∃ a, A a ∧ x= a ⋀ b).
Proof.
intros A b.
symmetry.
apply (lub_unique (join_set_lub)).
split;unfold ub.
- intros u (a,(Ha,Hy));subst.
  apply meet_mon_l. intuition.
- intros u H.
  apply (ord_trans _ (u ⋀ b));auto.
  rewrite <- (@join_bot_r _ _ _ CBL (u ⋀ b)).
  rewrite <- (@meet_neg _ _ _ _ BA b).
  rewrite (meet_commutative u),<- meet_distributive,meet_commutative.
  apply meet_mon_r.
  apply join_intro.
  intros x Hx.
  rewrite <- (@meet_top_r _ _ _ CBL x).
  rewrite <- (@join_neg _ _ _ _ BA b).
  rewrite meet_distributive.
  apply (ord_trans _ (u ⋁ (x ⋀ ¬ b))).
  + apply join_mon_l. apply H. exists x. intuition.
  + apply join_mon_r. intuition.
Qed.

Theorem join_meet_set `{CBA:CompleteBooleanAlgebra}:
  ∀ A b, (⊓ A) ⋁ b = ⊓ (fun x => ∃ a, A a ∧ x= a ⋁ b).
Proof.
dualityCBA @meet_join_set.
Qed.

Lemma neg_meet_set `{CBA:CompleteBooleanAlgebra}:
  ∀ A, (¬ (⊓ A)) = ⊔ (image_set neg A).
Proof.
intro A.
symmetry; apply neg_complement.
split;apply ord_antisym;auto.
- rewrite join_meet_set.
  apply meet_intro.
  intros x (a,(Ha,Hx)).
  subst. unfold image_set.
  apply (ord_trans _ (a ⋁ ¬a)).
  + rewrite join_neg. auto.
  + apply join_mon_r. apply join_elim. now exists a.
- rewrite meet_commutative,meet_join_set.
  apply join_intro.
  unfold image_set.
  intros x (a,((b,(Hb,Hx)),Ha)).
  subst.
  apply (ord_trans _ ((¬b) ⋀ b)).
  + apply meet_mon_r. intuition.
  + rewrite meet_commutative,meet_neg; intuition.
Qed.

Lemma neg_join_set `{CBA:CompleteBooleanAlgebra}:
  ∀ A, (¬ (⊔ A)) = ⊓ (image_set neg A).
Proof.
dualityCBA @neg_meet_set.
Qed.

Global Instance BA_HA `{BA:BooleanAlgebra}:HeytingAlgebra:=
{imp:= fun x => fun y => (¬ x) ⋁ y}.
Proof.
intros a b.
split.
- intros c H.
  rewrite <- (@meet_top_r _ _ _ _ c).
  rewrite <- (join_neg a).
  rewrite meet_distributive.
  apply (ord_trans _ (b ⋁ (c ⋀ (¬ a)))).
  + rewrite meet_commutative. now apply join_mon_l.
  + rewrite join_commutative.
      apply join_mon_l,meet_lb_r.
- rewrite meet_distributive.
  rewrite meet_neg,join_bot_l.
  apply meet_lb_r.
Defined.

Global Instance CBA_CHA `{CBA:CompleteBooleanAlgebra}:CompleteHeytingAlgebra.

Global Instance CBA_IS `{CBA:CompleteBooleanAlgebra}:ImplicativeStructure:=
{arrow:= fun x => fun y => (¬ x) ⋁ y}.
Proof.
  - intros. now apply join_mon_l,neg_mon.
  - intros. now apply join_mon_r.
  - intros a B. rewrite join_commutative, join_meet_set.
    apply meet_same_set;split.
    + intros x (b,(Hb,Ha)).
      unfold arrow_set_r.
      exists b;subst;intuition.
    + intros x (b,(Hb,Ha)).
      unfold arrow_set_r.
      exists b;subst;intuition.
Defined.

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

Lemma BA_K `{CBA:CompleteBooleanAlgebra}: K = ⊤.
Proof.
unfold K. apply ord_antisym; auto.
do 2 auto_meet_intro. subst. unfold arrow in *. cbn. rewrite <- top_join.
now rewrite join_commutative,join_associative,join_neg,join_top_r.
Qed.

Lemma BA_S `{CBA:CompleteBooleanAlgebra}: S = ⊤.
Proof.
rewrite lambda_S.
apply ord_antisym;auto.
auto_meet_intro. unfold abs. rewrite arrow_meet.
auto_meet_intro. intros y [z [[b Hc] Hy]]. subst. do 2 rewrite arrow_meet.
auto_meet_intro. intros y [z [[c [[e He] Hd]] Hy]]. subst.
apply adjunction.
apply adjunction with (b0:=b).
apply adjunction with (b0:=e).
repeat rewrite app_CBA.
rewrite meet_top_l.
repeat rewrite meet_associative. rewrite (meet_commutative e).
now rewrite meet_associative,meet_idempotent.
Qed.

Lemma BA_cc `{CBA:CompleteBooleanAlgebra}: cc = ⊤.
Proof.
unfold cc. apply ord_antisym; auto.
do 2 auto_meet_intro. subst. unfold arrow in *. cbn. rewrite <- top_join.
repeat (rewrite neg_join,double_neg). rewrite join_commutative,join_distributive.
rewrite join_neg,meet_top_r,<- join_associative. now rewrite join_neg,join_top_l.
Qed.

Global Instance CBA_IA `{CBA:CompleteBooleanAlgebra}:ImplicativeAlgebra:=
{separator:=(fun x => x=top); sep_K:=BA_K; sep_S:=BA_S; sep_cc:=BA_cc}.
Proof.
- intros. subst. unfold arrow in *. cbn in H0. now rewrite <- top_join,neg_top,join_bot_l in H0.
- intros. subst. apply ord_antisym;now auto.
Defined.