SepGPM.v

(** Requires:

   opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
   opam update
   opam install coq-iris=branch.gen_proofmode.2018-05-29.0.9b14f90a

*)

(**
   This file contains an instantiation of the Generalized Proof Mode
   (extending Iris) for CFML.
*)

Set Implicit Arguments.
From TLC Require Export LibCore.
From Sep Require Export TLCbuffer SepFunctor.

From iris Require bi proofmode.tactics.
(* We undo the setup done by Stdpp. *)
Global Generalizable No Variables.
Global Obligation Tactic := Coq.Program.Tactics.program_simpl.


(* ********************************************************************** *)
(* * Extension to the core interface that needs to be exposed to GPM *)

Module Type SepCoreHemptySig (SC : SepCore).
Import SC.

(** Implement a definition of heap_empty *)

Parameter heap_empty : heap.

(** Forces the definition of [hempty] to be the canonical one *)

Parameter hempty_eq : 
  hempty = (fun h => h = heap_empty).

End SepCoreHemptySig.



(* ********************************************************************** *)
(* * Subset of the interface of SepLogicSetup that needs to be exposed to GPM *)

Module Type SepSetupGPMSig (SC : SepCore).
Export SC.

Implicit Types h : heap.
Implicit Types H : hprop.
Implicit Types P : Prop.


(* ---------------------------------------------------------------------- *)
(* ** Definition of heap predicates *)

Definition hpure (P:Prop) : hprop :=
  hexists (fun (p:P) => hempty).

Definition hor (H1 H2 : hprop) : hprop :=
  fun h => H1 h \/ H2 h.

Definition hand (H1 H2 : hprop) : hprop :=
  fun h => H1 h /\ H2 h.

Definition hwand (H1 H2 : hprop) : hprop :=
  hexists (fun (H:hprop) => H \* (hpure (H \* H1 ==> H2))).

Definition qwand A (Q1 Q2:A->hprop) :=
  hforall (fun x => hwand (Q1 x) (Q2 x)).

Definition htop : hprop :=
  hexists (fun (H:hprop) => H).


(* ---------------------------------------------------------------------- *)
(* ** Some notation *)

