Commit f60f76e4 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Define persistently for proof mode by forcing every separation logic to declare an empty heap.

Add a few proofmode type class instance for hpure and htop.
parent b22f4b8f
......@@ -60,7 +60,7 @@ Implicit Types Q : val->hprop.
(** For uniformity with other instantiations of the Separation Logic
functor, we introduce local names for operations and lemmas on heaps. *)
Notation "'heap_empty'" := (fmap_empty : heap) : heap_scope.
Definition heap_empty : heap := fmap_empty.
Notation "h1 \u h2" := (fmap_union h1 h2)
(at level 37, right associativity) : heap_scope.
......@@ -166,7 +166,7 @@ Proof using.
iff (h1&h2&M1&M2&D&U) M.
{ forwards E: hempty_inv M1. subst.
rewrite~ heap_union_empty_l. }
{ exists~ heap_empty h. }
{ exists heap_empty h. unfold heap_empty. auto. }
Qed.
Lemma hstar_comm : forall H1 H2,
......@@ -269,6 +269,7 @@ Proof using.
exists h heap_empty. splits~.
{ unfold hsingle. splits~. }
{ applys~ hpure_intro. applys~ hempty_intro. }
{ unfold heap_empty. auto. }
Qed.
......
......@@ -109,7 +109,7 @@ Coercion heap_state (h : heap) : state :=
(* ** Operators *)
Definition hempty : hprop :=
fun h => h^f = fmap_empty /\ h^r = fmap_empty.
fun h => h = heap_empty.
Program Definition hstar (H1 H2 : hprop) : hprop :=
fun h => exists h1 h2,
......@@ -481,7 +481,7 @@ Proof using. hnfs~. Qed.
Lemma hempty_inv : forall h,
\[] h ->
h = heap_empty.
Proof using. introv M. applys~ heap_eq. Qed.
Proof using. introv M. auto. Qed.
(* ---------------------------------------------------------------------- *)
......@@ -655,14 +655,14 @@ Lemma normal_empty :
normal \[].
Proof using.
Transparent hempty hpure.
introv M. unfolds hempty, hpure. autos*.
introv M. unfolds hempty, hpure. subst. autos*.
Qed.
Lemma normal_pure : forall P,
normal \[P].
Proof using.
Transparent hpure.
introv (p&(M1&M2)). auto.
introv (p&M). unfolds hempty. subst. auto.
Qed.
Lemma normal_empty' : (* simpler proof *)
......@@ -765,18 +765,18 @@ Lemma RO_empty :
RO \[] = \[].
Proof using.
intros. apply pred_ext_1. intros h.
iff (h'&(M1f&M1r)&M2&M3) (M1&M2).
{ rewrite M1f,M1r in M3. rew_fmap. split~. }
{ exists h. rewrite M1,M2. splits~. { split~. } { rew_fmap~. } }
unfold hempty. iff (h'&M1&M2&M3) M1.
{ rewrite M1 in M3. rew_fmap. apply heap_eq. auto. }
{ exists h. rewrite M1. splits~. rew_fmap~. }
Qed.
Lemma RO_pure : forall P,
RO \[P] = \[P].
Proof using.
intros. apply pred_ext_1. intros h.
iff (h'&(M1p&(M1f&M1r))&M2&M3) (MP&(M1&M2)).
{ rewrite M1f,M1r in M3. rew_fmap. split~. split~. }
{ exists h. rewrite M1,M2. splits~. { split~. split~. } { rew_fmap~. } }
iff (h'&(M1p&M2)&M3&M4) (MP&M1); unfolds hempty.
{ rewrite M2 in M4. rew_fmap. split~. apply heap_eq. auto. }
{ exists h. rewrite M1. splits~. { split~. split~. } { rew_fmap~. } }
Qed.
Lemma RO_empty' : (* simpler proof *)
......
From Sep Require Export SepFunctor.
From iris Require Export bi.
From iris.proofmode Require Export tactics.
From iris.proofmode Require Import coq_tactics.
Module SepLogicProofMode (SL : SepLogicCore).
Module Export SS := SepLogicSetup SL.
Canonical Structure hpropC := leibnizC hprop.
(* TODO *)
Definition hpersistently (H : hprop) : hprop := H.
Definition hpersistently (H : hprop) : hprop :=
fun _ => H heap_empty.
(* TODO : remove plainly from the interface. *)
Definition hplainly (H : hprop) : hprop := H.
(* Proofmode's hpure has to be absorbing. So we redefine it here, and
we add later by hand the necessary infrastructure for hpure. *)
Definition hpure_proofmode (φ : Prop) : hprop := \[φ] \* \Top.
we add later by hand the necessary infrastructure for CFML's hpure. *)
Definition hpure_abs (φ : Prop) : hprop := \[φ] \* \Top.
Program Canonical Structure hpropI : bi :=
Bi hpropC _ _ (@pred_incl _) hempty hpure_proofmode hand hor
Bi hprop _ _ (@pred_incl _) hempty hpure_abs hand hor
(@pred_impl _) hforall hexists hstar hwand
hplainly hpersistently _ _.
Next Obligation. apply discrete_ofe_mixin, _. Qed.
Next Obligation.
Transparent hempty.
split; [split|..].
- intros ??; apply himpl_refl.
- intros ???; apply himpl_trans.
......@@ -38,12 +41,12 @@ Next Obligation.
- solve_proper.
- solve_proper.
- solve_proper.
- intros ?????. rewrite /hpure_proofmode hstar_pure.
- intros ?????. rewrite /hpure_abs hstar_pure.
split; [done|apply htop_intro].
- intros ??. rewrite /hpure_proofmode=>Hφ h Hh. apply Hφ.
+ rewrite /hpure_proofmode hstar_pure in Hh. apply Hh.
- 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_proofmode=>??? H. rewrite hstar_pure.
- 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 ??? [? _].
......@@ -71,20 +74,113 @@ Next Obligation.
rewrite (hstar_comm F) hstar_assoc hstar_pure in HF. destruct HF as [HR HF].
by apply HR.
- auto.
- auto.
- auto.
- auto.
- auto.
- auto.
- admit. (* TODO : remove plainly from the interface. *)
- admit. (* TODO : remove plainly from the interface. *)
- auto.
- auto.
- admit. (* TODO : remove plainly from the interface. *)
- auto.
- assert ( P : hpropC, P ==> hpersistently \[]).
{ unfold hpersistently, hempty=>P h HP. auto. }
admit. (* TODO : remove plainly from the interface. *)
- admit. (* TODO : remove plainly from the interface. *)
- unfold hpersistently=>P Q HPQ h. auto.
- auto.
- auto.
- admit. (* TODO : define hpersistently correctly. *)
- admit. (* TODO : define hpersistently correctly. *)
- admit. (* TODO : remove plainly from the interface. *)
- unfold hpersistently, hforall=>A Ψ h H x. auto.
- unfold hpersistently=>A Ψ h [x H]. exists x. auto.
- intros P Q h. replace (hpersistently P) with (\[P heap_empty] \* \Top).
{ rewrite hstar_assoc !hstar_pure=>-[? _]. auto using htop_intro. }
apply fun_ext_1=>h'. apply prop_ext. 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. unfold hempty. intros ? ->. split; [auto|apply HP].
Admitted.
Lemma hpure_pure φ : \[φ] = bi_affinely ⌜φ⌝.
Proof.
apply fun_ext_1=>h. apply prop_ext; 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.
Opaque hpure_abs.
(* 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 _ \[_]) => iPureIntro.
Hint Extern 0 (envs_entails _ \[]) => 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 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 comm. Qed.
(* FIXME : right now, [iPure] cannot introdue \[φ], because it would
have to sheck that the constext is empty. The only way to do this in
the current setup is to [rewrite hpure_pure], then introduce
the [affinely] modality and then [iPure]. This is not particularly
practical. *)
Global Instance from_and_hpure φ ψ : FromAnd \[φ ψ] \[φ] \[ψ].
Proof. rewrite /FromAnd !hpure_pure. iIntros ([??]). auto. Qed.
Global Instance from_sep_hpure φ ψ : FromSep \[φ ψ] \[φ] \[ψ].
Proof. rewrite /FromSep !hpure_pure. iIntros ([??]). auto. Qed.
Global Instance into_and_hpure (p : bool) φ ψ : IntoAnd p \[φ ψ] \[φ] \[ψ].
Proof.
unfold IntoAnd. do 2 f_equiv. iIntros ([??]). rewrite !hpure_pure. auto.
Qed.
Global Instance into_sep_hpure φ ψ : IntoSep \[φ ψ] \[φ] \[ψ].
Proof. unfold IntoSep. iIntros ([??]). rewrite !hpure_pure. auto. Qed.
Global Instance from_or_hpure φ ψ : FromOr \[φ ψ] \[φ] \[ψ].
Proof. unfold FromOr. iIntros ([?|?]); rewrite !hpure_pure; auto. Qed.
Global Instance into_or_hpure φ ψ : IntoOr \[φ ψ] \[φ] \[ψ].
Proof. unfold IntoOr. iIntros ([?|?]); rewrite !hpure_pure; auto. Qed.
Global Instance from_exist_hpure {A} (φ : A Prop) :
FromExist \[ x : A, φ x] (λ a : A, \[φ a]).
Proof. unfold FromExist. iDestruct 1 as (?) "%". rewrite !hpure_pure; eauto. Qed.
Global Instance into_exist_hpure {A} (φ : A Prop) :
IntoExist \[ x : A, φ x] (λ a : A, \[φ a]).
Proof. unfold IntoExist. iIntros ([??]). iExists _. rewrite !hpure_pure; eauto. Qed.
Global Instance from_forall_hpure `{Inhabited A} (φ : A Prop) :
FromForall \[ a : A, φ a] (λ a : A, \[φ a]).
Proof.
rewrite /FromForall hpure_pure. iIntros "H !#" (x).
by iDestruct ("H" $! x) as "%".
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.
End SepLogicProofMode.
......@@ -148,6 +148,7 @@ Module Type SepLogicCore.
(** Type of heaps *)
Parameter heap : Type.
Parameter heap_empty : heap.
(** Type of heap predicates *)
......@@ -159,7 +160,7 @@ Definition hprop := heap -> Prop.
(** Empty heap predicate, written [ \[] ]. *)
Parameter hempty : hprop.
Definition hempty : hprop := fun h => h = heap_empty.
Notation "\[]" := (hempty)
(at level 0) : heap_scope.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment