Require Import compcert.lib.Maps.
Require Import compcert.common.AST.
Require Import compcert.common.Values.
Require Import compcert.common.Globalenvs.

Require Import VST.msl.ageable.

Require Import VST.sepcomp.extspec.
Require Import VST.sepcomp.step_lemmas.

Require Import VST.veric.compcert_rmaps.
Require Import VST.veric.juicy_mem.

Definition pures_sub (phi phi' : rmap) :=
  forall adr,
  match resource_at phi adr with
    | PURE k pp => resource_at phi' adr
                 = PURE k (preds_fmap (approx (level phi')) (approx (level phi')) pp)
    | _ => True
  end.

Lemma pures_sub_trans phi1 phi2 phi3 :
  (level phi3 <= level phi2)%nat ->
  pures_sub phi1 phi2 ->
  pures_sub phi2 phi3 ->
  pures_sub phi1 phi3.
Proof.
(* Goal: forall (_ : le (@level rmap ag_rmap phi3) (@level rmap ag_rmap phi2)) (_ : pures_sub phi1 phi2) (_ : pures_sub phi2 phi3), pures_sub phi1 phi3 *)
  intros lev S1 S2. intros l; specialize (S1 l); specialize (S2 l).
(* Goal: match resource_at phi1 l with | NO sh n => True | YES sh r k p => True | PURE k pp => @eq resource (resource_at phi3 l) (PURE k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) pp)) end *)
  destruct (phi1 @ l); auto.
(* Goal: @eq resource (resource_at phi3 l) (PURE k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) p)) *)
  rewrite S1 in S2. rewrite S2.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) (preds_fmap (approx (@level rmap ag_rmap phi2)) (approx (@level rmap ag_rmap phi2)) p))) (PURE k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) p)) *)
  f_equal.
(* Goal: @eq preds (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) (preds_fmap (approx (@level rmap ag_rmap phi2)) (approx (@level rmap ag_rmap phi2)) p)) (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) p) *)
  rewrite (compose_rewr (preds_fmap _ _)).
(* Goal: @eq preds (@compose preds preds preds (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3))) (preds_fmap (approx (@level rmap ag_rmap phi2)) (approx (@level rmap ag_rmap phi2))) p) (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) p) *)
  rewrite preds_fmap_comp.
(* Goal: @eq preds (preds_fmap (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi2))) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx (@level rmap ag_rmap phi2)) (approx (@level rmap ag_rmap phi3))) p) (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) p) *)
  rewrite approx_oo_approx'; auto.
(* Goal: @eq preds (preds_fmap (approx (@level rmap ag_rmap phi3)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx (@level rmap ag_rmap phi2)) (approx (@level rmap ag_rmap phi3))) p) (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) p) *)
  rewrite approx'_oo_approx; auto.
Qed.

Lemma pures_sub_refl phi : pures_sub phi phi.
Proof.
(* Goal: pures_sub phi phi *)
  intros l.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) (preds_fmap (approx (@level rmap ag_rmap phi2)) (approx (@level rmap ag_rmap phi2)) p))) (PURE k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) p)) *)
  destruct (phi @ l) eqn:E; auto; f_equal.
(* Goal: @eq preds p (preds_fmap (approx (@level rmap ag_rmap phi)) (approx (@level rmap ag_rmap phi)) p) *)
  pose proof E as E_.
(* Goal: @eq preds p (preds_fmap (approx (@level rmap ag_rmap phi)) (approx (@level rmap ag_rmap phi)) p) *)
  rewrite <-resource_at_approx, E_ in E. simpl in E.
(* Goal: @eq preds p (preds_fmap (approx (@level rmap ag_rmap phi)) (approx (@level rmap ag_rmap phi)) p) *)
  congruence.
Qed.

Definition pures_eq (phi phi' : rmap) :=
  pures_sub phi phi' /\
  (forall adr,
   match resource_at phi' adr with
    | PURE k pp' => exists pp, resource_at phi adr = PURE k pp
    | _ => True
  end).

Lemma pures_eq_refl phi : pures_eq phi phi.
Proof.
(* Goal: pures_eq phi phi *)
  split. apply pures_sub_refl. intros l; destruct (phi @ l); eauto.
Qed.

Lemma pures_eq_trans phi1 phi2 phi3 :
  level phi3 <= level phi2 ->
  pures_eq phi1 phi2 ->
  pures_eq phi2 phi3 ->
  pures_eq phi1 phi3.
Proof.
(* Goal: pures_eq phi phi *)
  intros lev [S1 E1] [S2 E2]; split. apply pures_sub_trans with phi2; auto.
(* Goal: forall adr : AV.address, match resource_at phi3 adr with | NO sh n => True | YES sh r k p => True | PURE k pp' => @ex preds (fun pp : preds => @eq resource (resource_at phi1 adr) (PURE k pp)) end *)
  intros l; specialize (E1 l); specialize (E2 l).
(* Goal: match resource_at phi3 l with | NO sh n => True | YES sh r k p => True | PURE k pp' => @ex preds (fun pp : preds => @eq resource (resource_at phi1 l) (PURE k pp)) end *)
  destruct (phi3 @ l); auto. destruct E2 as (pp, E2). rewrite E2 in E1; auto.
Qed.
