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

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

Local Open Scope pred.

Lemma valid_rel_fashion {A} `{AG: ageable A} : valid_rel fashionR.
Proof.
(* Goal: @valid_rel A AG (@fashionR A AG A AG) *)
  split; hnf; intros.

(* Goal: @ex2 A (fun y' : A => @fashionR A AG A AG y' x) (fun y' : A => @age A AG z y') *)
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @fashionR A AG A AG z y') *)
  unfold fashionR in *.
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @fashionR A AG A AG z y') *)
  hnf in H.
(* Goal: @ex2 A (fun y' : A => @eq nat (@level A AG y') (@level A AG x)) (fun y' : A => @age A AG z y') *)
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @fashionR A AG A AG z y') *)
  case_eq (age1 z); intros.
(* Goal: @ex2 A (fun y' : A => @eq nat (@level A AG y') (@level A AG x)) (fun y' : A => @age A AG z y') *)
(* Goal: @ex2 A (fun y' : A => @eq nat (@level A AG y') (@level A AG x)) (fun y' : A => @age A AG z y') *)
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @fashionR A AG A AG z y') *)
  exists a.
(* Goal: @eq nat (@level A AG a) (@level A AG x) *)
(* Goal: @age A AG z a *)
(* Goal: @ex2 A (fun y' : A => @eq nat (@level A AG y') (@level A AG x)) (fun y' : A => @age A AG z y') *)
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @fashionR A AG A AG z y') *)
  rewrite (af_level2 age_facts y x) in H0; auto.
(* Goal: @eq nat (@level A AG a) (@level A AG x) *)
(* Goal: @age A AG z a *)
(* Goal: @ex2 A (fun y' : A => @eq nat (@level A AG y') (@level A AG x)) (fun y' : A => @age A AG z y') *)
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @fashionR A AG A AG z y') *)
  rewrite (af_level2 age_facts z a) in H0; auto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  auto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  rewrite (af_level1 age_facts) in H1; auto.
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat y (@level A H w'))) *)
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
  rewrite H1 in H0.
(* Goal: @ex2 A (fun y' : A => @eq nat (@level A AG y') (@level A AG x)) (fun y' : A => @age A AG z y') *)
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @fashionR A AG A AG z y') *)
  symmetry in H0.
(* Goal: @ex2 A (fun y' : A => @eq nat (@level A AG y') (@level A AG x)) (fun y' : A => @age A AG z y') *)
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @fashionR A AG A AG z y') *)
  rewrite <- (af_level1 age_facts) in H0.
(* Goal: @ex2 A (fun y' : A => @eq nat (@level A AG y') (@level A AG x)) (fun y' : A => @age A AG z y') *)
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @fashionR A AG A AG z y') *)
  rewrite H in H0; discriminate.

(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @fashionR A AG A AG z y') *)
  hnf in H.
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @fashionR A AG A AG z y') *)
  destruct (af_unage age_facts x). exists x0. apply H1.
(* Goal: @fashionR A AG A AG z x0 *)
  hnf.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  rewrite (af_level2 age_facts x0 x); auto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  rewrite (af_level2 age_facts z y); auto.
Qed.

Definition fashionM {A} `{ageable A} : modality
  := exist _ fashionR valid_rel_fashion.

Existing Instance ag_nat. Hint Resolve ag_nat.

