Require Import VST.msl.msl_standard.
Require Import VST.msl.seplog.
Require Import VST.veric.Clight_base.
Require Import VST.veric.compcert_rmaps.
Require Import VST.veric.juicy_mem.
Require Import VST.veric.juicy_mem_lemmas.
Require Import VST.veric.juicy_mem_ops.
Require Import VST.veric.juicy_extspec.
Require Import VST.veric.tycontext.
Require Import VST.veric.expr2.
Require Import VST.veric.semax.
Require Import VST.veric.semax_call.
Require Import VST.veric.semax_ext.
(*Require Import VST.veric.semax_ext_oracle.*)
Require Import VST.veric.juicy_safety.
Require Import VST.veric.Clight_new.
Require Import VST.veric.res_predicates.
Require Import VST.veric.SeparationLogic.
Require Import VST.sepcomp.semantics.
Require Import VST.sepcomp.extspec.
Require Import VST.floyd.reptype_lemmas.
Require Import VST.floyd.field_at.
Require Import VST.floyd.nested_field_lemmas.
Require Import VST.floyd.client_lemmas.
Require Import VST.floyd.jmeq_lemmas.
Require Import VST.concurrency.lksize.

(*Definition positive_mpred (R : mpred) :=
  forall phi, app_pred R phi -> exists l sh rsh k p, phi @ l = YES sh rsh k p.

Program Definition weak_positive_mpred (P: mpred): mpred :=
  fun w => positive_mpred (approx (S (level w)) P).
Next Obligation.
(* Goal: forall P : mpred, (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => exclusive_mpred (approx (S (@level rmap ag_rmap w)) P)) *)
  intros; hnf; intros.
  unfold positive_mpred in *.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  intros.
  apply H0.
  simpl in H1 |- *.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
  destruct H1; split; auto.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) P) (approx (S (@level rmap ag_rmap a')) P)) (@FF mpred Nveric) *)
  apply age_level in H.
  omega.
Defined.

Lemma corable_weak_positive R : seplog.corable (weak_positive_mpred R).
Proof.
Admitted. (* corable_weak_positive *)

Lemma positive_mpred_nonexpansive:
  nonexpansive weak_positive_mpred.
Proof.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  intros.
(* Goal: @nonexpansive rmap ag_rmap (fun y0 : @pred rmap ag_rmap => @jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (adr_range_dec (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (fun l' : address => yesat (SomeP rmaps.Mpred (fun _ : list Type => y0)) (LK LKSIZE (Z.sub (@snd block Z l') (@snd block Z (@pair block Z b (Ptrofs.unsigned y))))) sh l') noat x) *)
  hnf; intros.
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)) (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_hered.imp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)) (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))))) *)
  intros n ?.
(* Goal: @app_pred nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (weak_exclusive_mpred P) (weak_exclusive_mpred Q)) (@predicates_hered.imp rmap ag_rmap (weak_exclusive_mpred Q) (weak_exclusive_mpred P)))) n *)
  simpl in H |- *.
