From Stdlib Require Import Arith Lia Relation_Definitions RelationClasses Morphisms.

    Class KMalg :=
      {
        (* Elements of the algebera *)
        nodes : Type;
        (* Equivalence relation *)
        equiv : relation nodes;
        equiv_equiv :> Equivalence equiv;

        (* Operations on the algebra *)
        one : nodes; (* Greatest element *)
        zero : nodes; (* Lowest element *)
        meet : nodes -> nodes -> nodes;
        join : nodes -> nodes -> nodes;
        rpc : nodes -> nodes -> nodes; (* Relative Pseudo Complement *)
        box : nodes -> nodes; (* Box *)

        (* The operations respect the equivalence relation *)
        proper_meet : Proper (equiv ==> equiv ==> equiv) meet;
        proper_join : Proper (equiv ==> equiv ==> equiv) join;
        proper_rpc : Proper (equiv ==> equiv ==> equiv) rpc;
        proper_box : Proper (equiv ==> equiv) box;

        (* Property of one *)
        greatest a : equiv (meet a one) a;
        (* Property of zero *)
        lowest a : equiv (join a zero) a;
        (* Properties of meet *)
        mcomm a b : equiv (meet a b) (meet b a);
        massoc a b c : equiv (meet a (meet b c)) (meet (meet a b) c);
        mabsorp a b : equiv (meet a (join a b)) a;
        (* Properties of join *)
        jcomm a b : equiv (join a b) (join b a);
        jassoc a b c : equiv (join a (join b c)) (join (join a b) c);
        jabsorp a b : equiv (join a (meet a b)) a;
        (* Property of rpc *)
        residuation a b c : (equiv a (meet a (rpc b c))) <-> (equiv (meet a b) (meet (meet a b) c));
        (* Properties of box *)
        boxone : equiv (box one) one;
        normal a b : equiv (box (meet a b)) (meet (box a) (box b));
        coreflec a : equiv a (meet a (box a));
        lbx a : equiv (rpc (box a) a) a;
        nextalw a b : equiv (box a) (meet (box a) (join b (rpc b a)))
      }.

Infix "≡" := equiv (at level 70).
Existing Instance equiv_equiv.
Existing Instance proper_meet.
Existing Instance proper_join.
Existing Instance proper_rpc.
Existing Instance proper_box.

Section KMalg_props.

Variable KMH : KMalg.

Definition aleq a b : Prop := a ≡ meet a b.

Notation "a << b" := (a ≡ meet a b) (at level 80).

Fact high_one a : a << one.
Proof.
 symmetry; apply greatest.
Qed.

Fact ord_resid a b c : a << rpc b c <-> meet a b << c.
Proof.
split; intro; [ rewrite <- residuation | rewrite residuation ]; auto.
Qed.

Fact meet_id a : meet a a ≡ a.
Proof.
pose (mabsorp a zero). now rewrite (lowest a) in e.
Qed.

Fact join_id a : join a a ≡ a.
Proof.
pose (jabsorp a one). now rewrite greatest in e.
Qed.

Lemma meet_absorp0 a b : meet a (meet a b) ≡ meet a b.
Proof.
rewrite massoc. now rewrite meet_id.
Qed.

Lemma meet_absorp1 a b : meet b (meet a b) ≡ meet a b.
Proof.
rewrite (mcomm a b). rewrite massoc. now rewrite meet_id.
Qed.

Lemma meet_absorp2 a b : meet (meet a b) a ≡ meet a b.
Proof.
rewrite (mcomm a b). rewrite <- massoc. now rewrite meet_id.
Qed.

Lemma meet_absorp3 a b : meet (meet a b) b ≡ meet a b.
Proof.
rewrite <- massoc. now rewrite meet_id.
Qed.

Lemma aleq_trans a b c : a << b -> b << c -> a << c.
Proof.
intros H H0. rewrite H.
rewrite <- massoc. now rewrite <- H0.
Qed.

Lemma aleq_refl a : a << a.
Proof.
symmetry. apply meet_id.
Qed.

Lemma aleq_antisym a b : a << b -> b << a -> a ≡ b.
Proof.
intros H H0. rewrite H, H0. now rewrite meet_absorp1.
Qed.

Fact meet_elim1 a b : meet a b << a.
Proof.
 rewrite (mcomm (meet a b) a).
rewrite massoc. now rewrite meet_id.
Qed.

Fact meet_elim2 a b : meet a b << b.
Proof.
 rewrite <- massoc.
