Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

algebra/upred_tactics.v

@@ -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.

barrier/barrier.v

@@ -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 }}) ∧

heap_lang/heap.v

@@ -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.

program_logic/auth.v

@@ -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.

program_logic/model.v

@@ -31,11 +31,11 @@ End iProp.
 
 (* Solution *)
 Definition iPreProp (Λ : language) (Σ : iFunctor) : cofeT := iProp.result Λ Σ.
-Notation iRes Λ Σ := (res Λ Σ (laterC (iPreProp Λ Σ))).
-Notation iResRA Λ Σ := (resRA Λ Σ (laterC (iPreProp Λ Σ))).
-Notation iWld Λ Σ := (mapRA positive (agreeRA (laterC (iPreProp Λ Σ)))).
-Notation iPst Λ := (exclRA (istateC Λ)).
-Notation iGst Λ Σ := (ifunctor_car Σ (laterC (iPreProp Λ Σ))).
+Definition iRes Λ Σ := res Λ Σ (laterC (iPreProp Λ Σ)).
+Definition iResRA Λ Σ := resRA Λ Σ (laterC (iPreProp Λ Σ)).
+Definition iWld Λ Σ := mapRA positive (agreeRA (laterC (iPreProp Λ Σ))).
+Definition iPst Λ := exclRA (istateC Λ).
+Definition iGst Λ Σ := ifunctor_car Σ (laterC (iPreProp Λ Σ)).
 Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResRA Λ Σ).
 Definition iProp_unfold {Λ Σ} : iProp Λ Σ -n> iPreProp Λ Σ := solution_fold _.
 Definition iProp_fold {Λ Σ} : iPreProp Λ Σ -n> iProp Λ Σ := solution_unfold _.

program_logic/sts.v

@@ -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.