(* Goal: forall (y : rmap) (_ : ge n (@level rmap ag_rmap y)), and (forall (a' : rmap) (_ : @necR rmap ag_rmap y a') (_ : exclusive_mpred (approx (S (@level rmap ag_rmap a')) P)), exclusive_mpred (approx (S (@level rmap ag_rmap a')) Q)) (forall (a' : rmap) (_ : @necR rmap ag_rmap y a') (_ : exclusive_mpred (approx (S (@level rmap ag_rmap a')) Q)), exclusive_mpred (approx (S (@level rmap ag_rmap a')) P)) *)
  assert (forall y, (n >= level y)%nat -> (P y <-> Q y)).
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R R) (@predicates_hered.imp rmap ag_rmap R R))) *)
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))))) *)
  {
(* Goal: forall (y : rmap) (_ : ge n (@level rmap ag_rmap y)), iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    intros; specialize (H y H0).
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    destruct H.
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    specialize (H y). spec H; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    specialize (H1 y). spec H1; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    tauto.
  }
(* Goal: forall (y : rmap) (_ : ge n (@level rmap ag_rmap y)), and (forall (a' : rmap) (_ : @necR rmap ag_rmap y a') (_ : exclusive_mpred (approx (S (@level rmap ag_rmap a')) P)), exclusive_mpred (approx (S (@level rmap ag_rmap a')) Q)) (forall (a' : rmap) (_ : @necR rmap ag_rmap y a') (_ : exclusive_mpred (approx (S (@level rmap ag_rmap a')) Q)), exclusive_mpred (approx (S (@level rmap ag_rmap a')) P)) *)
  clear H.
(* Goal: forall (y : rmap) (_ : ge n (@level rmap ag_rmap y)), and (forall (a' : rmap) (_ : @necR rmap ag_rmap y a') (_ : exclusive_mpred (approx (S (@level rmap ag_rmap a')) P)), exclusive_mpred (approx (S (@level rmap ag_rmap a')) Q)) (forall (a' : rmap) (_ : @necR rmap ag_rmap y a') (_ : exclusive_mpred (approx (S (@level rmap ag_rmap a')) Q)), exclusive_mpred (approx (S (@level rmap ag_rmap a')) P)) *)
  intros; split; intros.
  + hnf in H2 |- *.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
    intros.
    apply H2; clear H2.
    simpl in H3 |- *.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
    destruct H3; split; auto.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
    apply H0; auto.
(* Goal: @app_pred rmap ag_rmap (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) Q) (approx (S (@level rmap ag_rmap a')) Q)) a *)
    apply necR_level in H1.
    omega.
  + hnf in H2 |- *.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
    intros.
    apply H2; clear H2.
    simpl in H3 |- *.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
    destruct H3; split; auto.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
    apply H0; auto.
(* Goal: @app_pred rmap ag_rmap (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) Q) (approx (S (@level rmap ag_rmap a')) Q)) a *)
    apply necR_level in H1.
    omega.
Qed.

Program Definition weak_precise_mpred (P: mpred): mpred :=
  fun w => precise (approx (S (level w)) P).
Next Obligation.
(* Goal: forall P : mpred, (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => exclusive_mpred (approx (S (@level rmap ag_rmap w)) P)) *)
  intros; hnf; intros.
  hnf in H0 |- *.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  intros.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
  apply (H0 w); auto.
  + simpl in H1 |- *; destruct H1; split; auto.
    apply age_level in H; omega.
  + simpl in H2 |- *; destruct H2; split; auto.
    apply age_level in H; omega.
Defined.

Lemma corable_weak_precise R : seplog.corable (weak_precise_mpred R).
Proof.
Admitted. (* corable_weak_precise *)

Lemma precise_mpred_nonexpansive: nonexpansive weak_precise_mpred.
Proof.
(* Goal: @nonexpansive rmap ag_rmap (fun y0 : @pred rmap ag_rmap => @jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (adr_range_dec (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (fun l' : address => yesat (SomeP rmaps.Mpred (fun _ : list Type => y0)) (LK LKSIZE (Z.sub (@snd block Z l') (@snd block Z (@pair block Z b (Ptrofs.unsigned y))))) sh l') noat x) *)
  hnf; intros.
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)) (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_hered.imp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)) (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))))) *)
  intros n ?.
(* Goal: @app_pred nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (weak_exclusive_mpred P) (weak_exclusive_mpred Q)) (@predicates_hered.imp rmap ag_rmap (weak_exclusive_mpred Q) (weak_exclusive_mpred P)))) n *)
  simpl in H |- *.
(* Goal: forall (y : rmap) (_ : ge n (@level rmap ag_rmap y)), and (forall (a' : rmap) (_ : @necR rmap ag_rmap y a') (_ : exclusive_mpred (approx (S (@level rmap ag_rmap a')) P)), exclusive_mpred (approx (S (@level rmap ag_rmap a')) Q)) (forall (a' : rmap) (_ : @necR rmap ag_rmap y a') (_ : exclusive_mpred (approx (S (@level rmap ag_rmap a')) Q)), exclusive_mpred (approx (S (@level rmap ag_rmap a')) P)) *)
  assert (forall y, (n >= level y)%nat -> (P y <-> Q y)).
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R R) (@predicates_hered.imp rmap ag_rmap R R))) *)
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))))) *)
  {
(* Goal: forall (y : rmap) (_ : ge n (@level rmap ag_rmap y)), iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    intros; specialize (H y H0).
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    destruct H.
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    specialize (H y). spec H; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    specialize (H1 y). spec H1; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    tauto.
  }
(* Goal: forall (y : rmap) (_ : ge n (@level rmap ag_rmap y)), and (forall (a' : rmap) (_ : @necR rmap ag_rmap y a') (_ : exclusive_mpred (approx (S (@level rmap ag_rmap a')) P)), exclusive_mpred (approx (S (@level rmap ag_rmap a')) Q)) (forall (a' : rmap) (_ : @necR rmap ag_rmap y a') (_ : exclusive_mpred (approx (S (@level rmap ag_rmap a')) Q)), exclusive_mpred (approx (S (@level rmap ag_rmap a')) P)) *)
  clear H.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  intros.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  split; intros.
  + hnf in H2 |- *; intros; apply (H2 w); auto.
    - destruct H3; split; auto.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
      apply H0; auto.
      apply necR_level in H1; omega.
    - destruct H4; split; auto.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
      apply H0; auto.
      apply necR_level in H1; omega.
  + hnf in H2 |- *; intros; apply (H2 w); auto.
    - destruct H3; split; auto.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
      apply H0; auto.
      apply necR_level in H1; omega.
    - destruct H4; split; auto.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
      apply H0; auto.
      apply necR_level in H1; omega.
Qed.*)

Lemma approx_derives_ge : forall n m P, (n <= m)%nat -> approx n P |-- approx m P.
Proof.
(* Goal: forall (n m : nat) (P : @pred rmap ag_rmap) (_ : le n m), @derives (@pred rmap ag_rmap) Nveric (approx n P) (approx m P) *)
  intros; change (predicates_hered.derives (approx n P) (approx m P)).
(* Goal: @predicates_hered.derives rmap ag_rmap (approx n P) (approx m P) *)
  intros ? []; split; auto; omega.
Qed.

Lemma approx_derives : forall P n, approx n P |-- P.
Proof.
(* Goal: forall (P : @pred rmap ag_rmap) (n : nat), @derives (@pred rmap ag_rmap) Nveric (approx n P) P *)
  exact approx_p.
Qed.

Definition exclusive_mpred (R : mpred) :=
  (R * R |-- FF)%logic.

Program Definition weak_exclusive_mpred (P: mpred): mpred :=
  fun w => exclusive_mpred (approx (S (level w)) P).
Next Obligation.
(* Goal: forall P : mpred, (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => exclusive_mpred (approx (S (@level rmap ag_rmap w)) P)) *)
  intros; hnf; intros.
(* Goal: exclusive_mpred (approx (S (@level rmap ag_rmap a')) P) *)
  unfold exclusive_mpred in *.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) P) (approx (S (@level rmap ag_rmap a')) P)) (@FF mpred Nveric) *)
  apply age_level in H.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) P) (approx (S (@level rmap ag_rmap a')) P)) (@FF mpred Nveric) *)
  eapply derives_trans, H0.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) P) (approx (S (@level rmap ag_rmap a')) P)) (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a)) P) (approx (S (@level rmap ag_rmap a)) P)) *)
  apply sepcon_derives; apply approx_derives_ge; omega.
Defined.

Lemma corable_weak_exclusive R : seplog.corable (weak_exclusive_mpred R).
Proof.
(* Goal: @corable mpred Nveric Sveric CSLveric (weak_exclusive_mpred R) *)
  change (corable.corable (weak_exclusive_mpred R)).
(* Goal: @corable.corable rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (weak_exclusive_mpred R) *)
  intro; simpl.
(* Goal: @eq Prop (exclusive_mpred (approx (S (@level rmap ag_rmap w)) R)) (exclusive_mpred (approx (S (@level rmap ag_rmap (@core rmap Join_rmap Sep_rmap w))) R)) *)
  rewrite level_core; auto.
Qed.

Lemma exclusive_mpred_nonexpansive:
  nonexpansive weak_exclusive_mpred.
Proof.
(* Goal: @nonexpansive rmap ag_rmap (fun y0 : @pred rmap ag_rmap => @jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (adr_range_dec (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (fun l' : address => yesat (SomeP rmaps.Mpred (fun _ : list Type => y0)) (LK LKSIZE (Z.sub (@snd block Z l') (@snd block Z (@pair block Z b (Ptrofs.unsigned y))))) sh l') noat x) *)
  hnf; intros.
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)) (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_hered.imp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)) (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))))) *)
  intros n ?.
(* Goal: @app_pred nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (weak_exclusive_mpred P) (weak_exclusive_mpred Q)) (@predicates_hered.imp rmap ag_rmap (weak_exclusive_mpred Q) (weak_exclusive_mpred P)))) n *)
  simpl in H |- *.
