Move stuff out of sections that does not depend on the section variables.

theories/prelude/list.v

@@ -2082,11 +2082,18 @@ Proof.
   end); clear go; intuition.
 Defined.
 
+Definition Forall_nil_2 := @Forall_nil A.
+Definition Forall_cons_2 := @Forall_cons A.
+Global Instance Forall_proper:
+  Proper (pointwise_relation _ (↔) ==> (=) ==> (↔)) (@Forall A).
+Proof. split; subst; induction 1; constructor; by firstorder auto. Qed.
+Global Instance Exists_proper:
+  Proper (pointwise_relation _ (↔) ==> (=) ==> (↔)) (@Exists A).
+Proof. split; subst; induction 1; constructor; by firstorder auto. Qed.
+
 Section Forall_Exists.
   Context (P : A → Prop).
 
-  Definition Forall_nil_2 := @Forall_nil A.
-  Definition Forall_cons_2 := @Forall_cons A.
   Lemma Forall_forall l : Forall P l ↔ ∀ x, x ∈ l → P x.
   Proof.
     split; [induction 1; inversion 1; subst; auto|].
@@ -2113,9 +2120,6 @@ Section Forall_Exists.
   Lemma Forall_impl (Q : A → Prop) l :
     Forall P l → (∀ x, P x → Q x) → Forall Q l.
   Proof. intros H ?. induction H; auto. Defined.
-  Global Instance Forall_proper:
-    Proper (pointwise_relation _ (↔) ==> (=) ==> (↔)) (@Forall A).
-  Proof. split; subst; induction 1; constructor; by firstorder auto. Qed.
   Lemma Forall_iff l (Q : A → Prop) :
     (∀ x, P x ↔ Q x) → Forall P l ↔ Forall Q l.
   Proof. intros H. apply Forall_proper. red; apply H. done. Qed.
@@ -2226,9 +2230,7 @@ Section Forall_Exists.
   Lemma Exists_impl (Q : A → Prop) l :
     Exists P l → (∀ x, P x → Q x) → Exists Q l.
   Proof. intros H ?. induction H; auto. Defined.
-  Global Instance Exists_proper:
-    Proper (pointwise_relation _ (↔) ==> (=) ==> (↔)) (@Exists A).
-  Proof. split; subst; induction 1; constructor; by firstorder auto. Qed.
+
   Lemma Exists_not_Forall l : Exists (not ∘ P) l → ¬Forall P l.
   Proof. induction 1; inversion_clear 1; contradiction. Qed.
   Lemma Forall_not_Exists l : Forall (not ∘ P) l → ¬Exists P l.
@@ -2291,7 +2293,26 @@ Proof.
     destruct Hj; subst. auto with lia.
 Qed.
 
+Lemma Forall2_same_length {A B} (l : list A) (k : list B) :
+  Forall2 (λ _ _, True) l k ↔ length l = length k.
+Proof.
+  split; [by induction 1; f_equal/=|].
+  revert k. induction l; intros [|??] ?; simplify_eq/=; auto.
+Qed.
+
 (** ** Properties of the [Forall2] predicate *)
+Lemma Forall_Forall2 {A} (Q : A → A → Prop) l :
+  Forall (λ x, Q x x) l → Forall2 Q l l.
+Proof. induction 1; constructor; auto. Qed.
+Lemma Forall2_forall `{Inhabited A} B C (Q : A → B → C → Prop) l k :
+  Forall2 (λ x y, ∀ z, Q z x y) l k ↔ ∀ z, Forall2 (Q z) l k.
+Proof.
+  split; [induction 1; constructor; auto|].
+  intros Hlk. induction (Hlk inhabitant) as [|x y l k _ _ IH]; constructor.
+  - intros z. by feed inversion (Hlk z).
+  - apply IH. intros z. by feed inversion (Hlk z).
+Qed.
+
 Section Forall2.
   Context {A B} (P : A → B → Prop).
   Implicit Types x : A.
@@ -2299,12 +2320,6 @@ Section Forall2.
   Implicit Types l : list A.
   Implicit Types k : list B.
 
-  Lemma Forall2_same_length l k :
-    Forall2 (λ _ _, True) l k ↔ length l = length k.
-  Proof.
-    split; [by induction 1; f_equal/=|].
-    revert k. induction l; intros [|??] ?; simplify_eq/=; auto.
-  Qed.
   Lemma Forall2_length l k : Forall2 P l k → length l = length k.
   Proof. by induction 1; f_equal/=. Qed.
   Lemma Forall2_length_l l k n : Forall2 P l k → length l = n → length k = n.
@@ -2329,18 +2344,7 @@ Section Forall2.
   Proof.
     intros H. revert k2. induction H; inversion_clear 1; intros; f_equal; eauto.
   Qed.
-  Lemma Forall2_forall `{Inhabited C} (Q : C → A → B → Prop) l k :
-    Forall2 (λ x y, ∀ z, Q z x y) l k ↔ ∀ z, Forall2 (Q z) l k.
-  Proof.
-    split; [induction 1; constructor; auto|].
-    intros Hlk. induction (Hlk inhabitant) as [|x y l k _ _ IH]; constructor.
-    - intros z. by feed inversion (Hlk z).
-    - apply IH. intros z. by feed inversion (Hlk z).
-  Qed.
 
