Retry "Let iLöb automatically revert and introduce spatial hypotheses."

algebra/upred.v

@@ -796,6 +796,12 @@ Proof.
 Qed.
 Lemma entails_wand P Q : (P ⊢ Q) → True ⊢ (P -★ Q).
 Proof. auto using wand_intro_l. Qed.
+Lemma wand_curry P Q R : (P -★ Q -★ R) ⊣⊢ (P ★ Q -★ R).
+Proof.
+  apply (anti_symm _).
+  - apply wand_intro_l. by rewrite (comm _ P) -assoc !wand_elim_r.
+  - do 2 apply wand_intro_l. by rewrite assoc (comm _ Q) wand_elim_r.
+Qed.
 
 Lemma sep_and P Q : (P ★ Q) ⊢ (P ∧ Q).
 Proof. auto. Qed.

heap_lang/lib/barrier/proof.v

@@ -140,7 +140,7 @@ Lemma wait_spec l P (Φ : val → iProp) :
 Proof.
   rename P into R; rewrite /recv /barrier_ctx.
   iIntros "[Hr HΦ]"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
-  iLöb "Hγ HQR HΦ" as "IH". wp_rec. wp_focus (! _)%E.
+  iLöb as "IH". wp_rec. wp_focus (! _)%E.
   iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]".
   wp_load. destruct p.
   - (* a Low state. The comparison fails, and we recurse. *)

heap_lang/lib/spawn.v

@@ -75,7 +75,7 @@ Lemma join_spec (Ψ : val → iProp) l (Φ : val → iProp) :
   (join_handle l Ψ ★ ∀ v, Ψ v -★ Φ v) ⊢ WP join (%l) {{ Φ }}.
 Proof.
   rewrite /join_handle; iIntros "[[% H] Hv]"; iDestruct "H" as {γ} "(#?&Hγ&#?)".
-  iLöb "Hγ Hv" as "IH". wp_rec. wp_focus (! _)%E.
+  iLöb as "IH". wp_rec. wp_focus (! _)%E.
   iInv N as "Hinv"; iDestruct "Hinv" as {v} "[Hl Hinv]".
   wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
   - iSplitL "Hl"; [iNext; iExists _; iFrame "Hl"; by iLeft|].

proofmode/coq_tactics.v

@@ -85,6 +85,9 @@ Definition envs_split {M}
 Definition envs_persistent {M} (Δ : envs M) :=
   if env_spatial Δ is Enil then true else false.
 
+Definition envs_clear_spatial {M} (Δ : envs M) : envs M :=
+  Envs (env_persistent Δ) Enil.
+
 (* Coq versions of the tactics *)
 Section tactics.
 Context {M : cmraT}.
@@ -92,6 +95,10 @@ Implicit Types Γ : env (uPred M).
 Implicit Types Δ : envs M.
 Implicit Types P Q : uPred M.
 
+Lemma of_envs_def Δ :
+  of_envs Δ = (■ envs_wf Δ ★ □ Π∧ env_persistent Δ ★ Π★ env_spatial Δ)%I.
+Proof. done. Qed.
+
 Lemma envs_lookup_delete_Some Δ Δ' i p P :
   envs_lookup_delete i Δ = Some (p,P,Δ')
   ↔ envs_lookup i Δ = Some (p,P) ∧ Δ' = envs_delete i p Δ.
@@ -227,9 +234,23 @@ Proof.
       env_split_fresh_1, env_split_fresh_2.
 Qed.
 
-Lemma env_special_nil_persistent Δ : envs_persistent Δ = true → PersistentP Δ.
+Lemma envs_clear_spatial_sound Δ :
+  Δ ⊢ (envs_clear_spatial Δ ★ Π★ env_spatial Δ)%I.
+Proof.
+  rewrite /of_envs /envs_clear_spatial /=; apply const_elim_sep_l=> Hwf.
+  rewrite right_id -assoc; apply sep_intro_True_l; [apply const_intro|done].
+  destruct Hwf; constructor; simpl; auto using Enil_wf.
+Qed.
+
+Lemma env_fold_wand Γ Q : env_fold uPred_wand Q Γ ⊣⊢ (Π★ Γ -★ Q).
+Proof.
+  revert Q; induction Γ as [|Γ IH i P]=> Q /=; [by rewrite wand_True|].
+  by rewrite IH wand_curry (comm uPred_sep).
+Qed.
+
+Lemma envs_persistent_persistent Δ : envs_persistent Δ = true → PersistentP Δ.
 Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
-Hint Immediate env_special_nil_persistent : typeclass_instances.
+Hint Immediate envs_persistent_persistent : typeclass_instances.
 
 (** * Adequacy *)
 Lemma tac_adequate P : Envs Enil Enil ⊢ P → True ⊢ P.
@@ -253,9 +274,9 @@ Qed.
 Lemma tac_clear Δ Δ' i p P Q :
   envs_lookup_delete i Δ = Some (p,P,Δ') → Δ' ⊢ Q → Δ ⊢ Q.
 Proof. intros. by rewrite envs_lookup_delete_sound // sep_elim_r. Qed.
-Lemma tac_clear_spatial Δ Δ1 Δ2 Q :
-  envs_split true [] Δ = Some (Δ1,Δ2) → Δ1 ⊢ Q → Δ ⊢ Q.
-Proof. intros. by rewrite envs_split_sound // sep_elim_l. Qed.
+Lemma tac_clear_spatial Δ Δ' Q :
+  envs_clear_spatial Δ = Δ' → Δ' ⊢ Q → Δ ⊢ Q.
+Proof. intros <- ?. by rewrite envs_clear_spatial_sound // sep_elim_l. Qed.
 
 Lemma tac_duplicate Δ Δ' i p j P Q :
   envs_lookup i Δ = Some (p, P) →
@@ -333,10 +354,10 @@ Lemma tac_löb Δ Δ' i Q :
   envs_app true (Esnoc Enil i (▷ Q)%I) Δ = Some Δ' →
   Δ' ⊢ Q → Δ ⊢ Q.
 Proof.
-  intros ?? HQ. rewrite (persistentP Δ) envs_app_sound //; simpl.
-  rewrite right_id -{2}(always_elim Q) -(löb (□ Q)); apply impl_intro_l.
-  rewrite -always_later -{1}(always_always (□ (▷ Q))) always_and_sep_l'.
-  by rewrite -always_sep wand_elim_r HQ.
+  intros ?? HQ. rewrite -(always_elim Q) -(löb (□ Q)) -always_later.
+  apply impl_intro_l, (always_intro _ _).
+  rewrite envs_app_sound //; simpl.
+  by rewrite right_id always_and_sep_l' wand_elim_r HQ.
 Qed.
 
 (** * Always *)
@@ -502,6 +523,12 @@ Proof.
   - by rewrite HQ wand_elim_r.
 Qed.
 
+Lemma tac_revert_spatial Δ Q :
+  envs_clear_spatial Δ ⊢ (env_fold uPred_wand Q (env_spatial Δ)) → Δ ⊢ Q.
+Proof.
+  intros HΔ. by rewrite envs_clear_spatial_sound HΔ env_fold_wand wand_elim_l.
+Qed.
+
 Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q :
   envs_split lr js Δ = Some (Δ1,Δ2) →
   envs_app (envs_persistent Δ1) (Esnoc Enil j P) Δ2 = Some Δ2' →

proofmode/environments.v

@@ -28,9 +28,18 @@ Inductive env_wf {A} : env A → Prop :=
 Fixpoint env_to_list {A} (E : env A) : list A :=
   match E with Enil => [] | Esnoc Γ _ x => x :: env_to_list Γ end.
 Coercion env_to_list : env >-> list.
+
 Instance env_dom {A} : Dom (env A) stringset :=
   fix go Γ := let _ : Dom _ _ := @go in
   match Γ with Enil => ∅ | Esnoc Γ i _ => {[ i ]} ∪ dom stringset Γ end.
+Fixpoint env_dom_list {A} (Γ : env A) : list string :=
+  match Γ with Enil => [] | Esnoc Γ i _ => i :: env_dom_list Γ end.
+
+Fixpoint env_fold {A B} (f : B → A → A) (x : A) (Γ : env B) : A :=
+  match Γ with
+  | Enil => x
+  | Esnoc Γ _ y => env_fold f (f y x) Γ
+  end.
 
 Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
   match Γapp with

proofmode/intro_patterns.v

@@ -118,15 +118,21 @@ Definition parse (s : string) : option (list intro_pat) :=
 Ltac parse s :=
   lazymatch type of s with
   | list intro_pat => s
-  | string => lazymatch eval vm_compute in (parse s) with
-              | Some ?pats => pats | _ => fail "invalid list intro_pat" s
-              end
+  | list string =>
+     lazymatch eval vm_compute in (mjoin <$> mapM parse s) with
+     | Some ?pats => pats | _ => fail "invalid list intro_pat" s
+     end
+  | string =>
+     lazymatch eval vm_compute in (parse s) with
+     | Some ?pats => pats | _ => fail "invalid list intro_pat" s
+     end
   end.
 Ltac parse_one s :=
   lazymatch type of s with
   | intro_pat => s
-  | string => lazymatch eval vm_compute in (parse s) with
-              | Some [?pat] => pat | _ => fail "invalid intro_pat" s
-              end
+  | string =>
+     lazymatch eval vm_compute in (parse s) with
+     | Some [?pat] => pat | _ => fail "invalid intro_pat" s
+     end
   end.
 End intro_pat.

proofmode/pviewshifts.v

@@ -81,7 +81,6 @@ Proof.
   eauto using tac_pvs_timeless.
 Qed.
 
-Hint Immediate env_special_nil_persistent : typeclass_instances.
 Lemma tac_pvs_assert {A} (fsa : FSA Λ Σ A) fsaV Δ Δ1 Δ2 Δ2' E lr js j P Q Φ :
   FSASplit Q E fsa fsaV Φ →
   envs_split lr js Δ = Some (Δ1,Δ2) →

proofmode/tactics.v

@@ -4,7 +4,7 @@ From iris.proofmode Require Export notation.
 From iris.prelude Require Import stringmap.
 
 Declare Reduction env_cbv := cbv [
-  env_lookup env_lookup_delete env_delete env_app
+  env_lookup env_fold env_lookup_delete env_delete env_app
     env_replace env_split_go env_split
   decide (* operational classes *)
   sumbool_rec sumbool_rect (* sumbool *)
@@ -13,7 +13,7 @@ Declare Reduction env_cbv := cbv [
   string_eq_dec string_rec string_rect (* strings *)
   env_persistent env_spatial envs_persistent
   envs_lookup envs_lookup_delete envs_delete envs_app
-    envs_simple_replace envs_replace envs_split].
+    envs_simple_replace envs_replace envs_split envs_clear_spatial].
 Ltac env_cbv :=
   match goal with |- ?u => let v := eval env_cbv in u in change v end.
 
@@ -365,6 +365,8 @@ Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2)
   iSpecialize H { x1 x2 x3 x4 x5 x6 x7 x8 }; last iApply H Hs.
 
 (** * Revert *)
+Tactic Notation "iRevert" "★" := eapply tac_revert_spatial; env_cbv.
+
 Tactic Notation "iForallRevert" ident(x) :=
   match type of x with
   | _ : Prop => revert x; apply tac_pure_revert
@@ -753,60 +755,45 @@ Tactic Notation "iNext":=
     |let P := match goal with |- upred_tactics.StripLaterL ?P _ => P end in
      apply _ || fail "iNext:" P "does not contain laters"|].
 
