Commit c55e52f9 authored by Robbert Krebbers's avatar Robbert Krebbers

Cancel a list of propositions.

I am now also using reification to obtain the indexes corresponding to
the stuff we want to cancel instead of relying on matching using Ltac.
parent 7ef8111b
Pipeline #97 passed with stage
......@@ -66,28 +66,30 @@ Module upred_reflection. Section upred_reflection.
| None => ESep e1 <$> cancel_go n e2
end
end.
Definition cancel (n: nat) (e: expr) : option expr := prune <$> cancel_go n e.
Definition cancel (ns : list nat) (e: expr) : option expr :=
prune <$> fold_right (mbind cancel_go) (Some e) ns.
Lemma flatten_cancel_go e e' n :
cancel_go n e = Some e' flatten e n :: flatten e'.
Proof.
revert e'; induction e as [| |e1 IH1 e2 IH2]; intros;
repeat (simplify_option_eq || case_match); auto.
* by rewrite IH1 //.
* by rewrite IH2 // Permutation_middle.
- by rewrite IH1 //.
- by rewrite IH2 // Permutation_middle.
Qed.
Lemma flatten_cancel e e' n :
cancel n e = Some e' flatten e n :: flatten e'.
Lemma flatten_cancel e e' ns :
cancel ns e = Some e' flatten e ns ++ flatten e'.
Proof.
rewrite /cancel fmap_Some=> -[e'' [? ->]].
by rewrite flatten_prune -flatten_cancel_go.
rewrite /cancel fmap_Some=> -[{e'}e' [He ->]]; rewrite flatten_prune.
revert e' He; induction ns as [|n ns IH]=> e' He; simplify_option_eq; auto.
rewrite Permutation_middle -flatten_cancel_go //; eauto.
Qed.
Lemma cancel_entails Σ e1 e2 e1' e2' n :
cancel n e1 = Some e1' cancel n e2 = Some e2'
Lemma cancel_entails Σ e1 e2 e1' e2' ns :
cancel ns e1 = Some e1' cancel ns e2 = Some e2'
eval Σ e1' eval Σ e2' eval Σ e1 eval Σ e2.
Proof.
intros ??. rewrite !eval_flatten.
rewrite (flatten_cancel e1 e1' n) // (flatten_cancel e2 e2' n) //; csimpl.
apply uPred.sep_mono_r.
rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl.
rewrite !fmap_app !big_sep_app. apply uPred.sep_mono_r.
Qed.
Class Quote (Σ1 Σ2 : list (uPred M)) (P : uPred M) (e : expr) := {}.
......@@ -96,6 +98,13 @@ Module upred_reflection. Section upred_reflection.
rlist.QuoteLookup Σ1 Σ2 P i Quote Σ1 Σ2 P (EVar i) | 1000.
Global Instance quote_sep Σ1 Σ2 Σ3 P1 P2 e1 e2 :
Quote Σ1 Σ2 P1 e1 Quote Σ2 Σ3 P2 e2 Quote Σ1 Σ3 (P1 P2) (ESep e1 e2).
Class QuoteArgs (Σ: list (uPred M)) (Ps: list (uPred M)) (ns: list nat) := {}.
Global Instance quote_args_nil Σ : QuoteArgs Σ nil nil.
Global Instance quote_args_cons Σ Ps P ns n :
rlist.QuoteLookup Σ Σ P n
QuoteArgs Σ Ps ns QuoteArgs Σ (P :: Ps) (n :: ns).
End upred_reflection.
Ltac quote :=
......@@ -108,16 +117,13 @@ Module upred_reflection. Section upred_reflection.
end.
End upred_reflection.
Tactic Notation "cancel" constr(P) :=
let rec lookup Σ n :=
match Σ with
| P :: _ => n
| _ :: ?Σ => lookup Σ (S n)
end in
Tactic Notation "cancel" constr(Ps) :=
upred_reflection.quote;
match goal with
| |- upred_reflection.eval ?Σ _ upred_reflection.eval _ _ =>
let n' := lookup Σ 0%nat in
eapply upred_reflection.cancel_entails with (n:=n');
[cbv; reflexivity|cbv; reflexivity|simpl]
lazymatch type of (_ : upred_reflection.QuoteArgs Σ Ps _) with
upred_reflection.QuoteArgs _ _ ?ns' =>
eapply upred_reflection.cancel_entails with (ns:=ns');
[cbv; reflexivity|cbv; reflexivity|simpl]
end
end.
......@@ -268,9 +268,9 @@ Section proof.
rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l.
apply exist_elim=>i.
trans (pvs (heap_ctx heapN (barrier_inv l P (State Low {[ i ]})) saved_prop_own i P)).
- rewrite -pvs_intro. cancel (heap_ctx heapN).
rewrite {1}[saved_prop_own _ _]always_sep_dup. cancel (saved_prop_own i P).
rewrite /barrier_inv /waiting -later_intro. cancel (l '0)%I.
- rewrite -pvs_intro. cancel [heap_ctx heapN].
rewrite {1}[saved_prop_own _ _]always_sep_dup. cancel [saved_prop_own i P].
rewrite /barrier_inv /waiting -later_intro. cancel [l '0]%I.
rewrite -(exist_intro (const P)) /=. rewrite -[saved_prop_own _ _](left_id True%I ()%I).
apply sep_mono.
+ rewrite -later_intro. apply wand_intro_l. rewrite right_id.
......@@ -316,7 +316,7 @@ Section proof.
apply const_elim_sep_l=>Hs. destruct p; last done.
rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep.
eapply wp_store with (v' := '0); eauto with I ndisj.
u_strip_later. cancel (l '0)%I.
u_strip_later. cancel [l '0]%I.
apply wand_intro_l. rewrite -(exist_intro (State High I)).
rewrite -(exist_intro ). rewrite const_equiv /=; last by eauto with sts.
rewrite left_id -later_intro {2}/barrier_inv -!assoc. apply sep_mono_r.
......@@ -418,12 +418,8 @@ Section proof.
rewrite -(waiting_split _ _ _ Q R1 R2); [|done..].
rewrite {1}[saved_prop_own i1 _]always_sep_dup.
rewrite {1}[saved_prop_own i2 _]always_sep_dup.
cancel (saved_prop_own i1 R1).
cancel (saved_prop_own i2 R2).
cancel (l '0)%I.
cancel (waiting P I).
cancel (Q - R1 R2)%I.
cancel (saved_prop_own i Q).
cancel [saved_prop_own i1 R1; saved_prop_own i2 R2; l '0;
waiting P I; Q - R1 R2; saved_prop_own i Q]%I.
apply wand_intro_l. rewrite !assoc. eapply pvs_wand_r. rewrite /recv.
rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R1) -(exist_intro i1).
rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R2) -(exist_intro i2).
......@@ -433,8 +429,9 @@ Section proof.
* rewrite -sts_ownS_op; by eauto using sts_own_weaken with sts.
* rewrite const_equiv // !left_id.
rewrite {1}[heap_ctx _]always_sep_dup {1}[sts_ctx _ _ _]always_sep_dup.
do 2 cancel (heap_ctx heapN). do 2 cancel (sts_ctx γ N (barrier_inv l P)).
cancel (saved_prop_own i1 R1). cancel (saved_prop_own i2 R2).
cancel [heap_ctx heapN; heap_ctx heapN;
sts_ctx γ N (barrier_inv l P); sts_ctx γ N (barrier_inv l P);
saved_prop_own i1 R1; saved_prop_own i2 R2].
apply sep_intro_True_l.
{ rewrite -later_intro. apply wand_intro_l. by rewrite right_id. }
rewrite -later_intro. apply wand_intro_l. by rewrite right_id.
......@@ -449,12 +446,8 @@ Section proof.
rewrite -(ress_split _ _ _ Q R1 R2); [|done..].
rewrite {1}[saved_prop_own i1 _]always_sep_dup.
rewrite {1}[saved_prop_own i2 _]always_sep_dup.
cancel (saved_prop_own i1 R1).
cancel (saved_prop_own i2 R2).
cancel (l '1)%I.
cancel (Q - R1 R2)%I.
cancel (saved_prop_own i Q).
cancel (ress I).
cancel [saved_prop_own i1 R1; saved_prop_own i2 R2; l '1;
Q - R1 R2; saved_prop_own i Q; ress I]%I.
apply wand_intro_l. rewrite !assoc. eapply pvs_wand_r. rewrite /recv.
rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R1) -(exist_intro i1).
rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R2) -(exist_intro i2).
......@@ -464,8 +457,9 @@ Section proof.
* rewrite -sts_ownS_op; by eauto using sts_own_weaken with sts.
* rewrite const_equiv // !left_id.
rewrite {1}[heap_ctx _]always_sep_dup {1}[sts_ctx _ _ _]always_sep_dup.
do 2 cancel (heap_ctx heapN). do 2 cancel (sts_ctx γ N (barrier_inv l P)).
cancel (saved_prop_own i1 R1). cancel (saved_prop_own i2 R2).
cancel [heap_ctx heapN; heap_ctx heapN;
sts_ctx γ N (barrier_inv l P); sts_ctx γ N (barrier_inv l P);
saved_prop_own i1 R1; saved_prop_own i2 R2]%I.
apply sep_intro_True_l.
{ rewrite -later_intro. apply wand_intro_l. by rewrite right_id. }
rewrite -later_intro. apply wand_intro_l. by rewrite right_id.
......@@ -493,7 +487,7 @@ Section spec.
Lemma barrier_spec (heapN N : namespace) :
heapN N
(recv send : loc -> iProp -n> iProp),
( P, heap_ctx heapN ({{ True }} newchan '() {{ λ v, l, v = LocV l recv l P send l P }}))
( P, heap_ctx heapN {{ True }} newchan '() {{ λ v, l, v = LocV l recv l P send l P }})
( l P, {{ send l P P }} signal (LocV l) {{ λ _, True }})
( l P, {{ recv l P }} wait (LocV l) {{ λ _, P }})
( l P Q, {{ recv l (P Q) }} Skip {{ λ _, recv l P recv l Q }})
......
......@@ -117,8 +117,7 @@ Section heap.
rewrite -(exist_intro (op {[ l := Excl v ]})).
repeat erewrite <-exist_intro by apply _; simpl.
rewrite -of_heap_insert left_id right_id.
(* FIXME: cancel (auth_own heap_name {[l := Excl v]} -★ Φ (LocV l))%I. *)
rewrite !assoc. apply sep_mono_l.
cancel [auth_own heap_name {[l := Excl v]} - Φ (LocV l)]%I.
rewrite -(map_insert_singleton_op h); last by apply of_heap_None.
rewrite const_equiv ?left_id; last by apply (map_insert_valid h).
apply later_intro.
......
......@@ -56,8 +56,8 @@ Section auth.
rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
trans ( auth_inv γ φ auth_own γ a)%I.
{ rewrite /auth_inv -(exist_intro a) later_sep.
rewrite const_equiv // left_id. cancel ( φ a)%I.
rewrite -later_intro /auth_own -own_op auth_both_op. done. }
rewrite const_equiv // left_id. cancel [ φ a]%I.
by rewrite -later_intro /auth_own -own_op auth_both_op. }
rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
by rewrite always_and_sep_l.
Qed.
......
......@@ -85,7 +85,7 @@ Section sts.
rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
trans ( sts_inv γ φ sts_own γ s ( sts.tok s))%I.
{ rewrite /sts_inv -(exist_intro s) later_sep.
cancel ( φ s)%I.
cancel [ φ s]%I.
by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. }
rewrite (inv_alloc N) /sts_ctx pvs_frame_r.
by rewrite always_and_sep_l.
......
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