(* Goal: forall (y : rmap) (_ : ge n (@level rmap ag_rmap y)), and (forall (a' : rmap) (_ : @necR rmap ag_rmap y a') (_ : exclusive_mpred (approx (S (@level rmap ag_rmap a')) P)), exclusive_mpred (approx (S (@level rmap ag_rmap a')) Q)) (forall (a' : rmap) (_ : @necR rmap ag_rmap y a') (_ : exclusive_mpred (approx (S (@level rmap ag_rmap a')) Q)), exclusive_mpred (approx (S (@level rmap ag_rmap a')) P)) *)
  assert (forall y, (n >= level y)%nat -> (P y <-> Q y)).
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R R) (@predicates_hered.imp rmap ag_rmap R R))) *)
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))))) *)
  {
(* Goal: forall (y : rmap) (_ : ge n (@level rmap ag_rmap y)), iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    intros; specialize (H y H0).
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    destruct H.
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    specialize (H y). spec H; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    specialize (H1 y). spec H1; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    tauto.
  }
(* Goal: forall (y : rmap) (_ : ge n (@level rmap ag_rmap y)), and (forall (a' : rmap) (_ : @necR rmap ag_rmap y a') (_ : exclusive_mpred (approx (S (@level rmap ag_rmap a')) P)), exclusive_mpred (approx (S (@level rmap ag_rmap a')) Q)) (forall (a' : rmap) (_ : @necR rmap ag_rmap y a') (_ : exclusive_mpred (approx (S (@level rmap ag_rmap a')) Q)), exclusive_mpred (approx (S (@level rmap ag_rmap a')) P)) *)
  clear H.
(* Goal: forall (y : rmap) (_ : ge n (@level rmap ag_rmap y)), and (forall (a' : rmap) (_ : @necR rmap ag_rmap y a') (_ : exclusive_mpred (approx (S (@level rmap ag_rmap a')) P)), exclusive_mpred (approx (S (@level rmap ag_rmap a')) Q)) (forall (a' : rmap) (_ : @necR rmap ag_rmap y a') (_ : exclusive_mpred (approx (S (@level rmap ag_rmap a')) Q)), exclusive_mpred (approx (S (@level rmap ag_rmap a')) P)) *)
  intros; split; intros.
(* Goal: exclusive_mpred (approx (S (@level rmap ag_rmap a')) P) *)
  + unfold exclusive_mpred in *.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) P) (approx (S (@level rmap ag_rmap a')) P)) (@FF mpred Nveric) *)
    eapply derives_trans, H2.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) P) (approx (S (@level rmap ag_rmap a')) P)) (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) Q) (approx (S (@level rmap ag_rmap a')) Q)) *)
    match goal with |- ?P |-- ?Q => change (predicates_hered.derives P Q) end.
(* Goal: @predicates_hered.derives rmap ag_rmap (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) P) (approx (S (@level rmap ag_rmap a')) P)) (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) Q) (approx (S (@level rmap ag_rmap a')) Q)) *)
    intros ? (? & ? & J & [] & []).
(* Goal: @app_pred rmap ag_rmap (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) Q) (approx (S (@level rmap ag_rmap a')) Q)) a *)
    pose proof (join_level _ _ _ J) as [].
(* Goal: @app_pred rmap ag_rmap (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) Q) (approx (S (@level rmap ag_rmap a')) Q)) a *)
    apply necR_level in H1.
(* Goal: @app_pred rmap ag_rmap (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) Q) (approx (S (@level rmap ag_rmap a')) Q)) a *)
    do 3 eexists; eauto; split; split; try omega; apply H0; auto; omega.
(* Goal: exclusive_mpred (approx (S (@level rmap ag_rmap a')) P) *)
  + unfold exclusive_mpred in *.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) P) (approx (S (@level rmap ag_rmap a')) P)) (@FF mpred Nveric) *)
    eapply derives_trans, H2.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) P) (approx (S (@level rmap ag_rmap a')) P)) (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) Q) (approx (S (@level rmap ag_rmap a')) Q)) *)
    match goal with |- ?P |-- ?Q => change (predicates_hered.derives P Q) end.
(* Goal: @predicates_hered.derives rmap ag_rmap (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) P) (approx (S (@level rmap ag_rmap a')) P)) (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) Q) (approx (S (@level rmap ag_rmap a')) Q)) *)
    intros ? (? & ? & J & [] & []).
(* Goal: @app_pred rmap ag_rmap (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) Q) (approx (S (@level rmap ag_rmap a')) Q)) a *)
    pose proof (join_level _ _ _ J) as [].
(* Goal: @app_pred rmap ag_rmap (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) Q) (approx (S (@level rmap ag_rmap a')) Q)) a *)
    apply necR_level in H1.
(* Goal: @app_pred rmap ag_rmap (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap a')) Q) (approx (S (@level rmap ag_rmap a')) Q)) a *)
    do 3 eexists; eauto; split; split; try omega; apply H0; auto; omega.
Qed.

Definition lock_inv : share -> val -> mpred -> mpred :=
  fun sh v R =>
    (EX b : block, EX ofs : _,
      !!(v = Vptr b ofs) &&
      LKspec LKSIZE
        R sh (b, Ptrofs.unsigned ofs))%logic.

Definition rec_inv sh v (Q R: mpred): Prop :=
  (R = Q * |>lock_inv sh v R)%logic.

Definition weak_rec_inv sh v (Q R: mpred): mpred :=
  (! (R <=> Q * |>lock_inv sh v R))%pred.

Lemma lockinv_isptr sh v R : lock_inv sh v R = (!! isptr v && lock_inv sh v R)%logic.
Proof.
  assert (D : isptr v \/ ~isptr v) by (destruct v; simpl; auto).
  destruct D.
  - rewrite prop_true_andp; auto.
  - rewrite prop_false_andp; auto.
    apply pred_ext.
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    + unfold lock_inv. Transparent mpred. Intros b ofs. Opaque mpred. subst; simpl in *; tauto.
    + apply FF_left.
Qed.

Lemma unfash_fash_equiv: forall P Q: mpred,
  (P <=> Q |--
  (subtypes.unfash (subtypes.fash P): mpred) <=> (subtypes.unfash (subtypes.fash Q): mpred))%pred.
Proof.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  intros.
(* Goal: @nonexpansive rmap ag_rmap (fun y0 : @pred rmap ag_rmap => @jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (adr_range_dec (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (fun l' : address => yesat (SomeP rmaps.Mpred (fun _ : list Type => y0)) (LK LKSIZE (Z.sub (@snd block Z l') (@snd block Z (@pair block Z b (Ptrofs.unsigned y))))) sh l') noat x) *)
  hnf; intros.
  assert (forall y: rmap, (a >= level y)%nat -> (app_pred P y <-> app_pred Q y)).
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R R) (@predicates_hered.imp rmap ag_rmap R R))) *)
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))))) *)
  {
(* Goal: forall (y : rmap) (_ : ge n (@level rmap ag_rmap y)), iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    intros; specialize (H y H0).
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    destruct H.
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    specialize (H y). spec H; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    specialize (H1 y). spec H1; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    tauto.
  }
(* Goal: @nonexpansive rmap ag_rmap (fun y0 : @pred rmap ag_rmap => @jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (adr_range_dec (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (fun l' : address => yesat (SomeP rmaps.Mpred (fun _ : list Type => y0)) (LK LKSIZE (Z.sub (@snd block Z l') (@snd block Z (@pair block Z b (Ptrofs.unsigned y))))) sh l') noat x) *)
  hnf; intros.
(* Goal: @nonexpansive rmap ag_rmap (fun y0 : @pred rmap ag_rmap => @jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (adr_range_dec (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (fun l' : address => yesat (SomeP rmaps.Mpred (fun _ : list Type => y0)) (LK LKSIZE (Z.sub (@snd block Z l') (@snd block Z (@pair block Z b (Ptrofs.unsigned y))))) sh l') noat x) *)
  split; simpl; hnf; intros.
  + apply necR_level in H2.
    rewrite <- H0 by omega.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
    auto.
  + apply necR_level in H2.
(* Goal: @app_pred rmap ag_rmap P a'0 *)
    rewrite H0 by omega.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
    auto.
Qed.

Lemma iffp_equiv: forall P1 Q1 P2 Q2: mpred,
  ((P1 <=> Q1) && (P2 <=> Q2) |-- (P1 <--> P2) <=> (Q1 <--> Q2))%pred.
Proof.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  intros.
(* Goal: @nonexpansive rmap ag_rmap (fun y0 : @pred rmap ag_rmap => @jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (adr_range_dec (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (fun l' : address => yesat (SomeP rmaps.Mpred (fun _ : list Type => y0)) (LK LKSIZE (Z.sub (@snd block Z l') (@snd block Z (@pair block Z b (Ptrofs.unsigned y))))) sh l') noat x) *)
  hnf; intros.
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
  destruct H.
  assert (forall y: rmap, (a >= level y)%nat -> (app_pred P1 y <-> app_pred Q1 y)).
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R R) (@predicates_hered.imp rmap ag_rmap R R))) *)
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))))) *)
  {
(* Goal: forall (y : rmap) (_ : ge a (@level rmap ag_rmap y)), iff (@app_pred rmap ag_rmap P1 y) (@app_pred rmap ag_rmap Q1 y) *)
    intros; specialize (H y H1).
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    destruct H.
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    specialize (H y). spec H; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P1 y) (@app_pred rmap ag_rmap Q1 y) *)
    specialize (H2 y). spec H2; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    tauto.
  }
  assert (forall y: rmap, (a >= level y)%nat -> (app_pred P2 y <-> app_pred Q2 y)).
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R R) (@predicates_hered.imp rmap ag_rmap R R))) *)
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))))) *)
  {
(* Goal: forall (y : rmap) (_ : ge a (@level rmap ag_rmap y)), iff (@app_pred rmap ag_rmap P2 y) (@app_pred rmap ag_rmap Q2 y) *)
    intros; specialize (H0 y H2).
(* Goal: iff (@app_pred rmap ag_rmap P2 y) (@app_pred rmap ag_rmap Q2 y) *)
    destruct H0.
(* Goal: iff (@app_pred rmap ag_rmap P2 y) (@app_pred rmap ag_rmap Q2 y) *)
    specialize (H0 y). spec H0; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P2 y) (@app_pred rmap ag_rmap Q2 y) *)
    specialize (H3 y). spec H3; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    tauto.
  }