Program Definition fash {A: Type} `{NA: ageable A} (P: pred A): pred nat :=
      fun n => forall y, n >= level y -> P y.
Next Obligation.
(* Goal: @app_pred A NA P y *)
destruct P as [P HP].
(* Goal: @app_pred nat ag_nat (@fash A agA P) w' *)
simpl in *.
(* Goal: @app_pred A agA Q' a' *)
apply H0.
(* Goal: ge a (@level A NA y) *)
unfold age, age1, ag_nat,natAge1 in H.
(* Goal: ge a (@level A NA y) *)
destruct a; inv H.
(* Goal: le n' (S m) *)
omega.
Qed.

Notation "'#' e" := (fash e) (at level 30, right associativity): pred.

Lemma fash_K {A} `{H: ageable A}: forall (P Q: pred A),
                 # (P --> Q) |-- # P --> # Q.
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: @derives nat ag_nat (@fash A H (@imp A H P Q)) (@imp nat ag_nat (@fash A H P) (@fash A H Q)) *)
intros n ?.
(* Goal: @app_pred nat ag_nat (@imp nat ag_nat (@fash A H P) (@fash A H Q)) n *)
simpl in H.
(* Goal: @app_mode nat ag_nat (@laterM nat ag_nat) (@level A H w) (@level A H a') *)
simpl.
(* Goal: forall (a' : nat) (_ : @necR nat ag_nat n a') (_ : forall (y : A) (_ : ge a' (@level A H y)), @app_pred A H P y) (y : A) (_ : ge a' (@level A H y)), @app_pred A H Q y *)
intros w ? ? ? ?.
(* Goal: @app_pred A H Q y *)
apply (pred_nec_hereditary _ _ _ H1) in H0.
(* Goal: @app_pred A H Q y *)
clear n H1.
(* Goal: @app_pred A H Q y *)
specialize (H2 _ H3).
(* Goal: @app_pred A H Q y *)
simpl in H0.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
eapply H0; eauto.
Qed.

Lemma laterR_nat: forall (n n': nat), laterR n n' <-> (n > n')%nat.
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
split; induction 1; simpl; intros.
(* Goal: gt x y *)
(* Goal: gt x z *)
(* Goal: @laterR nat ag_nat (S n') n' *)
(* Goal: @laterR nat ag_nat (S m) n' *)
unfold age, age1 in H; simpl in H; unfold natAge1 in H. destruct x; inv H.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
auto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
apply gt_trans with y; auto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
constructor 1. unfold age, age1; simpl. auto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
constructor 2 with m; auto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
constructor 1. unfold age, age1; simpl. auto.
Qed.

Lemma fash_fash {A} `{NA: ageable A}:  forall P: pred A,  # # P = # P.
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
apply pred_ext; intro; simpl in *; intros.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
apply H with a; auto.
(* Goal: @app_pred nat ag_nat P n' *)
(* Goal: forall (a' : A) (_ : @app_mode A H (@laterM A H) w a'), @app_pred A H (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A H) p) (fun x : A => @app_pred nat ag_nat P (@level A H x)) (unfash_obligation_1 A H P)) a' *)
subst.
(* Goal: @app_pred A agA Q y *)
apply H.
(* Goal: le n' (S m) *)
unfold natLevel in H0. omega.
Qed.

Lemma fash_derives {A} `{agA : ageable A}:
     forall (P Q: pred A), P |-- Q  ->  # P |-- # Q.
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: @derives nat ag_nat (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P' Q')) *)
intros w ?.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intro; intros.
(* Goal: @app_pred A agA Q y *)
apply H.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
eapply H0; auto.
Qed.

Lemma fash_and {A} `{H : ageable A}: forall (P Q:pred A),
  # (P && Q) = # P && # Q.
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
  intros; apply pred_ext; hnf; intros.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  split; hnf; intros; destruct (H0 y H1); auto.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
  hnf; intros.
(* Goal: @app_pred A H (@andp A H P Q) y *)
  destruct H0.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  split; auto.
Qed.

Definition fashionable  (P: pred nat) := # P = P.

Notation "P '>=>' Q" := (# (P --> Q)) (at level 55, right associativity) : pred.
Notation "P '<=>' Q" := (# (P <--> Q)) (at level 57, no associativity) : pred.

Lemma subp_eqp {A} `{ageable A} : forall G (P Q: pred A),
  G |-- P >=> Q ->
  G |-- Q >=> P ->
  G |-- P <=> Q.
Proof.
(* Goal: @derives A agA P Q *)
  repeat intro.
(* Goal: @app_pred A H (@andp A H (@imp A H P Q) (@imp A H Q P)) y *)
  split.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  eapply H0; eauto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  eapply H1; eauto.
Qed.

Lemma eqp_subp {A} `{ageable A} : forall G P Q,
  G |-- P <=> Q ->
  G |-- P >=> Q.
Proof.
(* Goal: @derives A agA P Q *)
  repeat intro.
(* Goal: @app_pred A H P a' *)
  apply H0 in H1.
(* Goal: le n' (S m) *)
  simpl in H1.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  destruct (H1 _ H2); auto.
Qed.

Lemma eqp_subp2 {A} `{ageable A} : forall G P Q,
  G |-- P <=> Q ->
  G |-- Q >=> P.
Proof.
(* Goal: @derives A agA P Q *)
  repeat intro.
(* Goal: @app_pred A H P a' *)
  apply H0 in H1.
(* Goal: le n' (S m) *)
  simpl in H1.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  destruct (H1 _ H2); auto.
Qed.

Lemma eqp_comm : forall {A} `{ageable A} (P Q:pred A),
  P <=> Q = Q <=> P.
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
  intros. apply pred_ext.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H Q P) (@imp A H P Q))) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) *)
  apply subp_eqp.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
    apply eqp_subp2. hnf; auto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
    apply eqp_subp. hnf; auto.
(* Goal: @derives nat ag_nat (@fash A H (@andp A H (@imp A H Q P) (@imp A H P Q))) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P))) *)
  apply subp_eqp.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
    apply eqp_subp2. hnf; auto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
    apply eqp_subp. hnf; auto.
Qed.

Lemma subp_refl {A} `{ageable A} : forall G P,
  G |-- P >=> P.
Proof.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  repeat intro; auto.
Qed.

Lemma subp_trans {A} `{ageable A} : forall G P Q R,
  G |-- P >=> Q ->
  G |-- Q >=> R ->
  G |-- P >=> R.
Proof.
(* Goal: @derives A agA P Q *)
  repeat intro.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  eapply H1; eauto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  eapply H0; eauto.
Qed.

Lemma subp_top {A} `{ageable A} : forall G P,
  G |-- P >=> TT.
Proof.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  repeat intro; simpl; auto.
Qed.

Lemma subp_bot {A} `{ageable A} : forall G P,
  G |-- FF >=> P.
Proof.
(* Goal: forall (G : @pred nat ag_nat) (P : @pred A H), @derives nat ag_nat G (@fash A H (@imp A H (@FF A H) P)) *)
  repeat intro; simpl in *; intuition.
Qed.

Lemma subp_andp {A} `{ageable A} : forall G P P' Q Q',
  G |-- P >=> P' ->
  G |-- Q >=> Q' ->
  G |-- P && Q >=> (P' && Q').
Proof.
(* Goal: @derives A agA P Q *)
  repeat intro.
(* Goal: @app_pred A H (@andp A H (@imp A H P Q) (@imp A H Q P)) y *)
  destruct H5; split.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  eapply H0; eauto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  eapply H1; eauto.
Qed.

Lemma subp_imp {A} `{ageable A} : forall G P P' Q Q',
  G |-- P' >=> P ->
  G |-- Q >=> Q' ->
  G |-- (P --> Q) >=> (P' --> Q').
Proof.
(* Goal: @derives A agA P Q *)
  repeat intro.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  eapply H1; eauto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  apply H5; auto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  eapply H0; eauto.
Qed.

Lemma subp_orp {A} `{ageable A} : forall G P P' Q Q',
  G |-- P >=> P' ->
  G |-- Q >=> Q' ->
  G |-- (P || Q) >=> (P' || Q').
Proof.
(* Goal: @derives A agA P Q *)
  repeat intro.
(* Goal: @app_pred A H (@orp A H P' Q') a' *)
  destruct H5; [ left | right ].
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  eapply H0; eauto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  eapply H1; eauto.
Qed.

Lemma subp_subp {A}{agA: ageable A}:
  forall (G: pred nat) (P Q R S: pred A),
   G |-- (R >=> P) ->
   G |-- (Q >=> S) ->
   G |-- (P >=> Q) >=> (R >=> S).
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
 intros.
(* Goal: @derives nat ag_nat (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P' Q')) *)
 intros w ?.
 specialize (H _ H1). specialize (H0 _ H1). clear G H1.
 intros ? ? ? ? ? ? ? ? ? ?.
(* Goal: @app_pred A agA Q' a' *)
 eapply H0.
 3: eapply H3.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
 5: eapply H; auto.
 2: eassumption. 3: eassumption.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
 apply necR_level in H2. apply le_trans with (level y); auto. apply le_trans with (level a'); auto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
 auto.
 apply necR_level in H5.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
 apply le_trans with (level y0); auto. apply le_trans with a'; auto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
 apply necR_level in H2.  apply le_trans with (level y); auto.
Qed.

Lemma subp_allp {A} `{ageable A} : forall G B (X Y:B -> pred A),
  (forall x:B, G |-- X x >=> Y x) ->
  G |-- allp X >=> allp Y.
Proof.
(* Goal: @derives A agA P Q *)
  repeat intro.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  eapply H0; eauto.
Qed.

Lemma subp_exp {A} `{ageable A} : forall G B (X Y:B -> pred A),
  (forall x:B, G |-- X x >=> Y x) ->
  G |-- exp X >=> exp Y.
Proof.
(* Goal: @derives A agA P Q *)
  repeat intro.
(* Goal: @app_pred A H (@exp A H B Y) a' *)
  destruct H4; exists x.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  eapply H0; eauto.
Qed.

Lemma subp_allp_spec {A} `{ageable A} : forall G B (X:B -> pred A) x,
  G |-- allp X >=> X x.
Proof.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  repeat intro; eauto.
Qed.

Lemma subp_exp_spec {A} `{ageable A} : forall G B(X:B -> pred A) x,
  G |-- X x >=> exp X.
Proof.
(* Goal: @derives A agA P Q *)
  repeat intro.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  exists x; auto.
Qed.


Lemma later_fash1 {A} `{agA: ageable A}:
   forall P, |> # P |-- # |> P.
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: @derives nat ag_nat (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P' Q')) *)
intros w ?.
(* Goal: @app_pred nat ag_nat (@fash A agA (@box A agA (@laterM A agA) P)) w *)
intros w' ? w'' ?.
(* Goal: @app_pred nat ag_nat (@fash A agA P) w' *)
simpl in *.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
eapply (H (level w'')); auto.
(* Goal: @laterR nat ag_nat w (@level A agA w'') *)
apply later_nat.
(* Goal: @laterR nat ag_nat (@level A H w) (@level A H a') *)
apply laterR_level in H1.
(* Goal: le n' (S m) *)
omega.
Qed.

Lemma later_fash {A} `{agA : ageable A}:
    forall P, |> # P = # |> P.
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: @eq (@pred nat ag_nat) (@box nat ag_nat (@laterM nat ag_nat) (@fash A agA P)) (@fash A agA (@box A agA (@laterM A agA) P)) *)
apply pred_ext.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A agA P)) (@fash A agA (@box A agA (@laterM A agA) P)) *)
(* Goal: @derives nat ag_nat (@fash A agA (@box A agA (@laterM A agA) P)) (@box nat ag_nat (@laterM nat ag_nat) (@fash A agA P)) *)
apply later_fash1.
(** backward direction **)
(* Goal: @derives nat ag_nat (@fash A agA (@box A agA (@laterM A agA) P)) (@box nat ag_nat (@laterM nat ag_nat) (@fash A agA P)) *)
intros w ? w' ?.
(* Goal: @app_pred nat ag_nat (@fash A agA P) w' *)
simpl in *.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: @app_pred A agA P y *)
destruct (af_unage age_facts y).
(* Goal: @app_pred A agA P y *)
apply (H x).
(* Goal: ge w (@level A agA x) *)
(* Goal: @laterR A agA x y *)
apply later_nat in H0.
(* Goal: ge w (@level A agA x) *)
(* Goal: @laterR A agA x y *)
apply age_level in H2.
(* Goal: le n' (S m) *)
omega.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
constructor 1; auto.
Qed.

Lemma subp_later1 {A} `{ageable A} : forall P Q,
   |>(P >=> Q)  |--   |>P >=> |>Q.
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
eapply derives_trans; [apply later_fash1 | ].
(* Goal: @derives nat ag_nat (@fash A H (@box A H (@laterM A H) (@imp A H P Q))) (@fash A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q))) *)
rewrite later_imp.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
intros ? ?; auto.
Qed.

Lemma subp_later {A} `{ageable A} : forall P Q,
   |>(P >=> Q) = |>P >=> |>Q.
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: @eq (@pred nat ag_nat) (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
rewrite later_fash.
(* Goal: @eq (@pred nat ag_nat) (@fash A H (@box A H (@laterM A H) (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
f_equal.
(* Goal: @eq (@pred A H) (@box A H (@laterM A H) (@imp A H P Q)) (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) *)
apply later_imp.
Qed.

Lemma eqp_later1 {A} `{ageable A} : forall P Q,
   |>(P <=> Q)  |--   |>P <=> |>Q.
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: @derives nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
eapply derives_trans; [apply later_fash1 | ].
(* Goal: @eq (@pred A H) (@box A H (@laterM A H) (@andp A H (@imp A H P Q) (@imp A H Q P))) (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
rewrite later_and.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
repeat rewrite later_imp. auto.
Qed.

Lemma eqp_later {A} `{ageable A} : forall P Q,
    (|>(P <=> Q) = |>P <=> |>Q)%pred.
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: @eq (@pred nat ag_nat) (@box nat ag_nat (@laterM nat ag_nat) (@fash A H (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
rewrite later_fash.
(* Goal: @eq (@pred nat ag_nat) (@fash A H (@box A H (@laterM A H) (@andp A H (@imp A H P Q) (@imp A H Q P)))) (@fash A H (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P)))) *)
f_equal.
(* Goal: @eq (@pred A H) (@box A H (@laterM A H) (@andp A H (@imp A H P Q) (@imp A H Q P))) (@andp A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q)) (@imp A H (@box A H (@laterM A H) Q) (@box A H (@laterM A H) P))) *)
rewrite later_and.
(* Goal: @derives nat ag_nat (@fash A H (@box A H (@laterM A H) (@imp A H P Q))) (@fash A H (@imp A H (@box A H (@laterM A H) P) (@box A H (@laterM A H) Q))) *)
repeat rewrite later_imp.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
auto.
Qed.


Program Definition unfash {A} `{agA: ageable A} (P: pred nat) : pred A :=
     fun x => P (level x).
Next Obligation.
(* Goal: @app_pred nat ag_nat P (@level A agA a') *)
 apply age_level in H.
(* Goal: @app_pred nat ag_nat P (@level A agA a') *)
 rewrite H in H0.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
 eapply pred_hereditary; eauto. unfold age;  simpl. auto.
Qed.

Notation "'!' e" := (unfash e) (at level 30, right associativity): pred.

Lemma level_later {A} `{H : ageable A}: forall {w: A} {n': nat},
         laterR (level w) n' ->
       exists w', laterR w w' /\ n' = level w'.
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat n' (@level A H w'))) *)
remember (level w) as n.
(* Goal: @app_pred nat ag_nat P n' *)
(* Goal: forall (a' : A) (_ : @app_mode A H (@laterM A H) w a'), @app_pred A H (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A H) p) (fun x : A => @app_pred nat ag_nat P (@level A H x)) (unfash_obligation_1 A H P)) a' *)
revert w Heqn; induction H0; intros; subst.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
case_eq (age1 w); intros.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
exists a; split. constructor; auto.
(* Goal: @app_pred A H Q y *)
symmetry; unfold age in H0; simpl in H0.
(* Goal: @app_pred A H Q y *)
  unfold natAge1 in H0; simpl in H0. revert H0; case_eq (level w); intros; inv H2.
(* Goal: @eq nat (@level A H a) y *)
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat y (@level A H w'))) *)
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
  apply age_level in H1. congruence. rewrite age1_level0 in H1.
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat y (@level A H w'))) *)
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
   rewrite H1 in H0. inv H0.
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
 specialize (IHclos_trans1 _ (refl_equal _)).
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
  destruct IHclos_trans1 as [w2 [? ?]].
(* Goal: @app_pred nat ag_nat P n' *)
(* Goal: forall (a' : A) (_ : @app_mode A H (@laterM A H) w a'), @app_pred A H (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A H) p) (fun x : A => @app_pred nat ag_nat P (@level A H x)) (unfash_obligation_1 A H P)) a' *)
  subst.
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
  specialize (IHclos_trans2 _ (refl_equal _)).
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
  destruct IHclos_trans2 as [w3 [? ?]].
(* Goal: @app_pred nat ag_nat P n' *)
(* Goal: forall (a' : A) (_ : @app_mode A H (@laterM A H) w a'), @app_pred A H (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A H) p) (fun x : A => @app_pred nat ag_nat P (@level A H x)) (unfash_obligation_1 A H P)) a' *)
  subst.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  exists w3; split; auto. econstructor 2; eauto.
Qed.

Lemma later_unfash {A} `{H : ageable A}:
     forall P, |> (unfash P: pred A) = unfash ( |> P).
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
unfold unfash; intros.
(* Goal: @eq (@pred A H) (@box A H (@laterM A H) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A H) p) (fun x : A => @app_pred nat ag_nat P (@level A H x)) (unfash_obligation_1 A H P))) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A H) p) (fun x : A => @app_pred nat ag_nat (@box nat ag_nat (@laterM nat ag_nat) P) (@level A H x)) (unfash_obligation_1 A H (@box nat ag_nat (@laterM nat ag_nat) P))) *)
apply pred_ext; intros w ?; hnf in *.
(* Goal: @app_pred nat ag_nat (@fash nat ag_nat (@andp nat ag_nat (@imp nat ag_nat P Q) (@imp nat ag_nat Q P))) w *)
intros n' ?.
(* Goal: le n' (S m) *)
simpl in H1. destruct (level_later H1) as [w' [? ?]].
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  subst. apply H0. auto.
(* Goal: @app_pred A agA Q' a' *)
 intros ? ?. simpl in H1. apply H0. simpl.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  apply laterR_level in H1. rewrite laterR_nat; auto.
Qed.

Lemma subp_derives {A} `{agA : ageable A} :
  forall (P P' Q Q': pred A),
    P' |-- P ->
    Q |-- Q' ->
    (P >=> Q) |-- (P' >=> Q').
Proof.

(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: @derives nat ag_nat (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P' Q')) *)
intros w ?.
(* Goal: @app_pred nat ag_nat (@fash A agA (@imp A agA P' Q')) w *)
intros ? ? ? ? ?.
(* Goal: @app_pred A agA Q' a' *)
apply H0.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
eapply H1; eauto.
Qed.

Lemma derives_subp {A} `{agA : ageable A} :
      forall (P Q: pred A) (st: nat), (P |-- Q) -> (P >=> Q) st.
Proof.

(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: @app_pred nat ag_nat (@fash A agA (@imp A agA P Q)) st *)
intros w' ? w'' ? ?.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
eauto.
Qed.

Lemma exp_subp' {A} `{H : ageable A}:
  forall (T: Type) (P Q: T -> pred A) (st: nat),
                (forall x, (P x >=> Q x) st) -> ((EX x : T, P x) >=> (EX x : T, Q x)) st.
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: @derives A agA P Q *)
repeat intro.
(* Goal: @app_pred A H (@exp A H T (fun x : T => Q x)) a' *)
destruct H3 as [x ?]; exists x.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
eapply H0; eauto.
Qed.

Lemma fash_subp {A} `{agA: ageable A}:
    forall (P Q: pred A), fashionable (P >=> Q).
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: fashionable (@fash A agA (@imp A agA P Q)) *)
unfold fashionable.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
rewrite fash_fash. auto.
Qed.
Hint Resolve @fash_subp.

Lemma fash_allp {A} {agA:ageable A}:
  forall  (B: Type) (F: B -> pred A),
      # (allp F) = allp (fun z: B => # F z).
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: @derives nat ag_nat (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P' Q')) *)
apply pred_ext; intros w ?.
(* Goal: @app_pred nat ag_nat (@allp nat ag_nat B (fun z : B => @fash A agA (F z))) w *)
(* Goal: @app_pred nat ag_nat (@fash A agA (@allp A agA B F)) w *)
intro z.
(* Goal: @app_pred nat ag_nat (@fash A agA (F z)) w *)
(* Goal: @app_pred nat ag_nat (@fash A agA (@allp A agA B F)) w *)
intros ? ?.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
eapply H; eauto.
(* Goal: @app_pred nat ag_nat (@fash A agA (@allp A agA B F)) w *)
intros ? ? ?.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
eapply H; auto.
Qed.

 Lemma subp_i1 {A}{agA: ageable A}:
  forall (P : pred nat) (Q R: pred A ), !P && Q |-- R -> P |-- Q >=> R.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
Proof. intros.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
  intros n ?. intros ? ? ? ? ?. apply H. split; auto.
 eapply pred_nec_hereditary. apply H2.
(* Goal: @app_pred A agA Q' a' *)
 assert (P (level y)). eapply pred_nec_hereditary; try apply H0.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
 apply nec_nat. auto. apply H4.
Qed.

Lemma eqp_nat: forall P Q: pred nat, (P <=> Q) = (P <--> Q).
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: @derives nat ag_nat (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P' Q')) *)
apply pred_ext; intros w ?.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
specialize (H _ (le_refl _)); auto.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
intros n' ?. inv H0; auto.
(* Goal: @app_pred A agA Q y *)
eapply pred_nec_hereditary; try apply H.
(* Goal: @necR nat ag_nat (S m) n' *)
apply nec_nat.
(* Goal: le n' (S m) *)
unfold level in H1. simpl in H1. unfold natLevel in H1. omega.
Qed.

Lemma prop_andp_subp {A}{agA : ageable A}:
  forall (P: Prop) Q R w, (P -> app_pred (Q >=> R) w) -> app_pred ((!!P && Q) >=> R) w.
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: @derives A agA P Q *)
repeat intro.
(* Goal: @app_pred A agA R a' *)
destruct H2.
(* Goal: @app_pred A agA R a' *)
apply H in H2.
(* Goal: @eq (@pred nat ag_nat) (@fash A agA (@imp A agA P Q)) (@fash A agA (@imp A agA P Q)) *)
eapply H2; eauto.
Qed.

Lemma subp_e {A}{agA : ageable A}: forall P Q : pred A, TT |-- P >=> Q -> P |-- Q.
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @derives nat ag_nat (@TT nat ag_nat) (@fash A agA (@imp A agA P Q))), @derives A agA P Q *)
intros.
(* Goal: @derives A agA P Q *)
repeat intro.
(* Goal: @app_pred A agA Q a *)
apply (H (@level _ agA a) I a (le_refl _) a (necR_refl _) H0).
Qed.


