(*
 * Copyright (c) 2009, Andrew Appel, Robert Dockins and Aquinas Hobor.
 *
 *)

(** This library defines boolean algrbas defined from an order-theoretic
    perspective.  In short, a boolean algrbra is a complemented distributive
    lattice.  We additionally require that the boolean algrbra be non-trivial.

    From this definition we can recover the axioms of boolean algrbras as
    defined in universal algebra.

    We also define module interfaces for boolean algrbras with a splitting
    operator, with a relativization operator, and those which support
    token counting.

    We then say that a share model is a boolean algebra which satisfies
    all three module interfaces.  We also require that the elements
    have a decidable equality.


    Note: This file makes heavy use of math symbols in UTF8 encoding.
    You may need to adust your system to properly handle UTF8.
*)

Require Import base.
Require Import sepalg.

Module Type BOOLEAN_ALGEBRA.
  Parameters (t:Type) (Ord : t -> t -> Prop)
     (top bot : t) (lub glb : t -> t -> t) (comp : t -> t).

  Delimit Scope ba with ba. Open Scope ba.
  Notation "x ⊑ y" := (Ord x y) (at level 55, no associativity) : ba.
  Notation "⊤" := top : ba.
  Notation "⊥" := bot : ba.
  Notation "x ⊔ y" := (lub x y) (at level 45, right associativity) : ba.
  Notation "x ⊓ y" := (glb x y) (at level 47, right associativity) : ba.
  Notation "¬ x" := (comp x) (at level 15, right associativity) : ba.

  Axiom ord_refl : forall x, x ⊑ x.
  Axiom ord_trans : forall x y z, x ⊑ y -> y ⊑ z -> x ⊑ z.
  Axiom ord_antisym : forall x y, x ⊑ y -> y ⊑ x -> x = y.

  Axiom lub_upper1 : forall x y, x ⊑ x ⊔ y.
  Axiom lub_upper2 : forall x y, y ⊑ x ⊔ y.
  Axiom lub_least : forall x y z, x ⊑ z -> y ⊑ z -> (x ⊔ y) ⊑ z.

  Axiom glb_lower1 : forall x y, (x ⊓ y) ⊑ x.
  Axiom glb_lower2 : forall x y, (x ⊓ y) ⊑ y.
  Axiom glb_greatest : forall x y z, z ⊑ x -> z ⊑ y -> z ⊑ (x ⊓ y).

  Axiom top_correct : forall x, x ⊑ ⊤.
  Axiom bot_correct : forall x, ⊥ ⊑ x.

  Axiom distrib1 : forall x y z, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z).
  Axiom distrib2 : forall x y z, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z).

  Axiom comp1 : forall x, x ⊔ ¬x = ⊤.
  Axiom comp2 : forall x, x ⊓ ¬x = ⊥.

  Axiom lat_nontrivial : ⊤ <> ⊥.

  Hint Resolve ord_refl ord_antisym lub_upper1 lub_upper2 lub_least
         glb_lower1 glb_lower2 glb_greatest top_correct bot_correct
         ord_trans distrib1 distrib2 : ba.
End BOOLEAN_ALGEBRA.

