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.HeytingAlgebras.
Require Import ImpAlg.ImplicativeStructures.
Require Import ImpAlg.ImplicativeAlgebras.
Require Import ImpAlg.Adequacy.
Require Import ImpAlg.Combinators.
Require Import ImpAlg.ParAlgebras.
Require Import ImpAlg.TensorAlgebras.

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 (b,(Hb,Ha)).
      unfold arrow_set_r.
      exists b;subst;intuition.
    + intros (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.
Qed.

Global Instance CBA_PS `{CBA:CompleteBooleanAlgebra}:ParStructure:=
{pneg:=neg; par:=join}.
Proof.
  - intros. eapply ord_trans;[apply join_mon_l|apply join_mon_r];intuition.
  - intros. now apply neg_mon.
  - intros a B. rewrite join_meet_set.
    apply meet_same_set;split.
    + intros (b,(Hb,Ha)). subst.
      unfold par_set_l.
      exists b;subst;intuition.
    + intros (b,(Hb,Ha)). subst.
      unfold par_set_r.
      exists b;subst;intuition.
  - intros a B. rewrite join_commutative,join_meet_set.
     apply meet_same_set;split.
    + intros (b,(Hb,Ha)). subst.
      unfold par_set_r.
      exists b;subst;intuition.
    + intros (b,(Hb,Ha)). subst.
      unfold par_set_r.
      exists b;subst;intuition.
  - intro a. apply neg_meet_set.
Defined.

Lemma join_distributive_l `{CBA:CompleteBooleanAlgebra}:
  ∀ a b c,(b ⋀ c) ⋁ a = (b ⋁ a) ⋀ (c ⋁ a).
Proof.
intros a b c.
rewrite join_commutative,join_distributive.
now repeat rewrite join_commutative with (a0:= a).
Qed.

Lemma meet_distributive_l `{CBA:CompleteBooleanAlgebra}:
  ∀ a b c,(b ⋁ c) ⋀ a = (b ⋀ a) ⋁ (c ⋀ a).
Proof.
intros a b c.
rewrite meet_commutative,meet_distributive.
now repeat rewrite meet_commutative with (a0:= a).
Qed.

Lemma join_neg_l `{CBA:CompleteBooleanAlgebra}: ∀ (a:X), (¬a) ⋁ a = ⊤.
Proof.
intro a. now rewrite join_commutative,join_neg.
Qed.

Lemma join3_neg1 `{CBA:CompleteBooleanAlgebra}: ∀ (a b:X), (¬a) ⋁ (b ⋁ a) = ⊤.
Proof.
  intros a b.
  now rewrite join_commutative, join_associative,join_neg,join_top_r.
Qed.

Lemma join3_neg3 `{CBA:CompleteBooleanAlgebra}: ∀ (a b:X), a ⋁ (b ⋁ (¬ a)) = ⊤.
Proof.
  intros a b.
  now rewrite join_commutative,join_associative,join_neg_l,join_top_r.
Qed.

Lemma BA_PS1 `{CBA:CompleteBooleanAlgebra}: PS1 = ⊤.
Proof.
unfold TS1. apply ord_antisym; auto.
auto_meet_intro. cbn. rewrite <- top_join.
now rewrite neg_join,meet_idempotent,join_neg_l.
Qed.

Lemma BA_PS2 `{CBA:CompleteBooleanAlgebra}: PS2 = ⊤.
Proof.
unfold TS2.
apply ord_antisym;auto.
do 2 auto_meet_intro. cbn. rewrite <- top_join.
now rewrite <- join_associative,(@join_commutative _ _ _ _ (a)), join_neg,join_top_l.
Qed.

Lemma BA_PS3 `{CBA:CompleteBooleanAlgebra}: PS3 = ⊤.
Proof.
unfold TS3.
apply ord_antisym;auto.
do 2 auto_meet_intro. cbn. rewrite <- top_join.
rewrite neg_join.
rewrite join_commutative,join_distributive.
repeat rewrite join_associative.
rewrite join3_neg3,meet_top_r.
now rewrite join_neg,join_top_r.
Qed.

Lemma BA_PS4 `{CBA:CompleteBooleanAlgebra}: PS4 = ⊤.
Proof.
unfold TS4.
apply ord_antisym;auto.
do 3 auto_meet_intro. cbn. rewrite <- top_join.
rewrite neg_join,double_neg.
rewrite neg_join.
rewrite join_commutative with (b:=(a1 ⋁ a0)).
rewrite join_distributive.
repeat rewrite join_associative.
rewrite join3_neg3,meet_top_l.
rewrite join_commutative.
rewrite join_distributive.
repeat rewrite join_associative.
rewrite join3_neg3,join_top_r,meet_top_r.
rewrite join_neg_l.
now repeat rewrite join_top_r.
Qed.

Lemma BA_PS5 `{CBA:CompleteBooleanAlgebra}: PS5 = ⊤.
Proof.
unfold TS5.
apply ord_antisym;auto.
do 3 auto_meet_intro. cbn. rewrite <- top_join.
rewrite neg_join.
rewrite join_commutative,join_distributive.
replace (a ⋁ a0 ⋁ a1 ⋁ (¬ a)) with ⊤.
- rewrite meet_top_l.
  rewrite neg_join.
  repeat rewrite join_associative,join_distributive.
  rewrite join3_neg3,meet_top_l.
  rewrite join_neg.
  now repeat rewrite join_top_r.
- rewrite join_commutative.
  repeat rewrite <- join_associative.
  rewrite join_neg_l.
  now repeat rewrite join_top_l.
Qed.


Global Instance CBA_PA `{CBA:CompleteBooleanAlgebra}:ParAlgebra:=
{psep:=(fun x => x=top); psep_PS1:=BA_PS1; psep_PS2:=BA_PS2;
psep_PS3:=BA_PS3;psep_PS4:=BA_PS4;psep_PS5:=BA_PS5}.
Proof.
- intros. subst. cbn in H0. now rewrite <- top_join,neg_top,join_bot_l in H0.
- intros. subst. apply ord_antisym;now auto.
Qed.

Global Instance CBA_TS `{CBA:CompleteBooleanAlgebra}:@TensorStructure _ _ _ CL:=
{tneg:=neg; tensor:=meet}.
Proof.
  - intros. eapply ord_trans;[apply meet_mon_l|apply meet_mon_r];intuition.
  - intros. now apply neg_mon.
  - intros a B. rewrite meet_join_set.
    apply join_same_set;split.
    + intros (b,(Hb,Ha)). subst.
      exists b;subst;intuition.
    + intros (b,(Hb,Ha)). subst.
      exists b;subst;intuition.
  - intros a B. rewrite meet_commutative,meet_join_set.
     apply join_same_set;split.
    + intros (b,(Hb,Ha)). subst.
      exists b;subst;intuition.
    + intros (b,(Hb,Ha)). subst.
      exists b;subst;intuition.
  - intro a. apply neg_join_set.
Defined.

Ltac rp_rw a:=repeat rewrite a.
Ltac auto_rw_t:=
repeat (rp_rw double_neg;
        rp_rw neg_meet; rp_rw neg_join;
        rp_rw join3_neg1; rp_rw join3_neg3;
        rp_rw join_associative;
        rp_rw join_neg_l;
        rp_rw join_neg;
        rp_rw join_top_l; rp_rw join_top_r;
        rp_rw meet_top_l; rp_rw meet_top_r
        ); try easy.

Lemma BA_TS1 `{CBA:CompleteBooleanAlgebra}: TS1 = ⊤.
Proof.
unfold TS1. apply ord_antisym; auto.
auto_meet_intro. cbn. rewrite <- top_join.
rewrite meet_idempotent. auto_rw_t.
Qed.

Lemma BA_TS2 `{CBA:CompleteBooleanAlgebra}: TS2 = ⊤.
Proof.
unfold TS2. apply ord_antisym;auto.
do 2 auto_meet_intro. cbn. rewrite <- top_join.
auto_rw_t.
Qed.

Lemma BA_TS3 `{CBA:CompleteBooleanAlgebra}: TS3 = ⊤.
Proof.
unfold TS3. apply ord_antisym;auto.
do 2 auto_meet_intro. cbn. rewrite <- top_join.
auto_rw_t. rewrite join_distributive.
auto_rw_t.
Qed.

Lemma BA_TS4 `{CBA:CompleteBooleanAlgebra}: TS4 = ⊤.
Proof.
unfold TS4. apply ord_antisym;auto.
do 3 auto_meet_intro. cbn. rewrite <- top_join. subst.
auto_rw_t.
replace ((¬ a1) ⋁ ((¬ a) ⋁ (a1 ⋀ a0))) with
((¬ a1) ⋁ ((¬ a) ⋁ a0)).
- rewrite join_commutative.
  rewrite join_distributive.
  auto_rw_t.
- repeat rewrite <- join_associative.
  rewrite join_distributive. auto_rw_t.
Qed.

Lemma BA_TS5 `{CBA:CompleteBooleanAlgebra}: TS5 = ⊤.
Proof.
unfold TS5.
apply ord_antisym;auto.
do 3 auto_meet_intro. cbn. rewrite <- top_join.
auto_rw_t.
rewrite join_commutative,join_distributive. auto_rw_t.
rewrite join_distributive_l. auto_rw_t.
rewrite join_commutative. auto_rw_t.
Qed.


Global Instance CBA_TA `{CBA:CompleteBooleanAlgebra}:TensorAlgebra:=
{tsep:=(fun x => x=top); tsep_TS1:=BA_TS1; tsep_TS2:=BA_TS2;
tsep_TS3:=BA_TS3;tsep_TS4:=BA_TS4;tsep_TS5:=BA_TS5}.
Proof.
- intros. subst. cbn in H0. now rewrite <- top_join,neg_meet,neg_top,double_neg,join_bot_l in H0.
- intros. subst. apply ord_antisym;now auto.
Qed.