(* Goal: forall P : mpred, (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => exclusive_mpred (approx (S (@level rmap ag_rmap w)) P)) *)
  split; intros; hnf; intros.
  + split; [destruct H5 as [? _] | destruct H5 as [_ ?]]; intros ? HH; specialize (H5 _ HH).
    - apply necR_level in H4.
(* Goal: forall _ : @app_pred rmap ag_rmap P2 a'0, @app_pred rmap ag_rmap P1 a'0 *)
      apply necR_level in HH.
      rewrite <- H1, <- H2 by omega.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
      auto.
    - apply necR_level in H4.
(* Goal: forall _ : @app_pred rmap ag_rmap P2 a'0, @app_pred rmap ag_rmap P1 a'0 *)
      apply necR_level in HH.
      rewrite <- H1, <- H2 by omega.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
      auto.
  + split; [destruct H5 as [? _] | destruct H5 as [_ ?]]; intros ? HH; specialize (H5 _ HH).
    - apply necR_level in H4.
(* Goal: forall _ : @app_pred rmap ag_rmap P2 a'0, @app_pred rmap ag_rmap P1 a'0 *)
      apply necR_level in HH.
(* Goal: forall _ : @app_pred rmap ag_rmap P2 a'0, @app_pred rmap ag_rmap P1 a'0 *)
      rewrite H1, H2 by omega.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
      auto.
    - apply necR_level in H4.
