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

_CoqProject

@@ -94,6 +94,7 @@ heap_lang/lib/spawn.v
 heap_lang/lib/par.v
 heap_lang/lib/assert.v
 heap_lang/lib/lock.v
+heap_lang/lib/counter.v
 heap_lang/lib/barrier/barrier.v
 heap_lang/lib/barrier/specification.v
 heap_lang/lib/barrier/protocol.v

algebra/agree.v

@@ -148,8 +148,8 @@ Arguments agreeC : clear implicits.
 Arguments agreeR : clear implicits.
 
 Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B :=
-  {| agree_car n := f (x n); agree_is_valid := agree_is_valid x |}.
-Solve Obligations with auto using agree_valid_S.
+  {| agree_car n := f (x n); agree_is_valid := agree_is_valid x;
+     agree_valid_S := agree_valid_S _ x |}.
 Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
 Proof. by destruct x. Qed.
 Lemma agree_map_compose {A B C} (f : A → B) (g : B → C) (x : agree A) :

algebra/auth.v

@@ -162,6 +162,9 @@ Qed.
 Canonical Structure authUR :=
   UCMRAT (auth A) auth_cofe_mixin auth_cmra_mixin auth_ucmra_mixin.
 
+Global Instance auth_frag_persistent a : Persistent a → Persistent (◯ a).
+Proof. do 2 constructor; simpl; auto. by apply persistent_core. Qed.
+
 (** Internalized properties *)
 Lemma auth_equivI {M} (x y : auth A) :
   x ≡ y ⊣⊢ (authoritative x ≡ authoritative y ∧ auth_own x ≡ auth_own y : uPred M).

algebra/cmra.v

@@ -758,35 +758,70 @@ Section nat.
   Instance nat_validN : ValidN nat := λ n x, True.
   Instance nat_pcore : PCore nat := λ x, Some 0.
   Instance nat_op : Op nat := plus.
+  Definition nat_op_plus x y : x ⋅ y = x + y := eq_refl.
   Lemma nat_included (x y : nat) : x ≼ y ↔ x ≤ y.
   Proof.
     split.
     - intros [z ->]; unfold op, nat_op; lia.
     - exists (y - x). by apply le_plus_minus.
   Qed.
-  Lemma nat_cmra_mixin : CMRAMixin nat.
+  Lemma nat_ra_mixin : RAMixin nat.
   Proof.
-    apply discrete_cmra_mixin, ra_total_mixin; try by eauto.
+    apply ra_total_mixin; try by eauto.
     - solve_proper.
     - intros x y z. apply Nat.add_assoc.
     - intros x y. apply Nat.add_comm.
     - by exists 0.
   Qed.
-  Canonical Structure natR : cmraT :=
-    CMRAT nat (@discrete_cofe_mixin _ equivL _) nat_cmra_mixin.
+  Canonical Structure natR : cmraT := discreteR nat nat_ra_mixin.
 
   Instance nat_empty : Empty nat := 0.
   Lemma nat_ucmra_mixin : UCMRAMixin nat.
   Proof. split; apply _ || done. Qed.
   Canonical Structure natUR : ucmraT :=
-    UCMRAT nat (@discrete_cofe_mixin _ equivL _) nat_cmra_mixin nat_ucmra_mixin.
+    discreteUR nat nat_ra_mixin nat_ucmra_mixin.
 
   Global Instance nat_cmra_discrete : CMRADiscrete natR.
   Proof. constructor; apply _ || done. Qed.
-  Global Instance nat_persistent (x : ()) : Persistent x.
-  Proof. by constructor. Qed.
 End nat.
 