Notation "'Hexists' x1 , H" := (hexists (fun x1 => H))
  (at level 39, x1 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 , H" := (Hexists x1, Hexists x2, H)
  (at level 39, x1 ident, x2 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 x3 , H" := (Hexists x1, Hexists x2, Hexists x3, H)
  (at level 39, x1 ident, x2 ident, x3 ident, H at level 50) : heap_scope.

Notation "\[ P ]" := (hpure P)
  (at level 0, P at level 99, format "\[ P ]") : heap_scope.

Notation "\Top" := (htop) : heap_scope.

Notation "H1 \--* H2" := (hwand H1 H2)
  (at level 43) : heap_scope.

Notation "Q1 \---* Q2" := (qwand Q1 Q2)
  (at level 43) : heap_scope.


(* ---------------------------------------------------------------------- *)
(* ** Definition of [local] *)

Notation "'~~' B" := (hprop->(B->hprop)->Prop)
  (at level 8, only parsing) : type_scope.

Definition local B (F:~~B) : ~~B :=
  fun (H:hprop) (Q:B->hprop) =>
    H ==> Hexists H1 H2 Q1,
       H1 \* H2 \* \[F H1 Q1 /\ Q1 \*+ H2 ===> Q \*+ \Top].

Definition is_local B (F:~~B) :=
  F = local F.


(* ---------------------------------------------------------------------- *)
(* ** Properties *)

Parameter himpl_frame_r : forall H1 H2 H2',
  H2 ==> H2' ->
  (H1 \* H2) ==> (H1 \* H2').

Parameter hstar_pure : forall P H h,
  (\[P] \* H) h = (P /\ H h).

Parameter hpure_intro : forall P h,
  \[] h ->
  P ->
  \[P] h.

Parameter hpure_inv : forall P h,
  \[P] h ->
  P /\ \[] h.

Parameter htop_intro : forall h,
  \Top h.

Parameter himpl_htop_r : forall H H',
  H ==> H' ->
  H ==> H' \* \Top.

Global Opaque hempty hpure hstar hexists htop.


(* ---------------------------------------------------------------------- *)
(* ** Tactics *)

Ltac hpull_xpull_iris_hook := idtac.

Ltac xlocal_core := idtac.

Parameter local_ramified_frame : forall B (Q1:B->hprop) H1 F H Q,
  is_local F ->
  F H1 Q1 ->
  H ==> H1 \* (Q1 \---* Q) ->
  F H Q.

End SepSetupGPMSig.




(* ********************************************************************** *)
(* * Proof Mode *)


Module SepLogicGPM (SC : SepCore) (SCH: SepCoreHemptySig SC) (SS : SepSetupGPMSig SC).
Export SS SCH.


(* ********************************************************************** *)
(* * Instantiating Iris Proof Mode *)

Module ProofModeInstantiate.

Import iris.bi.bi iris.proofmode.coq_tactics.
Export iris.proofmode.tactics.

Canonical Structure hpropC := leibnizC hprop.

Definition hpersistently (H : hprop) : hprop :=
  fun _ => H heap_empty.

(* Proofmode's hpure has to be absorbing. So we redefine it here, and
   we add later by hand the necessary infrastructure for CFML's hpure. *)
Definition hpure_abs (φ : Prop) : hprop := \[φ] \* \Top.

Program Canonical Structure hpropI : bi :=
  Bi hprop _ _ (@pred_incl _) hempty hpure_abs hand hor
     (@pred_impl _) hforall hexists hstar hwand hpersistently _ _.
Next Obligation. apply discrete_ofe_mixin, _. Qed.
Next Obligation.
  Transparent hempty.
  split; [split|..].
  - intros ??; apply himpl_refl.
  - intros ???; apply himpl_trans.
  - intros. rewrite leibniz_equiv_iff. split=>?.
    + subst. auto.
    + apply himpl_antisym; naive_solver.
  - by intros ??? ->%LibAxioms.prop_ext.
  - solve_proper.
  - solve_proper.
  - solve_proper.
  - by intros ???? ->%fun_ext_1.
  - by intros ???? ->%fun_ext_1.
  - solve_proper.
  - solve_proper.
  - solve_proper.
  - intros ?????. rewrite /hpure_abs hstar_pure.
    split; [done|apply htop_intro].
  - intros ??. rewrite /hpure_abs=>Hφ h Hh. apply Hφ.
    + rewrite /hpure_abs hstar_pure in Hh. apply Hh.
    + rewrite hstar_pure. split; [done|]. apply htop_intro.
  - rewrite /hpure_abs=>??? H. rewrite hstar_pure.
    split; [|by apply htop_intro]. intros x. specialize (H x).
    rewrite hstar_pure in H. apply H.
  - by intros ??? [? _].
  - by intros ??? [_ ?].
  - intros P Q R HQ HR ?. by split; [apply HQ|apply HR].
  - by left.
  - by right.
  - intros P Q R HP HQ ? [|]. by apply HP. by apply HQ.
  - intros P Q R H ???. apply H. by split.
  - intros P Q R H ? []. by apply H.
  - intros A P Ψ H ???. by apply H.
  - intros A Ψ a ? H. apply H.
  - by eexists.
  - intros A Φ Q H ? []. by eapply H.
  - intros ??????. eapply pred_incl_trans. by apply himpl_frame_r.
    rewrite (hstar_comm P Q') (hstar_comm Q Q'). by apply himpl_frame_r.
  - intros. by rewrite hstar_hempty_l.
  - intros. by rewrite hstar_hempty_l.
  - intros. by rewrite hstar_comm.
  - intros. by rewrite hstar_assoc.
  - intros P Q R H ??. exists P. rewrite hstar_comm hstar_pure. auto.
  - intros P Q R H. eapply pred_incl_trans.
    { rewrite hstar_comm. by apply himpl_frame_r. }
    unfold hwand. rewrite hstar_comm hstar_hexists=>h [F HF].
    rewrite (hstar_comm F) hstar_assoc hstar_pure in HF. destruct HF as [HR HF].
    by apply HR.
  - intros P Q H h. apply H.
  - auto.
  - unfold hpersistently. rewrite hempty_eq. intros h _. auto.
  - auto.
  - auto.
  - intros P Q h. replace (hpersistently P) with (\[P heap_empty] \* \Top).
    { rewrite hstar_assoc !hstar_pure=>-[? _]. auto using htop_intro. }
    extens=>h'. rewrite hstar_pure /hpersistently. naive_solver auto using htop_intro.
  - intros P Q h [HP HQ]. rewrite -(hstar_hempty_l Q) in HQ.
    eapply himpl_frame_l, HQ. rewrite hempty_eq. intros ? ->. apply HP.
Qed.

Lemma hpure_pure φ : \[φ] = bi_affinely ⌜φ⌝.
Proof.
  extens=>h. split.
  - split; [by eapply hpure_inv|by apply (himpl_htop_r (H:=\[φ]))].
  - intros [? Hφ]. apply hpure_intro; [done|].
    change ((\[φ] \* \Top%I) h) in Hφ. rewrite hstar_pure in Hφ. naive_solver.
Qed.
Lemma htop_True : \Top = True%I.
Proof.
  extens=>h. split=>?.
  - rewrite /bi_pure /= /hpure_abs hstar_pure. auto.
  - apply htop_intro.
Qed.
Opaque hpure_abs.

Ltac unfold_proofmode :=
  change (@bi_and hpropI) with hand;
  change (@bi_or hpropI) with hor;
  change (@bi_emp hpropI) with hempty;
  change (@bi_forall hpropI) with hforall;
  change (@bi_exist hpropI) with hexists;
  change (@bi_sep hpropI) with hstar;
  change (@bi_wand hpropI) with hwand.

End ProofModeInstantiate.



(* ********************************************************************** *)
(* * Tactics for better integration of Iris Proof Mode with CFML Iris *)

Module ProofMode.

Export ProofModeInstantiate.
Import iris.proofmode.coq_tactics. (* TODO: should it be Export? *)

(* We need to repeat all these hints appearing in proofmode/tactics.v,
   so that they state something about CFML connectives. [Hint Extern]
   patterns are not matched modulo canonical structure unification. *)

Hint Extern 0 (_ ==> _) => iStartProof.
Hint Extern 0 (envs_entails _ (hpure _)) => iPureIntro.
Hint Extern 0 (envs_entails _ (hempty)) => iEmpIntro.
Hint Extern 0 (envs_entails _ (hforall _)) => iIntros (?).
Hint Extern 0 (envs_entails _ (hwand _ _)) => iIntros "?".

Hint Extern 1 (envs_entails _ (hand _ _)) => iSplit.
Hint Extern 1 (envs_entails _ (hstar _ _)) => iSplit.
Hint Extern 1 (envs_entails _ (hexists _)) => iExists _.
Hint Extern 1 (envs_entails _ (hor _ _)) => iLeft.
Hint Extern 1 (envs_entails _ (hor _ _)) => iRight.

Hint Extern 2 (envs_entails _ (hstar _ _)) => progress iFrame : iFrame.

(* Specific instances for CFML. *)

Hint Extern 3 (envs_entails _ ?P) => is_evar P; iAccu.
Hint Extern 3 (envs_entails _ (?P _)) => is_evar P; iAccu.

Hint Extern 0 (envs_entails _ (\[_] \* _)) => iSplitR.
Hint Extern 0 (envs_entails _ (\[_] ∗ _)) => iSplitR.
Hint Extern 0 (envs_entails _ (_ \* \[_])) => iSplitL.
Hint Extern 0 (envs_entails _ (_ ∗ \[_])) => iSplitL.

Hint Extern 0 (envs_entails _ (\[] \* _)) => iSplitR.
Hint Extern 0 (envs_entails _ (\[] ∗ _)) => iSplitR.
Hint Extern 0 (envs_entails _ (_ \* \[])) => iSplitL.
Hint Extern 0 (envs_entails _ (_ ∗ \[])) => iSplitL.

(** * Specific Proofmode instances about hpure and htop. *)

Global Instance htop_absorbing : Absorbing \Top.
Proof. intros ??. apply htop_intro. Qed.
Global Instance htop_persistent : Persistent \Top.
Proof. intros ??. apply htop_intro. Qed.

Global Instance htop_into_pure : IntoPure \Top True.
Proof. unfold IntoPure. auto. Qed.
Global Instance htrop_from_pure a : FromPure a \Top True.
Proof. intros ??. apply htop_intro. Qed.

Global Instance hpure_affine φ : Affine \[φ].
Proof. rewrite hpure_pure. apply _. Qed.
Global Instance hpure_persistent φ : Persistent \[φ].
Proof. rewrite hpure_pure. apply _. Qed.

Global Instance hpure_into_pure φ : IntoPure \[φ] φ.
Proof. rewrite hpure_pure /IntoPure. by iDestruct 1 as "%". Qed.
Global Instance hpure_from_pure φ : FromPure true \[φ] φ.
Proof. by rewrite hpure_pure /FromPure /= /bi_affinely stdpp.base.comm. Qed.

Global Instance from_and_hpure φ ψ : FromAnd \[φ ∧ ψ] \[φ] \[ψ].
Proof. rewrite /FromAnd. auto. Qed.
Global Instance from_sep_hpure φ ψ : FromSep \[φ ∧ ψ] \[φ] \[ψ].
Proof. rewrite /FromSep. auto. Qed.
Global Instance into_and_hpure (p : bool) φ ψ : IntoAnd p \[φ ∧ ψ] \[φ] \[ψ].
Proof. rewrite /IntoAnd. (*  do 2 f_equiv. auto. TODO *) admit. Qed.
Global Instance into_sep_hpure φ ψ : IntoSep \[φ ∧ ψ] \[φ] \[ψ].
Proof. rewrite /IntoSep. auto. Qed.
Global Instance from_or_hpure φ ψ : FromOr \[φ ∨ ψ] \[φ] \[ψ].
Proof. rewrite /FromOr. auto. Qed.
Global Instance into_or_hpure φ ψ : IntoOr \[φ ∨ ψ] \[φ] \[ψ].
Proof. rewrite /IntoOr. auto. Qed.
Global Instance from_exist_hpure {A} (φ : A → Prop) :
  FromExist \[∃ x : A, φ x] (λ a : A, \[φ a]).
Proof. rewrite /FromExist. auto. Qed.
Global Instance into_exist_hpure {A} (φ : A → Prop) :
  IntoExist \[∃ x : A, φ x] (λ a : A, \[φ a]).
Proof. rewrite /IntoExist. auto. Qed.
Global Instance from_forall_hpure {A : Type} `{Inhabited A} (φ : A → Prop) :
  FromForall \[∀ a : A, φ a] (λ a : A, \[φ a]).
Proof. rewrite /FromForall. auto. Qed.
Global Instance frame_here_hpure p (φ : Prop) Q :
   FromPure true Q φ → Frame p \[φ] Q emp.
Proof.
  rewrite /FromPure /Frame=><- /=. destruct p=>/=; iIntros "[% _] !%"; auto.
Qed.

(** [PrepareHProp] / [iPrepare] tactic. *)

Class PrepareHProp (P Q : hprop) := prepare_hprop_eq : P = Q.
Hint Mode PrepareHProp ! - : typeclass_instances.
Arguments PrepareHProp _%I _%I.

Instance prepare_hprop_default (P : hprop) : PrepareHProp P P | 100.
Proof. done. Qed.

(* In the case [P ∗ Q] is under a definition, we do not wnat ot apply
   this instance, because it would unfold the definition. Hence, we
   use [Hint Extern] that will apply only if the star match without a
   definition. *)
Lemma prepare_hprop_curry (P Q R S : hprop) :
  PrepareHProp (P -∗ Q -∗ R) S → PrepareHProp (P ∗ Q -∗ R) S.
Proof.
  rewrite /PrepareHProp=><-. apply leibniz_equiv. iSplit.
  - iIntros "H ? ?"; iApply "H"; iFrame.
  - iIntros "H [??]". by iApply ("H" with "[$]").
Qed.
Hint Extern 1 (PrepareHProp ((_ ∗ _) -∗ _) _) =>
  simple eapply prepare_hprop_curry : typeclass_instances.
Hint Extern 1 (PrepareHProp ((_ \* _) -∗ _) _) =>
  simple eapply prepare_hprop_curry : typeclass_instances.
Hint Extern 1 (PrepareHProp ((_ ∗ _)%I \--* _) _) =>
  simple eapply prepare_hprop_curry : typeclass_instances.
Hint Extern 1 (PrepareHProp ((_ \* _) \--* _) _) =>
  simple eapply prepare_hprop_curry : typeclass_instances.

Instance prepare_hprop_hempty_wand (P Q : hprop) :
  PrepareHProp P Q → PrepareHProp (\[] -∗ P) Q.
Proof.
  rewrite /PrepareHProp=><-. apply leibniz_equiv. iSplit; [|by iIntros "$ _"].
  iIntros "H". by iApply "H".
Qed.
Instance prepare_hprop_next (P Q R : hprop) :
  PrepareHProp P Q → PrepareHProp (R -∗ P) (R -∗ Q) | 10.
Proof. by rewrite /PrepareHProp=> ->. Qed.

Instance prepare_hprop_forall {A} (Φ Ψ : A → hprop) :
  (∀ x, PrepareHProp (Φ x) (Ψ x)) → PrepareHProp (∀ x, Φ x) (∀ x, Ψ x).
Proof. rewrite /PrepareHProp=> H. by setoid_rewrite H. Qed.

Instance prepare_hprop_hstar (P P' Q Q' : hprop) :
  PrepareHProp P P' → PrepareHProp Q Q' → PrepareHProp (P ∗ Q) (P' ∗ Q') | 10.
Proof. by rewrite /PrepareHProp=>-> ->. Qed.

Lemma prepare_hprop_hemp_hstar (P Q : hprop) :
  PrepareHProp P Q → PrepareHProp (\[] \* P) Q.
Proof. rewrite /PrepareHProp=>->. by rewrite left_id. Qed.
Hint Extern 1 (PrepareHProp (\[] \* _) _) =>
  simple apply prepare_hprop_hemp_hstar : typeclass_instances.
Hint Extern 1 (PrepareHProp (\[] ∗ _) _) =>
  simple apply prepare_hprop_hemp_hstar : typeclass_instances.
Hint Extern 1 (PrepareHProp (emp%I \* _)%I _) =>
  simple apply prepare_hprop_hemp_hstar : typeclass_instances.
Hint Extern 1 (PrepareHProp (emp ∗ _) _) =>
  simple apply prepare_hprop_hemp_hstar : typeclass_instances.

Lemma prepare_hprop_hstar_hemp (P Q : hprop) :
  PrepareHProp P Q → PrepareHProp (P \* \[]) Q.
Proof. rewrite /PrepareHProp=>->. by rewrite right_id. Qed.
Hint Extern 1 (PrepareHProp (_ \* \[]) _) =>
  simple apply prepare_hprop_hstar_hemp : typeclass_instances.
Hint Extern 1 (PrepareHProp (_ ∗ \[]) _) =>
  simple apply prepare_hprop_hstar_hemp : typeclass_instances.
Hint Extern 1 (PrepareHProp (_ \* emp%I)%I _) =>
  simple apply prepare_hprop_hstar_hemp : typeclass_instances.
Hint Extern 1 (PrepareHProp (_ ∗ emp) _) =>
  simple apply prepare_hprop_hstar_hemp : typeclass_instances.

Instance prepare_hprop_absorbingly (P Q : hprop) :
  PrepareHProp P Q → PrepareHProp (<absorb> P) (<absorb> Q).
Proof. by unfold PrepareHProp=>->. Qed.


Lemma tac_prepare Δ (P Q : hprop) :
  PrepareHProp P Q →
  envs_entails Δ Q →
  envs_entails Δ P.
Proof. by rewrite /PrepareHProp=>->. Qed.

Ltac iPrepare :=
  iStartProof;
  eapply tac_prepare; [apply _|cbv beta].



(* ProofMode's [iIntros] tend to move pure facts in Coq's context.
   While, in general, this is desirable, this is not what we want
   after having applied [local_ramified_frame] because we would loose
   pure facts that will not be unified in [Q] when [Q] is an evar. As
   a result, we use a specific version of this lemma where Q1 is
   locked, and hence pure facts cannot escape.

   This specific version is only used when the post-condition is
   indeed an evar. *)
Lemma local_ramified_frame_locked {B} : forall (Q1 : B → hprop) H1 F H Q,
  is_local F ->
  F H1 Q1 ->
  H ==> H1 \* (locked Q1 \---* Q) ->
  F H Q.
Proof using. unlock. apply local_ramified_frame. Qed.

Ltac ram_apply lem :=
  lazymatch goal with
  | |- ?F _ ?Q =>
    (is_evar Q; eapply local_ramified_frame_locked) ||
    eapply local_ramified_frame
  end; [xlocal_core tt|eapply lem|iPrepare].


(** Fix for hpull/xpull to unfold proof mode functions *)

Ltac hpull_xpull_iris_hook tt ::=
  ProofModeInstantiate.unfold_proofmode.


End ProofMode.


End SepLogicGPM.