(* Goal: forall _ : @app_pred rmap ag_rmap P2 a'0, @app_pred rmap ag_rmap P1 a'0 *)
      apply necR_level in HH.
(* Goal: forall _ : @app_pred rmap ag_rmap P2 a'0, @app_pred rmap ag_rmap P1 a'0 *)
      rewrite H1, H2 by omega.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
      auto.
Qed.

Lemma sepcon_equiv: forall P1 Q1 P2 Q2: mpred,
  ((P1 <=> Q1) && (P2 <=> Q2) |-- (P1 * P2) <=> (Q1 * Q2))%pred.
Proof.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  intros.
(* Goal: @nonexpansive rmap ag_rmap (fun y0 : @pred rmap ag_rmap => @jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (adr_range_dec (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (fun l' : address => yesat (SomeP rmaps.Mpred (fun _ : list Type => y0)) (LK LKSIZE (Z.sub (@snd block Z l') (@snd block Z (@pair block Z b (Ptrofs.unsigned y))))) sh l') noat x) *)
  hnf; intros.
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
  destruct H.
  assert (forall y: rmap, (a >= level y)%nat -> (app_pred P1 y <-> app_pred Q1 y)).
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R R) (@predicates_hered.imp rmap ag_rmap R R))) *)
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))))) *)
  {
(* Goal: forall (y : rmap) (_ : ge a (@level rmap ag_rmap y)), iff (@app_pred rmap ag_rmap P1 y) (@app_pred rmap ag_rmap Q1 y) *)
    intros; specialize (H y H1).
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    destruct H.
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    specialize (H y). spec H; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P1 y) (@app_pred rmap ag_rmap Q1 y) *)
    specialize (H2 y). spec H2; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    tauto.
  }
  assert (forall y: rmap, (a >= level y)%nat -> (app_pred P2 y <-> app_pred Q2 y)).
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R R) (@predicates_hered.imp rmap ag_rmap R R))) *)
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))))) *)
  {
(* Goal: forall (y : rmap) (_ : ge a (@level rmap ag_rmap y)), iff (@app_pred rmap ag_rmap P2 y) (@app_pred rmap ag_rmap Q2 y) *)
    intros; specialize (H0 y H2).
(* Goal: iff (@app_pred rmap ag_rmap P2 y) (@app_pred rmap ag_rmap Q2 y) *)
    destruct H0.
(* Goal: iff (@app_pred rmap ag_rmap P2 y) (@app_pred rmap ag_rmap Q2 y) *)
    specialize (H0 y). spec H0; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P2 y) (@app_pred rmap ag_rmap Q2 y) *)
    specialize (H3 y). spec H3; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    tauto.
  }
(* Goal: forall P : mpred, (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w : rmap => exclusive_mpred (approx (S (@level rmap ag_rmap w)) P)) *)
  split; intros; hnf; intros.
  + destruct H5 as [w1 [w2 [? [? ?]]]].
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
    exists w1, w2; split; [| split]; auto.
    - apply necR_level in H4.
(* Goal: @app_pred rmap ag_rmap P2 w2 *)
      apply join_level in H5.
      rewrite <- H1 by omega; auto.
    - apply necR_level in H4.
(* Goal: @app_pred rmap ag_rmap P2 w2 *)
      apply join_level in H5.
      rewrite <- H2 by omega; auto.
  + destruct H5 as [w1 [w2 [? [? ?]]]].
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
    exists w1, w2; split; [| split]; auto.
    - apply necR_level in H4.
(* Goal: @app_pred rmap ag_rmap P2 w2 *)
      apply join_level in H5.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
      rewrite H1 by omega; auto.
    - apply necR_level in H4.
(* Goal: @app_pred rmap ag_rmap P2 w2 *)
      apply join_level in H5.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
      rewrite H2 by omega; auto.
Qed.