+Definition mnat := nat.
+
+Section mnat.
+  Instance mnat_valid : Valid mnat := λ x, True.
+  Instance mnat_validN : ValidN mnat := λ n x, True.
+  Instance mnat_pcore : PCore mnat := Some.
+  Instance mnat_op : Op mnat := Nat.max.
+  Definition mnat_op_max x y : x ⋅ y = x `max` y := eq_refl.
+  Lemma mnat_included (x y : mnat) : x ≼ y ↔ x ≤ y.
+  Proof.
+    split.
+    - intros [z ->]; unfold op, mnat_op; lia.
+    - exists y. by symmetry; apply Nat.max_r.
+  Qed.
+  Lemma mnat_ra_mixin : RAMixin mnat.
+  Proof.
+    apply ra_total_mixin; try by eauto.
+    - solve_proper.
+    - solve_proper.
+    - intros x y z. apply Nat.max_assoc.
+    - intros x y. apply Nat.max_comm.
+    - intros x. apply Max.max_idempotent.
+  Qed.
+  Canonical Structure mnatR : cmraT := discreteR mnat mnat_ra_mixin.
+
+  Instance mnat_empty : Empty mnat := 0.
+  Lemma mnat_ucmra_mixin : UCMRAMixin mnat.
+  Proof. split; apply _ || done. Qed.
+  Canonical Structure mnatUR : ucmraT :=
+    discreteUR mnat mnat_ra_mixin mnat_ucmra_mixin.
+
+  Global Instance mnat_cmra_discrete : CMRADiscrete mnatR.
+  Proof. constructor; apply _ || done. Qed.
+  Global Instance mnat_persistent (x : mnat) : Persistent x.
+  Proof. by constructor. Qed.
+End mnat.
+
 (** ** Product *)
 Section prod.
   Context {A B : cmraT}.

algebra/csum.v

@@ -292,6 +292,32 @@ Proof. eauto using csum_updateP_l. Qed.
 Lemma csum_updateP'_r (P : B → Prop) b :
   b ~~>: P → Cinr b ~~>: λ m', ∃ b', m' = Cinr b' ∧ P b'.
 Proof. eauto using csum_updateP_r. Qed.
