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

Require Import VST.msl.base.
Require Import VST.msl.ageable.

Delimit Scope pred with pred.
Local Open Scope pred.

(* A "pre-predicate" is hereditary iff whenever it is
   true at world a, it is also true at all worlds
   accessable from a via R.
 *)
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Definition hereditary {A} (R:A->A->Prop) (p:A->Prop) :=
  forall a a':A, R a a' -> p a -> p a'.

(* A predicate is a hereditary pre-predicate *)
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Definition pred (A:Type) {AG:ageable A} :=
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
  { p:A -> Prop | hereditary age p }.

Bind Scope pred with pred.

(* Here is some junk that makes the definition of "pred" opaque
   to most tactics but still 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 {A} `{ageable A} (p:pred A) : A -> Prop := proj1_sig p.
Definition pred_hereditary `{ageable} (p:pred A) := proj2_sig p.
Coercion app_pred : pred >-> Funclass.
Global Opaque pred.

Hint Resolve @pred_hereditary.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma nec_hereditary {A} `{ageable A} (p: A -> Prop) : hereditary age p ->
  forall a a':A, necR a a' -> p a -> p a'.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros.
(* Goal: p a' *)
  induction H1; auto.
(* Goal: @app_pred A H Q a'0 *)
  apply H0 with x; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma pred_nec_hereditary {A} `{ageable A} (p:pred A) :
  forall a a':A, necR a a' -> p a -> p a'.
Proof.
(* Goal: forall (a a' : A) (_ : @necR A H a a') (_ : @app_pred A H p a), @app_pred A H p a' *)
  apply nec_hereditary, pred_hereditary.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Program Definition mkPred {A} `{ageable A} (p:A -> Prop) : pred A :=
  fun x => forall x', necR x x' -> p x'.
Next Obligation.
(* Goal: forall (P : Prop) (Q R : @pred A agA) (_ : P) (_ : @derives A agA Q R), @derives A agA Q (@andp A agA (@prop A agA P) R) *)
  repeat intro.
(* Goal: @proj1_sig (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A H) p) (f b) a *)
  apply H1.
(* Goal: @necR A H a a'0 *)
  apply rt_trans with a'; auto.
(* Goal: clos_refl_trans A (@age A H) a a' *)
  apply rt_step; auto.
Qed.

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

(* "valid" relations are those that commute with aging.  These
   relations are the ones that can be turned into modalities.
 *)
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Definition valid_rel {A} `{ageable A} (R:relation A) : Prop :=
  commut A age R /\ commut A R age.

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

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

(* commutivity facts for the basic relations *)

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma valid_rel_commut_later1 {A} `{ageable A} : forall R,
  valid_rel R ->
  commut A laterR R.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros; hnf; intros.
(* Goal: @ex2 A (fun y' : A => R y' x) (fun y' : A => @laterR A H z y') *)
  revert z H2.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  induction H1; intros.
(* Goal: @app_pred A H (@box A H (@laterM A H) (@andp A H P Q)) w *)
  destruct H0.
(* Goal: @ex2 A (fun y' : A => R y' y) (fun y' : A => @laterR A H z y') *)
(* Goal: @ex2 A (fun y' : A => R y' z) (fun y' : A => @laterR A H z0 y') *)
  destruct (H0 _ _ H1 _ H2).
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @necR A H z y') *)
  exists x0; auto.
(* Goal: @laterR A H a a' *)
(* Goal: @app_pred A H P a' *)
  apply t_step; auto.
(* Goal: @ex2 A (fun y' : A => @laterR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @laterR A H z y') *)
  destruct (IHclos_trans1 _ H2).
(* Goal: @ex2 A (fun y' : A => @laterR A H y' x0) (fun y' : A => R x y') *)
  destruct (IHclos_trans2 _ H1).
(* Goal: @ex2 A (fun y' : A => @age A H y' z) (fun y' : A => @necR A H z0 y') *)
  exists x1; auto.
(* Goal: @laterR A H z0 x1 *)
  eapply t_trans; eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma valid_rel_commut_later2 {A} `{ageable A} : forall R,
  valid_rel R ->
  commut A R laterR.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros; hnf; intros.
(* Goal: @ex2 A (fun y' : A => @laterR A H y' x) (fun y' : A => R z y') *)
  revert x H1.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  induction H2; intros.
(* Goal: @app_pred A H (@box A H (@laterM A H) (@andp A H P Q)) w *)
  destruct H0.
(* Goal: @ex2 A (fun y' : A => @laterR A H y' x0) (fun y' : A => R x y') *)
(* Goal: @ex2 A (fun y' : A => @laterR A H y' x0) (fun y' : A => R x y') *)
  destruct (H3 _ _ H2 _ H1).
(* Goal: @ex2 A (fun y' : A => @age A H y' z) (fun y' : A => @necR A H z0 y') *)
  exists x1; auto.
(* Goal: @laterR A H a a' *)
(* Goal: @app_pred A H P a' *)
  apply t_step; auto.
(* Goal: @ex2 A (fun y' : A => @laterR A H y' x0) (fun y' : A => R x y') *)
  destruct (IHclos_trans2 _ H1).
(* Goal: @ex2 A (fun y' : A => @laterR A H y' x0) (fun y' : A => R x y') *)
  destruct (IHclos_trans1 _ H3).
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @necR A H z y') *)
  exists x2; auto.
(* Goal: @laterR A H z0 x1 *)
  eapply t_trans; eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma valid_rel_commut_nec1 {A} `{ageable A} : forall R,
  valid_rel R ->
  commut A necR R.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros; hnf; intros.
(* Goal: @ex2 A (fun y' : A => R y' x) (fun y' : A => @necR A H z y') *)
  apply nec_refl_or_later in H1; destruct H1; subst.
(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @necR A H z y') *)
(* Goal: @ex2 A (fun y' : A => @age A H y' z) (fun y' : A => @necR A H z0 y') *)
  exists z; auto.
(* Goal: @ex2 A (fun y' : A => R y' x) (fun y' : A => @necR A H z y') *)
  destruct (valid_rel_commut_later1 R H0 x y H1 z H2).
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @necR A H z y') *)
  exists x0; auto.
(* Goal: @necR A H a a' *)
  apply Rt_Rft; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma valid_rel_commut_nec2 {A} `{ageable A} : forall R,
  valid_rel R ->
  commut A R necR.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros; hnf; intros.
(* Goal: @ex2 A (fun y' : A => @necR A H y' x) (fun y' : A => R z y') *)
  apply nec_refl_or_later in H2; destruct H2; subst.
(* Goal: @app_pred A HA (@exp A HA B q) w *)
  exists x; auto.
(* Goal: @ex2 A (fun y' : A => @necR A H y' x) (fun y' : A => R z y') *)
  destruct (valid_rel_commut_later2 R H0 x y H1 z H2).
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @necR A H z y') *)
  exists x0; auto.
(* Goal: @necR A H a a' *)
  apply Rt_Rft; auto.
Qed.

Lemma valid_rel_age {A} `{ageable A} : valid_rel age.
Proof.
(* Goal: @valid_rel A H (@age A H) *)
  intros; split; hnf; intros; firstorder.
Qed.

Lemma valid_rel_later {A} `{ageable A} : valid_rel laterR.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros; split; hnf; intros.
(* Goal: @ex2 A (fun y' : A => @necR A H y' x) (fun y' : A => @age A H z y') *)
(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @necR A H z y') *)
  revert x H0.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  induction H1; intros.
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @necR A H z y') *)
  exists y; auto.
(* Goal: @laterR A H a a' *)
(* Goal: @app_pred A H P a' *)
  apply t_step; auto.
(* Goal: @ex2 A (fun y' : A => @age A H y' z) (fun y' : A => @laterR A H z0 y') *)
  destruct (IHclos_trans2 _ H0).
(* Goal: @ex2 A (fun y' : A => @laterR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @laterR A H z y') *)
  destruct (IHclos_trans1 _ H2).
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @necR A H z y') *)
  exists x2; auto.
(* Goal: @laterR A H z0 x1 *)
  eapply t_trans; eauto.

(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @necR A H z y') *)
  revert z H1.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  induction H0; intros.
(* Goal: @app_pred A HA (@exp A HA B q) w *)
  exists x; auto.
(* Goal: @laterR A H a a' *)
(* Goal: @app_pred A H P a' *)
  apply t_step; auto.
(* Goal: @ex2 A (fun y' : A => @age A H y' z) (fun y' : A => @laterR A H z0 y') *)
  destruct (IHclos_trans1 _ H1).
(* Goal: @ex2 A (fun y' : A => @age A H y' z) (fun y' : A => @laterR A H z0 y') *)
  destruct (IHclos_trans2 _ H0).
(* Goal: @ex2 A (fun y' : A => @age A H y' z) (fun y' : A => @necR A H z0 y') *)
  exists x1; auto.
(* Goal: @laterR A H z0 x1 *)
  eapply t_trans; eauto.
Qed.

Lemma valid_rel_nec {A} `{ageable A} : valid_rel necR.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros; split; hnf; intros.
(* Goal: @ex2 A (fun y' : A => @necR A H y' x) (fun y' : A => @age A H z y') *)
(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @necR A H z y') *)
  revert x H0.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  induction H1; intros.
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @necR A H z y') *)
  exists y; auto.
(* Goal: clos_refl_trans A (@age A H) a a' *)
  apply rt_step; auto.
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @necR A H z y') *)
  exists x0; auto.
(* Goal: @ex2 A (fun y' : A => @age A H y' z) (fun y' : A => @necR A H z0 y') *)
  destruct (IHclos_refl_trans2 _ H0).
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @necR A H z y') *)
  destruct (IHclos_refl_trans1 _ H2).
(* Goal: @ex2 A (fun y' : A => @necR A H y' x0) (fun y' : A => @age A H x y') *)
(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @necR A H z y') *)
  exists x2; auto.
(* Goal: @necR A H z0 x1 *)
  eapply rt_trans; eauto.

(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @necR A H z y') *)
  revert z H1.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  induction H0; intros.
(* Goal: @app_pred A HA (@exp A HA B q) w *)
  exists x; auto.
(* Goal: clos_refl_trans A (@age A H) a a' *)
  apply rt_step; auto.
(* Goal: @ex2 A (fun y' : A => @age A H y' x) (fun y' : A => @necR A H z y') *)
(* Goal: @ex2 A (fun y' : A => @age A H y' z) (fun y' : A => @necR A H z0 y') *)
  exists z; auto.

(* Goal: @ex2 A (fun y' : A => @age A H y' z) (fun y' : A => @necR A H z0 y') *)
  destruct (IHclos_refl_trans1 _ H1).
(* Goal: @ex2 A (fun y' : A => @age A H y' z) (fun y' : A => @necR A H z0 y') *)
  destruct (IHclos_refl_trans2 _ H0).
(* Goal: @ex2 A (fun y' : A => @age A H y' z) (fun y' : A => @necR A H z0 y') *)
  exists x1; auto.
(* Goal: @necR A H z0 x1 *)
  eapply rt_trans; eauto.
Qed.

(* Definitions of the basic modalities.
 *)
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Definition ageM {A} `{ageable A} : modality
  := exist _ age valid_rel_age.
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Definition laterM {A} `{ageable A} : modality
  := exist _ laterR valid_rel_later.
(*
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Definition necM {A} `{ageable A} : modality
  := exist _ necR valid_rel_nec.
*)

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.
 *)

(* Lifting pure mathematical facts to predicates *)

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Program Definition prop {A} `{ageable A}  (P: Prop) : pred A := (fun _  => P).

Definition TT {A} `{ageable A}: pred A := prop True.
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Definition FF  {A} `{ageable A}: pred A := prop False.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Program Definition imp {A} `{ageable A} (P Q:pred A) : pred A :=
   fun a:A => forall a':A, necR a a' -> P a' -> Q a'.
Next Obligation.
(* Goal: @app_pred A H P a' *)
  apply H1; auto.
(* Goal: @necR A H a a'0 *)
  apply rt_trans with a'; auto.
(* Goal: clos_refl_trans A (@age A H) a a' *)
  apply rt_step; auto.
Qed.
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Program Definition orp {A} `{ageable 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.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Program Definition andp {A} `{ageable A} (P Q:pred A) : pred A :=
   fun a:A => P a /\ Q a.

(* Universal and exp quantification
 *)

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Program Definition allp {A} `{ageable A} {B: Type} (f: B -> pred A) : pred A
  := fun a => forall b, f b a.
Next Obligation.
(* Goal: @app_pred A H (f b) a' *)
  apply pred_hereditary with a; auto.
(* Goal: @proj1_sig (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A H) p) (f b) a *)
  apply H1.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Program Definition exp {A} `{ageable A} {B: Type} (f: B -> pred A) : pred A
  := fun a => exists b, f b a.
Next Obligation.
(* Goal: @ex B (fun b : B => @app_pred A H (f b) a') *)
  destruct H1; exists x; eapply pred_hereditary; eauto.
Qed.


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

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Program Definition box {A} `{ageable A} (M:modality) (P:pred A) : pred A :=
  fun a:A => forall a', M a a' -> P a'.
Next Obligation.
(* Goal: @ex A (fun a'0 : A => and (@app_mode A H M a'0 a') (@app_pred A H P a'0)) *)
  destruct M as [M [H3 H4]]; simpl in *.
(* Goal: @app_pred A H P a'0 *)
  destruct (H4 _ _ H2 _ H0).
(* Goal: @app_pred A H Q a' *)
  apply pred_hereditary with x; auto.
(* Goal: @app_pred A H P a' *)
  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).
 *)

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Program Definition diamond {A} `{ageable A} (M:modality) (P:pred A) : pred A :=
  fun a:A => exists a', M a' a /\ P a'.
Next Obligation.
(* Goal: @ex A (fun a'0 : A => and (@app_mode A H M a'0 a') (@app_pred A H P a'0)) *)
  destruct M as [M [H3 H4]]; simpl in *.
(* Goal: @ex A (fun a'0 : A => and (M a'0 a') (@app_pred A H P a'0)) *)
  destruct H1 as [x [? ?]].
(* Goal: @ex A (fun a'0 : A => and (M a'0 a') (@app_pred A H P a'0)) *)
  destruct (H3 _ _ H0 _ H1).
(* Goal: @ex A (fun a'0 : A => and (R a'0 a') (@app_pred A H P a'0)) *)
  exists x0; split; auto.
(* Goal: @app_pred A H Q a' *)
  apply pred_hereditary with x; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Definition boxy {A} `{ageable A} (m: modality) (p: pred A): Prop :=  box m p = 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 " := (exp (fun x:T => P%pred)) (at level 65, x at level 99) : pred.
Notation "'ALL'  x ':' T  ',' P " := (allp (fun x:T => P%pred)) (at level 65, x at level 99) : pred.
Infix "||" := orp (at level 50, left associativity) : pred.
Infix "&&" := andp (at level 40, left associativity) : pred.
Notation "P '-->' Q" := (imp P Q) (at level 55, right associativity) : pred.
Notation "P '<-->' Q" := (andp (imp P Q) (imp Q P)) (at level 57, no associativity) : pred.
(* Notation "'[]' e" := (box necM e) (at level 30, right associativity): pred. *)
Notation "'|>' e" := (box laterM e) (at level 30, right associativity): pred.
Notation "'!!' e" := (prop e) (at level 25) : pred.

(* Rules for the propositional connectives *)
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma modus_ponens {A} `{ageable A} : forall (X P Q:pred A),
  X |-- P ->
  X |-- (P --> Q) ->
  X |-- Q.
Proof.
(* Goal: forall (X P Q : @pred A H) (_ : @derives A H X P) (_ : @derives A H X (@imp A H P Q)), @derives A H X Q *)
  unfold derives, imp; simpl; intuition eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma andp_right {A} `{ageable A} : forall (X P Q:pred A),
  X |-- P ->
  X |-- Q ->
  X |-- P && Q.
Proof.
(* Goal: forall (X P Q : @pred A H) (_ : @derives A H X P) (_ : @derives A H X Q), @derives A H X (@andp A H P Q) *)
  unfold derives, imp, andp; simpl; intuition.
Qed.


(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
  Lemma pred_ext' {A} `{ageable A}: forall (p1 p2:pred A),
    app_pred p1 = app_pred p2 ->
    p1 = p2.
  Proof.
(* Goal: forall (p1 p2 : @pred A H) (_ : @eq (forall _ : A, Prop) (@app_pred A H p1) (@app_pred A H p2)), @eq (@pred A H) p1 p2 *)
    intros; destruct p1; destruct p2; simpl in H.
(* Goal: @app_pred A H Q a'0 *)
   simpl in H0.
(* Goal: @eq (@pred A H) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A H) p) x h) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A H) p) x0 h0) *)
    subst x0.
(* Goal: @eq (@pred A H) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A H) p) x h) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A H) p) x h0) *)
    replace h0 with h by apply proof_irr.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
    auto.
  Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma pred_ext : forall A `{ageable A} (P Q:pred A),
  derives P Q -> derives Q P -> P = Q.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros.
(* Goal: @eq (@pred A H) P Q *)
  destruct P as [P HP].
(* Goal: @eq (@pred A H) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A H) p) P HP) Q *)
  destruct Q as [Q HQ].
(* Goal: @eq (@pred A H) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A H) p) P HP) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A H) p) Q HQ) *)
  unfold derives in *. simpl in *.
(* Goal: @eq (@pred A H) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A H) p) P HP) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A H) p) Q HQ) *)
   apply (exist_ext (A->Prop) (fun p => hereditary (@age _ H) p)).
(* Goal: @eq (forall _ : A, Prop) P Q *)
  extensionality a.
(* Goal: @eq Prop (P a) (Q a) *)
  apply prop_ext; intuition.
Qed.

Lemma andp_dup {A}{agA: ageable A}: forall P: pred A, P && P = P.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
Proof. intros. apply pred_ext; intros w ?. destruct H; auto. split; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma andp_left1{A}{agA: ageable A}: forall P Q R: pred A,  P |-- R -> P && Q |-- R.
(* Goal: forall (P : Prop) (Q R : @pred A agA) (_ : P) (_ : @derives A agA Q R), @derives A agA Q (@andp A agA (@prop A agA P) R) *)
Proof. repeat intro. destruct H0; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma andp_left2{A}{agA: ageable A}: forall P Q R: pred A,  Q |-- R -> P && Q |-- R.
(* Goal: forall (P : Prop) (Q R : @pred A agA) (_ : P) (_ : @derives A agA Q R), @derives A agA Q (@andp A agA (@prop A agA P) R) *)
Proof. repeat intro. destruct H0; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma orp_left{A}{agA: ageable A}: forall P Q R: pred A,  P |-- R -> Q |-- R -> P || Q |-- R.
(* Goal: forall (P : Prop) (Q R : @pred A agA) (_ : P) (_ : @derives A agA Q R), @derives A agA Q (@andp A agA (@prop A agA P) R) *)
Proof. repeat intro. destruct H1; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma orp_right1{A}{agA: ageable A}: forall P Q R: pred A,  P |-- Q -> P |-- Q || R.
(* Goal: forall (P : Prop) (Q R : @pred A agA) (_ : P) (_ : @derives A agA Q R), @derives A agA Q (@andp A agA (@prop A agA P) R) *)
Proof. repeat intro. left; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma orp_right2{A}{agA: ageable A}: forall P Q R: pred A,  P |-- R -> P |-- Q || R.
(* Goal: forall (P : Prop) (Q R : @pred A agA) (_ : P) (_ : @derives A agA Q R), @derives A agA Q (@andp A agA (@prop A agA P) R) *)
Proof. repeat intro. right; auto.
Qed.


(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma derives_trans {A}`{ageable A}:
    forall P Q R: pred A, P |-- Q -> Q |-- R -> P |-- R.
