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

ProofMode.md

@@ -114,7 +114,7 @@ introduction patterns:
 - `# ipat` : move the hypothesis to the persistent context.
 - `%` : move the hypothesis to the pure Coq context (anonymously).
 - `[ipat ipat]` : (separating) conjunction elimination.
-- `|ipat|ipat]` : disjunction elimination.
+- `[ipat|ipat]` : disjunction elimination.
 - `[]` : false elimination.
 
 Apart from this, there are the following introduction patterns that can only
@@ -186,7 +186,7 @@ Many of the proof mode tactics (such as `iDestruct`, `iApply`, `iRewrite`) can
 take both hypotheses and lemmas, and allow one to instantiate universal
 quantifiers and implications/wands of these hypotheses/lemmas on the fly.
 
-The syntax for the arguments, called _proof mode terms_ of these tactics is:
+The syntax for the arguments, called _proof mode terms_, of these tactics is:
 
         (H $! t1 ... tn with "spat1 .. spatn")
 

algebra/gmap.v

@@ -205,15 +205,12 @@ Qed.
 Lemma singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x.
 Proof. rewrite !cmra_valid_validN. by setoid_rewrite singleton_validN. Qed.
 
-Lemma insert_singleton_opN n m i x :
-  m !! i = None → <[i:=x]> m ≡{n}≡ {[ i := x ]} ⋅ m.
+Lemma insert_singleton_op m i x : m !! i = None → <[i:=x]> m = {[ i := x ]} ⋅ m.
 Proof.
-  intros Hi j; destruct (decide (i = j)) as [->|].
-  - by rewrite lookup_op lookup_insert lookup_singleton Hi right_id.
-  - by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id.
+  intros Hi; apply map_eq=> j; destruct (decide (i = j)) as [->|].
+  - by rewrite lookup_op lookup_insert lookup_singleton Hi right_id_L.
+  - by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id_L.
 Qed.
-Lemma insert_singleton_op m i x : m !! i = None → <[i:=x]> m ≡ {[ i := x ]} ⋅ m.
-Proof. rewrite !equiv_dist; naive_solver eauto using insert_singleton_opN. Qed.
 
 Lemma core_singleton (i : K) (x : A) cx :
   pcore x = Some cx → core ({[ i := x ]} : gmap K A) = {[ i := cx ]}.
@@ -252,9 +249,9 @@ Proof.
       * by rewrite Hi lookup_op lookup_singleton lookup_delete.
       * by rewrite lookup_op lookup_singleton_ne // lookup_delete_ne // left_id.
 Qed.
-Lemma dom_op m1 m2 : dom (gset K) (m1 ⋅ m2) ≡ dom _ m1 ∪ dom _ m2.
+Lemma dom_op m1 m2 : dom (gset K) (m1 ⋅ m2) = dom _ m1 ∪ dom _ m2.
 Proof.
-  apply elem_of_equiv; intros i; rewrite elem_of_union !elem_of_dom.
+  apply elem_of_equiv_L=> i; rewrite elem_of_union !elem_of_dom.
   unfold is_Some; setoid_rewrite lookup_op.
   destruct (m1 !! i), (m2 !! i); naive_solver.
 Qed.
@@ -303,8 +300,8 @@ Section freshness.
     { rewrite -not_elem_of_union -dom_op -not_elem_of_union; apply is_fresh. }
     exists (<[i:=x]>m); split.
     { by apply HQ; last done; apply not_elem_of_dom. }
-    rewrite insert_singleton_opN; last by apply not_elem_of_dom.
-    rewrite -assoc -insert_singleton_opN;
+    rewrite insert_singleton_op; last by apply not_elem_of_dom.
+    rewrite -assoc -insert_singleton_op;
       last by apply not_elem_of_dom; rewrite dom_op not_elem_of_union.
     by apply insert_validN; [apply cmra_valid_validN|].
   Qed.

heap_lang/lib/spawn.v

@@ -56,23 +56,23 @@ Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
   heap_ctx heapN ★ WP f #() {{ Ψ }} ★ (∀ l, join_handle l Ψ -★ Φ #l)
   ⊢ WP spawn e {{ Φ }}.
 Proof.
