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

README.md

@@ -20,33 +20,35 @@ Run `make` to build the full development.
 
 ## Structure
 
-* The folder [prelude](prelude) contains an extended "Standard Library" by
-  [Robbert Krebbers](http://robbertkrebbers.nl/thesis.html).
-* The folder [algebra](algebra) contains the COFE and CMRA constructions as well
-  as the solver for recursive domain equations.
-* The folder [base_logic](base_logic) defines the Iris base logic and the
-  primitive connectives.  It also contains derived constructions that are
+* The folder [prelude](theories/prelude) contains an extended "Standard Library"
+  by [Robbert Krebbers](http://robbertkrebbers.nl/thesis.html).
+* The folder [algebra](theories/algebra) contains the COFE and CMRA
+  constructions as well as the solver for recursive domain equations.
+* The folder [base_logic](theories/base_logic) defines the Iris base logic and
+  the primitive connectives.  It also contains derived constructions that are
   entirely independent of the choice of resources.
-  * The subfolder [lib](base_logic/lib) contains some generally useful
+  * The subfolder [lib](theories/base_logic/lib) contains some generally useful
     derived constructions.  Most importantly, it defines composeable
     dynamic resources and ownership of them; the other constructions depend
     on this setup.
-* The folder [program_logic](program_logic) specializes the base logic to build
-  Iris, the program logic.   This includes weakest preconditions that are
-  defined for any language satisfying some generic axioms, and some derived
+* The folder [program_logic](theories/program_logic) specializes the base logic
+  to build Iris, the program logic.   This includes weakest preconditions that
+  are defined for any language satisfying some generic axioms, and some derived
   constructions that work for any such language.
-* The folder [proofmode](proofmode) contains the Iris proof mode, which extends
-  Coq with contexts for persistent and spatial Iris assertions. It also contains
-  tactics for interactive proofs in Iris. Documentation can be found in
+* The folder [proofmode](theories/proofmode) contains the Iris proof mode, which
+  extends Coq with contexts for persistent and spatial Iris assertions. It also
+  contains tactics for interactive proofs in Iris. Documentation can be found in
   [ProofMode.md](ProofMode.md).
-* The folder [heap_lang](heap_lang) defines the ML-like concurrent heap language
-  * The subfolder [lib](heap_lang/lib) contains a few derived constructions
-    within this language, e.g., parallel composition.
-    Most notable here is [lib/barrier](heap_lang/lib/barrier), the implementation
-    and proof of a barrier as described in <http://doi.acm.org/10.1145/2818638>.
-* The folder [tests](tests) contains modules we use to test our infrastructure.
-  Users of the Iris Coq library should *not* depend on these modules; they may
-  change or disappear without any notice.
+* The folder [heap_lang](theories/heap_lang) defines the ML-like concurrent heap
+  language
+  * The subfolder [lib](theories/heap_lang/lib) contains a few derived
+    constructions within this language, e.g., parallel composition.
+    Most notable here is [lib/barrier](theories/heap_lang/lib/barrier), the
+    implementation and proof of a barrier as described in
+    <http://doi.acm.org/10.1145/2818638>.
+* The folder [tests](theories/tests) contains modules we use to test our
+  infrastructure. Users of the Iris Coq library should *not* depend on these
+  modules; they may change or disappear without any notice.
 
 ## Documentation
 

theories/base_logic/lib/invariants.v

@@ -28,44 +28,39 @@ Qed.
 Global Instance inv_persistent N P : PersistentP (inv N P).
 Proof. rewrite inv_eq /inv; apply _. Qed.
 
+Lemma fresh_inv_name (E : gset positive) N : ∃ i, i ∉ E ∧ i ∈ ↑N.
+Proof.
+  exists (coPpick (↑ N ∖ coPset.of_gset E)).
+  rewrite -coPset.elem_of_of_gset (comm and) -elem_of_difference.
+  apply coPpick_elem_of=> Hfin.
+  eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
+  apply of_gset_finite.
+Qed.
+
 Lemma inv_alloc N E P : ▷ P ={E}=∗ inv N P.
 Proof.
   rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]".
-  iMod (ownI_alloc (∈ ↑ N) P with "[HP Hw]") as (i) "(% & $ & ?)"; auto.
-  - intros Ef. exists (coPpick (↑ N ∖ coPset.of_gset Ef)).
-    rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
-    apply coPpick_elem_of=> Hfin.
-    eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
-    apply of_gset_finite.
-  - by iFrame.
-  - rewrite /uPred_except_0; eauto.
+  iMod (ownI_alloc (∈ ↑ N) P with "[$HP $Hw]")
+    as (i) "(% & $ & ?)"; auto using fresh_inv_name.
 Qed.
 
 Lemma inv_alloc_open N E P :
   ↑N ⊆ E → True ={E, E∖↑N}=∗ inv N P ∗ (▷P ={E∖↑N, E}=∗ True).
 Proof.
-  rewrite inv_eq /inv_def fupd_eq /fupd_def.
-  iIntros (Sub) "[Hw HE]".
-  iMod (ownI_alloc_open (∈ ↑ N) P with "Hw") as (i) "(% & Hw & #Hi & HD)".
-  - intros Ef. exists (coPpick (↑ N ∖ coPset.of_gset Ef)).
-    rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
-    apply coPpick_elem_of=> Hfin.
-    eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
-    apply of_gset_finite.
-  - iAssert (ownE {[i]} ∗ ownE (↑ N ∖ {[i]}) ∗ ownE (E ∖ ↑ N))%I with "[HE]" as "(HEi & HEN\i & HE\N)".
-    { rewrite -?ownE_op; [|set_solver|set_solver].
-      rewrite assoc_L. rewrite <-!union_difference_L; try done; set_solver. }
-    iModIntro. rewrite /uPred_except_0. iRight. iFrame.
-    iSplitL "Hw HEi".
-    + by iApply "Hw".
-    + iSplitL "Hi"; [eauto|].
-      iIntros "HP [Hw HE\N]".
-      iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[? HEi]".
-      iModIntro. iRight. iFrame. iSplitL; [|done].
-      iCombine "HEi" "HEN\i" as "HEN".
-      iCombine "HEN" "HE\N" as "HE".
-      rewrite -?ownE_op; [|set_solver|set_solver].
-      rewrite <-!union_difference_L; try done; set_solver.
+  rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros (Sub) "[Hw HE]".
+  iMod (ownI_alloc_open (∈ ↑ N) P with "Hw")
+    as (i) "(% & Hw & #Hi & HD)"; auto using fresh_inv_name.
+  iAssert (ownE {[i]} ∗ ownE (↑ N ∖ {[i]}) ∗ ownE (E ∖ ↑ N))%I
+    with "[HE]" as "(HEi & HEN\i & HE\N)".
+  { rewrite -?ownE_op; [|set_solver..].
+    rewrite assoc_L -!union_difference_L //. set_solver. }
+  do 2 iModIntro. iFrame "HE\N". iSplitL "Hw HEi"; first by iApply "Hw".
+  iSplitL "Hi"; first by eauto. iIntros "HP [Hw HE\N]".
+  iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[$ HEi]".
+  do 2 iModIntro. iSplitL; [|done].
+  iCombine "HEi" "HEN\i" as "HEN"; iCombine "HEN" "HE\N" as "HE".
+  rewrite -?ownE_op; [|set_solver..].
+  rewrite -!union_difference_L //; set_solver.
 Qed.
 
 Lemma inv_open E N P :

theories/base_logic/lib/sts.v

@@ -45,9 +45,9 @@ Section definitions.
   Proof. solve_proper. Qed.
   Global Instance sts_ctx_persistent `{!invG Σ} N φ : PersistentP (sts_ctx N φ).
   Proof. apply _. Qed.
-  Global Instance sts_own_peristent s : PersistentP (sts_own s ∅).
+  Global Instance sts_own_persistent s : PersistentP (sts_own s ∅).
   Proof. apply _. Qed.
-  Global Instance sts_ownS_peristent S : PersistentP (sts_ownS S ∅).
+  Global Instance sts_ownS_persistent S : PersistentP (sts_ownS S ∅).
   Proof. apply _. Qed.
 End definitions.
 

theories/base_logic/lib/wsat.v

@@ -165,5 +165,4 @@ Proof.
   iApply (big_sepM_insert _ I); first done.
   iFrame "HI". by iRight.
 Qed.
-
 End wsat.

theories/prelude/fin_maps.v

@@ -119,13 +119,13 @@ Context `{FinMap K M}.
 (** ** Setoids *)
 Section setoid.
   Context `{Equiv A}.
-  
+
   Lemma map_equiv_lookup_l (m1 m2 : M A) i x :
     m1 ≡ m2 → m1 !! i = Some x → ∃ y, m2 !! i = Some y ∧ x ≡ y.
   Proof. generalize (equiv_Some_inv_l (m1 !! i) (m2 !! i) x); naive_solver. Qed.
 
-  Context `{!Equivalence ((≡) : relation A)}.
-  Global Instance map_equivalence : Equivalence ((≡) : relation (M A)).
+  Global Instance map_equivalence :
+    Equivalence ((≡) : relation A) → Equivalence ((≡) : relation (M A)).
   Proof.
     split.
     - by intros m i.
@@ -147,7 +147,10 @@ Section setoid.
   Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
   Global Instance singleton_proper k :
     Proper ((≡) ==> (≡)) (singletonM k : A → M A).
-  Proof. by intros ???; apply insert_proper. Qed.
+  Proof.
+    intros ???; apply insert_proper; [done|].
+    intros ?. rewrite lookup_empty; constructor.
+  Qed.
   Global Instance delete_proper (i : K) :
     Proper ((≡) ==> (≡)) (delete (M:=M A) i).
   Proof. by apply partial_alter_proper; [constructor|]. Qed.
@@ -170,14 +173,12 @@ Section setoid.
     by do 2 destruct 1; first [apply Hf | constructor].
   Qed.
   Global Instance map_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (M A).
-  Proof.
-    intros m1 m2 Hm; apply map_eq; intros i.
-    by unfold_leibniz; apply lookup_proper.
-  Qed.
+  Proof. intros m1 m2 Hm; apply map_eq; intros i. apply leibniz_equiv, Hm. Qed.
   Lemma map_equiv_empty (m : M A) : m ≡ ∅ ↔ m = ∅.
   Proof.
-    split; [intros Hm; apply map_eq; intros i|by intros ->].
-    by rewrite lookup_empty, <-equiv_None, Hm, lookup_empty.
+    split; [intros Hm; apply map_eq; intros i|intros ->].
+    - generalize (Hm i). by rewrite lookup_empty, equiv_None.
+    - intros ?. rewrite lookup_empty; constructor.
   Qed.
   Global Instance map_fmap_proper `{Equiv B} (f : A → B) :
     Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap (M:=M) f).

theories/prelude/list.v

@@ -2753,9 +2753,8 @@ Section setoid.
     by setoid_rewrite equiv_option_Forall2.
   Qed.
 
-  Context {Hequiv: Equivalence ((≡) : relation A)}.
-
-  Global Instance list_equivalence : Equivalence ((≡) : relation (list A)).
+  Global Instance list_equivalence :
+    Equivalence ((≡) : relation A) → Equivalence ((≡) : relation (list A)).
   Proof.
     split.
     - intros l. by apply equiv_Forall2.
@@ -2766,48 +2765,53 @@ Section setoid.
   Proof. induction 1; f_equal; fold_leibniz; auto. Qed.
 
   Global Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡)) (@cons A).
-  Proof using -(Hequiv). by constructor. Qed.
+  Proof. by constructor. Qed.
   Global Instance app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@app A).
-  Proof using -(Hequiv). induction 1; intros ???; simpl; try constructor; auto. Qed.
+  Proof. induction 1; intros ???; simpl; try constructor; auto. Qed.
   Global Instance length_proper : Proper ((≡) ==> (=)) (@length A).
-  Proof using -(Hequiv). induction 1; f_equal/=; auto. Qed.
+  Proof. induction 1; f_equal/=; auto. Qed.
   Global Instance tail_proper : Proper ((≡) ==> (≡)) (@tail A).
-  Proof. by destruct 1. Qed.
+  Proof. destruct 1; try constructor; auto. Qed.
   Global Instance take_proper n : Proper ((≡) ==> (≡)) (@take A n).
-  Proof using -(Hequiv). induction n; destruct 1; constructor; auto. Qed.
+  Proof. induction n; destruct 1; constructor; auto. Qed.
   Global Instance drop_proper n : Proper ((≡) ==> (≡)) (@drop A n).
-  Proof using -(Hequiv). induction n; destruct 1; simpl; try constructor; auto. Qed.
+  Proof. induction n; destruct 1; simpl; try constructor; auto. Qed.
   Global Instance list_lookup_proper i :
     Proper ((≡) ==> (≡)) (lookup (M:=list A) i).
-  Proof. induction i; destruct 1; simpl; f_equiv; auto. Qed.
+  Proof. induction i; destruct 1; simpl; try constructor; auto. Qed.
   Global Instance list_alter_proper f i :
     Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (alter (M:=list A) f i).
-  Proof using -(Hequiv). intros. induction i; destruct 1; constructor; eauto. Qed.
+  Proof. intros. induction i; destruct 1; constructor; eauto. Qed.
   Global Instance list_insert_proper i :
     Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=list A) i).
-  Proof using -(Hequiv). intros ???; induction i; destruct 1; constructor; eauto. Qed.
+  Proof. intros ???; induction i; destruct 1; constructor; eauto. Qed.
   Global Instance list_inserts_proper i :
     Proper ((≡) ==> (≡) ==> (≡)) (@list_inserts A i).
-  Proof using -(Hequiv).
+  Proof.
     intros k1 k2 Hk; revert i.
     induction Hk; intros ????; simpl; try f_equiv; naive_solver.
   Qed.
   Global Instance list_delete_proper i :
     Proper ((≡) ==> (≡)) (delete (M:=list A) i).
-  Proof using -(Hequiv). induction i; destruct 1; try constructor; eauto. Qed.
+  Proof. induction i; destruct 1; try constructor; eauto. Qed.
   Global Instance option_list_proper : Proper ((≡) ==> (≡)) (@option_list A).
-  Proof. destruct 1; by constructor. Qed.
+  Proof. destruct 1; repeat constructor; auto. Qed.
   Global Instance list_filter_proper P `{∀ x, Decision (P x)} :
     Proper ((≡) ==> iff) P → Proper ((≡) ==> (≡)) (filter (B:=list A) P).
-  Proof using -(Hequiv). intros ???. rewrite !equiv_Forall2. by apply Forall2_filter. Qed.
+  Proof. intros ???. rewrite !equiv_Forall2. by apply Forall2_filter. Qed.
   Global Instance replicate_proper n : Proper ((≡) ==> (≡)) (@replicate A n).
-  Proof using -(Hequiv). induction n; constructor; auto. Qed.
+  Proof. induction n; constructor; auto. Qed.
   Global Instance reverse_proper : Proper ((≡) ==> (≡)) (@reverse A).
-  Proof. induction 1; rewrite ?reverse_cons; repeat (done || f_equiv). Qed.
+  Proof.
+    induction 1; rewrite ?reverse_cons; simpl; [constructor|].
+    apply app_proper; repeat constructor; auto.
+  Qed.
   Global Instance last_proper : Proper ((≡) ==> (≡)) (@last A).
-  Proof. induction 1 as [|????? []]; simpl; repeat (done || f_equiv). Qed.
+  Proof. induction 1 as [|????? []]; simpl; repeat constructor; auto. Qed.
   Global Instance resize_proper n : Proper ((≡) ==> (≡) ==> (≡)) (@resize A n).
-  Proof. induction n; destruct 2; simpl; repeat (auto || f_equiv). Qed.
+  Proof.
+    induction n; destruct 2; simpl; repeat (constructor || f_equiv); auto.
+  Qed.
 End setoid.
 
 (** * Properties of the monadic operations *)

theories/prelude/option.v

@@ -115,36 +115,38 @@ End Forall2.
 Instance option_equiv `{Equiv A} : Equiv (option A) := option_Forall2 (≡).
 
 Section setoids.
-  Context `{Equiv A} {Hequiv: Equivalence ((≡) : relation A)}.
+  Context `{Equiv A}.
   Implicit Types mx my : option A.
 
   Lemma equiv_option_Forall2 mx my : mx ≡ my ↔ option_Forall2 (≡) mx my.
-  Proof using -(Hequiv). done. Qed.
+  Proof. done. Qed.
 
-  Global Instance option_equivalence : Equivalence ((≡) : relation (option A)).
+  Global Instance option_equivalence :
+    Equivalence ((≡) : relation A) → Equivalence ((≡) : relation (option A)).
   Proof. apply _. Qed.
   Global Instance Some_proper : Proper ((≡) ==> (≡)) (@Some A).
-  Proof using -(Hequiv). by constructor. Qed.
+  Proof. by constructor. Qed.
   Global Instance Some_equiv_inj : Inj (≡) (≡) (@Some A).
-  Proof using -(Hequiv). by inversion_clear 1. Qed.
+  Proof. by inversion_clear 1. Qed.
   Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
-  Proof. intros x y; destruct 1; fold_leibniz; congruence. Qed.
+  Proof. intros x y; destruct 1; f_equal; by apply leibniz_equiv. Qed.
 
   Lemma equiv_None mx : mx ≡ None ↔ mx = None.
-  Proof. split; [by inversion_clear 1|by intros ->]. Qed.
+  Proof. split; [by inversion_clear 1|intros ->; constructor]. Qed.
   Lemma equiv_Some_inv_l mx my x :
     mx ≡ my → mx = Some x → ∃ y, my = Some y ∧ x ≡ y.
-  Proof using -(Hequiv). destruct 1; naive_solver. Qed.
+  Proof. destruct 1; naive_solver. Qed.
   Lemma equiv_Some_inv_r mx my y :
     mx ≡ my → my = Some y → ∃ x, mx = Some x ∧ x ≡ y.
-  Proof using -(Hequiv). destruct 1; naive_solver. Qed.
+  Proof. destruct 1; naive_solver. Qed.
   Lemma equiv_Some_inv_l' my x : Some x ≡ my → ∃ x', Some x' = my ∧ x ≡ x'.
-  Proof using -(Hequiv). intros ?%(equiv_Some_inv_l _ _ x); naive_solver. Qed.
-  Lemma equiv_Some_inv_r' mx y : mx ≡ Some y → ∃ y', mx = Some y' ∧ y ≡ y'.
+  Proof. intros ?%(equiv_Some_inv_l _ _ x); naive_solver. Qed.
+  Lemma equiv_Some_inv_r' `{!Equivalence ((≡) : relation A)} mx y :
+    mx ≡ Some y → ∃ y', mx = Some y' ∧ y ≡ y'.
   Proof. intros ?%(equiv_Some_inv_r _ _ y); naive_solver. Qed.
 
   Global Instance is_Some_proper : Proper ((≡) ==> iff) (@is_Some A).
-  Proof using -(Hequiv). inversion_clear 1; split; eauto. Qed.
+  Proof. inversion_clear 1; split; eauto. Qed.
   Global Instance from_option_proper {B} (R : relation B) (f : A → B) :
     Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f).
   Proof. destruct 3; simpl; auto. Qed.

theories/proofmode/tactics.v

@@ -1280,6 +1280,7 @@ Hint Extern 1 (of_envs _ ⊢ _) =>
   | |- _ ⊢ □ _ => iClear "*"; iAlways
   | |- _ ⊢ ∃ _, _ => iExists _
   | |- _ ⊢ |==> _ => iModIntro
+  | |- _ ⊢ ◇ _ => iModIntro
   end.
 Hint Extern 1 (of_envs _ ⊢ _) =>
   match goal with |- _ ⊢ (_ ∨ _)%I => iLeft end.