Module Type BA_FACTS.
  Declare Module BA:BOOLEAN_ALGEBRA.
  Export BA.

  Axiom ord_spec1 : forall x y, x ⊑ y <-> x = x ⊓ y.
  Axiom ord_spec2 : forall x y, x ⊑ y <-> x ⊔ y = y.

  Axiom lub_idem : forall x, (x ⊔ x) = x.
  Axiom lub_commute : forall x y, x ⊔ y = y ⊔ x.
  Axiom lub_bot : forall x, x ⊔ ⊥ = x.
  Axiom lub_top : forall x, x ⊔ ⊤ = ⊤.
  Axiom lub_absorb : forall x y, x ⊔ (x ⊓ y) = x.
  Axiom lub_assoc : forall x y z, (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z).

  Axiom glb_idem : forall x, x ⊓ x = x.
  Axiom glb_commute : forall x y, x ⊓ y = y ⊓ x.
  Axiom glb_bot : forall x, x ⊓ ⊥ = ⊥.
  Axiom glb_top : forall x, x ⊓ ⊤ = x.
  Axiom glb_absorb : forall x y, x ⊓ (x ⊔ y) = x.
  Axiom glb_assoc : forall x y z, (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z).

  Axiom distrib_spec : forall x y1 y2,
    x ⊔ y1 = x ⊔ y2 ->
    x ⊓ y1 = x ⊓ y2 ->
    y1 = y2.

  Axiom demorgan1 : forall x y, ¬(x ⊔ y) = ¬x ⊓ ¬y.
  Axiom demorgan2 : forall x y, ¬(x ⊓ y) = ¬x ⊔ ¬y.
  Axiom comp_inv : forall x, ¬¬x = x.

  Definition ba_join (x y z:t) := x ⊓ y = ⊥ /\ x ⊔ y = z.

  Axiom ba_saf: sepalgfacts ba_join.
  Definition ba_sa : sepalg t := SepAlg ba_saf.
  Existing Instance ba_sa.
End BA_FACTS.