-  iIntros {<-%of_to_val ?} "(#Hh&Hf&HΦ)". rewrite /spawn.
+  iIntros {<-%of_to_val ?} "(#Hh & Hf & HΦ)". rewrite /spawn.
   wp_let. wp_alloc l as "Hl". wp_let.
   iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
   iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
   { iNext. iExists (InjLV #0). iFrame; eauto. }
   wp_apply wp_fork. iSplitR "Hf".
-  - iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ"; rewrite /join_handle. eauto.
-  - wp_focus (f _). iApply wp_wand_l; iFrame "Hf"; iIntros {v} "Hv".
+  - iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ". rewrite /join_handle. eauto.
+  - wp_focus (f _). iApply wp_wand_l. iFrame "Hf"; iIntros {v} "Hv".
     iInv N as {v'} "[Hl _]"; first wp_done.
-    wp_store. iPvsIntro; iSplit; [iNext|done].
-    iExists (InjRV v); iFrame; eauto.
+    wp_store. iPvsIntro. iSplit; [iNext|done].
+    iExists (InjRV v). iFrame. eauto.
 Qed.
 
 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γ&#?)".
+  rewrite /join_handle; iIntros "[[% H] Hv]". iDestruct "H" as {γ} "(#?&Hγ&#?)".
   iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as {v} "[Hl Hinv]".
   wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
   - iPvsIntro; iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].

prelude/base.v

@@ -393,6 +393,8 @@ Proof. now intros -> ?. Qed.
 Instance unit_equiv : Equiv unit := λ _ _, True.
 Instance unit_equivalence : Equivalence (@equiv unit _).
 Proof. repeat split. Qed.
+Instance unit_leibniz : LeibnizEquiv unit.
+Proof. intros [] []; reflexivity. Qed.
 Instance unit_inhabited: Inhabited unit := populate ().
 
 (** ** Products *)
@@ -908,13 +910,6 @@ Class Collection A C `{ElemOf A C, Empty C, Singleton A C,
   elem_of_intersection X Y (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y;
   elem_of_difference X Y (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y
 }.
-Class CollectionOps A C `{ElemOf A C, Empty C, Singleton A C, Union C,
-    Intersection C, Difference C, IntersectionWith A C, Filter A C} : Prop := {
-  collection_ops :>> Collection A C;
-  elem_of_intersection_with (f : A → A → option A) X Y (x : A) :
-    x ∈ intersection_with f X Y ↔ ∃ x1 x2, x1 ∈ X ∧ x2 ∈ Y ∧ f x1 x2 = Some x;
-  elem_of_filter X P `{∀ x, Decision (P x)} x : x ∈ filter P X ↔ P x ∧ x ∈ X
-}.
 
 (** We axiomative a finite collection as a collection whose elements can be
 enumerated as a list. These elements, given by the [elements] function, may be

prelude/collections.v

@@ -467,35 +467,6 @@ Section collection.
   End dec.
 End collection.
 
-Section collection_ops.
-  Context `{CollectionOps A C}.
-
-  Lemma elem_of_intersection_with_list (f : A → A → option A) Xs Y x :
-    x ∈ intersection_with_list f Y Xs ↔ ∃ xs y,
-      Forall2 (∈) xs Xs ∧ y ∈ Y ∧ foldr (λ x, (≫= f x)) (Some y) xs = Some x.
-  Proof.
-    split.
-    - revert x. induction Xs; simpl; intros x HXs; [eexists [], x; intuition|].
-      rewrite elem_of_intersection_with in HXs; destruct HXs as (x1&x2&?&?&?).
-      destruct (IHXs x2) as (xs & y & hy & ? & ?); trivial.
-      eexists (x1 :: xs), y. intuition (simplify_option_eq; auto).
-    - intros (xs & y & Hxs & ? & Hx). revert x Hx.
-      induction Hxs; intros; simplify_option_eq; [done |].
-      rewrite elem_of_intersection_with. naive_solver.
-  Qed.
-
-  Lemma intersection_with_list_ind (P Q : A → Prop) f Xs Y :
-    (∀ y, y ∈ Y → P y) →
-    Forall (λ X, ∀ x, x ∈ X → Q x) Xs →
-    (∀ x y z, Q x → P y → f x y = Some z → P z) →
-    ∀ x, x ∈ intersection_with_list f Y Xs → P x.
-  Proof.
-    intros HY HXs Hf. induction Xs; simplify_option_eq; [done |].
-    intros x Hx. rewrite elem_of_intersection_with in Hx.
-    decompose_Forall. destruct Hx as (? & ? & ? & ? & ?). eauto.
-  Qed.
-End collection_ops.
-
 (** * Sets without duplicates up to an equivalence *)
 Section NoDup.
   Context `{SimpleCollection A B} (R : relation A) `{!Equivalence R}.

prelude/listset.v

@@ -42,10 +42,6 @@ Instance listset_intersection: Intersection (listset A) := λ l k,
   let (l') := l in let (k') := k in Listset (list_intersection l' k').
 Instance listset_difference: Difference (listset A) := λ l k,
   let (l') := l in let (k') := k in Listset (list_difference l' k').
-Instance listset_intersection_with: IntersectionWith A (listset A) := λ f l k,
-  let (l') := l in let (k') := k in Listset (list_intersection_with f l' k').
-Instance listset_filter: Filter A (listset A) := λ P _ l,
-  let (l') := l in Listset (filter P l').
 
 Instance: Collection A (listset A).
 Proof.
@@ -62,13 +58,6 @@ Proof.
   - intros. apply elem_of_remove_dups.
   - intros. apply NoDup_remove_dups.
 Qed.
-Global Instance: CollectionOps A (listset A).
-Proof.
-  split.
-  - apply _.
-  - intros ? [?] [?]. apply elem_of_list_intersection_with.
-  - intros [?] ??. apply elem_of_list_filter.
-Qed.
 End listset.
 
 (** These instances are declared using [Hint Extern] to avoid too
@@ -83,14 +72,10 @@ Hint Extern 1 (Union (listset _)) =>
   eapply @listset_union : typeclass_instances.
 Hint Extern 1 (Intersection (listset _)) =>
   eapply @listset_intersection : typeclass_instances.
-Hint Extern 1 (IntersectionWith _ (listset _)) =>
-  eapply @listset_intersection_with : typeclass_instances.
 Hint Extern 1 (Difference (listset _)) =>
   eapply @listset_difference : typeclass_instances.
 Hint Extern 1 (Elements _ (listset _)) =>
   eapply @listset_elems : typeclass_instances.
-Hint Extern 1 (Filter _ (listset _)) =>
-  eapply @listset_filter : typeclass_instances.
 
 Instance listset_ret: MRet listset := λ A x, {[ x ]}.
 Instance listset_fmap: FMap listset := λ A B f l,

prelude/listset_nodup.v

@@ -29,12 +29,6 @@ Instance listset_nodup_intersection: Intersection C := λ l k,
 Instance listset_nodup_difference: Difference C := λ l k,
   let (l',Hl) := l in let (k',Hk) := k
   in ListsetNoDup _ (NoDup_list_difference _ k' Hl).
-Instance listset_nodup_intersection_with: IntersectionWith A C := λ f l k,
-  let (l',Hl) := l in let (k',Hk) := k
-  in ListsetNoDup
-    (remove_dups (list_intersection_with f l' k')) (NoDup_remove_dups _).
-Instance listset_nodup_filter: Filter A C := λ P _ l,
-  let (l',Hl) := l in ListsetNoDup _ (NoDup_filter P _ Hl).
 
 Instance: Collection A C.
 Proof.
@@ -49,15 +43,6 @@ Qed.
 Global Instance listset_nodup_elems: Elements A C := listset_nodup_car.
 Global Instance: FinCollection A C.
 Proof. split. apply _. done. by intros [??]. Qed.
-Global Instance: CollectionOps A C.
-Proof.
-  split.
-  - apply _.
-  - intros ? [??] [??] ?. unfold intersection_with, elem_of,
-      listset_nodup_intersection_with, listset_nodup_elem_of; simpl.
-    rewrite elem_of_remove_dups. by apply elem_of_list_intersection_with.
-  - intros [??] ???. apply elem_of_list_filter.
-Qed.
 End list_collection.
 
 Hint Extern 1 (ElemOf _ (listset_nodup _)) =>
@@ -74,5 +59,3 @@ Hint Extern 1 (Difference (listset_nodup _)) =>
   eapply @listset_nodup_difference : typeclass_instances.
 Hint Extern 1 (Elements _ (listset_nodup _)) =>
   eapply @listset_nodup_elems : typeclass_instances.
-Hint Extern 1 (Filter _ (listset_nodup _)) =>
-  eapply @listset_nodup_filter : typeclass_instances.