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

Require Import base.
Require Import sepalg.
Require Import sepalg_generators.
Require Import sepalg_functors.
Require Import age_sepalg.

Require Import Wellfounded.

Delimit Scope pred with pred.
Local Open Scope pred.

(* Some relations we will turn into modalities.
   Also, the necR relation will be used as the
   ordering on our Kripke model.
 *)

Definition laterR   `{ASA A} : relation A := clos_trans A age.
Definition necR     `{ASA A} : relation A := clos_refl_trans A age.
Definition compareR `{ASA A} : relation A := @comparable A as_alg.
Definition extendR  `{ASA A} : relation A := join_sub.
Definition fashionR `{ASA A} : relation A := fashionable.

(* A "pre-predicate" is hereditary iff whenever it is
   true at world a, it is also true at all worlds
   accessable from a.
 *)
Definition hereditary `{ASA A} (p:A->Prop) :=
  forall a a':A, age a a' -> p a -> p a'.

(* A predicate is a hereditary pre-predicate *)
Definition pred (A:Type) {SA:sepalg A} {H:ASA SA} := { p:A -> Prop | hereditary p }.

(* Here is some junk that makes the definition of "pred" opaque
   to most tactics but sill allows the "Program" extension to
   see it is a subset type.  The coercion is sugar that allows us to use
   predicates easily.
 *)
Definition app_pred `{ASA A} (p:pred A) : A -> Prop := proj1_sig p.
Definition pred_hereditary `{ASA} (p:pred A) := proj2_sig p.
Coercion app_pred : pred >-> Funclass.
Global Opaque pred.

Hint Resolve @pred_hereditary.

Lemma pred_nec_hereditary `{ASA A} (p:pred A) :
  forall a a':A, necR a a' -> p a -> p a'.
Proof.
  intros.
  induction H0; auto.
  apply pred_hereditary with x; auto.
Qed.

Program Definition mkPred `{ASA A} (p:A -> Prop) : pred A :=
  fun x => forall x', necR x x' -> p x'.
Next Obligation.
  repeat intro.
  apply H1.
  apply rt_trans with a'; auto.
  apply rt_step; auto.
Qed.

(* The semantic notion of entailment.
 *)
Definition derives `{ASA A} (P Q:pred A) := forall a:A, P a -> Q a.
Implicit Arguments derives.
Arguments Scope derives [pred pred].

(* A utility lemma that applies functional extensionality
   and proof irrelevance.
 *)
Lemma equiv_eq `{ASA A} : forall (P Q:pred A),
  derives P Q -> derives Q P -> P = Q.
Proof.
  intros.
  destruct P; destruct Q; unfold derives in *; simpl in *.
  revert h0; replace x0 with x; intros.
  replace h0 with h by apply proof_irr; auto.
  extensionality a.
  apply prop_ext; intuition.
Qed.

Lemma derives_cut `{ASA A} : forall Q P R,
  derives P Q ->
  derives Q R ->
  derives P R.
Proof.
  repeat intro.
  apply H1.
  apply H0.
  auto.
Qed.

(* Utility lemmas about the relation between transitive closure
   and reflexive-transitive closure.
 *)
Section RtRft.
  Variable A:Type.
  Variable R:relation A.

  Let Rt := clos_trans A R.
  Let Rft := clos_refl_trans A R.

  Lemma Rt_Rft : forall x y, Rt x y -> Rft x y.
  Proof.
    intros; elim H; intros.
    apply rt_step; auto.
    eapply rt_trans; eauto.
  Qed.

  Lemma Rt_Rft_trans : forall x y z, Rt x y -> Rft y z -> Rt x z.
  Proof.
    intros x y z H H1; revert x H; elim H1; intros; auto.
    eapply t_trans; eauto; apply t_step; auto.
  Qed.

  Lemma Rft_Rt_trans : forall x y z, Rft x y -> Rt y z -> Rt x z.
  Proof.
    intros x y z H; revert z; elim H; intros; auto.
    eapply t_trans; eauto; apply t_step; auto.
  Qed.
End RtRft.


(* Utility facts about aging.
 *)
Lemma age_irreflexive `{ASA A}: forall x, age x x -> False.
Proof.
  intros A HA XA x.
  elim (asf_wf as_facts x); intros.
  apply H0 with x0; auto.
Qed.

Lemma transpose_clos_trans : forall A R x y,
  clos_trans A (transp A R) x y <-> transp A (clos_trans A R) x y.
Proof.
  unfold transp; intuition.

  elim H; intros.
  apply t_step; auto.
  apply t_trans with y0; auto.

  elim H; intros.
  apply t_step; auto.
  apply t_trans with y0; auto.
Qed.