-  Lemma Forall_Forall2 (Q : A → A → Prop) l :
-    Forall (λ x, Q x x) l → Forall2 Q l l.
-  Proof. induction 1; constructor; auto. Qed.
   Lemma Forall2_Forall_l (Q : A → Prop) l k :
     Forall2 P l k → Forall (λ y, ∀ x, P x y → Q x) k → Forall Q l.
   Proof. induction 1; inversion_clear 1; eauto. Qed.
@@ -2801,11 +2805,12 @@ Section setoid.
 End setoid.
 
 (** * Properties of the monadic operations *)
+Lemma list_fmap_id {A} (l : list A) : id <$> l = l.
+Proof. induction l; f_equal/=; auto. Qed.
+
 Section fmap.
   Context {A B : Type} (f : A → B).
 
-  Lemma list_fmap_id (l : list A) : id <$> l = l.
-  Proof. induction l; f_equal/=; auto. Qed.
   Lemma list_fmap_compose {C} (g : B → C) l : g ∘ f <$> l = g <$> f <$> l.
   Proof. induction l; f_equal/=; auto. Qed.
   Lemma list_fmap_ext (g : A → B) (l1 l2 : list A) :

theories/program_logic/gen_heap.v

@@ -46,12 +46,9 @@ Local Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
   (at level 20, q at level 50, format "l  ↦{ q }  -") : uPred_scope.
 Local Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : uPred_scope.
 
-Section gen_heap.
-  Context `{gen_heapG L V Σ}.
-  Implicit Types P Q : iProp Σ.
-  Implicit Types Φ : V → iProp Σ.
+Section to_gen_heap.
+  Context (L V : Type) `{Countable L}.
   Implicit Types σ : gmap L V.
-  Implicit Types h g : gen_heapUR L V.
 
   (** Conversion to heaps and back *)
   Lemma to_gen_heap_valid σ : ✓ to_gen_heap σ.
@@ -71,6 +68,14 @@ Section gen_heap.
   Lemma to_gen_heap_delete l σ :
     to_gen_heap (delete l σ) = delete l (to_gen_heap σ).
   Proof. by rewrite /to_gen_heap fmap_delete. Qed.
+End to_gen_heap.
+
+Section gen_heap.
+  Context `{gen_heapG L V Σ}.
+  Implicit Types P Q : iProp Σ.
+  Implicit Types Φ : V → iProp Σ.
+  Implicit Types σ : gmap L V.
+  Implicit Types h g : gen_heapUR L V.
 
   (** General properties of mapsto *)
   Global Instance mapsto_timeless l q v : TimelessP (l ↦{q} v).

theories/tests/barrier_client.v

@@ -13,7 +13,9 @@ Definition client : expr :=
     (worker 12 "b" "y" ||| worker 17 "b" "y").
 
 Section client.
-  Context `{!heapG Σ, !barrierG Σ, !spawnG Σ} (N : namespace).
+  Context `{!heapG Σ, !barrierG Σ, !spawnG Σ}.
+
+  Local Definition N := nroot .@ "barrier".
 
   Definition y_inv (q : Qp) (l : loc) : iProp Σ :=
     (∃ f : val, l ↦{q} f ∗ □ ∀ n : Z, WP f #n {{ v, ⌜v = #(n + 42)⌝ }})%I.
@@ -58,9 +60,7 @@ Section ClosedProofs.
 Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
 
 Lemma client_adequate σ : adequate client σ (λ _, True).
-Proof.
-  apply (heap_adequacy Σ)=> ?. apply (client_safe (nroot .@ "barrier")).
-Qed.
+Proof. apply (heap_adequacy Σ)=> ?. apply client_safe. Qed.
 
 End ClosedProofs.
 

theories/tests/one_shot.v

@@ -29,7 +29,7 @@ Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
 Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
 
 Section proof.
-Context `{!heapG Σ, !one_shotG Σ} (N : namespace).
+Context `{!heapG Σ, !one_shotG Σ}.
 
 Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
   (l ↦ NONEV ∗ own γ Pending ∨ ∃ n : Z, l ↦ SOMEV #n ∗ own γ (Shot n))%I.
@@ -40,7 +40,7 @@ Lemma wp_one_shot (Φ : val → iProp Σ) :
     □ WP f2 #() {{ g, □ WP g #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
-  iIntros "Hf /=".
+  iIntros "Hf /=". pose proof (nroot .@ "N") as N.
   rewrite -wp_fupd /one_shot_example /=. wp_seq. wp_alloc l as "Hl". wp_let.
   iMod (own_alloc Pending) as (γ) "Hγ"; first done.
   iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".