now rewrite meet_id.
Qed.

Lemma glb a b c : c << a -> c << b -> c << meet a b.
Proof.
intros H H0.
rewrite massoc. rewrite <- H. auto.
Qed.

Lemma meet_deep a b c d : a << c -> b << d -> meet a b << meet c d.
Proof.
intros H H0. apply glb.
- apply aleq_trans with a; auto. apply meet_elim1.
- apply aleq_trans with b; auto. apply meet_elim2.
Qed.

Fact join_inj1 a b : a << join a b.
Proof.
 symmetry; apply mabsorp.
Qed.

Fact join_inj2 a b : b << join a b.
Proof.
 symmetry. rewrite jcomm. apply mabsorp.
Qed.

Lemma eq_repres_aleq a b : a << b <-> b ≡ join a b.
Proof.
split; intro.
-
  assert (H0 : join a b ≡ join (meet a b) b) by now rewrite <- H. rewrite H0.
  symmetry. rewrite jcomm, mcomm; apply jabsorp.
- assert (H0: meet a b ≡ meet a (join a b)) by now rewrite <- H. rewrite H0.
  symmetry. apply mabsorp.
Qed.

Lemma lub a b c : a << c -> b << c -> join a b << c.
Proof.
repeat rewrite eq_repres_aleq; intros.
rewrite <- jassoc. rewrite <- H0. auto.
Qed.

Lemma join_deep a b c d : a << c -> b << d -> join a b << join c d.
Proof.
intros H H0. apply lub.
- apply aleq_trans with c; auto. apply join_inj1.
- apply aleq_trans with d; auto. apply join_inj2.
Qed.

Lemma distr_meet_join a b c : meet a (join b c) ≡ join (meet a b) (meet a c).
Proof.
apply aleq_antisym.
- simpl. rewrite mcomm. apply ord_resid. apply lub.
  + rewrite ord_resid. rewrite mcomm. apply join_inj1.
  + rewrite ord_resid. rewrite mcomm. apply join_inj2.
- apply lub.
  + apply meet_deep.
    * apply aleq_refl.
    * apply join_inj1.
  + apply meet_deep.
    * apply aleq_refl.
    * apply join_inj2.
Qed.

Lemma distr_join_meet a b c : join a (meet b c) ≡ meet (join a b) (join a c).
Proof.
apply aleq_antisym.
- apply lub.
  + apply glb; apply join_inj1.
  + apply meet_deep; apply join_inj2.
- apply ord_resid. apply lub; rewrite ord_resid.
  + rewrite mcomm. apply ord_resid. apply lub.
    * apply ord_resid. rewrite meet_id. apply join_inj1.
    * apply ord_resid. apply aleq_trans with a.
      -- apply meet_elim2.
      -- apply join_inj1.
  + rewrite mcomm. apply ord_resid. apply lub.
    * apply ord_resid. apply aleq_trans with a.
      -- apply meet_elim1.
      -- apply join_inj1.
    * apply ord_resid. rewrite mcomm. apply join_inj2.
Qed.

Lemma mp a b : meet a (rpc a b) << b.
Proof.
pose (a0 := meet_elim2 a (rpc a b)). rewrite ord_resid in a0.
rewrite mcomm in a0. now rewrite meet_absorp0 in a0.
Qed.

Lemma double_neg a : a << rpc (rpc a zero) zero.
Proof.
repeat rewrite ord_resid. rewrite mcomm. rewrite <- ord_resid. apply aleq_refl.
Qed.

Fact low_zero a : zero << a.
Proof.
apply eq_repres_aleq. symmetry.
rewrite jcomm. apply lowest.
Qed.

Fact Top_rpczz : one ≡ rpc zero zero.
Proof.
apply aleq_antisym.
- apply ord_resid.
  rewrite mcomm; rewrite <- high_one.
  apply aleq_refl.
- apply high_one.
Qed.

Lemma aleq_K a b : box (rpc a b) << rpc (box a) (box b).
Proof.
apply ord_resid. rewrite <- normal.
rewrite <- normal.
assert ((meet (rpc a b) a) ≡ meet (meet (rpc a b) a) b).
{ apply aleq_antisym.
  - apply glb. apply aleq_refl. rewrite mcomm; apply mp.
  - apply meet_elim1. }
now rewrite <- H.
Qed.