Lemma laterR_irreflexive `{ASA A} : forall x, laterR x x -> False.
Proof.
  intros A HA XA x.
  elim (wf_clos_trans _ (fun x y => age y x) (asf_wf as_facts) x); intros.
  apply H0 with x0; auto.
  red in H1.
  assert (transp _ (clos_trans A age) x0 x0).
  red; auto.
  rewrite <- transpose_clos_trans in H2.
  auto.
Qed.

Lemma nec_refl_or_later `{ASA A} : forall x y,
  necR x y -> x = y \/ laterR x y.
Proof.
  intros.
  elim H0; intros; auto.
  right; apply t_step; auto.
  destruct H2; destruct H4; subst; auto.
  right; apply t_trans with y0; auto.
Qed.


Lemma necR_antisym `{ASA A} : forall x y,
  necR x y -> necR y x -> x = y.
Proof.
  intros.
  apply nec_refl_or_later in H0.
  apply nec_refl_or_later in H1.
  intuition.
  elim (laterR_irreflexive x).
  eapply t_trans; eauto.
Qed.

Lemma age_later_nec `{ASA A} : forall x y z,
  age x y ->
  laterR x z ->
  necR y z.
Proof.
  intros A HA XA x y z H H1; revert y H.
  induction H1; intros.
  replace y0 with y.
  apply rt_refl.
  unfold age in *; congruence.
  apply rt_trans with y; auto.
  apply IHclos_trans1; auto.
  apply Rt_Rft; auto.
Qed.

(* "valid" relations are those that commute with aging.  These
   relations are the ones that can be turned into modalities.
 *)
Definition valid_rel `{ASA A} (R:relation A) : Prop :=
  commut A age R /\ commut A R age.

(* A modaility is a valid relation *)
Definition modality `{ASA A} := { R:relation A | valid_rel R }.

(* More black magic to make the definition of modaility mostly opaque. *)
Definition app_mode `{ASA A} (m:modality) : A -> A -> Prop := proj1_sig m.
Definition mode_valid `{ASA A} (m:modality) := proj2_sig m.
Global Opaque modality.
Coercion app_mode : modality >-> Funclass.

(* commutivity facts for the basic relations *)

Lemma valid_rel_commut_later1 `{ASA A} : forall R,
  valid_rel R ->
  commut A laterR R.
Proof.
  intros; hnf; intros.
  revert z H2.
  induction H1; intros.
  destruct H0.
  destruct (H0 _ _ H1 _ H2).
  exists x0; auto.
  apply t_step; auto.
  destruct (IHclos_trans1 _ H2).
  destruct (IHclos_trans2 _ H1).
  exists x1; auto.
  eapply t_trans; eauto.
Qed.

Lemma valid_rel_commut_later2 `{ASA A} : forall R,
  valid_rel R ->
  commut A R laterR.
Proof.
  intros; hnf; intros.
  revert x H1.
  induction H2; intros.
  destruct H0.
  destruct (H3 _ _ H2 _ H1).
  exists x1; auto.
  apply t_step; auto.
  destruct (IHclos_trans2 _ H1).
  destruct (IHclos_trans1 _ H3).
  exists x2; auto.
  eapply t_trans; eauto.
Qed.

Lemma valid_rel_commut_nec1 `{ASA A} : forall R,
  valid_rel R ->
  commut A necR R.
Proof.
  intros; hnf; intros.
  apply nec_refl_or_later in H1; destruct H1; subst.
  exists z; auto.
  apply rt_refl.
  destruct (valid_rel_commut_later1 R H0 x y H1 z H2).
  exists x0; auto.
  apply Rt_Rft; auto.
Qed.

Lemma valid_rel_commut_nec2 `{ASA A} : forall R,
  valid_rel R ->
  commut A R necR.
Proof.
  intros; hnf; intros.
  apply nec_refl_or_later in H2; destruct H2; subst.
  exists x; auto.
  apply rt_refl.
  destruct (valid_rel_commut_later2 R H0 x y H1 z H2).
  exists x0; auto.
  apply Rt_Rft; auto.
Qed.

Lemma valid_rel_age `{ASA A} : valid_rel age.
Proof.
  intros; split; hnf; intros; firstorder.
Qed.

Lemma valid_rel_later `{ASA A} : valid_rel laterR.
Proof.
  intros; split; hnf; intros.
  revert x H0.
  induction H1; intros.
  exists y; auto.
  apply t_step; auto.
  destruct (IHclos_trans2 _ H0).
  destruct (IHclos_trans1 _ H2).
  exists x2; auto.
  eapply t_trans; eauto.

  revert z H1.
  induction H0; intros.
  exists x; auto.
  apply t_step; auto.
  destruct (IHclos_trans1 _ H1).
  destruct (IHclos_trans2 _ H0).
  exists x1; auto.
  eapply t_trans; eauto.
Qed.

