Require Import compcert.common.Memory.
Require Import VST.msl.Coqlib2.
Require Import VST.msl.eq_dec.
Require Import VST.msl.ageable.
Require Import VST.msl.age_to.
Require Import VST.veric.coqlib4.
Require Import VST.veric.compcert_rmaps.

Set Bullet Behavior "Strict Subproofs".

Lemma pred_hered {A} {_ : ageable A} (P : pred A) : hereditary age (app_pred P).
Proof.
(* Goal: @hereditary A (@age A X) (@app_pred A X P) *)
  destruct P; auto.
Qed.

(* Goal: @eq nat n' (Init.Nat.sub (@level rmap ag_rmap r) n) *)
(* Goal: @eq ghost (ghost_of phi') (ghost_fmap (approx n) (approx n) (ghost_of phi)) *)
Lemma hereditary_necR {phi phi' : rmap} {P} :
  necR phi phi' ->
  hereditary age P ->
  P phi -> P phi'.
Proof.
(* Goal: forall (_ : @necR rmap ag_rmap phi phi') (_ : @hereditary rmap (fun x y : rmap => @age rmap ag_rmap y x) P) (_ : P phi'), P phi *)
  intros N H; induction N; auto.
(* Goal: forall _ : P y, P x *)
  apply H; auto.
Qed.

(* Goal: @eq nat n' (Init.Nat.sub (@level rmap ag_rmap r) n) *)
(* Goal: @eq ghost (ghost_of phi') (ghost_fmap (approx n) (approx n) (ghost_of phi)) *)
Lemma anti_hereditary_necR {phi phi' : rmap} {P} :
  necR phi phi' ->
  hereditary (fun x y => age y x) P ->
  P phi' -> P phi.
Proof.
(* Goal: forall (_ : @necR rmap ag_rmap phi phi') (_ : @hereditary rmap (fun x y : rmap => @age rmap ag_rmap y x) P) (_ : P phi'), P phi *)
  intros N H; induction N; auto.
(* Goal: forall _ : P y, P x *)
  apply H; auto.
Qed.

(* Goal: @eq nat n' (Init.Nat.sub (@level rmap ag_rmap r) n) *)
(* Goal: @eq ghost (ghost_of phi') (ghost_fmap (approx n) (approx n) (ghost_of phi)) *)
Lemma app_pred_age {R} {phi phi' : rmap} :
  age phi phi' ->
  app_pred R phi ->
  app_pred R phi'.
Proof.
(* Goal: forall (_ : @age rmap ag_rmap phi phi') (_ : @app_pred rmap ag_rmap R phi), @app_pred rmap ag_rmap R phi' *)
  destruct R as [R HR]; simpl.
(* Goal: forall (_ : @age rmap ag_rmap phi phi') (_ : R phi), R phi' *)
  apply HR.
Qed.

(* Goal: @eq nat n' (Init.Nat.sub (@level rmap ag_rmap r) n) *)
(* Goal: @eq ghost (ghost_of phi') (ghost_fmap (approx n) (approx n) (ghost_of phi)) *)
Lemma age_yes_sat {Phi Phi' phi phi' l z z' sh sh'} (R : pred rmap) :
  level Phi = level phi ->
  age Phi Phi' ->
  age phi phi' ->
  app_pred R phi ->
  Phi  @ l = YES sh sh' (LK z z') (SomeP rmaps.Mpred (fun _ => R)) ->
  app_pred (approx (S (level phi')) R) phi' /\
  Phi' @ l = YES sh sh' (LK z z') (SomeP rmaps.Mpred (fun _ => approx (level Phi') R)).
Proof.
(* Goal: forall (_ : @eq nat (@level rmap ag_rmap Phi) (@level rmap ag_rmap phi)) (_ : @age rmap ag_rmap Phi Phi') (_ : @age rmap ag_rmap phi phi') (_ : @app_pred rmap ag_rmap R phi) (_ : @eq resource (resource_at Phi l) (YES sh sh' (LK z z') (SomeP rmaps.Mpred (fun _ : list Type => R)))), and (@app_pred rmap ag_rmap (approx (S (@level rmap ag_rmap phi')) R) phi') (@eq resource (resource_at Phi' l) (YES sh sh' (LK z z') (SomeP rmaps.Mpred (fun _ : list Type => approx (@level rmap ag_rmap Phi') R)))) *)
  intros L A Au SAT AT.
(* Goal: and (@app_pred rmap ag_rmap (approx (S (@level rmap ag_rmap phi')) R) phi') (@eq resource (resource_at Phi' l) (YES sh sh' (LK z z') (SomeP rmaps.Mpred (fun _ : list Type => approx (@level rmap ag_rmap Phi') R)))) *)
  pose proof (app_pred_age Au SAT) as SAT'.
(* Goal: @app_pred rmap ag_rmap (approx (S (@level rmap ag_rmap phi')) R) phi' *)
  split.
(* Goal: @app_pred rmap ag_rmap (approx (S (@level rmap ag_rmap phi')) R) phi' *)
  - split.
    + apply age_level in A; apply age_level in Au. omega.
    + apply SAT'.
  - apply (necR_YES _ Phi') in AT.
    + rewrite AT.
(* Goal: @eq resource (resource_at phi loc) (resource_at phi loc) *)
      reflexivity.
    + constructor. assumption.
Qed.

(* Goal: @eq nat n' (Init.Nat.sub (@level rmap ag_rmap r) n) *)
(* Goal: @eq ghost (ghost_of phi') (ghost_fmap (approx n) (approx n) (ghost_of phi)) *)
Lemma age_resource_at {phi phi' loc} :
  age phi phi' ->
  phi' @ loc = resource_fmap (approx (level phi')) (approx (level phi')) (phi @ loc).
Proof.
(* Goal: forall _ : @age rmap ag_rmap phi phi', @eq resource (resource_at phi' loc) (resource_fmap (approx (@level rmap ag_rmap phi')) (approx (@level rmap ag_rmap phi')) (resource_at phi loc)) *)
  intros A.
  rewrite <- (age1_resource_at _ _ A loc (phi @ loc)).
  - reflexivity.
  - rewrite resource_at_approx. reflexivity.
Qed.

Lemma age_to_resource_at phi n loc : age_to n phi @ loc = resource_fmap (approx n) (approx n) (phi @ loc).
Proof.
(* Goal: lt (@level rmap ag_rmap phi') (S (@level rmap ag_rmap phi')) *)
  assert (D : (n <= level phi \/ n >= level phi)%nat) by omega.
  destruct D as [D | D]; swap 1 2.
  - rewrite age_to_ge; auto.
    rewrite <-resource_at_approx.
    match goal with
      |- _ = ?map ?f1 ?f2 (?map ?g1 ?g2 ?r) => transitivity (map (f1 oo g1) (g2 oo f2) r)
    end; swap 1 2.
    + destruct (phi @ loc); unfold "oo"; simpl; auto.
      * destruct p; auto.
        rewrite preds_fmap_fmap; auto.
      * destruct p; auto.
        rewrite preds_fmap_fmap; auto.
    + f_equal. rewrite approx'_oo_approx; auto.
      rewrite approx_oo_approx'; auto.
  - generalize (age_to_ageN n phi).
    generalize (age_to n phi); intros phi'.
    replace n with (level phi - (level phi - n))%nat at 2 3 by omega.
    generalize (level phi - n)%nat; intros k. clear n D.
    revert phi phi'; induction k; intros phi phi'.
    + unfold ageN in *; simpl.
      injection 1 as <-.
      simpl; replace (level phi - 0)%nat with (level phi) by omega.
      symmetry.
      apply resource_at_approx.
    + change (ageN (S k) phi) with
      (match age1 phi with Some w' => ageN k w' | None => None end).
      destruct (age1 phi) as [o|] eqn:Eo. 2:congruence.
      intros A; specialize (IHk _ _ A).
      rewrite IHk.
      pose proof age_resource_at Eo (loc := loc) as R.
      rewrite R.
      clear A R.
      rewrite (age_level _ _ Eo).
      simpl.
      match goal with
        |- ?map ?f1 ?f2 (?map ?g1 ?g2 ?r) = _ => transitivity (map (f1 oo g1) (g2 oo f2) r)
      end.
      * destruct (phi @ loc); unfold "oo"; simpl; auto.
        -- destruct p; auto.
           rewrite preds_fmap_fmap; auto.
        -- destruct p; auto.
           rewrite preds_fmap_fmap; auto.
      * f_equal. rewrite approx_oo_approx'; auto.
(* Goal: lt (@level rmap ag_rmap phi') (S (@level rmap ag_rmap phi')) *)
        omega.
        rewrite approx'_oo_approx; auto.
(* Goal: lt (@level rmap ag_rmap phi') (S (@level rmap ag_rmap phi')) *)
        omega.
Qed.

Lemma age_to_ghost_of phi n : ghost_of (age_to n phi) = ghost_fmap (approx n) (approx n) (ghost_of phi).
Proof.
(* Goal: @eq ghost (ghost_of (@age_to n rmap ag_rmap phi)) (ghost_fmap (approx n) (approx n) (ghost_of phi)) *)
  pose proof (age_to_ageN n phi).
(* Goal: @eq ghost (ghost_of (@age_to n rmap ag_rmap phi)) (ghost_fmap (approx n) (approx n) (ghost_of phi)) *)
  forget (age_to n phi) as phi'.
  remember (level phi - n) as n'.
(* Goal: @eq ghost (ghost_of phi') (ghost_fmap (approx n) (approx n) (ghost_of phi)) *)
  revert dependent n; revert dependent phi; induction n'; intros.
  - inv H.
    rewrite <- ghost_of_approx, ghost_fmap_fmap, approx'_oo_approx, approx_oo_approx' by omega; auto.
  - change (ageN (S n') phi) with
      (match age1 phi with Some w' => ageN n' w' | None => None end) in H.
(* Goal: @eq ghost (ghost_of phi') (ghost_fmap (approx n) (approx n) (ghost_of phi)) *)
    destruct (age1 phi) eqn: Hage; [|discriminate].
(* Goal: @eq ghost (ghost_of phi') (ghost_fmap (approx n) (approx n) (ghost_of phi)) *)
    pose proof (age_level _ _ Hage) as Hl.
    assert (n' = level r - n).
    { rewrite Hl, <- minus_Sn_m in Heqn' by omega; inversion Heqn'; auto. }
(* Goal: @eq ghost (ghost_of phi') (ghost_fmap (approx n) (approx n) (ghost_of phi)) *)
    rewrite (IHn' _ H n), (age1_ghost_of _ _ Hage) by (auto; omega).
(* Goal: @eq ghost (ghost_fmap (approx n) (approx n) (ghost_fmap (approx (@level rmap ag_rmap r)) (approx (@level rmap ag_rmap r)) (ghost_of phi))) (ghost_fmap (approx n) (approx n) (ghost_of phi)) *)
    rewrite ghost_fmap_fmap, approx_oo_approx', approx'_oo_approx by omega; auto.
Qed.