Module Type TOKEN_FACTORY.
  Declare Module BAF:BA_FACTS.
  Import BAF.

  Parameter isTokenFactory : t -> nat -> Prop.
  Parameter isToken : t -> nat -> Prop.

  Parameter splitToken : forall fac x n,
    isTokenFactory fac x ->
    { fac':t & {tok:t | isTokenFactory fac' (n+x) /\ isToken tok n /\ join fac' tok fac}}.

  Axiom absorbToken : forall fac x n,
    { fac':t & {tok:t | isTokenFactory fac' (n+x) /\ isToken tok n /\ join fac' tok fac}} ->
    isTokenFactory fac x.

  Axiom mergeToken : forall tok1 n1 tok2 n2 tok',
    isToken tok1 n1 ->
    isToken tok2 n2 ->
    join tok1 tok2 tok' ->
    isToken tok' (n1+n2).

  Axiom unmergeToken : forall tok n1 n2,
    isToken tok (n1+n2) ->
    { tok1:t & { tok2:t &
      isToken tok1 n1 /\ isToken tok2 n2 /\
      join tok1 tok2 tok }}.

  Axiom factoryOverlap : forall f1 f2 n1 n2,
    isTokenFactory f1 n1 -> isTokenFactory f2 n2 -> f1 ⊓ f2 <> ⊥.

  Axiom fullFactory : forall x, isTokenFactory x 0 <-> x = ⊤.
  Axiom identityToken : forall x, isToken x 0 <-> x = ⊥.

  Axiom nonidentityToken : forall x n, (n > 0)%nat -> isToken x n -> x <> ⊥.
  Axiom nonidentityFactory : forall x n, isTokenFactory x n -> x <> ⊥.
End TOKEN_FACTORY.

Module Type SPLITTABLE_LATTICE.
  Declare Module BAF:BA_FACTS.
  Import BAF.

  Parameter split : t -> t * t.

  Axiom split_disjoint : forall x1 x2 x,
    split x = (x1, x2) ->
    x1 ⊓ x2 = ⊥.

  Axiom split_together : forall x1 x2 x,
    split x = (x1, x2) ->
    x1 ⊔ x2 = x.

  Axiom split_nontrivial : forall x1 x2 x,
    split x = (x1, x2) ->
    (x1 = ⊥ \/ x2 = ⊥) ->
    x = ⊥.

End SPLITTABLE_LATTICE.

Module Type BA_RELATIV.
  Declare Module BAF:BA_FACTS.
  Import BAF.

  Parameter rel : t -> t -> t.

  Axiom rel_inj_l : forall a x y, a <> ⊥ -> rel a x = rel a y -> x = y.
  Axiom rel_inj_r : forall a b x, x <> ⊥ -> rel a x = rel b x -> a = b.

  Axiom rel_assoc : forall x y z, rel x (rel y z) = rel (rel x y) z.

  Axiom rel_preserves_glb : forall a x y, rel a (x ⊓ y) = (rel a x) ⊓ (rel a y).
  Axiom rel_preserves_lub : forall a x y, rel a (x ⊔ y) = (rel a x) ⊔ (rel a y).

  Axiom rel_bot1 : forall a, rel a ⊥ = ⊥.
  Axiom rel_bot2 : forall x, rel ⊥ x = ⊥.
  Axiom rel_top1 : forall a, rel a ⊤ = a.
  Axiom rel_top2 : forall x, rel ⊤ x = x.
End BA_RELATIV.

Module Type SHARE_MODEL.
  Declare Module BAF:BA_FACTS.

  Declare Module Splittable : SPLITTABLE_LATTICE
    with Module BAF:=BAF.
  Declare Module TokenFactory : TOKEN_FACTORY
    with Module BAF:=BAF.
  Declare Module Relativ : BA_RELATIV
    with Module BAF:=BAF.

  Export BAF.

  Parameter eq_dec : forall x y:t, {x=y} + {x<>y}.
End SHARE_MODEL.


Module BA_Facts (BA':BOOLEAN_ALGEBRA) :
  BA_FACTS with Module BA:=BA'.

  Module BA := BA'.
  Export BA.

  Lemma ord_spec1 : forall x y, x ⊑ y <-> x = x ⊓ y.
  Proof.
    split; intros.
    auto with ba.
    rewrite H; auto with ba.
  Qed.

  Lemma ord_spec2 : forall x y, x ⊑ y <-> x ⊔ y = y.
  Proof.
    intros; split; intros.
    auto with ba.
    rewrite <- H; auto with ba.
  Qed.

  Lemma lub_idem : forall x, x ⊔ x = x.
  Proof. auto with ba. Qed.

  Lemma glb_idem : forall x, x ⊓ x = x.
  Proof. auto with ba. Qed.

  Lemma lub_commute : forall x y, x ⊔ y = y ⊔ x.
  Proof. auto with ba. Qed.

  Lemma glb_commute : forall x y, x ⊓ y = y ⊓ x.
  Proof. auto with ba. Qed.

  Lemma lub_absorb : forall x y, x ⊔ (x ⊓ y) = x.
  Proof. auto with ba. Qed.

  Lemma glb_absorb : forall x y, x ⊓ (x ⊔ y) = x.
  Proof. auto with ba. Qed.

  Lemma lub_assoc : forall x y z, (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z).
  Proof.
    intros; apply ord_antisym; eauto with ba.
  Qed.

  Lemma glb_assoc : forall x y z, (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z).
  Proof.
    intros; apply ord_antisym; eauto with ba.
  Qed.

  Lemma glb_bot : forall x, x ⊓ ⊥ = ⊥.
  Proof. auto with ba. Qed.

  Lemma lub_top : forall x, x ⊔ ⊤ = ⊤.
  Proof. auto with ba. Qed.

  Lemma lub_bot : forall x, x ⊔ ⊥ = x.
  Proof. auto with ba. Qed.

  Lemma glb_top : forall x, x ⊓ ⊤ = x.
  Proof. auto with ba. Qed.

  Lemma distrib_spec : forall x y1 y2,
    x ⊔ y1 = x ⊔ y2 ->
    x ⊓ y1 = x ⊓ y2 ->
    y1 = y2.
  Proof.
    intros.
    rewrite <- (lub_absorb y2 x).
    rewrite glb_commute.
    rewrite <- H0.
    rewrite distrib2.
    rewrite lub_commute.
    rewrite <- H.
    rewrite (lub_commute x y1).
    rewrite (lub_commute y2 y1).
    rewrite <- distrib2.
    rewrite <- H0.
    rewrite glb_commute.
    rewrite lub_absorb.
    auto.
  Qed.

  Lemma comp_inv : forall x, ¬¬x = x.
  Proof.
    intro x.
    apply distrib_spec with (¬x).
    rewrite comp1.
    rewrite lub_commute.
    rewrite comp1.
    auto.
    rewrite comp2.
    rewrite glb_commute.
    rewrite comp2.
    auto.
  Qed.

  Lemma demorgan1 : forall x y, ¬(x ⊔ y) =  ¬x ⊓ ¬y.
  Proof.
    intros x y.
    apply distrib_spec with (x ⊔ y).
    rewrite comp1.
    rewrite distrib2.
    rewrite (lub_assoc x y (¬y)).
    rewrite comp1.
    rewrite lub_top.
    rewrite glb_top.
    rewrite (lub_commute x y).
    rewrite lub_assoc.
    rewrite comp1.
    rewrite lub_top.
    auto.
    rewrite comp2.
    rewrite glb_commute.
    rewrite distrib1.
    rewrite (glb_commute (¬x) (¬y)).
    rewrite glb_assoc.
    rewrite (glb_commute (¬x) x).
    rewrite comp2.
    rewrite glb_bot.
    rewrite lub_commute.
    rewrite lub_bot.
    rewrite (glb_commute (¬y) (¬x)).
    rewrite glb_assoc.
    rewrite (glb_commute (¬y) y).
    rewrite comp2.
    rewrite glb_bot.
    auto.
  Qed.

  Lemma demorgan2 : forall x y, ¬(x ⊓ y) = (¬x) ⊔ (¬y).
  Proof.
    intros x y.
    apply distrib_spec with (x ⊓ y).
    rewrite comp1.
    rewrite lub_commute.
    rewrite distrib2.
    rewrite (lub_commute (¬x) (¬y)).
    rewrite lub_assoc.
    rewrite (lub_commute (¬x) x).
    rewrite comp1.
    rewrite lub_top.
    rewrite glb_commute.
    rewrite glb_top.
    rewrite (lub_commute (¬y) (¬x)).
    rewrite lub_assoc.
    rewrite (lub_commute (¬y) y).
    rewrite comp1.
    rewrite lub_top.
    auto.
    rewrite comp2.
    rewrite distrib1.
    rewrite (glb_commute x y).
    rewrite glb_assoc.
    rewrite comp2.
    rewrite glb_bot.
    rewrite lub_commute.
    rewrite lub_bot.
    rewrite (glb_commute y x).
    rewrite glb_assoc.
    rewrite comp2.
    rewrite glb_bot.
    auto.
  Qed.

  Definition ba_join (x y z:t) := x ⊓ y = ⊥ /\ x ⊔ y = z.

  Lemma ba_saf: sepalgfacts ba_join.
  Proof.
    apply SepAlgFacts.

    (* saf_eq *)
    unfold ba_join; intuition; congruence.

    (* saf_assoc *)
    unfold ba_join; intuition.
    exists (b ⊔ c); intuition.
    rewrite <- H2 in H.
    rewrite <- H.
    apply ord_antisym.
    eauto with ba.
    rewrite H; auto with ba.
    cut (a ⊓ c = ⊥); intros.
    rewrite distrib1.
    rewrite H1.
    rewrite lub_commute; rewrite lub_bot; auto.
    apply ord_antisym.
    apply ord_trans with (d ⊓ c).
    rewrite <- H2.
    eauto with ba.
    rewrite H; auto with ba.
    auto with ba.
    rewrite <- lub_assoc.
    rewrite H2; auto.

    (* saf_com *)
    unfold ba_join; intros a b c [H1 H2].
    rewrite glb_commute.
    rewrite lub_commute.
    auto.

    (* saf_cancellation *)
    unfold ba_join; intuition.
    apply distrib_spec with b.
    rewrite lub_commute; rewrite H2.
    rewrite lub_commute; rewrite H3.
    trivial.
    rewrite glb_commute; rewrite H1.
    rewrite glb_commute; rewrite H.
    trivial.

    (* saf_exist_units *)
    intros x; exists ⊥; split.
    rewrite glb_commute; apply glb_bot.
    rewrite lub_commute; apply lub_bot.

    (* saf_self_join *)
    intros.
    destruct H.
    rewrite lub_idem in H0.
    auto.
  Qed.

  Definition ba_sa : sepalg t :=  SepAlg ba_saf.
End BA_Facts.