Lemma valid_rel_nec `{ASA A} : valid_rel necR.
Proof.
  intros; split; hnf; intros.
  revert x H0.
  induction H1; intros.
  exists y; auto.
  apply rt_step; auto.
  exists x0; auto.
  apply rt_refl.
  destruct (IHclos_refl_trans2 _ H0).
  destruct (IHclos_refl_trans1 _ H2).
  exists x2; auto.
  eapply rt_trans; eauto.

  revert z H1.
  induction H0; intros.
  exists x; auto.
  apply rt_step; auto.
  exists z; auto.
  apply rt_refl.

  destruct (IHclos_refl_trans1 _ H1).
  destruct (IHclos_refl_trans2 _ H0).
  exists x1; auto.
  eapply rt_trans; eauto.
Qed.

Lemma valid_rel_fashion `{ASA A} : valid_rel fashionR.
Proof.
  intros A HA XA.
  split; hnf; intros.

  hnf in H.
  inv H0; rewrite H in H2; inv H2.
  exists x'; auto.
  hnf in H0.
  inv H.
  exists (unage x).
  apply (asf_unage as_facts).
  apply intro_fashion_some with y x; auto.
  apply (asf_unage as_facts).
  apply intro_fashion_none; auto.
  exists (unage x).
  apply (asf_unage as_facts).
  apply intro_fashion_some with y x; auto.
  apply (asf_unage as_facts).
  apply intro_fashion_some with x' y'; auto.
Qed.

Lemma valid_rel_compare `{ASA A} : valid_rel compareR.
Proof.
  intros A HA XA.
  split; hnf; intros.

  apply comparable_common_unit in H0.
  destruct H0 as [w [? ?]].
  destruct (asf_commute2 as_facts _ _ _ _ H1 H)
    as [u [v [? [? ?]]]].
  destruct (asf_commute1 as_facts _ _ _ _ H0 H3)
    as [u' [v' [? [? ?]]]].
  assert (u' = v').
  unfold age in *; congruence.
  subst v'.
  exists u'; auto.
  assert (x = v).
  unfold age in *; congruence.
  subst v.
  apply common_unit_comparable.
  exists u; auto.

  apply comparable_common_unit in H.
  destruct H as [w [? ?]].
  destruct (asf_commute4 as_facts _ _ _ _ H H0)
    as [u [v [? [? ?]]]].
  destruct (asf_commute3 as_facts _ _ _ _ H1 H3)
    as [u' [v' [? [? ?]]]].
  exists v'; auto.
  apply common_unit_comparable.
  destruct (join_ex_units u) as [uu Huu].
  red in Huu.
  exists uu; split.
  destruct (join_assoc _ _ _ _ _ Huu H2) as [q [? ?]].
  assert (q = z).
  eapply join_eq; eauto.
  subst q; auto.
  destruct (join_assoc _ _ _ _ _ Huu H5) as [q [? ?]].
  assert (q = v').
  eapply join_eq; eauto.
  subst q.
  auto.
Qed.

Lemma valid_rel_extend `{ASA A} : valid_rel extendR.
Proof.
  intros A HA XA; intros; split; hnf; intros.
  destruct H0 as [w ?].
  destruct (asf_commute2 as_facts _ _ _ _ H0 H)
    as [u [v [? [? ?]]]].
  exists u; auto.
  exists v; auto.

  destruct H.
  destruct (asf_commute3 as_facts _ _ _ _ H H0)
    as [u [v [? [? ?]]]].
  exists v; auto.
  exists u; auto.
Qed.

(* Definitions of the basic modalities.
 *)
Definition ageM `{ASA A} : modality
  := exist _ age valid_rel_age.
Definition laterM `{ASA A} : modality
  := exist _ laterR valid_rel_later.
Definition necM `{ASA A} : modality
  := exist _ necR valid_rel_nec.
Definition compareM `{ASA A} : modality
  := exist _ compareR valid_rel_compare.
Definition extendM `{ASA A} : modality
  := exist _ extendR valid_rel_extend.
Definition fashionM `{ASA A} : modality
  := exist _ fashionR valid_rel_fashion.

Hint Resolve rt_refl rt_trans t_trans.
Hint Unfold necR.
Obligation Tactic := unfold hereditary; intuition;
    first [eapply pred_hereditary; eauto; fail | eauto ].

(* Definitions of the basic propositional conectives.
 *)

Program Definition TT `{ASA A}: pred A := fun a:A => True.
Program Definition FF  `{ASA A}: pred A := fun a:A => False.
Program Definition implies `{ASA A} (P Q:pred A) : pred A :=
   fun a:A => forall a':A, necR a a' -> P a' -> Q a'.
Next Obligation.
  apply H1; auto.
  apply rt_trans with a'; auto.
  apply rt_step; auto.
Qed.
Program Definition union `{ASA A} (P Q:pred A) : pred A :=
   fun a:A => P a \/ Q a.
Next Obligation.
  left; eapply pred_hereditary; eauto.
  right; eapply pred_hereditary; eauto.
Qed.

Program Definition intersection `{ASA A} (P Q:pred A) : pred A :=
   fun a:A => P a /\ Q a.

(* Universal and existential quantification
 *)

Program Definition universal `{ASA A} {B: Type} (f: B -> pred A) : pred A
  := fun a => forall b, f b a.
