A very simple separation logic canceler by reflection.

_CoqProject

@@ -51,6 +51,7 @@ algebra/excl.v
 algebra/iprod.v
 algebra/functor.v
 algebra/upred.v
+algebra/upred_tactics.v
 algebra/upred_big_op.v
 program_logic/model.v
 program_logic/adequacy.v

algebra/upred_tactics.v

+From algebra Require Export upred.
+From algebra Require Export upred_big_op.
+
+Module upred_reflection. Section upred_reflection.
+  Context {M : cmraT}.
+
+  Inductive expr :=
+    | ETrue : expr
+    | EVar : nat → expr
+    | ESep : expr → expr → expr.
+  Fixpoint eval (Σ : list (uPred M)) (e : expr) : uPred M :=
+    match e with
+    | ETrue => True
+    | EVar n => from_option True%I (Σ !! n)
+    | ESep e1 e2 => eval Σ e1 ★ eval Σ e2
+    end.
+  Fixpoint flatten (e : expr) : list nat :=
+    match e with
+    | ETrue => []
+    | EVar n => [n]
+    | ESep e1 e2 => flatten e1 ++ flatten e2
+    end.
+
+  Notation eval_list Σ l :=
+    (uPred_big_sep ((λ n, from_option True%I (Σ !! n)) <$> l)).
+  Lemma eval_flatten Σ e : eval Σ e ≡ eval_list Σ (flatten e).
+  Proof.
+    induction e as [| |e1 IH1 e2 IH2];
+      rewrite /= ?right_id ?fmap_app ?big_sep_app ?IH1 ?IH2 //. 
+  Qed.
+  Lemma flatten_entails Σ e1 e2 :
+    flatten e2 `contains` flatten e1 → eval Σ e1 ⊑ eval Σ e2.
+  Proof.
+    intros. rewrite !eval_flatten. by apply big_sep_contains, fmap_contains.
+  Qed.
+  Lemma flatten_equiv Σ e1 e2 :
+    flatten e2 ≡ₚ flatten e1 → eval Σ e1 ≡ eval Σ e2.
+  Proof. intros He. by rewrite !eval_flatten He. Qed.
+
+  Fixpoint prune (e : expr) : expr :=
+    match e with
+    | ETrue => ETrue
+    | EVar n => EVar n
+    | ESep e1 e2 =>
+       match prune e1, prune e2 with
+       | ETrue, e2' => e2'
+       | e1', ETrue => e1'
+       | e1', e2' => ESep e1' e2'
+       end
+    end.
+  Lemma flatten_prune e : flatten (prune e) = flatten e.
+  Proof.
+    induction e as [| |e1 IH1 e2 IH2]; simplify_eq/=; auto.
+    rewrite -IH1 -IH2. by repeat case_match; rewrite ?right_id_L.
+  Qed.
+  Lemma prune_correct Σ e : eval Σ (prune e) ≡ eval Σ e.
+  Proof. by rewrite !eval_flatten flatten_prune. Qed.
+
+  Fixpoint cancel_go (n : nat) (e : expr) : option expr :=
+    match e with
+    | ETrue => None
+    | EVar n' => if decide (n = n') then Some ETrue else None
+    | ESep e1 e2 => 
+       match cancel_go n e1 with
+       | Some e1' => Some (ESep e1' e2)
+       | None => ESep e1 <$> cancel_go n e2
+       end
+    end.
+  Definition cancel (n: nat) (e: expr) : option expr := prune <$> cancel_go n e.
+  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.
+  Qed.
+  Lemma flatten_cancel e e' n :
+    cancel n e = Some e' → flatten e ≡ₚ n :: flatten e'.
+  Proof.
+    rewrite /cancel fmap_Some=> -[e'' [? ->]].
+    by rewrite flatten_prune -flatten_cancel_go.
+  Qed.
+  Lemma cancel_entails Σ e1 e2 e1' e2' n :
+    cancel n e1 = Some e1' → cancel n 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.
+  Qed.
+
+  Class Quote (Σ1 Σ2 : list (uPred M)) (P : uPred M) (e : expr) := {}.
+  Global Instance quote_True Σ : Quote Σ Σ True ETrue.
+  Global Instance quote_var Σ1 Σ2 P i:
+    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).
+  End upred_reflection.
+
+  Ltac quote :=
+    match goal with
+    | |- ?P1 ⊑ ?P2 =>
+      lazymatch type of (_ : Quote [] _ P1 _) with Quote _ ?Σ2 _ ?e1 =>
+      lazymatch type of (_ : Quote Σ2 _ P2 _) with Quote _ ?Σ3 _ ?e2 =>
+        change (eval Σ3 e1 ⊑ eval Σ3 e2)
+      end end
+    end.
+End upred_reflection.
+
+Tactic Notation "cancel" constr(P) :=
+  let rec lookup Σ n :=
+    match Σ with
+    | P :: _ => n
+    | _ :: ?Σ => lookup Σ (S n)
+    end in
+  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]
+  end.