-Tactic Notation "iLöb" "as" constr (H) :=
-  eapply tac_löb with _ H;
-    [reflexivity || fail "iLöb: non-empty spatial context"
-    |env_cbv; reflexivity || fail "iLöb:" H "not fresh"|].
-
-Tactic Notation "iLöb" "{" ident(x1) "}" "as" constr (H) :=
-  iRevert { x1 }; iLöb as H; iIntros { x1 }.
-Tactic Notation "iLöb" "{" ident(x1) ident(x2) "}" "as" constr (H) :=
-  iRevert { x1 x2 }; iLöb as H; iIntros { x1 x2 }.
-Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) "}" "as" constr (H) :=
-  iRevert { x1 x2 x3 }; iLöb as H; iIntros { x1 x2 x3 }.
+(* This is pretty ugly, but without Ltac support for manipulating lists of
+idents I do not know how to do this better. *)
+Ltac iLöbCore IH tac_before tac_after :=
+  match goal with
+  | |- of_envs ?Δ ⊢ _ =>
+     let Hs := constr:(rev (env_dom_list (env_spatial Δ))) in
+     iRevert ★; tac_before;
+     eapply tac_löb with _ IH;
+       [reflexivity
+       |env_cbv; reflexivity || fail "iLöb:" IH "not fresh"|];
+    tac_after;  iIntros Hs
+  end.
+
+Tactic Notation "iLöb" "as" constr (IH) := iLöbCore IH idtac idtac.
+Tactic Notation "iLöb" "{" ident(x1) "}" "as" constr (IH) :=
+  iLöbCore IH ltac:(iRevert { x1 }) ltac:(iIntros { x1 }).
+Tactic Notation "iLöb" "{" ident(x1) ident(x2) "}" "as" constr (IH) :=
+  iLöbCore IH ltac:(iRevert { x1 x2 }) ltac:(iIntros { x1 x2 }).
+Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) "}" "as" constr (IH) :=
+  iLöbCore IH ltac:(iRevert { x1 x2 x3 }) ltac:(iIntros { x1 x2 x3 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4) "}" "as"
-    constr (H):=
-  iRevert { x1 x2 x3 x4 }; iLöb as H; iIntros { x1 x2 x3 x4 }.
-Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) "}" "as" constr (H) :=
-  iRevert { x1 x2 x3 x4 x5 }; iLöb as H; iIntros { x1 x2 x3 x4 x5 }.
-Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ident(x6) "}" "as" constr (H) :=
-  iRevert { x1 x2 x3 x4 x5 x6 }; iLöb as H; iIntros { x1 x2 x3 x4 x5 x6 }.
-Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ident(x6) ident(x7) "}" "as" constr (H) :=
-  iRevert { x1 x2 x3 x4 x5 x6 x7 }; iLöb as H; iIntros { x1 x2 x3 x4 x5 x6 x7 }.
-Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ident(x6) ident(x7) ident(x8) "}" "as" constr (H) :=
-  iRevert { x1 x2 x3 x4 x5 x6 x7 x8 };
-    iLöb as H; iIntros { x1 x2 x3 x4 x5 x6 x7 x8 }.
-
-Tactic Notation "iLöb" constr(Hs) "as" constr (H) :=
-  iRevert Hs; iLöb as H; iIntros Hs.
-Tactic Notation "iLöb" "{" ident(x1) "}" constr(Hs) "as" constr (H) :=
-  iRevert { x1 } Hs; iLöb as H; iIntros { x1 } Hs.
-Tactic Notation "iLöb" "{" ident(x1) ident(x2) "}" constr(Hs) "as" constr (H) :=
-  iRevert { x1 x2 } Hs; iLöb as H; iIntros { x1 x2 } Hs.
-Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) "}" constr(Hs) "as"
-    constr (H) :=
-  iRevert { x1 x2 x3 } Hs; iLöb as H; iIntros { x1 x2 x3 } Hs.
-Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4) "}"
-    constr(Hs) "as" constr (H) :=
-  iRevert { x1 x2 x3 x4 } Hs; iLöb as H; iIntros { x1 x2 x3 x4 } Hs.
+    constr (IH):=
+  iLöbCore IH ltac:(iRevert { x1 x2 x3 x4 }) ltac:(iIntros { x1 x2 x3 x4 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) "}" constr(Hs) "as" constr (H) :=
-  iRevert { x1 x2 x3 x4 x5 } Hs; iLöb as H; iIntros { x1 x2 x3 x4 x5 } Hs.
+    ident(x5) "}" "as" constr (IH) :=
+  iLöbCore IH ltac:(iRevert { x1 x2 x3 x4 x5 })
+              ltac:(iIntros { x1 x2 x3 x4 x5 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ident(x6) "}" constr(Hs) "as" constr (H) :=
-  iRevert { x1 x2 x3 x4 x5 x6 } Hs; iLöb as H; iIntros { x1 x2 x3 x4 x5 x6 } Hs.
+    ident(x5) ident(x6) "}" "as" constr (IH) :=
+  iLöbCore IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 })
+              ltac:(iIntros { x1 x2 x3 x4 x5 x6 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ident(x6) ident(x7) "}" constr(Hs) "as" constr (H) :=
-  iRevert { x1 x2 x3 x4 x5 x6 x7 } Hs;
-    iLöb as H; iIntros { x1 x2 x3 x4 x5 x6 x7 } Hs.
+    ident(x5) ident(x6) ident(x7) "}" "as" constr (IH) :=
+  iLöbCore IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 x7 })
+              ltac:(iIntros { x1 x2 x3 x4 x5 x6 x7 }).
 Tactic Notation "iLöb" "{" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ident(x6) ident(x7) ident(x8) "}" constr(Hs) "as" constr (H) :=
-  iRevert { x1 x2 x3 x4 x5 x6 x7 x8 } Hs;
-    iLöb as H; iIntros { x1 x2 x3 x4 x5 x6 x7 x8 } Hs.
+    ident(x5) ident(x6) ident(x7) ident(x8) "}" "as" constr (IH) :=
+  iLöbCore IH ltac:(iRevert { x1 x2 x3 x4 x5 x6 x7 x8 })
+              ltac:(iIntros { x1 x2 x3 x4 x5 x6 x7 x8 }).
 
 (** * Assert *)
 Tactic Notation "iAssert" constr(Q) "as" constr(pat) "with" constr(Hs) :=

tests/heap_lang.v

@@ -42,7 +42,7 @@ Section LiftingTests.
     n1 < n2 →
     Φ #(n2 - 1) ⊢ WP FindPred #n2 #n1 @ E {{ Φ }}.
   Proof.
-    iIntros {Hn} "HΦ". iLöb {n1 Hn} "HΦ" as "IH".
+    iIntros {Hn} "HΦ". iLöb {n1 Hn} as "IH".
     wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
     - iApply "IH" "% HΦ". omega.
     - iPvsIntro. by assert (n1 = n2 - 1) as -> by omega.