+Lemma csum_local_update_l (a1 a2 : A) af :
+  (∀ af', af = Cinl <$> af' → a1 ~l~> a2 @ af') → Cinl a1 ~l~> Cinl a2 @ af.
+Proof.
+  intros Ha. split; destruct af as [[af'| |]|]=>//=.
+  - by eapply (Ha (Some af')).
+  - by eapply (Ha None).
+  - destruct (Ha (Some af') (reflexivity _)) as [_ Ha'].
+    intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
+    by apply (Ha' n (Some mz)). by apply (Ha' n None).
+  - destruct (Ha None (reflexivity _)) as [_ Ha'].
+    intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
+    by apply (Ha' n (Some mz)). by apply (Ha' n None).
+Qed.
+Lemma csum_local_update_r (b1 b2 : B) bf :
+  (∀ bf', bf = Cinr <$> bf' → b1 ~l~> b2 @ bf') → Cinr b1 ~l~> Cinr b2 @ bf.
+Proof.
+  intros Hb. split; destruct bf as [[|bf'|]|]=>//=.
+  - by eapply (Hb (Some bf')).
+  - by eapply (Hb None).
+  - destruct (Hb (Some bf') (reflexivity _)) as [_ Hb'].
+    intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
+    by apply (Hb' n (Some mz)). by apply (Hb' n None).
+  - destruct (Hb None (reflexivity _)) as [_ Hb'].
+    intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
+    by apply (Hb' n (Some mz)). by apply (Hb' n None).
+Qed.
 End cmra.
 
 Arguments csumR : clear implicits.

algebra/updates.v

@@ -125,6 +125,13 @@ Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1
 Proof.
   rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
 Qed.
+Lemma cmra_update_valid0 x y :
+  (✓{0} x → x ~~> y) → x ~~> y.
+Proof.
+  intros H n mz Hmz. apply H, Hmz.
+  apply (cmra_validN_le n); last lia.
+  destruct mz. eapply cmra_validN_op_l, Hmz. apply Hmz.
+Qed.
 
 (** ** Frame preserving updates for total CMRAs *)
 Section total_updates.
@@ -232,3 +239,16 @@ Section option.
   Lemma option_update x y : x ~~> y → Some x ~~> Some y.
   Proof. rewrite !cmra_update_updateP; eauto using option_updateP with subst. Qed.
 End option.
+
+(** * Natural numbers  *)
+Lemma nat_local_update (x y : nat) mz : x ~l~> y @ mz.
+Proof.
+  split; first done.
+  compute -[plus]; destruct mz as [z|]; intros n [z'|]; lia.
+Qed.
+
+Lemma mnat_local_update (x y : mnat) mz : x ≤ y → x ~l~> y @ mz.
+Proof.
+  split; first done.
+  compute -[max]; destruct mz as [z|]; intros n [z'|]; lia.
+Qed.

algebra/upred.v

@@ -564,6 +564,8 @@ Proof. intros ->; apply iff_refl. Qed.
 
 Lemma pure_mono φ1 φ2 : (φ1 → φ2) → ■ φ1 ⊢ ■ φ2.
 Proof. intros; apply pure_elim with φ1; eauto using pure_intro. Qed.
+Lemma pure_iff φ1 φ2 : (φ1 ↔ φ2) → ■ φ1 ⊣⊢ ■ φ2.
+Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
 Lemma and_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∧ P' ⊢ Q ∧ Q'.
 Proof. auto. Qed.
 Lemma and_mono_l P P' Q : (P ⊢ Q) → P ∧ P' ⊢ Q ∧ P'.

heap_lang/lib/counter.v

+(* Monotone counter, but using an explicit CMRA instead of auth *)
+From iris.program_logic Require Export global_functor.
+From iris.program_logic Require Import auth.
+From iris.proofmode Require Import invariants ghost_ownership coq_tactics.
+From iris.heap_lang Require Import proofmode notation.
+Import uPred.
+
+Definition newcounter : val := λ: <>, ref #0.
+Definition inc : val :=
+  rec: "inc" "l" :=
+    let: "n" := !'"l" in
+    if: CAS '"l" '"n" (#1 + '"n") then #() else '"inc" '"l".
+Definition read : val := λ: "l", !'"l".
+Global Opaque newcounter inc get.
+
+(** The CMRA we need. *)
+Class counterG Σ := CounterG { counter_tokG :> authG heap_lang Σ mnatUR }.
+Definition counterGF : gFunctorList := [authGF mnatUR].
+Instance inGF_counterG `{H : inGFs heap_lang Σ counterGF} : counterG Σ.
+Proof. destruct H; split; apply _. Qed.
+
+Section proof.
+Context {Σ : gFunctors} `{!heapG Σ, !counterG Σ}.
+Context (heapN : namespace).
+Local Notation iProp := (iPropG heap_lang Σ).
+
+Definition counter_inv (l : loc) (n : mnat) : iProp := (l ↦ #n)%I.
+
+Definition counter (l : loc) (n : nat) : iProp :=
+  (∃ N γ, heapN ⊥ N ∧ heap_ctx heapN ∧
+          auth_ctx γ N (counter_inv l) ∧ auth_own γ (n:mnat))%I.
+
+(** The main proofs. *)
+Global Instance counter_persistent l n : PersistentP (counter l n).
+Proof. apply _. Qed.
+
+Lemma newcounter_spec N (R : iProp) Φ :
+  heapN ⊥ N →
+  heap_ctx heapN ★ (∀ l, counter l 0 -★ Φ #l) ⊢ WP newcounter #() {{ Φ }}.
+Proof.
+  iIntros {?} "[#Hh HΦ]". rewrite /newcounter. wp_seq. wp_alloc l as "Hl".
+  iPvs (auth_alloc (counter_inv l) N _ (O:mnat) with "[Hl]")
+    as {γ} "[#? Hγ]"; try by auto.
+  iPvsIntro. iApply "HΦ". rewrite /counter; eauto 10.
+Qed.
+
+Lemma inc_spec l j (Φ : val → iProp) :
+  counter l j ★ (counter l (S j) -★ Φ #()) ⊢ WP inc #l {{ Φ }}.
+Proof.
+  iIntros "[Hl HΦ]". iLöb as "IH". wp_rec.
+  iDestruct "Hl" as {N γ} "(% & #? & #Hγ & Hγf)".
+  wp_focus (! _)%E; iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
+  iIntros "{$Hγ $Hγf}"; iIntros {j'} "[% Hl] /="; rewrite {2}/counter_inv.
+  wp_load; iPvsIntro; iExists j; iSplit; [done|iIntros "{$Hl} Hγf"].
+  wp_let; wp_op.
+  wp_focus (CAS _ _ _); iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
+  iIntros "{$Hγ $Hγf}"; iIntros {j''} "[% Hl] /="; rewrite {2}/counter_inv.
+  destruct (decide (j `max` j'' = j `max` j')) as [Hj|Hj].
+  - wp_cas_suc; first (by do 3 f_equal); iPvsIntro.
+    iExists (1 + j `max` j')%nat; iSplit.
+    { iPureIntro. apply mnat_local_update. abstract lia. }
+    rewrite {2}/counter_inv !mnat_op_max (Nat.max_l (S _)); last abstract lia.
+    rewrite Nat2Z.inj_succ -Z.add_1_l.
+    iIntros "{$Hl} Hγf". wp_if.
+    iPvsIntro; iApply "HΦ"; iExists N, γ; repeat iSplit; eauto.
+    iApply (auth_own_mono with "Hγf"). apply mnat_included. abstract lia.
+  - wp_cas_fail; first (rewrite !mnat_op_max; by intros [= ?%Nat2Z.inj]).
+    iPvsIntro. iExists j; iSplit; [done|iIntros "{$Hl} Hγf"].
+    wp_if. iApply ("IH" with "[Hγf] HΦ"). rewrite {3}/counter; eauto 10.
+Qed.
+
+Lemma read_spec l j (Φ : val → iProp) :
+  counter l j ★ (∀ i, ■ (j ≤ i)%nat → counter l i -★ Φ #i)
+  ⊢ WP read #l {{ Φ }}.
+Proof.
+  iIntros "[Hc HΦ]". iDestruct "Hc" as {N γ} "(% & #? & #Hγ & Hγf)".
+  rewrite /read. wp_let. iApply (auth_fsa (counter_inv l) (wp_fsa _) _ N); auto.
+  iIntros "{$Hγ $Hγf}"; iIntros {j'} "[% Hl] /=".
+  wp_load; iPvsIntro; iExists (j `max` j'); iSplit.
+  { iPureIntro; apply mnat_local_update; abstract lia. }
+  rewrite !mnat_op_max -Nat.max_assoc Nat.max_idempotent; iIntros "{$Hl} Hγf".
+  iApply ("HΦ" with "[%]"); first abstract lia; rewrite /counter; eauto 10.
+Qed.
+End proof.

heap_lang/proofmode.v

@@ -105,7 +105,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
       [let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_alloc:" e' "not a value"
       |iAssumption || fail "wp_alloc: cannot find heap_ctx"
-      |done || eauto with ndisj
+      |solve_ndisj
       |apply _
       |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
         eexists; split;
@@ -126,7 +126,7 @@ Tactic Notation "wp_load" :=
       |fail 1 "wp_load: cannot find 'Load' in" e];
     eapply tac_wp_load;
       [iAssumption || fail "wp_load: cannot find heap_ctx"
-      |done || eauto with ndisj
+      |solve_ndisj
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
@@ -145,7 +145,7 @@ Tactic Notation "wp_store" :=
       [let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_store:" e' "not a value"
       |iAssumption || fail "wp_store: cannot find heap_ctx"
-      |done || eauto with ndisj
+      |solve_ndisj
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
@@ -167,7 +167,7 @@ Tactic Notation "wp_cas_fail" :=
       |let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_cas_fail:" e' "not a value"
       |iAssumption || fail "wp_cas_fail: cannot find heap_ctx"
-      |done || eauto with ndisj
+      |solve_ndisj
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
@@ -189,7 +189,7 @@ Tactic Notation "wp_cas_suc" :=
       |let e' := match goal with |- to_val ?e' = _ => e' end in
        wp_done || fail "wp_cas_suc:" e' "not a value"
       |iAssumption || fail "wp_cas_suc: cannot find heap_ctx"
-      |done || eauto with ndisj
+      |solve_ndisj
       |apply _
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"

prelude/base.v

@@ -7,6 +7,7 @@ structures. *)
 Global Generalizable All Variables.
 Global Set Automatic Coercions Import.
 Global Set Asymmetric Patterns.
+Global Unset Transparent Obligations.
 From Coq Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid.
 Obligation Tactic := idtac.
 

prelude/fin_maps.v

@@ -527,6 +527,12 @@ Proof.
   - by rewrite lookup_fmap, !lookup_insert.
   - by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
 Qed.
+Lemma fmap_delete {A B} (f: A → B) m i: f <$> delete i m = delete i (f <$> m).
+Proof.
+  apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
+  - by rewrite lookup_fmap, !lookup_delete.
+  - by rewrite lookup_fmap, !lookup_delete_ne, lookup_fmap by done.
+Qed.
 Lemma omap_insert {A B} (f : A → option B) m i x y :
   f x = Some y → omap f (<[i:=x]>m) = <[i:=y]>(omap f m).
 Proof.

prelude/list.v

@@ -1265,6 +1265,21 @@ Proof.
     take_app_alt by (rewrite ?app_length, ?take_length, ?Hk; lia).
 Qed.
 
+(** ** Properties of the [imap] function *)
+Lemma imap_cons {B} (f : nat → A → B) x l :
+  imap f (x :: l) = f 0 x :: imap (f ∘ S) l.
+Proof.
+  unfold imap. simpl. f_equal. generalize 0.
+  induction l; intros n; simpl; repeat (auto||f_equal).
+Qed.
+Lemma imap_ext {B} (f g : nat → A → B) l :
+  (∀ i x, f i x = g i x) →
+  imap f l = imap g l.
+Proof.
+  unfold imap. intro EQ. generalize 0.
+  induction l; simpl; intros n; f_equal; auto.
+Qed.
+
 (** ** Properties of the [mask] function *)
 Lemma mask_nil f βs : mask f βs (@nil A) = [].
 Proof. by destruct βs. Qed.

prelude/numbers.v

@@ -32,6 +32,8 @@ Notation "(<)" := lt (only parsing) : nat_scope.
 
 Infix "`div`" := Nat.div (at level 35) : nat_scope.
 Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
+Infix "`max`" := Nat.max (at level 35) : nat_scope.
+Infix "`min`" := Nat.min (at level 35) : nat_scope.
 
 Instance nat_eq_dec: ∀ x y : nat, Decision (x = y) := eq_nat_dec.
 Instance nat_le_dec: ∀ x y : nat, Decision (x ≤ y) := le_dec.
@@ -504,6 +506,8 @@ Infix "+" := Qp_plus : Qp_scope.
 Infix "-" := Qp_minus : Qp_scope.
 Infix "/" := Qp_div : Qp_scope.
 
+Instance Qp_inhabited : Inhabited Qp := populate 1%Qp.
+
 Lemma Qp_eq x y : x = y ↔ Qp_car x = Qp_car y.
 Proof.
   split; [by intros ->|].

prelude/strings.v

@@ -2,7 +2,12 @@
 (* This file is distributed under the terms of the BSD license. *)
 From Coq Require Import Ascii.
 From Coq Require Export String.
-From iris.prelude Require Export countable.
+From iris.prelude Require Export list.
+From iris.prelude Require Import countable.
+
+(* To avoid randomly ending up with String.length because this module is
+imported hereditarily somewhere. *)
+Notation length := List.length.
 
 (** * Fix scopes *)
 Open Scope string_scope.

prelude/tactics.v

@@ -412,10 +412,11 @@ Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
 It will search for the first subterm of the goal matching [pat], and then call [tac]
 with that subterm. *)
 Ltac find_pat pat tac :=
-  match goal with |- context [?x] =>
-                  unify pat x with typeclass_instances;
-                  tryif tac x then idtac else fail 2
-end.
+  match goal with
+  |- context [?x] =>
+      unify pat x with typeclass_instances;
+      tryif tac x then idtac else fail 2
+  end.
 
 (** Coq's [firstorder] tactic fails or loops on rather small goals already. In 
 particular, on those generated by the tactic [unfold_elem_ofs] which is used

program_logic/auth.v

@@ -55,6 +55,14 @@ Section auth.
 
   Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ★ auth_own γ b.
   Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
+
+  Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a.
+  Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.
+
+  Global Instance auth_own_persistent γ a :
+    Persistent a → PersistentP (auth_own γ a).
+  Proof. rewrite /auth_own. apply _. Qed.
+
   Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a.
   Proof. by rewrite /auth_own own_valid auth_validI. Qed.
 

program_logic/namespaces.v

@@ -37,7 +37,7 @@ Section ndisjoint.
   Global Instance ndisjoint_comm : Comm iff ndisjoint.
   Proof. intros N1 N2. rewrite /disjoint /ndisjoint; naive_solver. Qed.
 
-  Lemma ndot_ne_disjoint N (x y : A) : x ≠ y → N .@ x ⊥ N .@ y.
+  Lemma ndot_ne_disjoint N x y : x ≠ y → N .@ x ⊥ N .@ y.
   Proof. intros Hxy. exists (N .@ x), (N .@ y); naive_solver. Qed.
 
   Lemma ndot_preserve_disjoint_l N1 N2 x : N1 ⊥ N2 → N1 .@ x ⊥ N2.
@@ -55,26 +55,17 @@ Section ndisjoint.
     rewrite !elem_coPset_suffixes; intros [q ->] [q' Hq]; destruct Hne.
     by rewrite !list_encode_app !assoc in Hq; apply list_encode_suffix_eq in Hq.
   Qed.
+
+  Lemma ndisj_subseteq_difference N1 N2 E :
+    N1 ⊥ N2 → nclose N1 ⊆ E → nclose N1 ⊆ E ∖ nclose N2.
+  Proof. intros ?%ndisj_disjoint. set_solver. Qed.
 End ndisjoint.
 
-(* This tactic solves goals about inclusion and disjointness
-   of masks (i.e., coPsets) with set_solver, taking
-   disjointness of namespaces into account. *)
-(* TODO: This tactic is by far now yet as powerful as it should be.
-   For example, given [N1 ⊥ N2], it should be able to solve
-   [nclose (ndot N1 x) ⊥ N2]. It should also solve
-   [ndot N x ⊥ ndot N y] if x ≠ y is in the context or
-   follows from [discriminate]. *)
-Ltac set_solver_ndisj :=
-  repeat match goal with
-  (* TODO: Restrict these to have type namespace *)
-  | [ H : ?N1 ⊥ ?N2 |-_ ] => apply ndisj_disjoint in H
-  end; set_solver.
-(* TODO: restrict this to match only if this is ⊆ of coPset *)
-Hint Extern 500 (_ ⊆ _) => set_solver_ndisj : ndisj.
 (* The hope is that registering these will suffice to solve most goals
-   of the form [N1 ⊥ N2].
-   TODO: Can this prove x ≠ y if discriminate can? *)
-Hint Resolve ndot_ne_disjoint : ndisj.
+of the form [N1 ⊥ N2] and those of the form [((N1 ⊆ E ∖ N2) ∖ ..) ∖ Nn]. *)
+Hint Resolve ndisj_subseteq_difference : ndisj.
+Hint Extern 0 (_ ⊥ _) => apply ndot_ne_disjoint; congruence : ndisj.
 Hint Resolve ndot_preserve_disjoint_l : ndisj.
 Hint Resolve ndot_preserve_disjoint_r : ndisj.
+
+Ltac solve_ndisj := solve [eauto with ndisj].

proofmode/classes.v

@@ -112,10 +112,10 @@ Global Arguments from_and : clear implicits.
 Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2.
 Proof. done. Qed.
 Global Instance from_and_sep_persistent_l P1 P2 :
-  PersistentP P1 → FromAnd (P1 ★ P2) P1 P2.
+  PersistentP P1 → FromAnd (P1 ★ P2) P1 P2 | 9.
 Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
 Global Instance from_and_sep_persistent_r P1 P2 :
-  PersistentP P2 → FromAnd (P1 ★ P2) P1 P2.
+  PersistentP P2 → FromAnd (P1 ★ P2) P1 P2 | 10.
 Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
 Global Instance from_and_always P Q1 Q2 :
   FromAnd P Q1 Q2 → FromAnd (□ P) (□ Q1) (□ Q2).

proofmode/intro_patterns.v

@@ -13,7 +13,7 @@ Inductive intro_pat :=
   | INext : intro_pat
   | IForall : intro_pat
   | IAll : intro_pat
-  | IClear : list string → intro_pat.
+  | IClear : list (bool * string) → intro_pat. (* true = frame, false = clear *)
 
 Module intro_pat.
 Inductive token :=
@@ -71,8 +71,7 @@ Inductive stack_item :=
   | SList : stack_item
   | SConjList : stack_item
   | SBar : stack_item
-  | SAmp : stack_item
-  | SClear : stack_item.
+  | SAmp : stack_item.
 Notation stack := (list stack_item).
 
 Fixpoint close_list (k : stack)
@@ -108,13 +107,6 @@ Fixpoint close_conj_list (k : stack)
   | _ => None
   end.
 
-Fixpoint close_clear (k : stack) (ss : list string) : option stack :=
-  match k with
-  | SPat (IName s) :: k => close_clear k (s :: ss)
-  | SClear :: k => Some (SPat (IClear (reverse ss)) :: k)
-  | _ => None
-  end.
-
 Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   match ts with
   | [] => Some k
@@ -135,9 +127,18 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   | TNext :: ts => parse_go ts (SPat INext :: k)
   | TAll :: ts => parse_go ts (SPat IAll :: k)
   | TForall :: ts => parse_go ts (SPat IForall :: k)
-  | TClearL :: ts => parse_go ts (SClear :: k)
-  | TClearR :: ts => close_clear k [] ≫= parse_go ts
+  | TClearL :: ts => parse_clear ts [] k
+  | _ => None
+  end
+with parse_clear (ts : list token)
+    (ss : list (bool * string)) (k : stack) : option stack :=
+  match ts with
+  | TFrame :: TName s :: ts => parse_clear ts ((true,s) :: ss) k
+  | TName s :: ts => parse_clear ts ((false,s) :: ss) k
+  | TClearR :: ts => parse_go ts (SPat (IClear (reverse ss)) :: k)
+  | _ => None
   end.
+
 Definition parse (s : string) : option (list intro_pat) :=
   match k ← parse_go (tokenize s) [SList]; close_list k [] [] with
   | Some [SPat (IList [ps])] => Some ps

proofmode/invariants.v

@@ -39,7 +39,7 @@ Tactic Notation "iInvCore" constr(N) "as" constr(H) :=