diff --git a/theories/prelude/list.v b/theories/prelude/list.v index fbe2850ca4e2e1de7f09934f72ae3e896458e497..ecf9fdac4a5a3ff9328a9eced060f642c57b301e 100644 --- a/theories/prelude/list.v +++ b/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) : diff --git a/theories/program_logic/gen_heap.v b/theories/program_logic/gen_heap.v index a19923ef3b567dddbae688266c8562b18db2ebbd..a84e52a1f75b4163a2006fa9dea4156f8339e5e2 100644 --- a/theories/program_logic/gen_heap.v +++ b/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). diff --git a/theories/tests/barrier_client.v b/theories/tests/barrier_client.v index d27cddd6a1241f5f463ee5b580f5eb840e537cc2..eabcb4ca9d695d061a35885d67f1eacdf63f44fa 100644 --- a/theories/tests/barrier_client.v +++ b/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. diff --git a/theories/tests/one_shot.v b/theories/tests/one_shot.v index 26a34a28fe947ff4e2ee7c09c481d8632caa38fb..8c1d21336ffb1dafa0a3852c4f840e72554d0b48 100644 --- a/theories/tests/one_shot.v +++ b/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".