Lemma later_equiv: forall P Q: mpred,
  (P <=> Q |-- |> P <=> |> Q)%pred.
Proof.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  intros.
(* Goal: @nonexpansive rmap ag_rmap (fun y0 : @pred rmap ag_rmap => @jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (adr_range_dec (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (fun l' : address => yesat (SomeP rmaps.Mpred (fun _ : list Type => y0)) (LK LKSIZE (Z.sub (@snd block Z l') (@snd block Z (@pair block Z b (Ptrofs.unsigned y))))) sh l') noat x) *)
  hnf; intros.
  assert (forall y: rmap, (a >= level y)%nat -> (app_pred P y <-> app_pred Q y)).
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R R) (@predicates_hered.imp rmap ag_rmap R R))) *)
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))))) *)
  {
(* Goal: forall (y : rmap) (_ : ge n (@level rmap ag_rmap y)), iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    intros; specialize (H y H0).
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    destruct H.
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    specialize (H y). spec H; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    specialize (H1 y). spec H1; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    tauto.
  }
(* Goal: @nonexpansive rmap ag_rmap (fun y0 : @pred rmap ag_rmap => @jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (adr_range_dec (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (fun l' : address => yesat (SomeP rmaps.Mpred (fun _ : list Type => y0)) (LK LKSIZE (Z.sub (@snd block Z l') (@snd block Z (@pair block Z b (Ptrofs.unsigned y))))) sh l') noat x) *)
  hnf; intros.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  split; hnf; intros; simpl in *; intros.
  + specialize (H3 _ H4).
(* Goal: @app_pred rmap ag_rmap Q a *)
    apply necR_level in H2.
(* Goal: @app_pred rmap ag_rmap P a'0 *)
    apply laterR_level in H4.
    rewrite <- H0 by omega.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
    auto.
  + specialize (H3 _ H4).
(* Goal: @app_pred rmap ag_rmap Q a *)
    apply necR_level in H2.
(* Goal: @app_pred rmap ag_rmap P a'0 *)
    apply laterR_level in H4.
(* Goal: @app_pred rmap ag_rmap P a'0 *)
    rewrite H0 by omega.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
    auto.
Qed.

Lemma nonexpansive_lock_inv : forall sh p, nonexpansive (lock_inv sh p).
Proof.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  intros.
(* Goal: @nonexpansive rmap ag_rmap (lock_inv sh p) *)
  unfold lock_inv.
(* Goal: @nonexpansive rmap ag_rmap (fun y : @pred rmap ag_rmap => @exp (@pred rmap ag_rmap) Nveric Ptrofs.int (fun ofs : Ptrofs.int => @andp (@pred rmap ag_rmap) Nveric (@prop (@pred rmap ag_rmap) Nveric (@eq val p (Vptr b ofs))) (LKspec LKSIZE y sh (@pair block Z b (Ptrofs.unsigned ofs))))) *)
  apply @exists_nonexpansive.
(* Goal: forall x : block, @nonexpansive rmap ag_rmap (fun y : @pred rmap ag_rmap => @exp (@pred rmap ag_rmap) Nveric Ptrofs.int (fun ofs : Ptrofs.int => @andp (@pred rmap ag_rmap) Nveric (@prop (@pred rmap ag_rmap) Nveric (@eq val p (Vptr x ofs))) (LKspec LKSIZE y sh (@pair block Z x (Ptrofs.unsigned ofs))))) *)
  intros b.
(* Goal: @nonexpansive rmap ag_rmap (fun y : @pred rmap ag_rmap => @exp (@pred rmap ag_rmap) Nveric Ptrofs.int (fun ofs : Ptrofs.int => @andp (@pred rmap ag_rmap) Nveric (@prop (@pred rmap ag_rmap) Nveric (@eq val p (Vptr b ofs))) (LKspec LKSIZE y sh (@pair block Z b (Ptrofs.unsigned ofs))))) *)
  apply @exists_nonexpansive.
(* Goal: forall x : Ptrofs.int, @nonexpansive rmap ag_rmap (fun y : @pred rmap ag_rmap => @andp (@pred rmap ag_rmap) Nveric (@prop (@pred rmap ag_rmap) Nveric (@eq val p (Vptr b x))) (LKspec LKSIZE y sh (@pair block Z b (Ptrofs.unsigned x)))) *)
  intros y.
(* Goal: @nonexpansive rmap ag_rmap (fun y0 : @pred rmap ag_rmap => @andp (@pred rmap ag_rmap) Nveric (@prop (@pred rmap ag_rmap) Nveric (@eq val p (Vptr b y))) (LKspec LKSIZE y0 sh (@pair block Z b (Ptrofs.unsigned y)))) *)
  apply @conj_nonexpansive.
(* Goal: @nonexpansive rmap ag_rmap (fun _ : @pred rmap ag_rmap => @prop (@pred rmap ag_rmap) Nveric (@eq val p (Vptr b y))) *)
(* Goal: @nonexpansive rmap ag_rmap (fun x : @pred rmap ag_rmap => LKspec LKSIZE x sh (@pair block Z b (Ptrofs.unsigned y))) *)
  apply @const_nonexpansive.

(* Goal: @nonexpansive rmap ag_rmap (fun x : @pred rmap ag_rmap => LKspec LKSIZE x sh (@pair block Z b (Ptrofs.unsigned y))) *)
  unfold LKspec.
(* Goal: @nonexpansive rmap ag_rmap (fun x : @pred rmap ag_rmap => @predicates_hered.andp rmap ag_rmap (@predicates_hered.allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (adr_range_dec (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (fun l' : address => yesat (SomeP rmaps.Mpred (fun _ : list Type => x)) (LK LKSIZE (Z.sub (@snd block Z l') (@snd block Z (@pair block Z b (Ptrofs.unsigned y))))) sh l') noat)) noghost) *)
  apply conj_nonexpansive, const_nonexpansive.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  apply forall_nonexpansive; intros.
(* Goal: @nonexpansive rmap ag_rmap (fun y0 : @pred rmap ag_rmap => @jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (adr_range_dec (@pair block Z b (Ptrofs.unsigned y)) LKSIZE) (fun l' : address => yesat (SomeP rmaps.Mpred (fun _ : list Type => y0)) (LK LKSIZE (Z.sub (@snd block Z l') (@snd block Z (@pair block Z b (Ptrofs.unsigned y))))) sh l') noat x) *)
  hnf; intros.
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)) (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_hered.imp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)) (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))))) *)
  intros n ?.
  assert (forall y: rmap, (n >= level y)%nat -> (app_pred P y <-> app_pred Q y)).
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R R) (@predicates_hered.imp rmap ag_rmap R R))) *)
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))))) *)
  {
    clear - H.
(* Goal: forall (y : rmap) (_ : ge n (@level rmap ag_rmap y)), iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    intros; specialize (H y H0).
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    destruct H.
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    specialize (H y). spec H; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    specialize (H1 y). spec H1; [auto |].
(* Goal: iff (@app_pred rmap ag_rmap P y) (@app_pred rmap ag_rmap Q y) *)
    tauto.
  }
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  simpl; split; intros.
  + if_tac; auto.
(* Goal: @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at a' x) (YES sh rsh (LK LKSIZE (Z.sub (@snd block Z x) (Ptrofs.unsigned y))) (SomeP rmaps.Mpred (fun _ : list Type => approx (@level rmap ag_rmap a') P)))) *)
    destruct H3 as [p0 ?].
(* Goal: @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at a' x) (YES sh rsh (LK LKSIZE (Z.sub (@snd block Z x) (Ptrofs.unsigned y))) (SomeP rmaps.Mpred (fun _ : list Type => approx (@level rmap ag_rmap a') P)))) *)
    exists p0.
(* Goal: @eq resource (resource_at a' x) (YES sh p0 (LK LKSIZE (Z.sub (@snd block Z x) (Ptrofs.unsigned y))) (SomeP rmaps.Mpred (fun _ : list Type => approx (@level rmap ag_rmap a') P))) *)
    rewrite H3; f_equal.
(* Goal: @eq preds (SomeP rmaps.Mpred (fun _ : list Type => approx (@level rmap ag_rmap a') Q)) (SomeP rmaps.Mpred (fun _ : list Type => approx (@level rmap ag_rmap a') P)) *)
    f_equal.
(* Goal: @eq (forall _ : list Type, @pred rmap ag_rmap) (fun _ : list Type => approx (@level rmap ag_rmap a') Q) (fun _ : list Type => approx (@level rmap ag_rmap a') P) *)
    extensionality ts; clear ts.
(* Goal: @eq (@pred rmap ag_rmap) (approx (@level rmap ag_rmap a') Q) (approx (@level rmap ag_rmap a') P) *)
    clear H3 H4 p0.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
    apply predicates_hered.pred_ext; hnf; intros ? [? ?]; split; auto.
    - apply necR_level in H2.
      rewrite <- H0 by omega; auto.
    - apply necR_level in H2.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
      rewrite H0 by omega; auto.
  + if_tac; auto.
(* Goal: @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at a' x) (YES sh rsh (LK LKSIZE (Z.sub (@snd block Z x) (Ptrofs.unsigned y))) (SomeP rmaps.Mpred (fun _ : list Type => approx (@level rmap ag_rmap a') P)))) *)
    destruct H3 as [p0 ?].
(* Goal: @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at a' x) (YES sh rsh (LK LKSIZE (Z.sub (@snd block Z x) (Ptrofs.unsigned y))) (SomeP rmaps.Mpred (fun _ : list Type => approx (@level rmap ag_rmap a') P)))) *)
    exists p0.
(* Goal: @eq resource (resource_at a' x) (YES sh p0 (LK LKSIZE (Z.sub (@snd block Z x) (Ptrofs.unsigned y))) (SomeP rmaps.Mpred (fun _ : list Type => approx (@level rmap ag_rmap a') P))) *)
    rewrite H3; f_equal.
(* Goal: @eq preds (SomeP rmaps.Mpred (fun _ : list Type => approx (@level rmap ag_rmap a') Q)) (SomeP rmaps.Mpred (fun _ : list Type => approx (@level rmap ag_rmap a') P)) *)
    f_equal.
(* Goal: @eq (forall _ : list Type, @pred rmap ag_rmap) (fun _ : list Type => approx (@level rmap ag_rmap a') Q) (fun _ : list Type => approx (@level rmap ag_rmap a') P) *)
    extensionality ts; clear ts.
(* Goal: @eq (@pred rmap ag_rmap) (approx (@level rmap ag_rmap a') Q) (approx (@level rmap ag_rmap a') P) *)
    clear H3 H4 p0.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
    apply predicates_hered.pred_ext; hnf; intros ? [? ?]; split; auto.
    - apply necR_level in H2.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
      rewrite H0 by omega; auto.
    - apply necR_level in H2.
      rewrite <- H0 by omega; auto.
Qed.

Lemma rec_inv1_nonexpansive: forall sh v Q,
  nonexpansive (weak_rec_inv sh v Q).
Proof.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  intros.
(* Goal: @nonexpansive rmap ag_rmap (fun Q : @pred rmap ag_rmap => weak_rec_inv sh v Q R) *)
  unfold weak_rec_inv.