Lemma box_monot a b : a << b -> box a << box b.
Proof.
intro H.
assert (rpc a b ≡ one).
{ apply aleq_antisym.
  - apply high_one.
  - apply ord_resid. now rewrite mcomm; rewrite greatest. }
assert (box (rpc a b) ≡ one).
{ rewrite H0. apply boxone. }
rewrite <- (greatest (box a)). rewrite <- H1.
rewrite mcomm. apply ord_resid. apply aleq_K.
Qed.

Lemma transitive a : box a << box (box a).
Proof.
apply coreflec.
Qed.

Lemma alg_A1 a b : one << rpc a (rpc b a).
Proof.
repeat rewrite ord_resid. rewrite (mcomm one a). rewrite greatest.
apply meet_elim1.
Qed.

Lemma alg_A2 a b c : one << rpc (rpc a (rpc b c)) (rpc (rpc a b) (rpc a c)).
Proof.
repeat rewrite ord_resid. rewrite (mcomm one (rpc a (rpc b c))). rewrite greatest.
rewrite mcomm.
apply aleq_trans with (meet a (meet (rpc b c) (rpc a b))).
- rewrite massoc. rewrite (massoc a). apply meet_deep.
  + apply glb.
    * apply meet_elim1.
    * apply mp.
  + apply aleq_refl.
- rewrite (mcomm (rpc b c) _). apply aleq_trans with (meet a (meet b (rpc b c))).
  + apply glb.
    * apply meet_elim1.
    * rewrite massoc. apply meet_deep.
      -- apply mp.
      -- apply aleq_refl.
  + apply aleq_trans with (meet b (rpc b c)).
    * apply meet_elim2.
    * apply mp.
Qed.

Lemma alg_A3 a b : one << rpc a (join a b).
Proof.
rewrite ord_resid. rewrite mcomm; rewrite greatest. apply join_inj1.
Qed.

Lemma alg_A4 a b : one << rpc b (join a b).
Proof.
rewrite ord_resid. rewrite mcomm; rewrite greatest. apply join_inj2.
Qed.

Lemma alg_A5 a b c : one << rpc (rpc a c) (rpc (rpc b c) (rpc (join a b) c)).
Proof.
repeat rewrite ord_resid. rewrite (mcomm one _). rewrite greatest.
rewrite mcomm. repeat rewrite <- ord_resid.
apply lub; rewrite ord_resid.
- apply aleq_trans with (meet a (rpc a c)).
  + rewrite massoc. apply meet_elim1.
  + apply mp.
- rewrite (mcomm (rpc a c) _). apply aleq_trans with (meet b (rpc b c)).
  + rewrite massoc. apply meet_elim1.
  + apply mp.
Qed.

Lemma alg_A6 a b : one << rpc (meet a b) a.
Proof.
rewrite ord_resid. rewrite mcomm; rewrite greatest. apply meet_elim1.
Qed.

Lemma alg_A7 a b : one << rpc (meet a b) b.
Proof.
rewrite ord_resid. rewrite mcomm; rewrite greatest. apply meet_elim2.
Qed.

Lemma alg_A8 a b c : one << rpc (rpc c a) (rpc (rpc c b) (rpc c (meet a b))).
Proof.
repeat rewrite ord_resid. rewrite (mcomm one _). rewrite greatest.
rewrite mcomm. apply glb.
- apply aleq_trans with (meet c (rpc c a)).
  + rewrite massoc. apply meet_elim1.
  + apply mp.
- rewrite (mcomm (rpc c a) _). apply aleq_trans with (meet c (rpc c b)).
  + rewrite massoc. apply meet_elim1.
  + apply mp.
Qed.

Lemma alg_A9 a : one << rpc zero a.
Proof.
rewrite ord_resid. rewrite eq_repres_aleq.
rewrite mcomm; rewrite greatest. rewrite jcomm. symmetry; apply lowest.
Qed.

Lemma alg_MA1 a b : one << rpc (box (rpc a b)) (rpc (box a) (box b)).
Proof.
rewrite ord_resid. rewrite mcomm; rewrite greatest.
apply aleq_K.
Qed.

Lemma alg_MA2 a : one << rpc (rpc (box a) a) a.
Proof.
apply ord_resid. rewrite mcomm; rewrite greatest.
rewrite lbx. apply aleq_refl.
Qed.

Lemma alg_MA3 a b : one << rpc (box a) (join b (rpc b a)).
Proof.
rewrite ord_resid. rewrite mcomm; rewrite greatest.
apply nextalw.
Qed.

End KMalg_props.