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

Integrate Proofmode.v into SepTactics.v. Add ProofMode support for LambdaSep WP.

parent f60f76e4
......@@ -7,4 +7,3 @@ LambdaSepCredits
LambdaSepRO
LambdaCF
LambdaCFCredits
ProofMode
......@@ -1186,10 +1186,10 @@ Qed.
*)
(* ---------------------------------------------------------------------- *)
(** Weakest precondition *)
(** Proof mode instances *)
Module WP.
Module ProofMode.
Export SepBasicTactics.ProofMode.
Definition wp (t:trm) (Q:val->hprop) : hprop :=
Hexists H, H \* \[triple t H Q].
......@@ -1202,4 +1202,13 @@ Proof using.
{ applys~ rule_consequence (rm M). xpull~. }
Qed.
End WP.
Instance triple_as_valid t H Q : AsValid (triple t H Q) (H - wp t Q).
Proof. rewrite /AsValid wp_equiv. apply as_valid. Qed.
Instance frame_wp p t R Φ Ψ :
( v, Frame p R (Φ v) (Ψ v)) Frame p R (wp t Φ) (wp t Ψ).
Proof.
rewrite /Frame /wp=> HR. iIntros "[HR H]". iDestruct "H" as (H) "[HH %]".
iExists (H ?p R)%I. iFrame. iPureIntro. eapply rule_frame_consequence=>//.
iIntros (?) "[??]". iApply HR. iFrame.
Qed.
End ProofMode.
......@@ -14,7 +14,7 @@ COQFLAGS:=-w -notation-overridden,-implicits-in-term
# Compilation.
# Note: double space below is important for export.sh
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder LambdaSepCredits LambdaCFCredits LambdaSepRO ExampleList ProofMode
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder LambdaSepCredits LambdaCFCredits LambdaSepRO ExampleList
# The official list of files that should be compiled by [make]
......
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.
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 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
hplainly 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 ??? ->%prop_ext.
- solve_proper.
- solve_proper.
- solve_proper.
- by intros ???? ->%fun_ext_1.
- by intros ???? ->%fun_ext_1.
- solve_proper.
- 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.
- auto.
- 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.
- 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.
......@@ -29,9 +29,9 @@ Contents of this file includes:
[xapply] apply the frame rule in a generic manner, and produce a
[is_local] subgoal as side-condition.
- [xlocal] automatically discharges goals of the form [is_local F].
- An instantiation of the Iris Proof Mode for CFML.
Author: Arthur Charguéraud.
Author: Arthur Charguéraud and Jacques-Henri Jourdan.
License: MIT.
*)
......@@ -40,6 +40,10 @@ 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.
Module SepLogicTactics (SL : SepLogicCore).
Module Export SS := SepLogicSetup SL.
......@@ -1929,6 +1933,186 @@ Tactic Notation "xunfolds" constr(E) :=
Tactic Notation "xunfolds" constr(E) "at" constr(n) :=
xunfold E at n; xunfolds_post tt.
(* ********************************************************************** *)
(* * Instantiating Iris Proof Mode *)
Module ProofMode.
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.
(* 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 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
hplainly 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 ??? ->%prop_ext.
- solve_proper.
- solve_proper.
- solve_proper.
- by intros ???? ->%fun_ext_1.
- by intros ???? ->%fun_ext_1.
- solve_proper.
- 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.
- auto.
- 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.
- 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 stdpp.base.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. 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. 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.
End ProofMode.
(* ---------------------------------------------------------------------- *)
......
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