Merge branch 'reorder_requires' into 'master'

Reorder Requires so that we do not depend of Export bugs.

See merge request !313

ProofGuide.md

@@ -6,6 +6,24 @@ This complements the tactic documentation for the [proof mode](ProofMode.md) and
 [HeapLang](HeapLang.md) as well as the documentation of syntactic conventions in
 the [style guide](StyleGuide.md).
 
+## Order of `Requires`
+
+In Coq, declarations in modules imported later may override the
+previous definition. Therefore, in order to make sure the most
+relevant declarations and notations always take priority, we recommend
+importing dependencies from the furthest to the closest.
+
+In particular, when importing Iris, Stdpp and Coq stdlib modules, we
+recommend importing in the following order:
+- Coq
+- stdpp
+- iris.bi
+- iris.proofmode
+- iris.algebra
+- iris.base_logic
+- iris.program_logic
+- iris.heap_lang
+
 ## Combinators for functors
 
 In Iris, the type of propositions [iProp] is described by the solution to the

tests/atomic.v

-From iris.heap_lang Require Export lifting notation.
-From iris.program_logic Require Export atomic.
 From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export atomic.
+From iris.heap_lang Require Export lifting notation.
 From iris.heap_lang Require Import proofmode notation atomic_heap.
 Set Default Proof Using "Type".
 

tests/heap_lang2.v

 (* Test yet another way of importing heap_lang modules that used to break
 printing *)
-From iris.heap_lang Require Export lifting notation.
 From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Export lifting notation.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 

tests/ipm_paper.v

@@ -3,8 +3,8 @@
 Interactive Proofs in Higher-Order Concurrent Separation Logic
 Robbert Krebbers, Amin Timany and Lars Birkedal
 POPL 2017 *)
-From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import base_logic.
 From iris.program_logic Require Export hoare.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".

tests/list_reverse.v

 (** Correctness of in-place list reversal *)
+From iris.proofmode Require Export tactics.
 From iris.program_logic Require Export total_weakestpre weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 

tests/mosel_paper.v

@@ -5,8 +5,8 @@ Separation Logic
 Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti,
 Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
 ICFP 2018 *)
-From iris.proofmode Require Import tactics monpred.
 From iris.bi Require Import monpred.
+From iris.proofmode Require Import tactics monpred.
 
 Lemma example_1 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A → PROP) :
   P ∗ (∃ a, Φ a ∨ Ψ a) -∗ ∃ a, (P ∗ Φ a) ∨ (P ∗ Ψ a).

tests/one_shot.v

+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import excl agree csum.
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
-From iris.algebra Require Import excl agree csum.
 From iris.heap_lang Require Import assert proofmode notation adequacy.
-From iris.proofmode Require Import tactics.
 From iris.heap_lang.lib Require Import par.
 Set Default Proof Using "Type".
 

tests/one_shot_once.v

+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import frac agree csum.
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
-From iris.algebra Require Import frac agree csum.
 From iris.heap_lang Require Import assert proofmode notation adequacy.
-From iris.proofmode Require Import tactics.
 From iris.heap_lang.lib Require Import par.
 Set Default Proof Using "Type".
 

tests/tree_sum.v

+From iris.proofmode Require Export tactics.
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Export lang.
-From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 

theories/algebra/auth.v

+From iris.proofmode Require Import tactics.
 From iris.algebra Require Export frac agree local_updates.
 From iris.algebra Require Import proofmode_classes.
 From iris.base_logic Require Import base_logic.
-From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 (** Authoritative CMRA with fractional authoritative parts. [auth] has 3 types

theories/algebra/big_op.v

-From iris.algebra Require Export monoid.
 From stdpp Require Export functions gmap gmultiset.
+From iris.algebra Require Export monoid.
 Set Default Proof Using "Type*".
 Local Existing Instances monoid_ne monoid_assoc monoid_comm
   monoid_left_id monoid_right_id monoid_proper

theories/algebra/cmra.v

-From iris.algebra Require Export ofe monoid.
 From stdpp Require Import finite.
+From iris.algebra Require Export ofe monoid.
 Set Default Proof Using "Type".
 
 Class PCore (A : Type) := pcore : A → option A.

theories/algebra/cmra_big_op.v

-From iris.algebra Require Export big_op cmra.
 From stdpp Require Import gmap gmultiset.
+From iris.algebra Require Export big_op cmra.
 Set Default Proof Using "Type*".
 
 (** Option *)
@@ -33,4 +33,4 @@ Proof.
   { rewrite big_opMS_empty. set_solver. }
   rewrite -equiv_None big_opMS_disj_union big_opMS_singleton equiv_None op_None IH.
   set_solver.
-Qed.
\ No newline at end of file
+Qed.

theories/algebra/coPset.v

+From stdpp Require Export sets coPset.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
-From stdpp Require Export sets coPset.
 Set Default Proof Using "Type".
 (** This is pretty much the same as algebra/gset, but I was not able to
 generalize the construction without breaking canonical structures. *)

theories/algebra/csum.v

 From iris.algebra Require Export cmra.
-From iris.base_logic Require Import base_logic.
 From iris.algebra Require Import local_updates.
+From iris.base_logic Require Import base_logic.
 Set Default Proof Using "Type".
 Local Arguments pcore _ _ !_ /.
 Local Arguments cmra_pcore _ !_ /.

theories/algebra/frac_auth.v

-From iris.algebra Require Export frac auth.
-From iris.algebra Require Export updates local_updates.
+From iris.algebra Require Export frac auth updates local_updates.
 From iris.algebra Require Import proofmode_classes.
 
 (** Authoritative CMRA where the NON-authoritative parts can be fractional.

theories/algebra/functions.v

+From stdpp Require Import finite.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates.
-From stdpp Require Import finite.
 Set Default Proof Using "Type".
 
 Definition discrete_fun_insert `{EqDecision A} {B : A → ofeT}

theories/algebra/gmap.v

-From iris.algebra Require Export cmra.
 From stdpp Require Export list gmap.
-From iris.algebra Require Import updates local_updates.
+From iris.algebra Require Export cmra.
+From iris.algebra Require Import updates local_updates proofmode_classes.
 From iris.base_logic Require Import base_logic.
-From iris.algebra Require Import proofmode_classes.
 Set Default Proof Using "Type".
 
 Section cofe.

theories/algebra/gmultiset.v

+From stdpp Require Export sets gmultiset countable.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
-From stdpp Require Export sets gmultiset countable.
 Set Default Proof Using "Type".
 
 (* The multiset union CMRA *)

theories/algebra/gset.v

+From stdpp Require Export sets gmap mapset.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
-From stdpp Require Export sets gmap mapset.
 Set Default Proof Using "Type".
 
 (* The union CMRA *)

theories/algebra/list.v

-From iris.algebra Require Export cmra.
 From stdpp Require Export list.
-From iris.base_logic Require Import base_logic.
+From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
+From iris.base_logic Require Import base_logic.
 Set Default Proof Using "Type".
 
 Section cofe.

theories/algebra/namespace_map.v

-From iris.algebra Require Export gmap coPset local_updates.
 From stdpp Require Import namespaces.
-From iris.algebra Require Import updates.
-From iris.algebra Require Import proofmode_classes.
+From iris.algebra Require Export gmap coPset local_updates.
+From iris.algebra Require Import updates proofmode_classes.
 Set Default Proof Using "Type".
 
 (** The camera [namespace_map A] over a camera [A] provides the connectives

theories/algebra/proofmode_classes.v

-From iris.proofmode Require Export classes.
 From iris.algebra Require Export cmra.
+From iris.proofmode Require Export classes.
 
 (* There are various versions of [IsOp] with different modes:
 
@@ -51,4 +51,4 @@ Proof. by constructor. Qed.
 (* This one has a higher precendence than [is_op_op] so we get a [+] instead of
 an [⋅]. *)
 Global Instance is_op_plus (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
-Proof. done. Qed.
\ No newline at end of file
+Proof. done. Qed.

theories/algebra/ufrac_auth.v

@@ -16,11 +16,9 @@ difference:
 - We no longer have the [◯U{1} a] is the exclusive fragmental element (cf.
   [frac_auth_frag_validN_op_1_l]).
 *)
-From iris.algebra Require Export auth frac.
-From iris.algebra Require Import ufrac.
-From iris.algebra Require Export updates local_updates.
-From iris.algebra Require Import proofmode_classes.
 From Coq Require Import QArith Qcanon.
+From iris.algebra Require Export auth frac updates local_updates.
+From iris.algebra Require Import ufrac proofmode_classes.
 
 Definition ufrac_authR (A : cmraT) : cmraT :=
   authR (optionUR (prodR ufracR A)).

theories/base_logic/base_logic.v

-From iris.base_logic Require Export derived proofmode.
 From iris.bi Require Export bi.
+From iris.base_logic Require Export derived proofmode.
 Set Default Proof Using "Type".
 
 (* The trick of having multiple [uPred] modules, which are all exported in

theories/base_logic/bi.v

@@ -43,7 +43,7 @@ Proof.
   - exact: @exist_intro.
   - exact: @exist_elim.
   - exact: sep_mono.
-  - exact: True_sep_1. 
+  - exact: True_sep_1.
   - exact: True_sep_2.
   - exact: sep_comm'.
   - exact: sep_assoc'.

theories/base_logic/bupd_alt.v

-From iris.base_logic Require Export base_logic.
 From iris.proofmode Require Import tactics.
+From iris.base_logic Require Export base_logic.
 
 (** This file contains an alternative version of basic updates, that is
 expression in terms of just the plain modality [■]. *)

theories/base_logic/derived.v

-From iris.base_logic Require Export bi.
 From iris.bi Require Export bi.
+From iris.base_logic Require Export bi.
 Set Default Proof Using "Type".
-Import bi base_logic.bi.uPred.
+Import bi.bi base_logic.bi.uPred.
 
 (** Derived laws for Iris-specific primitive connectives (own, valid).
     This file does NOT unseal! *)

theories/base_logic/lib/auth.v

-From iris.base_logic.lib Require Export invariants.
+From iris.proofmode Require Import tactics.
 From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
-From iris.proofmode Require Import tactics.
+From iris.base_logic.lib Require Export invariants.
 Set Default Proof Using "Type".
 Import uPred.
 

theories/base_logic/lib/boxes.v

-From iris.base_logic.lib Require Export invariants.
-From iris.algebra Require Import excl auth gmap agree.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import excl auth gmap agree.
+From iris.base_logic.lib Require Export invariants.
 Set Default Proof Using "Type".
 Import uPred.
 
@@ -131,7 +131,7 @@ Proof.
   iIntros (??) "[#HγQ Hinv] H". iDestruct "H" as (Φ) "[#HeqP Hf]".
   iExists ([∗ map] γ'↦_ ∈ delete γ f, Φ γ')%I.
   iInv N as (b) "[>Hγ _]".
-  iDestruct (big_opM_delete _ f _ false with "Hf")
+  iDestruct (big_sepM_delete _ f _ false with "Hf")
     as "[[>Hγ' #[HγΦ ?]] ?]"; first done.
   iDestruct (box_own_auth_agree γ b false with "[-]") as %->; first by iFrame.
   iModIntro. iSplitL "Hγ"; first iExists false; eauto.
@@ -148,7 +148,7 @@ Lemma slice_fill E q f γ P Q :
 Proof.
   iIntros (??) "#[HγQ Hinv] HQ H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iInv N as (b') "[>Hγ _]".
-  iDestruct (big_opM_delete _ f _ false with "Hf")
+  iDestruct (big_sepM_delete _ f _ false with "Hf")
     as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
   iMod (box_own_auth_update γ b' false true with "[$Hγ $Hγ']") as "[Hγ Hγ']".
   iModIntro. iSplitL "Hγ HQ"; first (iNext; iExists true; by iFrame).
@@ -165,7 +165,7 @@ Lemma slice_empty E q f P Q γ :
 Proof.
   iIntros (??) "#[HγQ Hinv] H"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iInv N as (b) "[>Hγ HQ]".
-  iDestruct (big_opM_delete _ f with "Hf")
+  iDestruct (big_sepM_delete _ f with "Hf")
     as "[[>Hγ' #[HγΦ Hinv']] ?]"; first done.
   iDestruct (box_own_auth_agree γ b true with "[-]") as %->; first by iFrame.
   iFrame "HQ".

theories/base_logic/lib/cancelable_invariants.v

-From iris.base_logic.lib Require Export invariants.
 From iris.bi.lib Require Import fractional.
-From iris.algebra Require Export frac.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Export frac.
+From iris.base_logic.lib Require Export invariants.
 Set Default Proof Using "Type".
 Import uPred.
 

theories/base_logic/lib/fancy_updates.v

-From iris.base_logic.lib Require Export own.
 From stdpp Require Export coPset.
-From iris.base_logic.lib Require Import wsat.
-From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import gmap auth agree gset coPset.
+From iris.base_logic.lib Require Export own.
+From iris.base_logic.lib Require Import wsat.
 Set Default Proof Using "Type".
 Export invG.
 Import uPred.

theories/base_logic/lib/fancy_updates_from_vs.v

 (* This file shows that the fancy update can be encoded in terms of the
 view shift, and that the laws of the fancy update can be derived from the
 laws of the view shift. *)
-From iris.base_logic Require Export base_logic.
-From iris.proofmode Require Import tactics.
 From stdpp Require Export coPset.
+From iris.proofmode Require Import tactics.
+From iris.base_logic Require Export base_logic.
 Set Default Proof Using "Type*".
 
 Section fupd.

theories/base_logic/lib/gen_heap.v

-From iris.algebra Require Import auth gmap frac agree namespace_map.
 From stdpp Require Export namespaces.
-From iris.base_logic.lib Require Export own.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth gmap frac agree namespace_map.
+From iris.base_logic.lib Require Export own.
 Set Default Proof Using "Type".
 Import uPred.
 

theories/base_logic/lib/invariants.v

-From iris.base_logic.lib Require Export fancy_updates.
 From stdpp Require Export namespaces.
-From iris.base_logic.lib Require Import wsat.
-From iris.algebra Require Import gmap.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import gmap.
+From iris.base_logic.lib Require Export fancy_updates.
+From iris.base_logic.lib Require Import wsat.
 Set Default Proof Using "Type".
 Import uPred.
 

theories/base_logic/lib/iprop.v

-From iris.base_logic Require Export base_logic.
 From iris.algebra Require Import gmap.
 From iris.algebra Require cofe_solver.
+From iris.base_logic Require Export base_logic.
 Set Default Proof Using "Type".
 
 (** In this file we construct the type [iProp] of propositions of the Iris

theories/base_logic/lib/na_invariants.v

-From iris.base_logic.lib Require Export invariants.
-From iris.algebra Require Import gset coPset.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import gset coPset.
+From iris.base_logic.lib Require Export invariants.
 Set Default Proof Using "Type".
 Import uPred.
 

theories/base_logic/lib/own.v

-From iris.algebra Require Import functions gmap.
+From iris.algebra Require Import functions gmap proofmode_classes.
 From iris.base_logic.lib Require Export iprop.
-From iris.algebra Require Import proofmode_classes.
 Set Default Proof Using "Type".
 Import uPred.
 

theories/base_logic/lib/proph_map.v

+From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth excl list gmap.
 From iris.base_logic.lib Require Export own.
-From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 

theories/base_logic/lib/saved_prop.v

-From iris.base_logic Require Export own.
-From iris.algebra Require Import agree.
 From stdpp Require Import gmap.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import agree.
+From iris.base_logic Require Export own.
 Set Default Proof Using "Type".
 Import uPred.
 

theories/base_logic/lib/sts.v

-From iris.base_logic.lib Require Export invariants.
-From iris.algebra Require Export sts.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Export sts.
+From iris.base_logic.lib Require Export invariants.
 Set Default Proof Using "Type".
 Import uPred.
 

theories/base_logic/lib/viewshifts.v

-From iris.base_logic.lib Require Export invariants.
 From iris.proofmode Require Import tactics.
+From iris.base_logic.lib Require Export invariants.
 Set Default Proof Using "Type".
 
 Definition vs `{!invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=

theories/base_logic/lib/wsat.v

-From iris.base_logic.lib Require Export own.
 From stdpp Require Export coPset.
-From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import gmap auth agree gset coPset.
+From iris.base_logic.lib Require Export own.
 Set Default Proof Using "Type".
 
 (** All definitions in this file are internal to [fancy_updates] with the
@@ -129,9 +129,9 @@ Proof.
   rewrite /ownI /wsat -!lock.
   iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[Hw HI]".
   iDestruct (invariant_lookup I i P with "[$]") as (Q ?) "#HPQ".
-  iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
+  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
   - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
-    iExists I. iFrame "Hw". iApply (big_opM_delete _ _ i); eauto.
+    iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
     iFrame "HI"; eauto.
   - iDestruct (ownE_singleton_twice with "[$HiE $HiE']") as %[].
 Qed.
@@ -140,9 +140,9 @@ Proof.
   rewrite /ownI /wsat -!lock.
   iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[Hw HI]".
   iDestruct (invariant_lookup with "[$]") as (Q ?) "#HPQ".
-  iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
+  iDestruct (big_sepM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
   - iDestruct (ownD_singleton_twice with "[$]") as %[].
-  - iExists I. iFrame "Hw". iApply (big_opM_delete _ _ i); eauto.
+  - iExists I. iFrame "Hw". iApply (big_sepM_delete _ _ i); eauto.
     iFrame "HI". iLeft. iFrame "HiD". by iNext; iRewrite "HPQ".
 Qed.
 
@@ -165,7 +165,7 @@ Proof.
   iModIntro; iExists i;  iSplit; [done|]. rewrite /ownI; iFrame "HiP".
   iExists (<[i:=P]>I); iSplitL "Hw".
   { by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
-  iApply (big_opM_insert _ I); first done.
+  iApply (big_sepM_insert _ I); first done.
   iFrame "HI". iLeft. by rewrite /ownD; iFrame.
 Qed.
 
@@ -188,7 +188,7 @@ Proof.
   rewrite -/(ownD _). iFrame "HD".
   iIntros "HE". iExists (<[i:=P]>I); iSplitL "Hw".
   { by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
-  iApply (big_opM_insert _ I); first done.
+  iApply (big_sepM_insert _ I); first done.
   iFrame "HI". by iRight.
 Qed.
 End wsat.

theories/base_logic/proofmode.v

-From iris.base_logic Require Export derived.
 From iris.algebra Require Import proofmode_classes.
+From iris.base_logic Require Export derived.
 
 Import base_logic.bi.uPred.
 

theories/base_logic/upred.v

-From iris.algebra Require Export cmra updates.
-From iris.bi Require Import notation.
 From stdpp Require Import finite.
-From Coq.Init Require Import Nat.
+From iris.bi Require Import notation.
+From iris.algebra Require Export cmra updates.
 Set Default Proof Using "Type".
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|] : core.
 Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption] : core.

theories/bi/big_op.v

-From iris.algebra Require Export big_op.
-From iris.bi Require Import derived_laws_sbi.
 From stdpp Require Import countable fin_sets functions.
+From iris.bi Require Import derived_laws_sbi.
+From iris.algebra Require Export big_op.
 Set Default Proof Using "Type".
 Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
 

theories/bi/embedding.v

-From iris.algebra Require Import monoid.
 From iris.bi Require Import interface derived_laws_sbi big_op plainly updates.
+From iris.algebra Require Import monoid.
 
 Class Embed (A B : Type) := embed : A → B.
 Arguments embed {_ _ _} _%I : simpl never.

theories/bi/interface.v

-From iris.algebra Require Export ofe.
 From iris.bi Require Export notation.
+From iris.algebra Require Export ofe.
 Set Primitive Projections.
 
 Section bi_mixin.

theories/bi/lib/atomic.v

+From stdpp Require Import coPset namespaces.
 From iris.bi Require Export bi updates laterable.
 From iris.bi.lib Require Import fixpoint.
-From stdpp Require Import coPset namespaces.
 From iris.proofmode Require Import coq_tactics tactics reduction.
 Set Default Proof Using "Type".
 

theories/bi/weakestpre.v

 From stdpp Require Export coPset.
-From iris.program_logic Require Import language.
 From iris.bi Require Import interface derived_connectives.
+From iris.program_logic Require Import language.
 
 Inductive stuckness := NotStuck | MaybeStuck.
 

theories/heap_lang/adequacy.v

-From iris.program_logic Require Export weakestpre adequacy.
+From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth.