Require Import VST.msl.base.
Require Import VST.msl.sepalg.
Require Import VST.msl.predicates_sa.

Local Open Scope pred.

Definition corable {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_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}
  (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) (P : pred A), @eq Prop (@corable A JA PA SA P) (forall (x y : A) (_ : @eq A (@core A JA SA x) (@core A JA SA y)) (_ : P x), P y) *)
  unfold corable; intros; apply prop_ext; split; intros.
  + rewrite H in H1 |- *.
(* Goal: P (@core A JA SA y) *)
    rewrite <- H0.
(* Goal: P (@core A JA SA x) *)
    auto.
  + pose proof core_idem w.
(* Goal: @eq Prop (P w) (P (@core A JA SA w)) *)
    pose proof (H _ _ H0).
(* Goal: @eq Prop (P w) (P (@core A JA SA w)) *)
    pose proof (H _ _ (eq_sym H0)).
(* Goal: P (@core A JA SA x) *)
    apply prop_ext; split; auto.
Qed.

Lemma corable_andp {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
  forall P Q, corable P -> corable Q -> corable (P && Q).
Proof.
(* Goal: forall (P Q : pred A) (_ : @corable A JA PA SA P) (_ : @corable A JA PA SA Q), @corable A JA PA SA (@orp A P Q) *)
 unfold corable; intros.
(* Goal: @eq Prop (@andp A P Q w) (@andp A 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}:
  forall P Q, corable P -> corable Q -> corable (P || Q).
Proof.
(* Goal: forall (P Q : pred A) (_ : @corable A JA PA SA P) (_ : @corable A JA PA SA Q), @corable A JA PA SA (@orp A P Q) *)
 unfold corable; intros.
(* Goal: @eq Prop (@orp A P Q w) (@orp A 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}:
  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) (_ : forall b : B, @corable A JA PA SA (P b)), @corable A JA PA SA (@allp A B P) *)
 unfold corable, allp; intros.
(* Goal: @eq Prop (forall b : B, P b w) (forall b : B, P b (@core A JA SA w)) *)
 apply prop_ext; split; simpl; intros.
(* Goal: P (@core A JA SA x) *)
 rewrite <- H; auto. rewrite H; auto.
Qed.
Lemma corable_exp {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_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) (_ : forall b : B, @corable A JA PA SA (P b)), @corable A JA PA SA (@exp A B P) *)
 unfold corable, exp; intros.
 apply prop_ext; split; simpl; intros;  destruct H0 as [b ?]; exists b.
(* Goal: P (@core A JA SA x) *)
 rewrite <- H; auto. rewrite H; auto.
Qed.
Lemma corable_prop{A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
  forall P, corable (prop P).
Proof.
(* Goal: forall P : Prop, @corable A JA PA SA (@prop A P) *)
 unfold corable, prop; intros.
(* Goal: P (@core A JA SA x) *)
 apply prop_ext; split; simpl; intros; auto.
Qed.

Lemma corable_imp {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A} :
  forall P Q, corable P -> corable Q -> corable (P --> Q).
Proof.
(* Goal: forall (P Q R : pred A) (_ : @corable A JA PA SA P), @eq (forall _ : A, Prop) (@sepcon A JA (@andp A P Q) R) (@andp A P (@sepcon A JA Q R)) *)
  intros.
(* Goal: @corable A JA PA SaA (@wand A JA 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)) (_ : @imp A P Q x), @imp A P Q y *)
  unfold imp in *.
(* Goal: forall (x y : A) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : forall (x0 z : A) (_ : @join A JA x0 x z) (_ : P x0), Q z) (x0 z : A) (_ : @join A JA x0 y z) (_ : P x0), Q z *)
  simpl in *.
(* Goal: forall (P Q R : pred A) (_ : @corable A JA PA SA P), @eq (forall _ : A, Prop) (@sepcon A JA (@andp A P Q) R) (@andp A P (@sepcon A JA Q R)) *)
  intros.
(* Goal: P (@core A JA SA x) *)
  eapply H0; eauto.
Qed.

Lemma corable_sepcon {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
  forall P Q, corable P -> corable Q -> corable (P * Q).
Proof.
(* Goal: forall (P Q R : pred A) (_ : @corable A JA PA SA P), @eq (forall _ : A, Prop) (@sepcon A JA (@andp A P Q) R) (@andp A P (@sepcon A JA Q R)) *)
  intros.
(* Goal: @corable A JA PA SaA (@wand A JA 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)) (_ : @sepcon A JA P Q x), @sepcon A JA P Q y *)
  unfold sepcon.
(* Goal: forall (P Q R : pred A) (_ : @corable A JA PA SA P), @eq (forall _ : A, Prop) (@sepcon A JA (@andp A P Q) R) (@andp A P (@sepcon A JA Q R)) *)
  intros.
(* Goal: @ex A (fun x : A => @ex A (fun y0 : A => and (@join A JA x y0 y) (and (P x) (Q y0)))) *)
  simpl in H2 |- *.
(* Goal: @ex A (fun x : A => @ex A (fun y0 : A => and (@join A JA x y0 y) (and (P x) (Q y0)))) *)
  destruct H2 as [x' [x'' [? [? ?]]]].
(* Goal: @ex A (fun x : A => @ex A (fun y0 : A => and (@join A JA x y0 y) (and (P x) (Q y0)))) *)
  pose proof join_core H2.
(* Goal: @ex A (fun x : A => @ex A (fun y0 : A => and (@join A JA x y0 y) (and (P x) (Q y0)))) *)
  pose proof join_core (join_comm H2).
(* Goal: @ex A (fun x : A => @ex A (fun y0 : A => and (@join A JA x y0 y) (and (P x) (Q y0)))) *)
  exists (core y), y.
(* Goal: and (@join A JA (@core A JA SA y) y y) (and (P (@core A JA SA y)) (Q y)) *)
  repeat split.
  + apply core_unit.
  + apply H with x'; auto.
(* Goal: @eq A (@core A JA SaA x0) (@core A JA SaA (@core A JA SaA x)) *)
    rewrite core_idem.
(* Goal: @eq A (@core A JA SaA x0) (@core A JA SaA x) *)
    congruence.
  + apply H0 with x''; auto.
(* Goal: @eq A (@core A JA SaA x0) (@core A JA SaA x) *)
    congruence.
Qed.

Lemma corable_wand: forall {A:Type} {JA: Join A} {PA: Perm_alg A} {SaA: Sep_alg A} (P Q: pred A), corable P -> corable Q -> corable (P -* Q).
Proof.
(* Goal: forall (P Q R : pred A) (_ : @corable A JA PA SA P), @eq (forall _ : A, Prop) (@sepcon A JA (@andp A P Q) R) (@andp A P (@sepcon A JA Q R)) *)
  intros.
(* Goal: @corable A JA PA SaA (@wand A JA 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)) (_ : @wand A JA P Q x), @wand A JA P Q y *)
  unfold wand in *.
(* Goal: forall (x y : A) (_ : @eq A (@core A JA SaA x) (@core A JA SaA y)) (_ : forall (x0 z : A) (_ : @join A JA x0 x z) (_ : P x0), Q z) (x0 z : A) (_ : @join A JA x0 y z) (_ : P x0), Q z *)
  simpl in *.
(* Goal: forall (P Q R : pred A) (_ : @corable A JA PA SA P), @eq (forall _ : A, Prop) (@sepcon A JA (@andp A P Q) R) (@andp A P (@sepcon A JA Q R)) *)
  intros.
(* Goal: Q z *)
  pose proof join_core H3.
(* Goal: Q z *)
  pose proof join_core (join_comm H3).
(* Goal: Q z *)
  apply H0 with x; [congruence |].
(* Goal: Q x *)
  apply (H2 (core x) x).
  + apply core_unit.
  + apply H with x0; auto.
(* Goal: @eq A (@core A JA SaA x0) (@core A JA SaA (@core A JA SaA x)) *)
    rewrite core_idem.
(* Goal: @eq A (@core A JA SaA x0) (@core A JA SaA x) *)
    congruence.
Qed.

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