Require Import VST.msl.base.
Require Import VST.msl.ageable.
Require Import VST.msl.sepalg.
Require Import VST.msl.sepalg_generators.
Require Import VST.msl.age_sepalg.
Require Import VST.msl.predicates_hered.
Require Import VST.msl.predicates_sl.

Local Open Scope pred.

Definition corable {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}
         (P: pred A) := forall w, P w = P (core w).

Lemma corable_spec: forall {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}
  (P: pred A),
    corable P = forall x y:A, core x = core y -> P x -> P y.
Proof.
(* Goal: forall (A : Type) (JA : Join A) (PA : @Perm_alg A JA) (SA : @Sep_alg A JA) (agA : ageable A) (AgeA : @Age_alg A JA agA) (P : @pred A agA), @eq Prop (@corable A JA PA SA agA AgeA P) (forall (x y : A) (_ : @eq A (@core A JA SA x) (@core A JA SA y)) (_ : @app_pred A agA P x), @app_pred A agA P y) *)
  unfold corable; intros; apply prop_ext; split; intros.
  + rewrite H in H1 |- *.
(* Goal: @app_pred A agA P (@core A JA SA y) *)
    rewrite <- H0.
(* Goal: @corable A JA PA SA agA AgeA P *)
    auto.
  + pose proof core_idem w.
(* Goal: @eq Prop (@app_pred A agA P w) (@app_pred A agA P (@core A JA SA w)) *)
    pose proof (H _ _ H0).
(* Goal: @eq Prop (@app_pred A agA P w) (@app_pred A agA P (@core A JA SA w)) *)
    pose proof (H _ _ (eq_sym H0)).
(* Goal: @corable A JA PA SA agA AgeA P *)
    apply prop_ext; split; auto.
Qed.

Lemma corable_andp {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall P Q, corable P -> corable Q -> corable (P && Q).
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @corable A JA PA SA agA AgeA P) (_ : @corable A JA PA SA agA AgeA Q), @corable A JA PA SA agA AgeA (@orp A agA P Q) *)
 unfold corable; intros.
(* Goal: @eq Prop (@app_pred A agA (@andp A agA P Q) w) (@app_pred A agA (@andp A agA P Q) (@core A JA SA w)) *)
 apply prop_ext; split; intros [? ?]; split; congruence.
Qed.
Lemma corable_orp {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall P Q, corable P -> corable Q -> corable (P || Q).
Proof.
(* Goal: forall (P Q : @pred A agA) (_ : @corable A JA PA SA agA AgeA P) (_ : @corable A JA PA SA agA AgeA Q), @corable A JA PA SA agA AgeA (@orp A agA P Q) *)
 unfold corable; intros.
(* Goal: @eq Prop (@app_pred A agA (@orp A agA P Q) w) (@app_pred A agA (@orp A agA P Q) (@core A JA SA w)) *)
 apply prop_ext; split; (intros [?|?]; [left|right]; congruence).
Qed.
Lemma corable_allp {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall {B: Type} (P:  B -> pred A) ,
      (forall b, corable (P b)) -> corable (allp P).
Proof.
(* Goal: forall (B : Type) (P : forall _ : B, @pred A agA) (_ : forall b : B, @corable A JA PA SA agA AgeA (P b)), @corable A JA PA SA agA AgeA (@allp A agA B P) *)
 unfold corable, allp; intros.
(* Goal: @eq Prop (@app_pred A agA (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A agA) p) (fun a : A => forall b : B, @app_pred A agA (P b) a) (predicates_hered.allp_obligation_1 A agA B P)) w) (@app_pred A agA (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A agA) p) (fun a : A => forall b : B, @app_pred A agA (P b) a) (predicates_hered.allp_obligation_1 A agA B P)) (@core A JA SA w)) *)
 apply prop_ext; split; simpl; intros.
(* Goal: @corable A JA PA SA agA AgeA P *)
 rewrite <- H; auto. rewrite H; auto.
Qed.
Lemma corable_exp {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall {B: Type} (P:  B -> pred A) ,
      (forall b, corable (P b)) -> corable (exp P).
Proof.
(* Goal: forall (B : Type) (P : forall _ : B, @pred A agA) (_ : forall b : B, @corable A JA PA SA agA AgeA (P b)), @corable A JA PA SA agA AgeA (@exp A agA B P) *)
 unfold corable, exp; intros.
 apply prop_ext; split; simpl; intros;  destruct H0 as [b ?]; exists b.
(* Goal: @corable A JA PA SA agA AgeA P *)
 rewrite <- H; auto. rewrite H; auto.
Qed.
Lemma corable_prop{A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall P, corable (prop P).
Proof.
(* Goal: forall P : Prop, @corable A JA PA SA agA AgeA (@prop A agA P) *)
 unfold corable, prop; intros.
(* Goal: @corable A JA PA SA agA AgeA P *)
 apply prop_ext; split; simpl; intros; auto.
Qed.

Lemma corable_imp {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A} {agA: ageable A}{AgeA: Age_alg A}:
  forall P Q, corable P -> corable Q -> corable (P --> Q).
Proof.
(* Goal: forall (P Q R : @pred A agA) (_ : @corable A JA PA SA agA AgeA P), @eq (@pred A agA) (@sepcon A JA PA agA AgeA Q (@andp A agA R P)) (@andp A agA P (@sepcon A JA PA agA AgeA Q R)) *)
  intros.
(* Goal: @corable A JA PA SaA agA XA (@wand A JA PA agA XA P Q) *)
  rewrite corable_spec in H, H0 |- *.
(* Goal: forall (x y : A) (_ : @eq A (@core A JA SA x) (@core A JA SA y)) (_ : @app_pred A agA (@imp A agA P Q) x), @app_pred A agA (@imp A agA P Q) y *)
  unfold imp in *.
(* Goal: @app_pred A agA (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A agA) p) (fun a : A => forall (a' : A) (_ : @app_mode A agA (@laterM A agA) a a'), @app_pred A agA P a') (predicates_hered.box_obligation_1 A agA (@laterM A agA) P)) y *)
  simpl in *.
(* Goal: forall (P Q R : @pred A agA) (_ : @corable A JA PA SA agA AgeA P), @eq (@pred A agA) (@sepcon A JA PA agA AgeA Q (@andp A agA R P)) (@andp A agA P (@sepcon A JA PA agA AgeA Q R)) *)
  intros.
(* Goal: @app_pred A agA P a' *)
  rename a' into y'.
(* Goal: @app_pred A agA Q y' *)
  pose proof H3.
(* Goal: @app_pred A agA Q y' *)
  apply necR_power_age in H5.
(* Goal: @app_pred A agA Q y' *)
  destruct H5 as [n ?H].
(* Goal: @app_pred A agA Q y' *)
  destruct (power_age_parallel' _ y' _ n (eq_sym H1) H5) as [x' [?H ?H]].
(* Goal: @app_pred A agA Q y' *)
  apply (H0 _ _ (eq_sym H7)).
(* Goal: @app_pred A agA Q x' *)
  apply H2.
  + apply necR_power_age; exists n; auto.
  + apply (H _ _ H7); auto.
Qed.

Lemma corable_sepcon {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
  forall P Q, corable P -> corable Q -> corable (P * Q).
Proof.
(* Goal: forall (P Q R : @pred A agA) (_ : @corable A JA PA SA agA AgeA P), @eq (@pred A agA) (@sepcon A JA PA agA AgeA Q (@andp A agA R P)) (@andp A agA P (@sepcon A JA PA agA AgeA Q R)) *)
  intros.
(* Goal: @corable A JA PA SaA agA XA (@wand A JA PA agA XA P Q) *)
  rewrite corable_spec in H, H0 |- *.
(* Goal: forall (x y : A) (_ : @eq A (@core A JA SA x) (@core A JA SA y)) (_ : @app_pred A agA (@sepcon A JA PA agA AgeA P Q) x), @app_pred A agA (@sepcon A JA PA agA AgeA P Q) y *)
  unfold sepcon.
(* Goal: forall (P Q R : @pred A agA) (_ : @corable A JA PA SA agA AgeA P), @eq (@pred A agA) (@sepcon A JA PA agA AgeA Q (@andp A agA R P)) (@andp A agA P (@sepcon A JA PA agA AgeA Q R)) *)
  intros.
(* Goal: @app_pred A agA (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A agA) p) (fun x : A => @ex A (fun y : A => @ex A (fun z : A => and (@join A JA y z x) (and (@app_pred A agA P y) (@app_pred A agA Q z))))) (predicates_sl.sepcon_obligation_1 A JA agA AgeA P Q)) y *)
  simpl in H2 |- *.
(* Goal: @ex A (fun y0 : A => @ex A (fun z : A => and (@join A JA y0 z y) (and (@app_pred A agA P y0) (@app_pred A agA Q z)))) *)
  destruct H2 as [x' [x'' [? [? ?]]]].
(* Goal: @ex A (fun y0 : A => @ex A (fun z : A => and (@join A JA y0 z y) (and (@app_pred A agA P y0) (@app_pred A agA Q z)))) *)
  pose proof join_core H2.
(* Goal: @ex A (fun y0 : A => @ex A (fun z : A => and (@join A JA y0 z y) (and (@app_pred A agA P y0) (@app_pred A agA Q z)))) *)
  pose proof join_core (join_comm H2).
(* Goal: @ex A (fun y0 : A => @ex A (fun z : A => and (@join A JA y0 z y) (and (@app_pred A agA P y0) (@app_pred A agA Q z)))) *)
  exists (core y), y.
(* Goal: and (@join A JA (@core A JA SA y) y y) (and (@app_pred A agA P (@core A JA SA y)) (@app_pred A agA Q y)) *)
  repeat split.
  + apply core_unit.
  + apply H with x'; auto.
(* Goal: @eq A (@core A JA SaA w') (@core A JA SaA (@core A JA SaA x')) *)
    rewrite core_idem.
(* Goal: @eq A (@core A JA SaA w') (@core A JA SaA x') *)
    congruence.
  + apply H0 with x''; auto.
(* Goal: @eq A (@core A JA SaA w') (@core A JA SaA x') *)
    congruence.
Qed.

Lemma corable_wand: forall {A:Type} {agA:ageable A} {JA: Join A} {PA: Perm_alg A} {SaA: Sep_alg A} {XA: Age_alg A} (P Q: pred A), corable P -> corable Q -> corable (P -* Q).
Proof.
(* Goal: forall (P Q R : @pred A agA) (_ : @corable A JA PA SA agA AgeA P), @eq (@pred A agA) (@sepcon A JA PA agA AgeA Q (@andp A agA R P)) (@andp A agA P (@sepcon A JA PA agA AgeA Q R)) *)
  intros.
(* Goal: @corable A JA PA SaA agA XA (@wand A JA PA agA XA P Q) *)
  rewrite corable_spec in H, H0 |- *.
(* Goal: forall (x y : A) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : @app_pred A agA (@wand A JA PA agA XA P Q) x), @app_pred A agA (@wand A JA PA agA XA P Q) y *)
  unfold wand in *.
(* Goal: @app_pred A agA (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A agA) p) (fun a : A => forall (a' : A) (_ : @app_mode A agA (@laterM A agA) a a'), @app_pred A agA P a') (predicates_hered.box_obligation_1 A agA (@laterM A agA) P)) y *)
  simpl in *.
(* Goal: forall (P Q R : @pred A agA) (_ : @corable A JA PA SA agA AgeA P), @eq (@pred A agA) (@sepcon A JA PA agA AgeA Q (@andp A agA R P)) (@andp A agA P (@sepcon A JA PA agA AgeA Q R)) *)
  intros.
(* Goal: @app_pred A agA Q z *)
  rename x' into y'.
(* Goal: @app_pred A agA Q z *)
  rename y0 into w'.
(* Goal: @app_pred A agA Q z *)
  rename z into z'.
(* Goal: @app_pred A agA Q z' *)
  apply necR_power_age in H3.
(* Goal: @app_pred A agA Q z' *)
  destruct H3 as [n ?H].
(* Goal: @app_pred A agA Q z' *)
  pose proof power_age_parallel' _ y' _ n (eq_sym H1) H3.
(* Goal: @app_pred A agA Q z' *)
  destruct H6 as [x' [?H ?H]].
(* Goal: @app_pred A agA Q z' *)
  pose proof join_core H4.
(* Goal: @app_pred A agA Q z' *)
  pose proof join_core (join_comm H4).
(* Goal: @app_pred A agA Q z' *)
  apply H0 with x'; [congruence |].
  apply (H2  x' (core x') x').
  + apply necR_power_age.
(* Goal: @corable A JA PA SA agA AgeA P *)
    exists n; auto.
  + apply join_comm, core_unit.
  + apply H with w'; auto.
(* Goal: @eq A (@core A JA SaA w') (@core A JA SaA (@core A JA SaA x')) *)
    rewrite core_idem.
(* Goal: @eq A (@core A JA SaA w') (@core A JA SaA x') *)
    congruence.
Qed.

Lemma corable_later: forall {A:Type} {agA:ageable A} {JA: Join A} {PA: Perm_alg A} {SaA: Sep_alg A} {XA: Age_alg A} P, corable P -> corable (|> P).
Proof.
(* Goal: forall (P Q R : @pred A agA) (_ : @corable A JA PA SA agA AgeA P), @eq (@pred A agA) (@sepcon A JA PA agA AgeA Q (@andp A agA R P)) (@andp A agA P (@sepcon A JA PA agA AgeA Q R)) *)
  intros.
(* Goal: @corable A JA PA SaA agA XA (@box A agA (@laterM A agA) P) *)
  rewrite corable_spec in H |- *.
(* Goal: forall (P Q R : @pred A agA) (_ : @corable A JA PA SA agA AgeA P), @eq (@pred A agA) (@sepcon A JA PA agA AgeA Q (@andp A agA R P)) (@andp A agA P (@sepcon A JA PA agA AgeA Q R)) *)
  intros.
(* Goal: @app_pred A agA (@box A agA (@laterM A agA) P) y *)
  unfold box in *.
(* Goal: @app_pred A agA (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A agA) p) (fun a : A => forall (a' : A) (_ : @app_mode A agA (@laterM A agA) a a'), @app_pred A agA P a') (predicates_hered.box_obligation_1 A agA (@laterM A agA) P)) y *)
  simpl in *.
(* Goal: forall (P Q R : @pred A agA) (_ : @corable A JA PA SA agA AgeA P), @eq (@pred A agA) (@sepcon A JA PA agA AgeA Q (@andp A agA R P)) (@andp A agA P (@sepcon A JA PA agA AgeA Q R)) *)
  intros.
(* Goal: @app_pred A agA P a' *)
  apply laterR_power_age in H2.
(* Goal: @app_pred A agA P a' *)
  destruct H2 as [n ?H].
(* Goal: @app_pred A agA P a' *)
  rename a' into y'.
(* Goal: @app_pred A agA P y' *)
  destruct (power_age_parallel' _ y' _ _ (eq_sym H0) H2) as [x' [? ?]].
(* Goal: @corable A JA PA SA agA AgeA P *)
  apply H with x'; auto.
(* Goal: @app_pred A agA P x' *)
  apply H1.
(* Goal: @laterR A agA x x' *)
  apply laterR_power_age.
(* Goal: @corable A JA PA SA agA AgeA P *)
  exists n; auto.
Qed.

Hint Resolve @corable_andp @corable_orp @corable_allp @corable_exp
                    @corable_imp @corable_prop @corable_sepcon @corable_wand @corable_later.

Lemma corable_andp_sepcon1{A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
   forall P Q R, corable P ->  (P && Q) * R = P && (Q * R).
Proof.
(* Goal: forall (P Q R : @pred A agA) (_ : @corable A JA PA SA agA AgeA P), @eq (@pred A agA) (@sepcon A JA PA agA AgeA Q (@andp A agA R P)) (@andp A agA P (@sepcon A JA PA agA AgeA Q R)) *)
intros.
(* Goal: @eq (@pred A agA) (@sepcon A JA PA agA AgeA (@andp A agA P Q) R) (@andp A agA P (@sepcon A JA PA agA AgeA Q R)) *)
apply pred_ext.
(* Goal: @derives A agA (@sepcon A JA PA agA AgeA (@andp A agA P Q) R) (@andp A agA P (@sepcon A JA PA agA AgeA Q R)) *)
(* Goal: @derives A agA (@andp A agA P (@sepcon A JA PA agA AgeA Q R)) (@sepcon A JA PA agA AgeA (@andp A agA P Q) R) *)
intros w [w1 [w2 [? [[? ?] ?]]]].
(* Goal: @app_pred A agA (@andp A agA P (@sepcon A JA PA agA AgeA Q R)) w *)
(* Goal: @derives A agA (@andp A agA P (@sepcon A JA PA agA AgeA Q R)) (@sepcon A JA PA agA AgeA (@andp A agA P Q) R) *)
split.
(* Goal: @app_pred A agA P w *)
(* Goal: @app_pred A agA (@sepcon A JA PA agA AgeA Q R) w *)
(* Goal: @derives A agA (@andp A agA P (@sepcon A JA PA agA AgeA Q R)) (@sepcon A JA PA agA AgeA (@andp A agA P Q) R) *)
apply join_core in H0.
(* Goal: @corable A JA PA SA agA AgeA P *)
rewrite H in H1|-*. rewrite <- H0; auto.
(* Goal: @corable A JA PA SA agA AgeA P *)
exists w1; exists w2; split; [| split]; auto.
(* Goal: @derives A agA (@andp A agA P (@sepcon A JA PA agA AgeA Q R)) (@sepcon A JA PA agA AgeA (@andp A agA P Q) R) *)
intros w [? [w1 [w2 [? [? ?]]]]].
(* Goal: @corable A JA PA SA agA AgeA P *)
exists w1; exists w2; split; [|split]; auto.
(* Goal: @corable A JA PA SA agA AgeA P *)
split; auto.
(* Goal: @app_pred A agA P w1 *)
apply join_core in H1.
(* Goal: @corable A JA PA SA agA AgeA P *)
rewrite H in H0|-*. rewrite H1; auto.
Qed.

(* The following 3 lemmas should not be necessary *)
Lemma corable_andp_sepcon2{A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
   forall P Q R, corable P ->  (Q && P) * R = P && (Q * R).
Proof.
(* Goal: @corable A JA PA SA agA AgeA P *)
intros. rewrite andp_comm. apply corable_andp_sepcon1. auto.
Qed.

Lemma corable_sepcon_andp1 {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
   forall P Q R, corable P ->  Q  * (P && R) = P && (Q * R).
Proof.
(* Goal: @corable A JA PA SA agA AgeA P *)
intros. rewrite sepcon_comm. rewrite corable_andp_sepcon1; auto. rewrite sepcon_comm; auto.
Qed.

Lemma corable_sepcon_andp2 {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
   forall P Q R, corable P ->  Q  * (R && P) = P && (Q * R).
Proof.
(* Goal: @corable A JA PA SA agA AgeA P *)
intros. rewrite sepcon_comm. rewrite andp_comm. rewrite corable_andp_sepcon1; auto. rewrite sepcon_comm; auto.
Qed.

(* This hint doesn't work well, hence the extra clauses in normalize1 and normalize1_in *)
Hint Rewrite @corable_andp_sepcon1 @corable_andp_sepcon2
                    @corable_sepcon_andp1 @corable_sepcon_andp2 using solve [auto with normalize typeclass_instances].