(* Goal: @nonexpansive rmap ag_rmap (fun Q : @pred rmap ag_rmap => @subtypes.unfash rmap ag_rmap (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)))) *)
  intros P1 P2.
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@subtypes.unfash rmap ag_rmap (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)))) (@subtypes.unfash rmap ag_rmap (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R))))) (@predicates_hered.imp rmap ag_rmap (@subtypes.unfash rmap ag_rmap (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)))) (@subtypes.unfash rmap ag_rmap (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R))))))) *)
  eapply predicates_hered.derives_trans; [| apply unfash_fash_equiv].
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R))) (@predicates_hered.imp rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R))))) *)
  eapply predicates_hered.derives_trans; [| apply iffp_equiv].
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
  apply predicates_hered.andp_right; auto.
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))))) *)
  eapply predicates_hered.derives_trans; [| apply sepcon_equiv].
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@predicates_hered.andp nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R R) (@predicates_hered.imp rmap ag_rmap R R))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))))))) *)
  apply predicates_hered.andp_right.
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R R) (@predicates_hered.imp rmap ag_rmap R R))) *)
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))))) *)
  {
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)) (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_hered.imp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)) (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))))) *)
    intros n ?.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
    split; intros; hnf; intros; auto.
  }
  rewrite <- subtypes.eqp_later.
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@box nat ag_nat (@laterM nat ag_nat) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (lock_inv sh v P1) (lock_inv sh v P2)) (@predicates_hered.imp rmap ag_rmap (lock_inv sh v P2) (lock_inv sh v P1))))) *)
  eapply predicates_hered.derives_trans, predicates_hered.now_later.
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (lock_inv sh v P1) (lock_inv sh v P2)) (@predicates_hered.imp rmap ag_rmap (lock_inv sh v P2) (lock_inv sh v P1)))) *)
  apply nonexpansive_lock_inv.
Qed.

Lemma rec_inv2_nonexpansive: forall sh v R,
  nonexpansive (fun Q => weak_rec_inv sh v Q R).
Proof.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  intros.
(* Goal: @nonexpansive rmap ag_rmap (fun Q : @pred rmap ag_rmap => weak_rec_inv sh v Q R) *)
  unfold weak_rec_inv.
(* Goal: @nonexpansive rmap ag_rmap (fun Q : @pred rmap ag_rmap => @subtypes.unfash rmap ag_rmap (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)))) *)
  intros P1 P2.
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@subtypes.unfash rmap ag_rmap (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)))) (@subtypes.unfash rmap ag_rmap (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R))))) (@predicates_hered.imp rmap ag_rmap (@subtypes.unfash rmap ag_rmap (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)))) (@subtypes.unfash rmap ag_rmap (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R))))))) *)
  eapply predicates_hered.derives_trans; [| apply unfash_fash_equiv].
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R))) (@predicates_hered.imp rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R))))) *)
  eapply predicates_hered.derives_trans; [| apply iffp_equiv].
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@predicates_hered.andp nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R R) (@predicates_hered.imp rmap ag_rmap R R))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))))))) *)
  apply predicates_hered.andp_right.
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R R) (@predicates_hered.imp rmap ag_rmap R R))) *)
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))))) *)
  {
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)) (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_hered.imp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)) (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))))) *)
    intros n ?.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
    split; intros; hnf; intros; auto.
  }
(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P2 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P1 (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))))) *)
  eapply predicates_hered.derives_trans; [| apply sepcon_equiv].
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
  apply predicates_hered.andp_right; auto.

(* Goal: @predicates_hered.derives nat ag_nat (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap P1 P2) (@predicates_hered.imp rmap ag_rmap P2 P1))) (@subtypes.fash rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)) (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) (@predicates_hered.imp rmap ag_rmap (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)) (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))))) *)
  intros n ?.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
  split; intros; hnf; intros; auto.
Qed.

Lemma exclusive_weak_exclusive: forall R,
  exclusive_mpred R ->
  TT |-- weak_exclusive_mpred R.
Proof.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  intros.
(* Goal: @derives mpred Nveric (@TT mpred Nveric) (weak_exclusive_mpred R) *)
  change (predicates_hered.derives TT (weak_exclusive_mpred R)).
(* Goal: @predicates_hered.derives rmap ag_rmap (@TT (@pred rmap ag_rmap) Nveric) (weak_rec_inv sh v Q R) *)
  intros w _.
(* Goal: @app_pred rmap ag_rmap (weak_exclusive_mpred R) w *)
  simpl.
(* Goal: exclusive_mpred (approx (S (@level rmap ag_rmap w)) R) *)
  eapply derives_trans, H.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (approx (S (@level rmap ag_rmap w)) R) (approx (S (@level rmap ag_rmap w)) R)) (@sepcon mpred Nveric Sveric R R) *)
  apply sepcon_derives; apply approx_derives.
Qed.

Lemma rec_inv_weak_rec_inv: forall sh v Q R,
  rec_inv sh v Q R ->
  TT |-- weak_rec_inv sh v Q R.
Proof.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  intros.
(* Goal: @derives mpred Nveric (@TT mpred Nveric) (weak_rec_inv sh v Q R) *)
  change (predicates_hered.derives TT (weak_rec_inv sh v Q R)).
(* Goal: @predicates_hered.derives rmap ag_rmap (@TT (@pred rmap ag_rmap) Nveric) (weak_rec_inv sh v Q R) *)
  intros w _.
  hnf in H |- *.
(* Goal: forall (y : rmap) (_ : ge (@level rmap ag_rmap w) (@level rmap ag_rmap y)), @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  intros.
(* Goal: @app_pred rmap ag_rmap (@predicates_hered.andp rmap ag_rmap (@predicates_hered.imp rmap ag_rmap R (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R)))) (@predicates_hered.imp rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap Q (@box rmap ag_rmap (@laterM rmap ag_rmap) (lock_inv sh v R))) R)) y *)
  rewrite H at 1 4.
(* Goal: @app_pred rmap ag_rmap Q a'0 *)
  split; intros; hnf; intros; auto.
Qed.
