Commit 8f523096 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Make ProofMode tactics work in RO mode.

Generalization of xpull in the case of RO triples, which are not local.
ram_apply locks the intermediate assertion if the post-condition is an evar.
use rule_seq instead of rule_seq' in ExampleListProofMode.
parent 0e67038d
......@@ -67,8 +67,8 @@ Lemma MCell_hstar_MCell_inv : forall p1 p2 x1 x2 y1 y2,
MCell x1 y1 p1 \* MCell x2 y2 p2 ==+> \[p1 <> p2].
Proof using.
intros. do 2 rewrite MCell_eq. tests C: (p1 = p2).
{ iClean. iIntros. iDestruct (hstar_hfield_same_loc_disjoint with "[$]") as %[]. }
{ iClean. auto with iFrame. }
{ iPrepare. iIntros. iDestruct (hstar_hfield_same_loc_disjoint with "[$]") as %[]. }
{ iPrepare. auto with iFrame. }
Qed.
......@@ -112,7 +112,7 @@ Lemma rule_set_hd : forall p v' v vq,
(MCell v' vq p)
(fun r => \[r = val_unit] \* MCell v vq p).
Proof using.
intros. unfold MCell. ram_apply rule_set_field. auto with iFrame.
intros. unfold MCell. ram_apply rule_set_field. auto with iFrame.
Qed.
Hint Extern 1 (Register_spec val_set_hd) => Provide rule_set_hd.
......@@ -174,9 +174,10 @@ Lemma rule_new_cell' : forall v q,
Proof using.
intros. eapply rule_app_fun2 =>//=; [].
eapply rule_let; [apply rule_alloc_cell|]=>p /=. xpull=> p' v' q' ->.
eapply rule_seq'. { rewrite MCell_eq. ram_apply rule_set_hd. auto with iFrame. }
eapply rule_seq'. { ram_apply rule_set_tl. auto with iFrame. }
eapply rule_val. auto with iFrame.
eapply rule_seq; last admit.
{ rewrite MCell_eq. ram_apply rule_set_hd. auto with iFrame. }
unlock. eapply rule_seq; last admit. { ram_apply rule_set_tl. auto with iFrame. }
unlock. eapply rule_val. iPrepare. auto with iFrame.
Qed.
Hint Extern 1 (Register_spec val_new_cell) => Provide rule_new_cell.
......@@ -304,18 +305,18 @@ Proof using.
intros L. induction_wf: list_sub_wf L. intros p.
applys rule_app_fix=>//=. applys rule_if'.
- ram_apply rule_neq. auto with iFrame.
- xpull=>[= Hp]. rewrite true_eq_isTrue_eq in Hp.
- unlock. xpull=>[= Hp]. rewrite true_eq_isTrue_eq in Hp.
xchange (MList_not_null_inv_cons p); [by auto|]. xpull=>p' x L' ?. subst.
applys rule_let. { ram_apply rule_get_tl. iIntros "?$%??". iAccu. }
move=> q /=. xpull=>->.
applys rule_let. { ram_apply (IH L'); [done|]. iIntros "?$%??". iAccu. }
move=> n /=. xpull=>->. ram_apply rule_add.
iIntros "??%->". iSplitR.
applys rule_let. { ram_apply rule_get_tl. auto with iFrame. }
unlock. move=> q /=. xpull=>->.
applys rule_let. { ram_apply (IH L'); [done|]. auto with iFrame. }
unlock. move=> n /=. xpull=>->. ram_apply rule_add.
iIntros "??" (?) "->". iSplitR.
{ iPureIntro. f_equal. math. } { iApply MList_cons. iFrame. }
- eapply rule_val. iClean. iIntros "HL" ([= Hp]). revert Hp.
- unlock. eapply rule_val. iPrepare. iIntros "HL" ([= Hp]). revert Hp.
rewrite false_eq_isTrue_eq=>/not_not_inv. intros [= ->].
iDestruct (MList_null_inv with "HL") as "[$ ->]". auto.
- iIntros ([] Hb) "[? %]"=>//. destruct Hb. eexists _. auto.
- unlock. iIntros ([] Hb) "[? %]"=>//. destruct Hb. eexists _. auto.
Qed.
(* ********************************************************************** *)
......@@ -344,33 +345,34 @@ Lemma rule_mlist_length_loop : forall L p,
Proof using.
intros L p. eapply rule_app_fun=>//=.
applys rule_let. { ram_apply rule_ref. auto with iFrame. }
move=> ? /=. xpull=>r ->.
unlock. move=> ? /=. xpull=>r ->.
applys rule_let. { ram_apply rule_ref. auto with iFrame. }
move=> ? /=. xpull=>n ->. applys rule_seq'.
unlock. move=> ? /=. xpull=>n ->. applys rule_seq; last admit.
- applys rule_while=>t R.
cuts K: (forall (nacc:int),
triple t (n ~~~> nacc \* MList L p \* r ~~~> p)
(λ r0 : val, \[r0 = '()] \* n ~~~> (nacc + length L)%Z \* MList L p)).
{ ram_apply K. auto with iFrame. }
gen p. induction_wf: list_sub_wf L=>p nacc. apply R. applys rule_if'.
+ eapply rule_let. ram_apply rule_get. { iIntros "??$ % ??". iAccu. }
move=>pp /=. xpull=>->. ram_apply rule_neq. eauto with iFrame.
+ xpull. intros [=Hp]. rewrite true_eq_isTrue_eq in Hp.
xchange (MList_not_null_inv_cons p); [by auto|iClean; auto with iFrame|].
xpull=>p' x L' ?. subst. applys rule_seq'.
* applys rule_seq'. { ram_apply rule_incr. auto with iFrame. }
eapply rule_let. { ram_apply rule_get. iIntros "$???%??". iAccu. }
xpull=>? -> /=. eapply rule_let.
{ ram_apply rule_get_tl. iIntros "??$?%??". iAccu. }
move=>? /=. xpull=>->. ram_apply rule_set. auto with iFrame.
* ram_apply (IH L'); [done|]. iIntros. iFrame. iIntros (?) "$ Hn ?". iSplitL "Hn".
+ eapply rule_let. ram_apply rule_get. { auto with iFrame. }
unlock. move=>pp /=. xpull=>->. ram_apply rule_neq. eauto with iFrame.
+ unlock. xpull. intros [=Hp]. rewrite true_eq_isTrue_eq in Hp.
xchange (MList_not_null_inv_cons p); [by auto|iPrepare; auto with iFrame|].
xpull=>p' x L' ?. subst. applys rule_seq; last admit.
* applys rule_seq; last admit. { ram_apply rule_incr. auto with iFrame. }
unlock. eapply rule_let. { ram_apply rule_get. auto with iFrame. }
unlock. xpull=>? -> /=. eapply rule_let.
{ ram_apply rule_get_tl. auto with iFrame. }
unlock. move=>? /=. xpull=>->. ram_apply rule_set. auto with iFrame.
* unlock. ram_apply (IH L'); [done|]. iIntros. iFrame.
iIntros (?) "$ Hn ?". iSplitL "Hn".
-- by math_rewrite ((nacc + 1) + length L' = nacc + S (length (L')))%Z.
-- iApply MList_cons. iFrame.
+ iApply rule_val_htop. iClean. iIntros "? HL ?" ([= Hp]).
+ unlock. iApply rule_val_htop. iPrepare. iIntros "? HL ?" ([= Hp]).
revert Hp. rewrite false_eq_isTrue_eq. intros [= ->]%not_not_inv.
iDestruct (MList_null_inv with "HL") as "[$ ->]". rewrite plus_zero_r. by iFrame.
+ iIntros ([] Hb) "(? & ? & ? & %)"=>//. destruct Hb. eexists _. auto.
- apply rule_htop_post. ram_apply rule_get. auto with iFrame.
+ unlock. iIntros ([] Hb) "(? & ? & ? & %)"=>//. destruct Hb. eexists _. auto.
- unlock. apply rule_htop_post. ram_apply rule_get. auto with iFrame.
Qed.
(* ********************************************************************** *)
......
......@@ -47,7 +47,7 @@ Lemma RO_himpl_RO_hstar_RO : forall H,
RO H ==> (RO H \* RO H).
Proof using. intros. applys RO_duplicatable. Qed.
Lemma rule_xchange : forall (H1 H1':hprop), H1 ==> H1' ->
Lemma rule_xchange : forall (H1 H1':hprop), H1 ==> H1' ->
forall t H H2 Q,
H ==> H1 \* H2 ->
triple t (H1' \* H2) Q ->
......@@ -59,7 +59,7 @@ Qed.
Lemma rule_frame_read_only_conseq : forall t H1 Q1 H2 H Q,
H ==> (H1 \* H2) ->
normal H1 ->
Normal H1 ->
triple t (RO H1 \* H2) Q1 ->
(Q1 \*+ H1) ===> Q ->
triple t H Q.
......@@ -71,12 +71,12 @@ Qed.
Lemma rule_get : forall v l,
triple (val_get (val_loc l))
triple (val_get (val_loc l))
(l ~~~> v)
(fun x => \[x = v] \* l ~~~> v).
Proof using.
intros. applys rule_frame_read_only_conseq (l ~~~> v).
{ hsimpl. } { applys normal_hsingle. (* todo: normal_hsingle? *) }
intros. applys rule_frame_read_only_conseq (l ~~~> v).
{ hsimpl. } { apply _. }
{ rew_heap. applys rule_get_ro. }
{ auto. }
Qed.
......@@ -90,7 +90,7 @@ Proof using. introv WP M1 M2. applys* rule_consequence WP. applys* rule_let. Qed
Lemma rule_frame : forall t H1 Q1 H2,
triple t H1 Q1 ->
normal H2 ->
Normal H2 ->
triple t (H1 \* H2) (Q1 \*+ H2).
Proof using.
introv M N. applys~ rule_frame_read_only.
......@@ -100,13 +100,13 @@ Qed.
Lemma rule_frame_conseq : forall t H1 Q1 H2 H Q,
H ==> H2 \* H1 ->
normal H1 ->
Normal H1 ->
triple t H2 Q1 ->
Q1 \*+ H1 ===> Q ->
triple t H Q.
Proof using. intros. applys* rule_consequence. applys* rule_frame. Qed.
Hint Resolve normal_hsingle.
Hint Resolve Normal_hsingle.
......@@ -175,7 +175,7 @@ Definition val_ref_update :=
val_set 'p 'y.
Lemma rule_ref_update : forall (f:val) (p:loc) (v:val) (H:hprop) (Q:val->hprop),
normal_post Q -> (* todo: this might not be needed if using "normally" *)
Normal_post Q -> (* todo: this might not be needed if using "normally" *)
(triple (f v)
PRE (RO(p ~~~> v) \* H)
POST Q)
......@@ -185,13 +185,13 @@ Lemma rule_ref_update : forall (f:val) (p:loc) (v:val) (H:hprop) (Q:val->hprop),
POST (fun r => \[r = val_unit] \* Hexists w, (p ~~~> w) \* (Q w))).
Proof using.
introv N M.
rew_nary; rew_vals_to_trms; applys rule_apps_funs;
rew_nary; rew_vals_to_trms; applys rule_apps_funs;
[unfold val_ref_update; rew_nary; reflexivity| auto | simpl].
applys rule_let.
{ applys rule_get. }
{ intros x; simpl; rew_heap. applys rule_extract_hprop ;=> E; subst x.
applys rule_let' \[]. { hsimpl. }
applys~ rule_frame_read_only_conseq (p ~~~> v).
applys~ rule_frame_read_only_conseq (p ~~~> v).
{ hsimpl. } { rew_heap. applys M. } { hsimpl. }
{ intros y; simpl; rew_heap. clear M.
applys~ rule_frame_conseq (Q y). hsimpl.
......
(**
This file formalizes example in Separation Logic with read-only predicates
Author: Arthur Charguéraud.
License: MIT.
*)
Set Implicit Arguments.
From Sep Require Import LambdaSepRO.
Import ProofMode.
Generalizable Variables A B.
Open Scope trm_scope.
Ltac auto_star ::= jauto.
Implicit Types p q : loc.
Implicit Types n : int.
Implicit Types v : val.
(* To move and factorize *)
Notation "F 'PRE' H 'POST' Q" :=
(F H Q)
(at level 69, only parsing) : heap_scope.
(* todo move *)
Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q,
F = (val_funs xs t1) ->
var_funs (LibList.length Vs) xs ->
triple (substs xs Vs t1) H Q ->
triple (trm_apps F Vs) H Q.
Proof using.
introv E N M. intros h1 h2 D H1.
forwards~ (h1'&v&N1&N2&N3&N4): (rm M) h2 H1.
exists h1' v. splits~. { subst. applys~ red_app_funs_val. }
Qed.
Lemma var_funs_exec_elim : forall (n:nat) xs,
var_funs_exec n xs -> (var_funs n xs).
Proof using. introv M. rewrite var_funs_exec_eq in M. rew_istrue~ in M. Qed.
Hint Resolve var_funs_exec_elim.
(* ********************************************************************** *)
(* * Formalisation of higher-order iterator on a reference *)
(* ---------------------------------------------------------------------- *)
(** Apply a function to the contents of a reference *)
Definition val_ref_apply :=
ValFun 'f 'p :=
Let 'x := val_get 'p in
'f 'x.
Lemma rule_ref_apply : forall (f:val) (p:loc) (v:val) (H:hprop) (Q:val->hprop),
(triple (f v)
PRE (RO(p ~~~> v) \* H)
POST Q)
->
(triple (val_ref_apply f p)
PRE (RO(p ~~~> v) \* H)
POST Q).
Proof using.
introv M.
rew_nary; rew_vals_to_trms; applys rule_apps_funs;
[unfold val_ref_apply; rew_nary; reflexivity| auto | simpl].
ram_apply_let rule_get_ro. { auto with iFrame. }
move=>X /=. unlock. xpull=>->. done.
Qed.
(* ---------------------------------------------------------------------- *)
(** In-place update of a reference by applying a function *)
Definition val_ref_update :=
ValFun 'f 'p :=
Let 'x := val_get 'p in
Let 'y := 'f 'x in
val_set 'p 'y.
Lemma rule_ref_update : forall (f:val) (p:loc) (v:val) (H:hprop) (Q:val->hprop),
Normal_post Q -> (* todo: this might not be needed if using "normally" *)
(triple (f v)
PRE (RO(p ~~~> v) \* H)
POST Q)
->
(triple (val_ref_update f p)
PRE (p ~~~> v \* H)
POST (fun r => \[r = val_unit] \* Hexists w, (p ~~~> w) \* (Q w))).
Proof using.
introv N M.
rew_nary; rew_vals_to_trms; applys rule_apps_funs;
[unfold val_ref_update; rew_nary; reflexivity| auto | simpl].
ram_apply_let rule_get_ro. { auto with iFrame. }
unlock. move=>x /=. xpull=>->. ram_apply_let M. { auto with iFrame. }
unlock. move=>y /=. ram_apply rule_set. { auto 10 with iFrame. }
Qed.
This diff is collapsed.
......@@ -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 LambdaSepCredits LambdaSepRO LambdaCFTactics LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder ExampleList LambdaCFCredits ExampleRO ExampleListProofMode
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaSepCredits LambdaSepRO LambdaCFTactics LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder ExampleList LambdaCFCredits ExampleRO ExampleROProofMode ExampleListProofMode
# LambdaCFRO
......
......@@ -1739,7 +1739,7 @@ Ltac xpull_check tt :=
(** Lemmas *)
Lemma xpull_start : forall B (F:~~B) H Q,
is_local F -> F (\[] \* H) Q -> F H Q.
F (\[] \* H) Q -> F H Q.
Proof using. intros. rew_heap in *. auto. Qed.
Lemma xpull_keep : forall B (F:~~B) H1 H2 H3 Q,
......@@ -1755,7 +1755,7 @@ Lemma xpull_starify : forall B (F:~~B) H1 H2 Q,
Proof using. intros. rew_heap in *. auto. Qed.
Lemma xpull_empty : forall B (F:~~B) H1 H2 Q,
is_local F -> (F (H1 \* H2) Q) -> F (H1 \* (\[] \* H2)) Q.
(F (H1 \* H2) Q) -> F (H1 \* (\[] \* H2)) Q.
Proof using. intros. rew_heap. auto. Qed.
Lemma xpull_hprop : forall B (F:~~B) H1 H2 P Q,
......@@ -1783,7 +1783,7 @@ Ltac xpull_setup tt :=
try match goal with |- ?H ==> ?H' =>
fail 100 "you should call hpull, not xpull" end;
ProofModeInstantiate.unfold_proofmode;
apply xpull_start; [ try xlocal | ].
apply xpull_start.
Ltac xpull_post_processing_for_hyp H :=
idtac.
......@@ -1792,16 +1792,23 @@ Ltac xpull_cleanup tt :=
remove_empty_heaps_formula tt;
gen_until_mark_with_processing ltac:(xpull_post_processing_for_hyp).
Ltac xpull_hprop tt :=
apply xpull_hprop; [ try xlocal | intro ].
Ltac xpull_hexists tt :=
apply xpull_hexists; [ try xlocal | intro ].
Ltac xpull_id tt :=
apply xpull_id; [ try xlocal | intro ].
Ltac xpull_step tt :=
let go HP :=
match HP with _ \* ?HN =>
match HN with
| ?H \* _ =>
match H with
| \[] => apply xpull_empty; try xlocal
| \[_] => apply xpull_hprop; [ try xlocal | intro ]
| hexists _ => apply xpull_hexists; [ try xlocal | intro ]
| _ ~> Id _ => apply xpull_id; [ try xlocal | intro ]
| \[] => apply xpull_empty
| \[_] => xpull_hprop tt
| hexists _ => xpull_hexists tt
| _ ~> Id _ => xpull_id tt
| _ \* _ => apply xpull_assoc
| _ => apply xpull_keep
end
......@@ -2293,7 +2300,7 @@ Proof.
rewrite /FromPure /Frame=><- /=. destruct p=>/=; iIntros "[% _] !%"; auto.
Qed.
(** [PrepareHProp] / [iClean] tactic. *)
(** [PrepareHProp] / [iPrepare] tactic. *)
Class PrepareHProp (P Q : hprop) := prepare_hprop_eq : P = Q.
Hint Mode PrepareHProp ! - : typeclass_instances.
......@@ -2364,18 +2371,38 @@ Hint Extern 1 (PrepareHProp (_ \* emp%I)%I _) =>
Hint Extern 1 (PrepareHProp (_ emp) _) =>
simple apply prepare_hprop_hstar_hemp : typeclass_instances.
Lemma tac_clean Δ (P Q : hprop) :
Lemma tac_prepare Δ (P Q : hprop) :
PrepareHProp P Q
envs_entails Δ Q
envs_entails Δ P.
Proof. by rewrite /PrepareHProp=>->. Qed.
Ltac iClean :=
Ltac iPrepare :=
iStartProof;
eapply tac_clean; [apply _|cbv beta].
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 :=
eapply local_ramified_frame; [xlocal|eapply lem|iClean].
lazymatch goal with
| |- ?F _ ?Q =>
(is_evar Q; eapply local_ramified_frame_locked) ||
eapply local_ramified_frame
end; [xlocal|eapply lem|iPrepare].
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