Next Obligation.
  apply pred_hereditary with a; auto.
  apply H1.
Qed.

Program Definition existential `{ASA A} {B: Type} (f: B -> pred A) : pred A
  := fun a => exists b, f b a.
Next Obligation.
  destruct H1; exists x; eapply pred_hereditary; eauto.
Qed.

(* Definitions of the BI connectives. *)

Program Definition emp `{ASA A} : pred A := identity.
Next Obligation.
  rewrite identity_unit_equiv.
  rewrite identity_unit_equiv in H1.
  unfold unit_for in *.
  destruct (age1_join _ _ H1 H0) as [y' [z' [? [? ?]]]].
  assert (a' = y' /\ a' = z') by (unfold age in *; split; congruence).
  destruct H5; subst; subst.
  auto.
Qed.

Program Definition sep_con `{ASA A} (p q:pred A) : pred A := fun x:A =>
  exists y:A, exists z:A, join y z x /\ p y /\ q z.
Next Obligation.
  destruct H1 as [y [z [? [? ?]]]].
  destruct (age1_join2 _ _ H1 H0) as [w [v [? [? ?]]]].
  exists w; exists v; split; auto.
  split.
  apply pred_hereditary with y; auto.
  apply pred_hereditary with z; auto.
Qed.

Program Definition wand `{ASA A} (p q:pred A) : pred A := fun x =>
  forall x' y z, necR x x' -> join x' y z -> p y -> q z.
Next Obligation.
  apply H1 with x' y; auto.
  apply rt_trans with a'; auto.
  apply rt_step; auto.
Qed.

(* Definition of the "box" modal operator.  This operator turns
   modalities (relations) into a "necessarily" type operator.
 *)

Program Definition box `{ASA A} (M:modality) (P:pred A) : pred A :=
  fun a:A => forall a', M a a' -> P a'.
Next Obligation.
  destruct M as [M [H3 H4]]; simpl in *.
  destruct (H4 _ _ H2 _ H0).
  apply pred_hereditary with x; auto.
  apply H1; auto.
Qed.

(* Definition of the "diamond" modal operator.  This operator
   turns modalities into a "possibly" type operator.  _However_,
   note that this is NOT the boolean dual to "box", as usually
   found in accounts of modal logic. Instead, this is the
   "proof-theoretic" dual as found in Restall's "A Introduction
   to Substructural Logic" (2000).
 *)

Program Definition diamond `{ASA A} (M:modality) (P:pred A) : pred A :=
  fun a:A => exists a', M a' a /\ P a'.
Next Obligation.
  destruct M as [M [H3 H4]]; simpl in *.
  destruct H1 as [x [? ?]].
  destruct (H3 _ _ H0 _ H1).
  exists x0; split; auto.
  apply pred_hereditary with x; auto.
Qed.

Definition boxy `{ASA A} (m: modality) (p: pred A): Prop :=  box m p = p.

(* Lifting pure mathematical facts to predicates *)
Program Definition prop `{ASA A}  (P: Prop) : pred A :=
   intersection emp (fun _  => P).

(* A pile of notations for the operators we have defined *)
Notation "P '|--' Q" := (derives P Q) (at level 80, no associativity).
Notation "'Ex_'  x ':' T ',' P " := (existential (fun x:T => P%pred)) (at level 65, x at level 99) : pred.
Notation "'All_'  x ':' T  ',' P " := (universal (fun x:T => P%pred)) (at level 65, x at level 99) : pred.
Infix "||" := union (at level 50, left associativity) : pred.
Infix "&&" := intersection (at level 40, left associativity) : pred.
Notation "P '-->' Q" := (implies P Q) (at level 55, right associativity) : pred.
Notation "P '<-->' Q" := (intersection (implies P Q) (implies Q P)) (at level 57, no associativity) : pred.
Notation "P '*' Q" := (sep_con P Q) : pred.
Notation "P '-*' Q" := (wand P Q) (at level 60, right associativity).
Notation "'[]' e" := (box necM e) (at level 30, right associativity): pred.
Notation "'#' e" := (box compareM e) (at level 30, right associativity): pred.
Notation "'|>' e" := (box laterM e) (at level 30, right associativity): pred.
Notation "'%' e"  := (box extendM e)(at level 30, right associativity): pred.
Notation "'!!' e" := (prop e) (at level 25) : pred.
Notation "P '>=>' Q" := (box fashionM (implies P Q)) (at level 55, right associativity) : pred.
Notation "P '<=>' Q" := (box fashionM (intersection (implies P Q) (implies Q P))) (at level 57, no associativity) : pred.

(* Rules for the propositional connectives *)
Lemma modus_ponens `{ASA A} : forall (X P Q:pred A),
  X |-- P ->
  X |-- (P --> Q) ->
  X |-- Q.
Proof.
  unfold derives, implies; simpl; intuition eauto.
Qed.

Lemma and_intro `{ASA A} : forall (X P Q:pred A),
  X |-- P ->
  X |-- Q ->
  X |-- P && Q.
Proof.
  unfold derives, implies, intersection; simpl; intuition.
Qed.

Lemma and1 `{ASA A} : forall (X P Q:pred A),
  X |-- P && Q --> P.
Proof.
  unfold derives, implies, intersection; simpl; intuition eauto.
Qed.

Lemma and2 `{ASA A} : forall (X P Q:pred A),
  X |-- P && Q --> Q.
Proof.
  unfold derives, implies, intersection; simpl; intuition eauto.
Qed.

Lemma and3 `{ASA A} : forall (X P Q R:pred A),
  X |-- (P --> Q) --> (P --> R) --> (P --> Q && R).
Proof.
  unfold derives, implies, intersection; simpl; intuition eauto.
Qed.

Lemma or1 `{ASA A} : forall (X P Q:pred A),
  X |-- P --> P || Q.
Proof.
  unfold derives, implies, union; simpl; intuition.
Qed.

Lemma or2 `{ASA A} : forall (X P Q:pred A),
  X |-- Q --> P || Q.
Proof.
  unfold derives, implies, union; simpl; intuition.
Qed.

Lemma or3 `{ASA A} : forall (X P Q R:pred A),
  X |-- (P --> R) --> (Q --> R) --> (P || Q --> R).
Proof.
  unfold derives, implies, union; simpl; intuition eauto.
Qed.

Lemma TTrule `{ASA A} : forall X P,
  X |-- P --> TT.
Proof.
  unfold derives, implies, TT; simpl; intuition.
Qed.

Lemma FFrule `{ASA A} : forall X P,
  X |-- FF --> P.
Proof.
  unfold derives, implies, FF; simpl; intuition.
Qed.

Lemma distribution `{ASA A} : forall (X P Q R:pred A),
  X |-- P && (Q || R) --> (P && Q) || (P && R).
Proof.
  unfold derives, implies, union, intersection; simpl; intuition.
Qed.

(* Characterize the relation between conjunction and implication *)
Lemma impl_and_adjoint `{ASA A} : forall (P Q R:pred A),
  (P && Q) |-- R <-> P |-- (Q --> R).
Proof.
  split; intros.
  hnf; intros; simpl; intros.
  apply H0.
  split; auto.
  apply pred_nec_hereditary with a; auto.
  hnf; intros.
  hnf in H0.
  unfold implies in H0; simpl in H0.
  destruct H1.
  apply H0 with a; auto.
Qed.

(* Some facts about modalities *)