Proof. firstorder. Qed.

Lemma exp_right:
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
  forall {B A: Type}{agA: ageable A}(x:B) p (q: B -> pred A),
    p |-- q x ->
    p |-- exp q.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @derives A agA p (@exp A agA B q) *)
eapply derives_trans; try apply H.
(* Goal: @app_pred A HA (@exp A HA B q) w *)
intros w ?; exists x; auto.
Qed.

Lemma exp_left:
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
  forall {B A: Type}{agA: ageable A}(p: B -> pred A) q,
  (forall x, p x |-- q) ->
   exp p |-- q.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @derives A agA (@exp A agA B p) q *)
intros w [x' ?].
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
eapply H; eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma and1 {A} `{ageable A} : forall (X P Q:pred A),
  X |-- P && Q --> P.
Proof.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  unfold derives, imp, andp; simpl; intuition eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma and2 {A} `{ageable A} : forall (X P Q:pred A),
  X |-- P && Q --> Q.
Proof.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  unfold derives, imp, andp; simpl; intuition eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma and3 {A} `{ageable A} : forall (X P Q R:pred A),
  X |-- (P --> Q) --> (P --> R) --> (P --> Q && R).
Proof.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  unfold derives, imp, andp; simpl; intuition eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma or1 {A} `{ageable A} : forall (X P Q:pred A),
  X |-- P --> P || Q.
Proof.
(* Goal: forall X P Q : @pred A H, @derives A H X (@imp A H Q (@orp A H P Q)) *)
  unfold derives, imp, orp; simpl; intuition.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma or2 {A} `{ageable A} : forall (X P Q:pred A),
  X |-- Q --> P || Q.
Proof.
(* Goal: forall X P Q : @pred A H, @derives A H X (@imp A H Q (@orp A H P Q)) *)
  unfold derives, imp, orp; simpl; intuition.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma or3 {A} `{ageable A} : forall (X P Q R:pred A),
  X |-- (P --> R) --> (Q --> R) --> (P || Q --> R).
Proof.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  unfold derives, imp, orp; simpl; intuition eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma TTrule {A} `{ageable A} : forall X P,
  X |-- P --> TT.
Proof.
(* Goal: forall X P : @pred A H, @derives A H X (@imp A H P (@TT A H)) *)
  unfold derives, imp, TT; simpl; intuition.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma FFrule {A} `{ageable A} : forall X P,
  X |-- FF --> P.
Proof.
(* Goal: forall X P : @pred A H, @derives A H X (@imp A H (@FF A H) P) *)
  unfold derives, imp, FF; simpl; intuition.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma distribution {A} `{ageable A} : forall (X P Q R:pred A),
  X |-- P && (Q || R) --> (P && Q) || (P && R).
Proof.
(* Goal: forall X P Q R : @pred A H, @derives A H X (@imp A H (@andp A H P (@orp A H Q R)) (@orp A H (@andp A H P Q) (@andp A H P R))) *)
  unfold derives, imp, orp, andp; simpl; intuition.
Qed.

(* Characterize the relation between conjunction and implication *)
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma imp_andp_adjoint {A} `{ageable A} : forall (P Q R:pred A),
  (P && Q) |-- R <-> P |-- (Q --> R).
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  split; intros.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  hnf; intros; simpl; intros.
(* Goal: @app_pred A agA (P x) a *)
  apply H0.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  split; auto.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  apply pred_nec_hereditary with a; auto.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  hnf; intros.
(* Goal: @app_pred A H R a *)
  hnf in H0.
(* Goal: @app_pred A H Q a'0 *)
  unfold imp in H0; simpl in H0.
(* Goal: @app_pred A H R a *)
  destruct H1.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  apply H0 with a; auto.
Qed.

(* Some facts about modalities *)

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma box_e0 {A} `{ageable A}: forall (M: modality) Q,
            reflexive _ M -> box M Q  |-- Q.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intro; intros.
(* Goal: @app_pred A H Q a *)
apply H1; simpl.
(* Goal: @app_pred A agA (P x) a *)
apply H0.
Qed.
Arguments box_e0 [A] _ _ _ _ _ _.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma boxy_i {A} `{ageable A}:
  forall (Q: pred A) (M: modality),
    reflexive _ M ->
    (forall w w', M w w' -> Q w -> Q w') ->
    boxy M Q.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @boxy A H M Q *)
unfold boxy.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
apply pred_ext; hnf; intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
eapply box_e0; eauto.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
hnf; intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
eapply H1; eauto.
Qed.

(*
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma necM_refl {A} `{ageable A}: reflexive _ necM.
Proof.
(* Goal: @app_pred A H (@andp A H P Q) w' *)
intros; intro; simpl.
unfold necR.
(* Goal: @necR nat ag_nat (@level A H x) (@level A H x) *)
(* Goal: @necR nat ag_nat (@level A H x) (@level A H z) *)
constructor 2.
Qed.

Hint Resolve @necM_refl.
*)

(* relationship between box and diamond *)
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma box_diamond {A} `{ageable A} : forall M (P Q:pred A),
  (diamond M P) |-- Q <-> P |-- (box M Q).
Proof.
(* Goal: forall (M : @modality A H) (P Q : @pred A H), iff (@derives A H (@diamond A H M P) Q) (@derives A H P (@box A H M Q)) *)
  unfold derives; intuition.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  hnf; intros.
(* Goal: @app_pred A agA (P x) a *)
  apply H0.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  hnf; eauto.
(* Goal: @app_pred A H Q a *)
  destruct H1 as [a' [? ?]].
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  apply H0 with a'; auto.
Qed.

(* Box is a normal modal operator *)

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma ruleNec {A} `{ageable A} : forall M (P:pred A),
  derives TT P ->
  derives TT (box M P).
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros.
(* Goal: @derives A H (@TT A H) (@box A H M P) *)
  rewrite <- box_diamond.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  hnf; intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  apply H0; hnf; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma axiomK {A} `{ageable A}: forall M (P Q:pred A),
  (box M (P --> Q)) |-- (box M P --> box M Q).
Proof.
(* Goal: forall (M : @modality A H) (P Q : @pred A H), @derives A H (@box A H M (@imp A H P Q)) (@imp A H (@box A H M P) (@box A H M Q)) *)
  intros; do 3 (hnf; intros).
(* Goal: @app_pred A agA (@allp A agA B F) w' *)
  destruct M as [R HR]; simpl in *.
(* Goal: @app_pred A H Q a'0 *)
  destruct (valid_rel_commut_nec2 R HR _ _ H3 _ H1).
(* Goal: @app_pred A H Q a'0 *)
  apply H0 with x; auto.
Qed.

(* Box and diamond are positive modal operators *)

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma box_positive {A} `{ageable A} : forall M (P Q:pred A),
  P |-- Q ->
  box M P |-- box M Q.
Proof.
(* Goal: forall (M : @modality A H) (P Q : @pred A H) (_ : @derives A H P Q), @derives A H (@box A H M P) (@box A H M Q) *)
  unfold derives, box; simpl; intuition.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma diamond_positive {A} `{ageable A} : forall M (P Q:pred A),
  P |-- Q ->
  diamond M P |-- diamond M Q.
Proof.
(* Goal: forall P : @pred A H, @derives A H P P *)
  unfold derives, diamond; simpl; firstorder.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma box_refl_trans {A} `{ageable A}: forall (m:modality) p,
  reflexive _ m ->
  transitive _ m ->
  box m (box m p) = box m p.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros.
(* Goal: @eq (@pred A agA) (@andp A agA (@orp A agA P Q) R) (@orp A agA (@andp A agA P R) (@andp A agA Q R)) *)
  apply pred_ext.
(* Goal: forall (P : Prop) (Q R : @pred A agA) (_ : P) (_ : @derives A agA Q R), @derives A agA Q (@andp A agA (@prop A agA P) R) *)
  repeat intro.
(* Goal: @app_pred A H p a' *)
(* Goal: @derives A H (@box A H m p) (@box A H m (@box A H m p)) *)
  assert (box m p a').
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  apply H2; auto.
(* Goal: @app_pred A H p a' *)
(* Goal: @derives A H (@box A H m p) (@box A H m (@box A H m p)) *)
  apply H4.
(* Goal: @app_pred A agA (P x) a *)
  apply H0.
(* Goal: forall (P : Prop) (Q R : @pred A agA) (_ : P) (_ : @derives A agA Q R), @derives A agA Q (@andp A agA (@prop A agA P) R) *)
  repeat intro.
(* Goal: @app_pred A H p a'0 *)
  apply H2.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  eapply H1; eauto.
Qed.

(* Disribuitivity of box over various connectives *)

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma box_and {A} `{ageable A}: forall R (P Q:pred A),
  box R (P && Q) = box R P && box R Q.
Proof.
  intros; apply pred_ext; hnf; intuition;
(* Goal: forall P : @pred A H, @derives A H P P *)
    unfold andp, box in *; simpl in *; firstorder.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma box_all {A} `{ageable A} : forall B R (F:B -> pred A),
  box R (allp F) = ALL x:B, box R (F x).
Proof.
  intros; apply pred_ext; hnf; intuition;
(* Goal: forall P : @pred A H, @derives A H P P *)
    unfold allp, box in *; simpl in *; firstorder.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma box_ex {A} `{ageable A} : forall B R (F:B->pred A),
  EX x:B, box R (F x) |-- box R (exp F).
Proof.
(* Goal: forall P : @pred A H, @derives A H P P *)
  unfold derives, exp, box; simpl; firstorder.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma box_or {A} `{ageable A} : forall R (P Q:pred A),
   box R P || box R Q |-- box R (P || Q).
Proof.
(* Goal: forall P : @pred A H, @derives A H P P *)
  unfold derives, orp, box; simpl; firstorder.
Qed.

(* Distributivity of diamond over various operators *)

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma diamond_or {A} `{ageable A} : forall R (P Q:pred A),
  diamond R (P || Q) = diamond R P || diamond R Q.
Proof.
  intros; apply pred_ext; hnf; intuition;
(* Goal: forall P : @pred A H, @derives A H P P *)
    unfold diamond, orp in *; simpl in *; firstorder.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma diamond_ex {A} `{ageable A} : forall B R (F:B -> pred A),
  diamond R (exp F) = EX x:B, diamond R (F x).
Proof.
  intros; apply pred_ext; hnf; intuition;
(* Goal: forall P : @pred A H, @derives A H P P *)
    unfold diamond, exp in *; simpl in *; firstorder.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma diamond_and {A} `{ageable A} : forall R (P Q:pred A),
  diamond R (P && Q) |-- diamond R P && diamond R Q.
Proof.
(* Goal: forall P : @pred A H, @derives A H P P *)
  unfold derives, andp, diamond; simpl; firstorder.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma diamond_all {A} `{ageable A} : forall B R (F:B->pred A),
  diamond R (allp F) |-- ALL x:B, diamond R (F x).
Proof.
(* Goal: forall P : @pred A H, @derives A H P P *)
  unfold derives, allp, diamond; simpl; firstorder.
Qed.


(* Lemmas about aging and the later operator *)

(*
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma nec_useless {A} `{ageable A} :
  forall P, []P = P.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  apply pred_ext; intros.
(* Goal: @app_pred A agA (P x) a *)
  hnf; intros; apply H0.
  simpl; apply necM_refl.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  hnf; intros.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  hnf; intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  apply pred_nec_hereditary with a; auto.
Qed.
*)

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma later_age {A} `{ageable A} : forall P,
  |>P = box ageM P.
Proof.
(* Goal: forall P : @pred A H, @eq (@pred A H) (@box A H (@laterM A H) P) (@box A H (@ageM A H) P) *)
  intros; apply pred_ext; do 2 (hnf; intros).
(* Goal: @app_pred A H Q a'0 *)
  simpl in H0.
(* Goal: @app_pred A agA (P x) a *)
  apply H0.
(* Goal: @laterR A H a a' *)
(* Goal: @app_pred A H P a' *)
  apply t_step; auto.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  revert H0; induction H1; intros.
(* Goal: @app_pred A H P a' *)
  apply H1; auto.
(* Goal: @app_pred A H P z *)
  apply pred_nec_hereditary with y.
(* Goal: @necR A H a a' *)
  apply Rt_Rft; auto.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  apply IHclos_trans1; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma now_later {A} `{ageable A} : forall P,
  P |-- |>P.
Proof.
(* Goal: forall (P : Prop) (Q R : @pred A agA) (_ : P) (_ : @derives A agA Q R), @derives A agA Q (@andp A agA (@prop A agA P) R) *)
  repeat intro.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  apply pred_nec_hereditary with a; auto.
(* Goal: @necR A H a a' *)
  apply Rt_Rft; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma now_later2 {A} `{ageable A} : forall G P,
  G |-- P ->
  G |-- |>P.
Proof.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  intros; apply @derives_trans with P; auto.
(* Goal: @derives A H P (@box A H (@laterM A H) P) *)
  apply now_later.
Qed.

(* The "induction" rule for later *)

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma goedel_loeb {A} `{ageable A} : forall (P Q:pred A),
  Q && |>P |-- P ->
  Q |-- P.
Proof.
(* Goal: forall (P Q : @pred A H) (_ : @derives A H (@andp A H Q (@box A H (@laterM A H) P)) P), @derives A H Q P *)
  intros; hnf; intro a.
(* Goal: forall _ : @app_pred A H Q a, @app_pred A H P a *)
  induction a using age_induction.
(* Goal: @app_pred A H Q a'0 *)
  intros; simpl in H0.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  eapply H0; auto.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  split; auto.
(* Goal: @app_pred A H (@box A H (@laterM A H) P) x *)
  rewrite later_age.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  simpl; intros.
(* Goal: @app_pred A H P a' *)
  apply H1; auto.
(* Goal: @app_pred A H Q a' *)
  apply pred_hereditary with x; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma loeb {A} `{ageable A} : forall (P:pred A),
     |>P |-- P    ->     TT |-- P.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros. apply goedel_loeb.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  apply andp_left2. auto.
Qed.

(* Later distributes over almost everything! *)

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma later_commute_dia {A} `{ageable A} : forall M (P:pred A),
  diamond M (|> P) |-- |> (diamond M P).
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros.
(* Goal: @app_pred A H (@box A H (@laterM A H) P) x *)
  repeat rewrite later_age.
(* Goal: @derives A H (@diamond A H M (@box A H (@ageM A H) P)) (@box A H (@ageM A H) (@diamond A H M P)) *)
  do 3 (hnf; intros).
(* Goal: @app_pred A H Q a'0 *)
  simpl in H0.
(* Goal: forall P : @pred A H, @derives A H P P *)
  firstorder.
(* Goal: @app_pred A H P a'0 *)
  destruct M as [R HR].
(* Goal: @app_pred A agA (@allp A agA B F) w' *)
  simpl in *.
(* Goal: @ex A (fun a'0 : A => and (R a'0 a') (@app_pred A H P a'0)) *)
  destruct HR.
(* Goal: @ex A (fun a'0 : A => and (R a'0 a') (@app_pred A H P a'0)) *)
  destruct (H3 _ _ H1 _ H0).
(* Goal: @ex A (fun a'0 : A => and (R a'0 a') (@app_pred A H P a'0)) *)
  exists x0; split; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma later_commute {A} `{ageable A} : forall M (P:pred A),
  box M (|>P) = |>(box M P).
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros.
(* Goal: @derives A H (@diamond A H M (@box A H (@ageM A H) P)) (@box A H (@ageM A H) (@diamond A H M P)) *)
  apply pred_ext; do 3 (hnf; intros).
(* Goal: @app_pred A H P a'0 *)
  destruct M as [R HR].
(* Goal: @app_pred A H P a'0 *)
(* Goal: @app_pred A H P a'0 *)
  destruct (valid_rel_commut_later2 R HR _ _ H2 _ H1).
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  apply H0 with x; simpl; auto.
(* Goal: @app_pred A H P a'0 *)
  destruct M as [R HR].
(* Goal: @app_pred A H P a'0 *)
  destruct (valid_rel_commut_later1 R HR _ _ H2 _ H1).
(* Goal: @app_pred A H Q a'0 *)
  apply H0 with x; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma later_and {A} `{ageable A} : forall P Q,
  |>(P && Q) = |>P && |> Q.
Proof.
(* Goal: forall P Q : @pred A H, @eq (@pred A H) (@box A H (@laterM A H) (@andp A H P Q)) (@andp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) *)
  intros; apply box_and.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma later_or {A} `{ageable A} : forall (P Q:pred A),
  |>(P || Q) = |>P || |>Q.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros.
(* Goal: @app_pred A H (@box A H (@laterM A H) P) x *)
  repeat rewrite later_age.
(* Goal: @eq (@pred A agA) (@andp A agA (@orp A agA P Q) R) (@orp A agA (@andp A agA P R) (@andp A agA Q R)) *)
  apply pred_ext.
  2: apply box_or.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  hnf; intros.
(* Goal: @app_pred A H Q a'0 *)
  simpl in H0.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  case_eq (age1 a); intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  destruct (H0 a0); auto.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  left; simpl; intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  replace a' with a0; auto.
(* Goal: @eq A a'0 a'1 *)
  congruence.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  right; simpl; intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  replace a' with a0; auto.
(* Goal: @eq A a'0 a'1 *)
  congruence.
(* Goal: @app_pred A H (@orp A H P Q) w' *)
(* Goal: @app_pred A H (@orp A H P Q) w' *)
  left.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  hnf; simpl; intros.
  hnf in H2.
  rewrite H1 in H2; discriminate.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma later_ex {A} `{ageable A} : forall B (F:B->pred A),
  B ->
  |>(exp F) = EX x:B, |>(F x).
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros.
(* Goal: @eq (@pred A agA) (@andp A agA (@orp A agA P Q) R) (@orp A agA (@andp A agA P R) (@andp A agA Q R)) *)
  apply pred_ext.
  2: apply box_ex.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  hnf; intros.
  rewrite later_age in H0.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  case_eq (age1 a); intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  destruct (H0 a0); auto.
(* Goal: @app_pred A H (@exp A H B (fun x : B => @andp A H (P x) Q)) a *)
(* Goal: @derives A H (@exp A H B (fun x : B => @andp A H (P x) Q)) (@andp A H (@exp A H B P) Q) *)
  exists x.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  rewrite later_age; simpl; intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  replace a' with a0; auto.
(* Goal: @eq A a'0 a'1 *)
  congruence.
  exists X.
(* Goal: @app_pred A H (@box A H (@laterM A H) P) x *)
  rewrite later_age.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  hnf; simpl; intros.
  unfold age in H2.
  rewrite H1 in H2; discriminate.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma later_ex'' {A} `{ageable A} : forall B (F:B->pred A),
  |>(exp F) |-- (EX x:B, |>(F x)) || |> FF.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  unfold derives; intros.
(* Goal: @app_pred A agA (@orp A agA (@prop A agA P) (@box A agA (@laterM A agA) (@FF A agA))) a *)
  simpl in H |- *.
(* Goal: or P (forall (a' : A) (_ : @laterR A agA a a'), False) *)
  destruct (age1 a) eqn:?H; [left | right].
(* Goal: @app_pred A H Q a'0 *)
  + simpl in H0.
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
    pose proof H0 a0.
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
    destruct H2 as [b ?].
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
    {
(* Goal: clos_trans A (@age A agA) a a0 *)
      constructor.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
      auto.
    }
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
    exists b.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
    intros.
(* Goal: @app_pred A H (F b) a' *)
    revert H2; apply pred_nec_hereditary.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
    eapply age_later_nec; eauto.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  + intros.
(* Goal: False *)
    clear - H2 H1.
(* Goal: False *)
    induction H2.
(* Goal: @eq A a'0 a'1 *)
    - hnf in H0; congruence.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
    - auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma later_imp {A} `{ageable A} : forall P Q,
  |>(P --> Q) = |>P --> |>Q.
Proof.
(* Goal: @app_pred A H (@box A H (@laterM A H) P) x *)
  intros; repeat rewrite later_age.
(* Goal: @eq (@pred A agA) (@andp A agA (@orp A agA P Q) R) (@orp A agA (@andp A agA P R) (@andp A agA Q R)) *)
  apply pred_ext.
(* Goal: @derives A H (@box A H (@ageM A H) (@imp A H P Q)) (@imp A H (@box A H (@ageM A H) P) (@box A H (@ageM A H) Q)) *)
(* Goal: @derives A H (@imp A H (@box A H (@ageM A H) P) (@box A H (@ageM A H) Q)) (@box A H (@ageM A H) (@imp A H P Q)) *)
  apply axiomK.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  hnf; intros.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  simpl; intros.
(* Goal: @app_pred A H Q a'0 *)
  simpl in H0.
(* Goal: @app_pred A H Q a'0 *)
  destruct valid_rel_nec.
(* Goal: @app_pred A H Q a'0 *)
  destruct (H5 _ _ H2 _ H1).
(* Goal: @app_pred A H Q a'0 *)
  apply H0 with x; auto.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  replace a'1 with a'0; auto.
(* Goal: @eq A a'0 a'1 *)
  congruence.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma TT_boxy {A} `{ageable A} : forall M,
  boxy M TT.
Proof.
(* Goal: forall M : @modality A H, @boxy A H M (@TT A H) *)
  intros; hnf.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  apply pred_ext; repeat intro; simpl; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma positive_boxy {A} `{ageable A} : forall P Q M,
  boxy M P ->
  P |-- Q ->
  P |-- box M Q.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros.
  rewrite <- H0.
(* Goal: @derives A H (@box A H M P) (@box A H M Q) *)
  apply box_positive.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma forallI {A} `{ageable A} : forall A G X,
  (forall x:A, G |-- X x) ->
  G |-- allp X.
Proof.
(* Goal: forall (P : Prop) (Q R : @pred A agA) (_ : P) (_ : @derives A agA Q R), @derives A agA Q (@andp A agA (@prop A agA P) R) *)
  repeat intro.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  eapply H0; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma TT_and {A} `{ageable A} : forall P,
  TT && P = P.
Proof.
(* Goal: forall (P : Prop) (Q R : @pred A agA) (_ : P) (_ : @derives A agA Q R), @derives A agA Q (@andp A agA (@prop A agA P) R) *)
  intros; apply pred_ext; repeat intro.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  destruct H0; auto.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  split; simpl; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma andp_comm {A} `{ageable A} : forall P Q,
  P && Q = Q && P.
Proof.
(* Goal: forall P Q : @pred A H, @eq (@pred A H) (@andp A H P Q) (@andp A H Q P) *)
  intros; apply pred_ext; unfold andp; repeat intro; simpl in *; intuition.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma andp_assoc {A} `{ageable A} : forall P Q R,
  (P && Q) && R = P && (Q && R).
Proof.
(* Goal: forall P Q R : @pred A H, @eq (@pred A H) (@andp A H (@andp A H P Q) R) (@andp A H P (@andp A H Q R)) *)
  intros; apply pred_ext; auto; unfold derives, andp; simpl; intuition.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma ex_and : forall {A} `{ageable A} B (P:B->pred A) Q,
  (exp P) && Q = EX x:B, P x && Q.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros. apply pred_ext.
(* Goal: forall (P : Prop) (Q R : @pred A agA) (_ : P) (_ : @derives A agA Q R), @derives A agA Q (@andp A agA (@prop A agA P) R) *)
  repeat intro. destruct H0. destruct H0.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  exists x. split; auto.
(* Goal: forall (P : Prop) (Q R : @pred A agA) (_ : P) (_ : @derives A agA Q R), @derives A agA Q (@andp A agA (@prop A agA P) R) *)
  repeat intro.
(* Goal: @app_pred A H (@box A H (@laterM A H) (@andp A H P Q)) w *)
  destruct H0. destruct H0.
(* Goal: @app_pred A HA (@exp A HA B q) w *)
  split; auto. exists x; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma FF_and : forall {A} `{ageable A} (P:pred A),
  FF && P = FF.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros. apply pred_ext; repeat intro.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  destruct H0; auto.
(* Goal: @app_pred A H (@andp A H (@FF A H) P) a *)
  elim H0.
Qed.


(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma boxy_e {A} `{H : ageable A}: forall (M: modality) P,  boxy M P ->
           forall w w', app_mode M w w' -> P w -> P w'.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
rewrite <- H0 in H2; eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma boxy_andp {A} `{H : ageable A}:
     forall (M: modality) , reflexive _ (app_mode M) ->
      forall P Q, boxy M P -> boxy M Q -> boxy M (P && Q).
Proof.
destruct M;
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @app_pred A agA (@allp A agA B F) w' *)
simpl in *.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
apply boxy_i; intros; auto.
(* Goal: @app_pred A H (@orp A H P Q) w' *)
destruct H4.
(* Goal: @app_pred A H (@andp A H P Q) w' *)
simpl.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
split; eapply boxy_e; eauto.
Qed.

Hint Resolve @boxy_andp.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma boxy_disjunction {A} `{H : ageable A}:
     forall (M: modality) , reflexive _ (app_mode M) ->
      forall P Q, boxy M P -> boxy M Q -> boxy M (P || Q).
Proof.
destruct M;
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @app_pred A agA (@allp A agA B F) w' *)
simpl in *.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
apply boxy_i; intros; auto.
(* Goal: @app_pred A H (@orp A H P Q) w' *)
destruct H4.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
left.  eapply boxy_e; eauto.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
right. eapply boxy_e; eauto.
Qed.

Hint Resolve @boxy_disjunction.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma boxy_exp {A} `{agA : ageable A}:
    forall (M: modality) T (P: T -> pred A),
     reflexive _ (app_mode M) ->
     (forall x, boxy M (P x)) -> boxy M (exp P).
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
apply boxy_i; auto; intros.
(* Goal: @app_pred A agA (@exp A agA T P) w' *)
destruct H2 as [x ?].
rewrite <- H0 in H2.
(* Goal: @app_pred A agA (@exp A agA T P) w' *)
specialize ( H2 w' H1).
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
econstructor; eauto.
Qed.

Hint Resolve @boxy_exp.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma boxy_prop {A} `{H : ageable A}:  forall (M: modality) P, reflexive _ (app_mode M) -> boxy M (prop P).
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
apply boxy_i; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma boxy_TT {A} `{H : ageable A}:  forall (M: modality), reflexive _ (app_mode M) -> boxy M TT.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
apply boxy_i; intros; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma boxy_FF {A} `{H : ageable A}:  forall (M: modality), reflexive _ (app_mode M) -> boxy M FF.
Proof.
(* Goal: forall (M : @modality A H) (_ : reflexive A (@app_mode A H M)), @boxy A H M (@FF A H) *)
intros; apply boxy_i; intros; auto; contradiction.
Qed.

Hint Resolve @boxy_TT.
Hint Resolve @boxy_FF.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma TT_i  {A} `{ageable A}: forall w: A,  app_pred TT w.
Proof.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
unfold TT, prop; simpl; auto.
Qed.

Hint Resolve @TT_i.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma prop_andp_left {A}{agA: ageable A}: forall (P: Prop) Q R, (P -> Q |-- R) -> !!P && Q |-- R.
Proof.
(* Goal: forall (P : Prop) (Q R : @pred A agA) (_ : P) (_ : @derives A agA Q R), @derives A agA Q (@andp A agA (@prop A agA P) R) *)
 repeat intro. destruct H0; auto. apply H; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma prop_andp_right {A}{agA: ageable A}: forall (P: Prop) Q R, P -> Q |-- R -> Q |-- !!P && R.
Proof.
(* Goal: forall (P : Prop) (Q R : @pred A agA) (_ : P) (_ : @derives A agA Q R), @derives A agA Q (@andp A agA (@prop A agA P) R) *)
 repeat intro. split; auto.
Qed.

Lemma prop_true_andp:
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
  forall (P: Prop) A `{ageable A} (Q: pred A), P -> (!! P && Q = Q).
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @eq (@pred A agA) (@andp A agA (@orp A agA P Q) R) (@orp A agA (@andp A agA P R) (@andp A agA Q R)) *)
apply pred_ext.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
unfold derives; intros ? [? ?]; auto.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
unfold derives; intros; split; auto.
Qed.

Lemma prop_false_andp:
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
  forall (P: Prop) A `{ageable A} (Q: pred A),
   ~P -> !! P && Q = FF.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @eq (@pred A agA) (@andp A agA (@orp A agA P Q) R) (@orp A agA (@andp A agA P R) (@andp A agA Q R)) *)
apply pred_ext.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
unfold derives; intros ? [? ?]; tauto.
(* Goal: @derives A H (@FF A H) (@andp A H (@prop A H P) Q) *)
unfold derives. intros ? [].
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma prop_andp_e {A} `{ageable A}:  forall P Q (w:A), (!! P && Q) w -> P /\ Q w.
Proof.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
intuition; destruct H0; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma prop_andp_i {A} `{ageable A}:  forall P Q (w:A), P /\ app_pred Q w -> (!! P && Q) w.
Proof.
(* Goal: forall (P : Prop) (Q : @pred A H) (w : A) (_ : and P (@app_pred A H Q w)), @app_pred A H (@andp A H (@prop A H P) Q) w *)
intuition.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
split; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma later_derives {A} `{agA : ageable A}: forall {P Q}, (P |-- Q) -> (|> P |-- |> Q).
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
unfold derives; intros.
(* Goal: @app_pred A agA (@box A agA (@laterM A agA) Q) a *)
intro; intros; eapply H.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma boxy_allp {A} `{agA : ageable A}:
  forall (M: modality) (B: Type) F,
     reflexive _ (app_mode M) ->
     (forall (x:B), boxy M (F x)) -> boxy M (allp F).
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @boxy A agA M (@allp A agA B F) *)
destruct M as [R V].
(* Goal: @app_pred A agA (@allp A agA B F) w' *)
simpl in *.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
apply boxy_i; auto.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @app_pred A agA (@allp A agA B F) w' *)
simpl in *.
(* Goal: @app_pred A agA (@allp A agA B (fun x : B => @imp A agA (p x) q)) w *)
(* Goal: @app_pred A agA (@imp A agA (@exp A agA B p) q) w *)
intro.
(* Goal: @app_pred A agA (F b) w' *)
specialize ( H2 b).
rewrite <- H0 in H2.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
apply H2; auto.
Qed.
Hint Resolve @boxy_allp.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma later_allp {A} `{agA : ageable A}:
       forall B P, |> (allp P) = allp (fun x:B => |> (P x)).
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
apply pred_ext; unfold derives; simpl; intros; eapply H; eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma later_prop {A} `{agA : ageable A}:
       forall P: Prop, |> (prop P) |-- prop P || |> FF.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  unfold derives; intros.
(* Goal: @app_pred A agA (@orp A agA (@prop A agA P) (@box A agA (@laterM A agA) (@FF A agA))) a *)
  simpl in H |- *.
(* Goal: or P (forall (a' : A) (_ : @laterR A agA a a'), False) *)
  destruct (age1 a) eqn:?H; [left | right].
  + apply (H a0).
(* Goal: @laterR A agA a a0 *)
    unfold laterR.
(* Goal: clos_trans A (@age A agA) a a0 *)
    constructor.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
    auto.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  + intros.
    clear - H0 H1.
(* Goal: False *)
    induction H1.
(* Goal: @eq A a'0 a'1 *)
    - hnf in H; congruence.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
    - auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma box_derives {A} `{ageable A} : forall M (P Q:pred A),
  P |-- Q ->  box M P |-- box M Q.
Proof. exact box_positive. Qed.

Lemma allp_derives:
(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
       forall {A: Type} `{agA: ageable A} (B: Type) (P Q: B -> pred A),
               (forall x:B, P x |-- Q x) -> (allp P |-- allp Q).
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @derives A agA (@allp A agA B P) (@allp A agA B Q) *)
intros w b ?.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
eapply H; eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma forall_pred_ext  {A} `{agA : ageable A}: forall B (P Q: B -> pred A),
 (ALL x : B, (P x <--> Q x)) |-- (ALL x : B, P x) <--> (ALL x: B, Q x) .
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @derives A agA (@allp A agA B (fun x : B => @andp A agA (@imp A agA (P x) (Q x)) (@imp A agA (Q x) (P x)))) (@andp A agA (@imp A agA (@exp A agA B (fun x : B => P x)) (@exp A agA B (fun x : B => Q x))) (@imp A agA (@exp A agA B (fun x : B => Q x)) (@exp A agA B (fun x : B => P x)))) *)
intros w ?.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
split; intros ? ? ? ?;  destruct (H b); eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma exists_pred_ext  {A} `{agA : ageable A}: forall B (P Q: B -> pred A),
 (ALL x : B, (P x <--> Q x)) |-- (EX x : B, P x) <--> (EX x: B, Q x) .
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @derives A agA (@allp A agA B (fun x : B => @andp A agA (@imp A agA (P x) (Q x)) (@imp A agA (Q x) (P x)))) (@andp A agA (@imp A agA (@exp A agA B (fun x : B => P x)) (@exp A agA B (fun x : B => Q x))) (@imp A agA (@exp A agA B (fun x : B => Q x)) (@exp A agA B (fun x : B => P x)))) *)
intros w ?.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
split; intros w' ? [? ?]; exists x; eapply H; eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma imp_pred_ext  {A} `{agA : ageable A}: forall B B' P Q,
       (B <--> B') && (B --> (P <--> Q))
 |-- (B --> P) <-->  (B' --> Q).
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @derives A agA (@andp A agA (@andp A agA (@imp A agA P P') (@imp A agA P' P)) (@andp A agA (@imp A agA Q Q') (@imp A agA Q' Q))) (@andp A agA (@imp A agA (@andp A agA P Q) (@andp A agA P' Q')) (@imp A agA (@andp A agA P' Q') (@andp A agA P Q))) *)
intros w [? ?].
split; intros w'' ? ? w3 ? ?.
(* Goal: @app_pred A agA (P x) a *)
eapply H0.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
4: eapply H2; eauto.
(* Goal: @app_pred A H p a' *)
(* Goal: @derives A H (@box A H m p) (@box A H m (@box A H m p)) *)
2: eapply H; try apply H4.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
econstructor 3; eauto.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
econstructor 3; eauto.
(* Goal: @necR nat ag_nat (@level A H x) (@level A H x) *)
(* Goal: @necR nat ag_nat (@level A H x) (@level A H z) *)
constructor 2.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
eapply H; eauto.
(* Goal: @app_pred A agA (P x) a *)
eapply H0.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
4: eapply H2; eauto.
(* Goal: @app_pred A H p a' *)
(* Goal: @derives A H (@box A H m p) (@box A H m (@box A H m p)) *)
2: eapply H; try apply H4.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
econstructor 3; eauto.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
econstructor 3; eauto.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
eapply H; eauto.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
econstructor 3; eauto.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
eapply H; eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma derives_refl {A: Type} `{ageable A}:
  forall (P: pred A), (P |-- P).
(* Goal: forall P : @pred A H, @derives A H P P *)
Proof. firstorder.
Qed.

Hint Resolve @derives_refl.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma andp_derives {A} `{ageable A}:
  forall P Q P' Q': pred A, P |-- P' -> Q |-- Q' -> P && Q |-- P' && Q'.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
intros w [? ?]; split; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma orp_derives {A} `{ageable A}:
  forall P Q P' Q': pred A, P |-- P' -> Q |-- Q' -> P || Q |-- P' || Q'.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
 apply orp_left. apply orp_right1; auto. apply orp_right2; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma exp_derives {A} `{HA : ageable A}:
       forall B (P: B -> pred A) Q , (forall x:B, P x |-- Q x) -> (exp P |-- exp Q).
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @derives A HA (@exp A HA B P) (@exp A HA B Q) *)
intros w [b ?].
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
exists b; eapply H; eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma box_ext {A} `{agA : ageable A}: forall (M: modality) P Q,
    box M (P <--> Q) |--  box M P <--> box M Q.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @derives A agA (@box A agA M (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA M P) (@box A agA M Q)) (@imp A agA (@box A agA M Q) (@box A agA M P))) *)
repeat rewrite box_and.
apply andp_right;
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
eapply derives_trans; try apply axiomK; intros ? [? ?]; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma andp_pred_ext {A} `{agA : ageable A}: forall P Q P' Q',
       (P <--> P') && (Q <--> Q') |--  (P && Q) <--> (P' && Q').
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @derives A agA (@andp A agA (@andp A agA (@imp A agA P P') (@imp A agA P' P)) (@andp A agA (@imp A agA Q Q') (@imp A agA Q' Q))) (@andp A agA (@imp A agA (@andp A agA P Q) (@andp A agA P' Q')) (@imp A agA (@andp A agA P' Q') (@andp A agA P Q))) *)
intros w [? ?].
(* Goal: @app_pred A agA (@andp A agA (@imp A agA (@andp A agA P Q) (@andp A agA P' Q')) (@imp A agA (@andp A agA P' Q') (@andp A agA P Q))) w *)
split; (intros w' ? [? ?]; split; [eapply H; eauto | eapply H0; eauto]).
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Program Definition exactly {A} `{ageable A} (x: A) : pred A := necR x.
Next Obligation.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
constructor 3 with a; auto.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
constructor 1; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma derives_TT {A} `{ageable A}: forall (P: pred A), P |-- TT.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
intros ? ?; auto.
Qed.
Hint Resolve @derives_TT.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma FF_derives {A} `{ageable A}: forall P, FF |-- P.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros. intros ? ?. hnf in H0; contradiction.
Qed.
Hint Immediate @FF_derives.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma necR_level' {A} `{H : ageable A}: forall {w w': A}, necR w w' ->
       @necR _ ag_nat (level w) (level w').
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
induction 1; simpl; intros.
(* Goal: @app_pred A H (@andp A H P Q) w' *)
apply age_level in H0. constructor 1.  unfold age, age1; simpl.  rewrite H0; reflexivity.
(* Goal: @necR nat ag_nat (@level A H x) (@level A H x) *)
(* Goal: @necR nat ag_nat (@level A H x) (@level A H z) *)
constructor 2.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
constructor 3 with (level y); auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma derives_imp {A} `{agA : ageable A}:
  forall P Q w, (P |-- Q) -> (P --> Q) w.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
intros ? _; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma exp_andp1 {A} `{ageable A}:
 forall B (p: B -> pred A) q, (exp p && q)%pred = (exp (fun x => p x && q))%pred.
Proof.
(* Goal: @eq (@pred A H) (@box A H (@laterM A H) (@andp A H P Q)) (@andp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) *)
intros; apply pred_ext; intros w ?.
(* Goal: @app_pred A H (@box A H (@laterM A H) (@andp A H P Q)) w *)
destruct H0.
(* Goal: @app_pred A H (@box A H (@laterM A H) (@andp A H P Q)) w *)
destruct H0.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
exists x; split; auto.
(* Goal: @app_pred A H (@box A H (@laterM A H) (@andp A H P Q)) w *)
destruct H0. destruct H0.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
split; auto.
(* Goal: @app_pred A HA (@exp A HA B q) w *)
exists x; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma exp_andp2 {A} `{HA: ageable A}:
 forall B p (q: B -> pred A), (p && exp q)%pred = (exp (fun x => p && q x))%pred.
Proof.
(* Goal: @eq (@pred A H) (@box A H (@laterM A H) (@andp A H P Q)) (@andp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) *)
intros; apply pred_ext; intros w ?.
(* Goal: @app_pred A HA (@andp A HA p (@exp A HA B q)) w *)
destruct H.
(* Goal: @app_pred A H (@box A H (@laterM A H) (@andp A H P Q)) w *)
destruct H0.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
exists x; split; auto.
(* Goal: @app_pred A HA (@andp A HA p (@exp A HA B q)) w *)
destruct H. destruct H.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
split; auto.
(* Goal: @app_pred A HA (@exp A HA B q) w *)
exists x; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma exp_imp_left {A} `{agA : ageable A}:  forall B (p: B -> pred A) q,
     (exp p --> q)%pred = allp (fun x => p x --> q)%pred.
Proof.
(* Goal: @eq (@pred A H) (@box A H (@laterM A H) (@andp A H P Q)) (@andp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) *)
intros; apply pred_ext; intros w ?.
(* Goal: @app_pred A agA (@allp A agA B (fun x : B => @imp A agA (p x) q)) w *)
(* Goal: @app_pred A agA (@imp A agA (@exp A agA B p) q) w *)
intro.
(* Goal: @app_pred A agA (@imp A agA (p b) q) w *)
(* Goal: @app_pred A agA (@imp A agA (@exp A agA B p) q) w *)
intros ?w ? ?.
(* Goal: @app_pred A agA q w0 *)
(* Goal: @app_pred A agA (@imp A agA (@exp A agA B p) q) w *)
eapply H.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
apply necR_trans with w0; auto.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
exists b; auto.
(* Goal: @app_pred A agA (@imp A agA (@exp A agA B p) q) w *)
intros ?w ? [? ?].
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
eapply H; eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma app_ext  {A: Type} `{ageable A} : forall (F G: A -> Prop) p1 p2 w,
         (F w = G w) ->
         app_pred (exist (hereditary age) F p1) w = app_pred (exist (hereditary age) G p2) w.
Proof.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
simpl; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma imp_derives {A} `{agA : ageable A}:
  forall P P' Q Q',
    P' |-- P ->
    Q |-- Q' ->
    P --> Q |-- P' --> Q'.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @derives A agA (@imp A agA P Q) (@imp A agA P' Q') *)
intros w ? w'' ? ?.
(* Goal: @app_pred A agA (P x) a *)
apply H0.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
eapply H1; eauto.
Qed.


(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma imp_lem0  {A} `{agA : ageable A}:  forall P st, (TT --> P) st -> P st.
Proof.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
intros; eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma conjoin_hyp0  {A} `{H : ageable A}:
      forall (P Q: pred A) w,  P w -> (P --> Q) w -> (TT --> Q) w.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @app_pred A agA (@imp A agA Q R) w *)
intros w' ? ?.
eapply H1;
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
eauto.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
eapply pred_nec_hereditary; eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma conjoin_hyp1 {A} `{agA : ageable A}: forall (P Q R: pred A)  w,
            P w -> (P&&Q --> R) w -> (Q --> R) w.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @app_pred A agA (@imp A agA Q R) w *)
intros w' ? ?.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
eapply H0; auto.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
split; eauto.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
eapply pred_nec_hereditary; eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma derives_e {A: Type} `{agA : ageable A}: forall p q (st: A),
      (p |-- q) -> p st -> q st.
Proof.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
auto.
Qed.

Ltac slurp :=
 apply imp_lem0;
  match goal with |-  app_pred (_ --> _)  ?st =>
        repeat match goal with
                   | H: app_pred ?P st |- app_pred (?b --> ?c) st =>
                       (apply (@conjoin_hyp0 _ _ P c st H) ||
                        (apply (@conjoin_hyp1 _ _ P b c st H)));
                       clear H
                   end;
        try (revert st; apply derives_e)
  end.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma test_slurp {A} `{agA : ageable A} :  forall  (P Q R S : pred A) w ,
        (P && (Q && R) --> S) w -> P w -> Q w -> R w -> S w.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
remember (app_pred (P && (Q && R) --> S) w) as hide.
(* Goal: @app_pred A agA S w *)
slurp.
(* Goal: @app_pred A agA (@imp A agA (@andp A agA P (@andp A agA Q R)) S) w *)
subst hide. assumption.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma later_andp {A} `{H : ageable A}:
  forall P Q, |> (P && Q) = |>P && |>Q.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: @eq (@pred A H) (@box A H (@laterM A H) (@andp A H P Q)) (@andp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) *)
apply pred_ext; intros w ?.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
split; intros w' ?; destruct (H0 _ H1); auto.
(* Goal: @app_pred A H (@box A H (@laterM A H) (@andp A H P Q)) w *)
destruct H0.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
intros w' ?; split; eauto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma True_andp_eq {A}`{ageable A}:
  forall (P: Prop) (Q: pred A), P -> (!!P && Q)%pred = Q.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
intros.
(* Goal: forall (P : Prop) (Q : @pred A H) (w : A) (_ : and P (@app_pred A H Q w)), @app_pred A H (@andp A H (@prop A H P) Q) w *)
apply pred_ext; intros w ?; hnf in *; simpl; intros; intuition.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma distrib_orp_andp {A}{agA: ageable A}:
   forall P Q R, (P||Q)&&R = (P&&R)||(Q&&R).
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
  intros. apply pred_ext.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  intros w [[?|?] ?]; [left|right]; split; auto.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  intros w [[? ?]|[? ?]]; split; auto. left; auto. right; auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma allp_right {B A: Type}{agA: ageable A}:
  forall (P: pred A) (Q: B -> pred A),
  (forall v, P |-- Q v) ->
   P |-- allp Q.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
 intros. intros w ? v; apply (H v); auto.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma allp_left {B}{A}{agA: ageable A}:
   forall (P: B -> pred A) x Q, P x |-- Q -> allp P |-- Q.
 Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
   intros. intros ? ?. apply H. apply H0.
Qed.

(* Goal: @laterR A H a a0 *)
(* Goal: @ex B (fun b : B => forall (a' : A) (_ : @laterR A H a a'), @app_pred A H (F b) a') *)
Lemma later_imp2 {A}{agA: ageable A}: forall P Q: pred A,
                 |> (P <--> Q) = |> P <--> |> Q.
Proof.
(* Goal: forall P Q : @pred A agA, @eq (@pred A agA) (@box A agA (@laterM A agA) (@andp A agA (@imp A agA P Q) (@imp A agA Q P))) (@andp A agA (@imp A agA (@box A agA (@laterM A agA) P) (@box A agA (@laterM A agA) Q)) (@imp A agA (@box A agA (@laterM A agA) Q) (@box A agA (@laterM A agA) P))) *)
 intros.
(* Goal: forall (p q : @pred A agA) (st : A) (_ : @derives A agA p q) (_ : @app_pred A agA p st), @app_pred A agA q st *)
  repeat rewrite <- later_imp. rewrite <- later_andp; auto.
Qed.