barrier/barrier.v

 From prelude Require Export functions.
-From algebra Require Export upred_big_op.
+From algebra Require Export upred_big_op upred_tactics.
 From program_logic Require Export sts saved_prop.
 From program_logic Require Import hoare.
 From heap_lang Require Export derived heap wp_tactics notation.
@@ -407,37 +407,30 @@ Section proof.
       rewrite left_id -later_intro {1 3}/barrier_inv.
       (* FIXME ssreflect rewrite fails if there are evars around. Also, this is very slow because we don't have a proof mode. *)
       rewrite -(waiting_split _ _ _ Q R1 R2); [|done..].
-      match goal with | |- _ ⊑ ?G => rewrite [G]lock end.
       rewrite {1}[saved_prop_own i1 _]always_sep_dup.
       rewrite {1}[saved_prop_own i2 _]always_sep_dup.
-      rewrite !assoc [(_ ★ _ i1 _)%I]comm.
-      rewrite !assoc [(_ ★ _ i _)%I]comm.
-      rewrite !assoc [(_ ★ (l ↦ _))%I]comm.
-      rewrite !assoc [(_ ★ (waiting _ _))%I]comm.
-      rewrite !assoc [(_ ★ (Q -★ _))%I]comm -!assoc 5!assoc.
-      unlock. apply sep_mono.
-      + (* This should really all be handled automatically. *)
-        rewrite !assoc [(_ ★ (l ↦ _))%I]comm -!assoc. apply sep_mono_r.
-        rewrite !assoc [(_ ★ _ i2 _)%I]comm -!assoc. apply sep_mono_r.
-        rewrite !assoc [(_ ★ _ i1 _)%I]comm -!assoc. apply sep_mono_r.
-        rewrite !assoc [(_ ★ _ i _)%I]comm -!assoc. apply sep_mono_r.
-        done.
-      + 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).
-        do 2 rewrite !(assoc (★)%I) [(_ ★ sts_ownS _ _ _)%I]comm.
-        rewrite -!assoc. rewrite [(sts_ownS _ _ _ ★ _ ★ _)%I]assoc -pvs_frame_r.
-        apply sep_mono.
-        * rewrite -sts_ownS_op; by eauto using sts_own_weaken with sts.
-        * rewrite const_equiv // !left_id.
-          rewrite {1}[heap_ctx _]always_sep_dup !assoc [(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
-          rewrite !assoc ![(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
-          rewrite {1}[sts_ctx _ _ _]always_sep_dup !assoc [(_ ★ sts_ctx _ _ _)%I]comm -!assoc. apply sep_mono_r.
-          rewrite !assoc ![(_ ★ sts_ctx _ _ _)%I]comm -!assoc. apply sep_mono_r.
-          rewrite comm. apply sep_mono_r. apply sep_intro_True_l.
-          { rewrite -later_intro. apply wand_intro_l. by rewrite right_id. }
-          apply sep_intro_True_r; first done.
-          { rewrite -later_intro. apply wand_intro_l. by rewrite right_id. }
+      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).
+      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).
+      do 2 rewrite !(assoc (★)%I) [(_ ★ sts_ownS _ _ _)%I]comm.
+      rewrite -!assoc. rewrite [(sts_ownS _ _ _ ★ _ ★ _)%I]assoc -pvs_frame_r.
+      apply sep_mono.
+      * rewrite -sts_ownS_op; by eauto using sts_own_weaken with sts.
+      * rewrite const_equiv // !left_id.
+        rewrite {1}[heap_ctx _]always_sep_dup !assoc [(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
+        rewrite !assoc ![(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
+        rewrite {1}[sts_ctx _ _ _]always_sep_dup !assoc [(_ ★ sts_ctx _ _ _)%I]comm -!assoc. apply sep_mono_r.
+        rewrite !assoc ![(_ ★ sts_ctx _ _ _)%I]comm -!assoc. apply sep_mono_r.
+        rewrite comm. apply sep_mono_r. apply sep_intro_True_l.
+        { rewrite -later_intro. apply wand_intro_l. by rewrite right_id. }
+        apply sep_intro_True_r; first done.
+        { rewrite -later_intro. apply wand_intro_l. by rewrite right_id. }
 (* Case II: High state. TODO: Lots of this script is just copy-n-paste of the previous one.
    Most of that is because the goals are fairly similar in structure, and the proof scripts
    are mostly concerned with manually managaing the structure (assoc, comm, dup) of
@@ -447,37 +440,30 @@ Section proof.
       rewrite const_equiv; last by eauto with sts.
       rewrite left_id -later_intro {1 3}/barrier_inv.
       rewrite -(ress_split _ _ _ Q R1 R2); [|done..].
-      match goal with | |- _ ⊑ ?G => rewrite [G]lock end.
       rewrite {1}[saved_prop_own i1 _]always_sep_dup.
       rewrite {1}[saved_prop_own i2 _]always_sep_dup.
-      rewrite !assoc [(_ ★ _ i1 _)%I]comm.
-      rewrite !assoc [(_ ★ _ i _)%I]comm.
-      rewrite !assoc [(_ ★ (l ↦ _))%I]comm.
-      rewrite !assoc [(_ ★ (ress _))%I]comm.
-      rewrite !assoc [(_ ★ (Q -★ _))%I]comm -!assoc 5!assoc.
-      unlock. apply sep_mono.
-      + (* This should really all be handled automatically. *)
-        rewrite !assoc [(_ ★ (l ↦ _))%I]comm -!assoc. apply sep_mono_r.
-        rewrite !assoc [(_ ★ _ i2 _)%I]comm -!assoc. apply sep_mono_r.
-        rewrite !assoc [(_ ★ _ i1 _)%I]comm -!assoc. apply sep_mono_r.
-        rewrite !assoc [(_ ★ _ i _)%I]comm -!assoc. apply sep_mono_r.
-        done.
-      + 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).
-        do 2 rewrite !(assoc (★)%I) [(_ ★ sts_ownS _ _ _)%I]comm.
-        rewrite -!assoc. rewrite [(sts_ownS _ _ _ ★ _ ★ _)%I]assoc -pvs_frame_r.
-        apply sep_mono.
-        * rewrite -sts_ownS_op; by eauto using sts_own_weaken with sts.
-        * rewrite const_equiv // !left_id.
-          rewrite {1}[heap_ctx _]always_sep_dup !assoc [(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
-          rewrite !assoc ![(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
-          rewrite {1}[sts_ctx _ _ _]always_sep_dup !assoc [(_ ★ sts_ctx _ _ _)%I]comm -!assoc. apply sep_mono_r.
-          rewrite !assoc ![(_ ★ sts_ctx _ _ _)%I]comm -!assoc. apply sep_mono_r.
-          rewrite comm. apply sep_mono_r. apply sep_intro_True_l.
-          { rewrite -later_intro. apply wand_intro_l. by rewrite right_id. }
-          apply sep_intro_True_r; first done.
-          { rewrite -later_intro. apply wand_intro_l. by rewrite right_id. }
+      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).
+      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).
+      do 2 rewrite !(assoc (★)%I) [(_ ★ sts_ownS _ _ _)%I]comm.
+      rewrite -!assoc. rewrite [(sts_ownS _ _ _ ★ _ ★ _)%I]assoc -pvs_frame_r.
+      apply sep_mono.
+      * rewrite -sts_ownS_op; by eauto using sts_own_weaken with sts.
+      * rewrite const_equiv // !left_id.
+        rewrite {1}[heap_ctx _]always_sep_dup !assoc [(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
+        rewrite !assoc ![(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
+        rewrite {1}[sts_ctx _ _ _]always_sep_dup !assoc [(_ ★ sts_ctx _ _ _)%I]comm -!assoc. apply sep_mono_r.
+        rewrite !assoc ![(_ ★ sts_ctx _ _ _)%I]comm -!assoc. apply sep_mono_r.
+        rewrite comm. apply sep_mono_r. apply sep_intro_True_l.
+        { rewrite -later_intro. apply wand_intro_l. by rewrite right_id. }
+        apply sep_intro_True_r; first done.
+        { rewrite -later_intro. apply wand_intro_l. by rewrite right_id. }
   Qed.
 
   Lemma recv_strengthen l P1 P2 :