Lemma box_e0 `{ASA A}: forall (M: modality) Q, 
            reflexive _ M -> box M Q  |-- Q.
Proof.
intros.
intro; intros.
apply H1; simpl.
apply H0.
Qed.
Implicit Arguments box_e0.

Lemma boxy_i `{ASA A}: 
  forall (Q: pred A) (M: modality),
    reflexive _ M -> 
    (forall w w', M w w' -> Q w -> Q w') ->
    boxy M Q.
Proof.
intros.
unfold boxy.
apply equiv_eq; hnf; intros.
eapply box_e0; eauto.
hnf; intros.
eapply H1; eauto.
Qed.

Lemma extendM_refl `{ASA A}: reflexive _ extendM.
Proof.
intros; intro; simpl; apply join_sub_refl.
Qed.

Lemma compareM_refl `{ASA A}: reflexive _ compareM.
Proof.
intros; intro; simpl.
apply comparable_refl.
Qed.

Lemma necM_refl `{ASA A}: reflexive _ necM.
Proof.
intros; intro; simpl.
unfold necR.
constructor 2.
Qed.

Hint Resolve @extendM_refl.
Hint Resolve @compareM_refl.
Hint Resolve @necM_refl.

(* relationship between box and diamond *)
Lemma box_diamond `{ASA A} : forall M (P Q:pred A),
  (diamond M P) |-- Q <-> P |-- (box M Q).
Proof.
  unfold derives; intuition.
  hnf; intros.
  apply H0.
  hnf; eauto.
  destruct H1 as [a' [? ?]].
  apply H0 with a'; auto.
Qed.

(* Box is a normal modal operator *)

Lemma ruleNec `{ASA A} : forall M (P:pred A),
  derives TT P ->
  derives TT (box M P).
Proof.
  intros.
  rewrite <- box_diamond.
  hnf; intros.
  apply H0; hnf; auto.
Qed.

Lemma axiomK `{ASA A}: forall M (P Q:pred A),
  (box M (P --> Q)) |-- (box M P --> box M Q).
Proof.
  intros; do 3 (hnf; intros).
  destruct M as [R HR]; simpl in *.
  destruct (valid_rel_commut_nec2 R HR _ _ H3 _ H1).
  apply H0 with x; auto.
Qed.

(* Box and diamond are positive modal operators *)

Lemma box_positive `{ASA A} : forall M (P Q:pred A),
  P |-- Q ->
  box M P |-- box M Q.
Proof.
  unfold derives, box; simpl; intuition.
Qed.

Lemma diamond_positive `{ASA A} : forall M (P Q:pred A),
  P |-- Q ->
  diamond M P |-- diamond M Q.
Proof.
  unfold derives, diamond; simpl; firstorder.
Qed.

Lemma box_refl_trans `{ASA A}: forall (m:modality) p,
  reflexive _ m ->
  transitive _ m ->
  box m (box m p) = box m p.
Proof.
  intros.
  apply equiv_eq.
  repeat intro.
  assert (box m p a').
  apply H2; auto.
  apply H4.
  apply H0.
  repeat intro.
  apply H2.
  eapply H1; eauto.
Qed.

(* Disribuitivity of box over various connectives *)

Lemma box_and `{ASA A}: forall R (P Q:pred A),
  box R (P && Q) = box R P && box R Q.
Proof.
  intros; apply equiv_eq; hnf; intuition;
    unfold intersection, box in *; simpl in *; firstorder.
Qed.

Lemma box_all `{ASA A} : forall B R (F:B -> pred A),
  box R (universal F) = All_ x:B, box R (F x).
Proof.
  intros; apply equiv_eq; hnf; intuition;
    unfold universal, box in *; simpl in *; firstorder.
Qed.

Lemma box_ex `{ASA A} : forall B R (F:B->pred A),
  Ex_ x:B, box R (F x) |-- box R (existential F).
Proof.
  unfold derives, existential, box; simpl; firstorder.
Qed.

Lemma box_or `{ASA A} : forall R (P Q:pred A),
   box R P || box R Q |-- box R (P || Q).
Proof.
  unfold derives, union, box; simpl; firstorder.
Qed.

(* Distributivity of diamond over various operators *)

Lemma diamond_or `{ASA A} : forall R (P Q:pred A),
  diamond R (P || Q) = diamond R P || diamond R Q.
Proof.
  intros; apply equiv_eq; hnf; intuition;
    unfold diamond, union in *; simpl in *; firstorder.
Qed.

Lemma diamond_ex `{ASA A} : forall B R (F:B -> pred A),
  diamond R (existential F) = Ex_ x:B, diamond R (F x).
Proof.
  intros; apply equiv_eq; hnf; intuition;
    unfold diamond, existential in *; simpl in *; firstorder.
Qed.

Lemma diamond_and `{ASA A} : forall R (P Q:pred A),
  diamond R (P && Q) |-- diamond R P && diamond R Q.
Proof.
  unfold derives, intersection, diamond; simpl; firstorder.
Qed.

Lemma diamond_all `{ASA A} : forall B R (F:B->pred A),
  diamond R (universal F) |-- All_ x:B, diamond R (F x).
Proof.
  unfold derives, universal, diamond; simpl; firstorder.
Qed.


(* Rules for the BI connectives *)

Lemma wand_con_adjoint `{ASA A} : forall (P Q R:pred A),
  (P * Q) |-- R <-> P |-- (Q -* R).
Proof.
  split; intros.
  hnf; intros; simpl; intros.
  apply H0.
  exists x'; exists y.
  intuition.
  apply pred_nec_hereditary with a; auto.
  hnf; intros.
  hnf in H0.
  unfold wand in H0; simpl in H0.
  destruct H1 as [w [v [? [? ?]]]].
  eapply H0; eauto.
Qed.

Lemma con_assoc `{ASA A} : forall (P Q R:pred A),
  (P * Q) * R = P * (Q * R).
Proof.
  intros; apply equiv_eq; hnf; intros.
  destruct H0 as [x [y [? [? ?]]]].
  destruct H1 as [z [w [? [? ?]]]].
  destruct (join_assoc _ _ _ _ _ H1 H0) as [q [? ?]].
  exists z; exists q; intuition.
  exists w; exists y; intuition.
  destruct H0 as [x [y [? [? ?]]]].
  destruct H2 as [z [w [? [? ?]]]].
  apply join_com in H0.
  apply join_com in H2.
  destruct (join_assoc _ _ _ _ _ H2 H0) as [q [? ?]].
  exists q; exists w; intuition.
  apply join_com; auto.
  exists x; exists z; intuition.
  apply join_com; auto.
Qed.

Lemma con_comm `{ASA A} : forall (P Q:pred A),
  P * Q = Q * P.
Proof.
  intros; apply equiv_eq; hnf; intros.
  destruct H0 as [x [y [? [? ?]]]].
  exists y; exists x; intuition; apply join_com; auto.
  destruct H0 as [x [y [? [? ?]]]].
  exists y; exists x; intuition; apply join_com; auto.
Qed.

Lemma split_con `{ASA A} : forall (P Q R S:pred A),
  P |-- Q ->
  R |-- S ->
  (P * R) |-- (Q * S).
Proof.
  intros; hnf; intros.
  destruct H2 as [x [y [? [? ?]]]].
  exists x; exists y; intuition.
Qed.

Lemma con_cut `{ASA A} : forall (P Q R S:pred A),
  P |-- (Q -* R) ->
  S |-- Q ->
  (P * S) |-- R.
Proof.
  intros.
  rewrite wand_con_adjoint.
  hnf; intros.
  simpl; intros.
  eapply H0; eauto.
Qed.

Lemma con_emp1 `{ASA A} : forall (P:pred A),
  emp * P = P.
Proof.
  intros; apply equiv_eq; hnf; intros.
  destruct H0 as [x [y [? [? ?]]]].
  simpl in H1.
  replace a with y; auto.
  destruct (join_ex_units a) as [u ?].
  exists u; exists a; intuition.
  simpl.
  apply unit_identity with a; auto.
Qed.

Lemma con_emp2 `{ASA A} : forall (P:pred A),
  P * emp = P.
Proof.
  intros.
  rewrite con_comm.
  apply con_emp1.
Qed.


(* Lemmas about aging and the later operator *)

Lemma nec_useless `{ASA A} :
  forall P, []P = P.
intros.
  apply equiv_eq; intros.
  hnf; intros; apply H0.
  simpl; apply necM_refl.
  hnf; intros.
  hnf; intros.
  apply pred_nec_hereditary with a; auto.
Qed.


Lemma later_age `{ASA A} : forall P,
  |>P = box ageM P.
Proof.
  intros; apply equiv_eq; do 2 (hnf; intros).
  simpl in H0.
  apply H0.
  apply t_step; auto.
  revert H0; induction H1; intros.
  apply H1; auto.
  apply pred_nec_hereditary with y.
  apply Rt_Rft; auto.
  apply IHclos_trans1; auto.
Qed.

Lemma now_later `{ASA A} : forall P,
  P |-- |>P.
Proof.
  repeat intro.
  apply pred_nec_hereditary with a; auto.
  apply Rt_Rft; auto.
Qed.

Lemma now_later2 `{ASA A} : forall G P,
  G |-- P ->
  G |-- |>P.
Proof.
  intros; apply derives_cut with P; auto.
  apply now_later.
Qed.

(* The "induction" rule for later *)

Lemma goedel_loeb `{ASA A} : forall (P Q:pred A),
  Q && |>P |-- P ->
  Q |-- P.
Proof.
  intros; hnf; intro a.
  induction a using age_induction.
  intros; simpl in H0.
  eapply H0; auto.
  split; auto.
  rewrite later_age.
  simpl; intros.
  apply H1; auto.
  apply pred_hereditary with a; auto.
Qed.

(* Later distributes over almost everything! *)

Lemma later_commute_dia `{ASA A} : forall M (P:pred A),
  diamond M (|> P) |-- |> (diamond M P).
Proof.
  intros.
  repeat rewrite later_age.
  do 3 (hnf; intros).
  simpl in H0.
  firstorder.
  destruct M as [R HR].
  simpl in *.
  destruct HR.
  destruct (H3 _ _ H1 _ H0).
  exists x0; split; auto.
Qed.


Lemma later_commute `{ASA A} : forall M (P:pred A),
  box M (|>P) = |>(box M P).
Proof.
  intros.
  apply equiv_eq; do 3 (hnf; intros).
  destruct M as [R HR].
  destruct (valid_rel_commut_later2 R HR _ _ H2 _ H1).
  apply H0 with x; simpl; auto.
  destruct M as [R HR].
  destruct (valid_rel_commut_later1 R HR _ _ H2 _ H1).
  apply H0 with x; auto.
Qed.

Lemma later_and `{ASA A} : forall P Q,
  |>(P && Q) = |>P && |> Q.
Proof.
  intros; apply box_and.
Qed.

Lemma later_or `{ASA A} : forall (P Q:pred A),
  |>(P || Q) = |>P || |>Q.
Proof.
  intros.
  repeat rewrite later_age.
  apply equiv_eq.
  2: apply box_or.
  hnf; intros.
  simpl in H0.
  case_eq (age1 a); intros.
  destruct (H0 a0); auto.
  left; simpl; intros.
  replace a' with a0; auto.
  congruence.
  right; simpl; intros.
  replace a' with a0; auto.
  congruence.
  left.
  hnf; simpl; intros.
  hnf in H2.
  rewrite H1 in H2; discriminate.
Qed.

Lemma later_ex `{ASA A} : forall B (F:B->pred A),
  B ->
  |>(existential F) = Ex_ x:B, |>(F x).
Proof.
  intros.
  apply equiv_eq.
  2: apply box_ex.
  hnf; intros.
  rewrite later_age in H0.
  case_eq (age1 a); intros.
  destruct (H0 a0); auto.
  exists x.
  rewrite later_age; simpl; intros.
  replace a' with a0; auto.
  congruence.
  exists X.
  rewrite later_age.
  hnf; simpl; intros.
  unfold age in H2.
  rewrite H1 in H2; discriminate.
Qed.

Lemma later_impl `{ASA A} : forall P Q,
  |>(P --> Q) = |>P --> |>Q.
Proof.
  intros; repeat rewrite later_age.
  apply equiv_eq.
  apply axiomK.
  hnf; intros.
  simpl; intros.
  simpl in H0.
  destruct valid_rel_nec.
  destruct (H5 _ _ H2 _ H1).
  apply H0 with x; auto.
  intros.
  replace a'1 with a'0; auto.
  congruence.
Qed.


Lemma later_wand `{ASA A} : forall P Q,
  |>(P -* Q) = |>P -* |>Q.
Proof.
  intros.
  repeat rewrite later_age.
  apply equiv_eq; hnf; intros.
  simpl; intros.
  simpl in H0.
  case_eq (age1 a); intros. 
  spec H0 a0 H5.
  apply nec_refl_or_later in H1.
  destruct H1; subst.
  destruct (age1_join2 _ _ H2 H4) as [w [v [? [? ?]]]].
  eapply H0; eauto.
  replace a0 with w; auto.
  congruence.
  assert (necR a0 x').
  eapply age_later_nec; eauto.
  destruct (age1_join2 _ _ H2 H4) as [w [v [? [? ?]]]].
  apply H0 with w v; auto.
  apply rt_trans with x'; auto.
  apply rt_step; auto.
  apply nec_refl_or_later in H1; destruct H1; subst.
  destruct (age1_join2 _ _ H2 H4) as [w [v [? [? ?]]]].
  hnf in H6.
  rewrite H5 in H6; discriminate.
  clear -H1 H5.
  elimtype False.
  revert H5; induction H1; auto.
  intros.
  unfold age in H0.
  rewrite H0 in H5; discriminate.

  simpl; intros.
  simpl in H0.
  destruct (valid_rel_nec).
  destruct (H6 _ _ H2 _ H1).
  destruct (unage1_join _ _ H3 H7) as [w [v [? [? ?]]]].
  apply H0 with x w v; auto.
  intros.
  replace a'0 with y; auto.
  congruence.
Qed.

Lemma later_con `{ASA A} : forall P Q,
  |>(P * Q) = |>P * |>Q.
Proof.
  intros.
  repeat rewrite later_age.
  apply equiv_eq; hnf; intros.
  simpl in H0.
  case_eq (age1 a); intros.
  destruct (H0 a0) as [w [v [? [? ?]]]]; auto.
  destruct (unage1_join2 _ _ H2 H1) as [w' [v' [? [? ?]]]].
  exists w'; exists v'; intuition.
  simpl; intros.
  replace a' with w; auto.
  unfold age in *; congruence.
  simpl; intros.
  replace a' with v; auto.
  unfold age in *; congruence.
  destruct (join_ex_units a).
  exists x; exists a.
  intuition.
  hnf; intros.
  red in u.
  simpl in H2.
  destruct (age1_join _ _ u H2) as [s [t [? [? ?]]]].
  unfold age in H5.
  rewrite H1 in H5; discriminate.
  hnf; intros.
  simpl in H2.
  unfold age in H2.
  rewrite H1 in H2; discriminate.
  
  destruct H0 as [w [v [? [? ?]]]].
  hnf; intros.
  simpl in H3.
  destruct (age1_join2 _ _ H0 H3) as [w' [v' [? [? ?]]]].
  exists w'; exists v'; intuition.
Qed.


Lemma TT_boxy `{ASA A} : forall M,
  boxy M TT.
Proof.
  intros; hnf.
  apply equiv_eq; repeat intro; simpl; auto.
Qed.

Lemma positive_boxy `{ASA A} : forall P Q M,
  boxy M P ->
  P |-- Q ->
  P |-- box M Q.
Proof.
  intros.
  rewrite <- H0.
  apply box_positive.
  auto.
Qed.

Lemma forallI `{ASA A} : forall A G X,
  (forall x:A, G |-- X x) ->
  G |-- universal X.
Proof.
  repeat intro.
  eapply H0; auto.
Qed.

Lemma TT_and `{ASA A} : forall P,
  TT && P = P.
Proof.
  intros; apply equiv_eq; repeat intro.
  destruct H0; auto.
  split; simpl; auto.
Qed.

Lemma and_comm `{ASA A} : forall P Q,
  P && Q = Q && P.
Proof.
  intros; apply equiv_eq; unfold intersection; repeat intro; simpl in *; intuition.
Qed.

Lemma and_assoc `{ASA A} : forall P Q R,
  P && (Q && R) = (P && Q) && R.
Proof.
  intros; apply equiv_eq; auto; unfold derives, intersection; simpl; intuition.
Qed.