...
 
Commits (2)
......@@ -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
......
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".
......
(* 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".
......
......@@ -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".
......
(** 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".
......
......@@ -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).
......
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".
......
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".
......
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".
......
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
......
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
......
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.
......
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.
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. *)
......
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 _ !_ /.
......
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.
......
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}
......
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.
......
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 *)
......
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 *)
......
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.
......
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
......
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.
......@@ -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)).
......
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
......
......@@ -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'.
......
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 [■]. *)
......
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! *)
......
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.
......
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".
......
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.
......
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.
......
(* 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.
......
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.
......
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.
......
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
......
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.
......
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.
......
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.
......
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.
......
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.
......
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 Σ :=
......
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.
......
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.
......
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.
......
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.
......
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.
......
From iris.algebra Require Export ofe.
From iris.bi Require Export notation.
From iris.algebra Require Export ofe.
Set Primitive Projections.
Section bi_mixin.
......
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".
......
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.
......
From iris.program_logic Require Export weakestpre adequacy.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth.
From iris.heap_lang Require Import proofmode notation.
From iris.base_logic.lib Require Import proph_map.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre adequacy.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Class heapPreG Σ := HeapPreG {
......
From stdpp Require Import fin_maps.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lifting.
From iris.heap_lang Require Import tactics notation.
From iris.proofmode Require Import tactics.
From stdpp Require Import fin_maps.
Set Default Proof Using "Type".
(** This file defines the [array] connective, a version of [mapsto] that works
......
From iris.program_logic Require Export language ectx_language ectxi_language.
From iris.heap_lang Require Export locations.
From iris.algebra Require Export ofe.
From stdpp Require Export binders strings.
From stdpp Require Import gmap.
From iris.algebra Require Export ofe.
From iris.program_logic Require Export language ectx_language ectxi_language.
From iris.heap_lang Require Export locations.
Set Default Proof Using "Type".
(** heap_lang. A fairly simple language used for common Iris examples.
......
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
From iris.heap_lang Require Export lifting notation.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.bi.lib Require Import fractional.
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.
Set Default Proof Using "Type".
(** A general logically atomic interface for a heap. *)
......
From iris.program_logic Require Export weakestpre.
From iris.base_logic.lib Require Export invariants.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac_auth auth.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation atomic_heap par.
From iris.bi.lib Require Import fractional.
Set Default Proof Using "Type".
(** Show that implementing fetch-and-add on top of CAS preserves logical
......
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export invariants.
From iris.heap_lang Require Export lifting notation.
Set Default Proof Using "Type".
Structure lock Σ `{!heapG Σ} := Lock {
......@@ -36,4 +36,3 @@ Existing Instances is_lock_ne is_lock_persistent locked_timeless.
Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) N γ lk:
Proper (() ==> ()) (is_lock L N γ lk) := ne_proper _.
From iris.heap_lang Require Export spawn.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Export spawn.
Set Default Proof Using "Type".
Import uPred.
......
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
Set Default Proof Using "Type".
Definition spawn : val :=
......
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
From iris.heap_lang.lib Require Import lock.
Set Default Proof Using "Type".
......
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl auth gset.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl auth gset.
From iris.heap_lang.lib Require Export lock.
Set Default Proof Using "Type".
Import uPred.
......
From stdpp Require Import fin_maps.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth gmap.
From iris.base_logic Require Export gen_heap.
From iris.base_logic.lib Require Export proph_map.
......@@ -5,8 +7,6 @@ From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics notation.
From iris.proofmode Require Import tactics.
From stdpp Require Import fin_maps.
Set Default Proof Using "Type".
Class heapG Σ := HeapG {
......
From iris.algebra Require Import base.
From stdpp Require Import countable numbers gmap.
From iris.algebra Require Import base.
Record loc := { loc_car : Z }.
......
From iris.heap_lang Require Export lang.
From stdpp Require Import gmap.
From iris.heap_lang Require Export lang.
(* This file contains some metatheory about the heap_lang language,
which is not needed for verifying programs. *)
......
From iris.program_logic Require Export weakestpre total_weakestpre.
From iris.program_logic Require Import atomic.
From iris.proofmode Require Import coq_tactics reduction.
From iris.proofmode Require Export tactics.
From iris.program_logic Require Export weakestpre total_weakestpre.
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Export tactics lifting array.
From iris.heap_lang Require Import notation.
Set Default Proof Using "Type".
......
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export total_adequacy.
From iris.heap_lang Require Export adequacy.
From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Definition heap_total Σ `{!heapPreG Σ} s e σ φ :
......
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import gmap auth agree gset coPset.
From iris.base_logic.lib Require Import wsat.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
Set Default Proof Using "Type".
Import uPred.
......
From stdpp Require Import namespaces.
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics classes.
From iris.bi.lib Require Export atomic.
From iris.bi Require Import telescopes.
From iris.bi.lib Require Export atomic.
From iris.proofmode Require Import tactics classes.
From iris.program_logic Require Export weakestpre.
Set Default Proof Using "Type".
(* This hard-codes the inner mask to be empty, because we have yet to find an
......
(** Some derived lemmas for ectx-based languages *)
From iris.program_logic Require Export ectx_language weakestpre lifting.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export ectx_language weakestpre lifting.
Set Default Proof Using "Type".
Section wp.
......
From iris.program_logic Require Export weakestpre.
From iris.base_logic.lib Require Export viewshifts.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export viewshifts.
From iris.program_logic Require Export weakestpre.
Set Default Proof Using "Type".
Definition ht `{!irisG Λ Σ} (s : stuckness) (E : coPset) (P : iProp Σ)
......
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
Set Default Proof Using "Type".
Section lifting.
......
From iris.proofmode Require Import tactics classes.
From iris.algebra Require Import excl auth.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import lifting adequacy.
From iris.program_logic Require ectx_language.
From iris.algebra Require Import excl auth.
From iris.proofmode Require Import tactics classes.
Set Default Proof Using "Type".
(**
......
From iris.program_logic Require Export total_weakestpre adequacy.
From iris.algebra Require Import gmap auth agree gset coPset list.
From iris.bi Require Import big_op fixpoint.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import gmap auth agree gset coPset list.
From iris.program_logic Require Export total_weakestpre adequacy.
Set Default Proof Using "Type".
Import uPred.
......
(** Some derived lemmas for ectx-based languages *)
From iris.program_logic Require Export ectx_language.
From iris.program_logic Require Export total_weakestpre total_lifting.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export ectx_language total_weakestpre total_lifting.
Set Default Proof Using "Type".
Section wp.
......
From iris.program_logic Require Export total_weakestpre.
From iris.bi Require Export big_op.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export total_weakestpre.
Set Default Proof Using "Type".
Section lifting.
......
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics.
From iris.bi Require Import fixpoint big_op.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
Set Default Proof Using "Type".
Import uPred.
......
From iris.proofmode Require Import base tactics classes.
From iris.base_logic.lib Require Export fancy_updates.
From iris.program_logic Require Export language.
(* FIXME: If we import iris.bi.weakestpre earlier texan triples do not
get pretty-printed correctly. *)
From iris.bi Require Export weakestpre.
From iris.proofmode Require Import base tactics classes.
Set Default Proof Using "Type".
Import uPred.
......
From Coq Require Export Ascii.
From stdpp Require Export strings.
From iris.algebra Require Export base.
From Coq Require Export Ascii.
Set Default Proof Using "Type".
(** * Utility definitions used by the proofmode *)
......
From stdpp Require Import namespaces.
From iris.bi Require Export bi.
From iris.proofmode Require Import base.
From iris.proofmode Require Export modalities.
From stdpp Require Import namespaces.
Set Default Proof Using "Type".
Import bi.
......
From iris.proofmode Require Import base.
From iris.algebra Require Export base.
From iris.bi Require Export bi.
From iris.bi Require Import tactics.
From iris.proofmode Require Import base.
From iris.algebra Require Export base.
Set Default Proof Using "Type".
Import bi.
......
From iris.proofmode Require Import coq_tactics reduction.
From iris.proofmode Require Import base intro_patterns spec_patterns sel_patterns.
From stdpp Require Import namespaces hlist pretty.
From iris.bi Require Export bi telescopes.
From stdpp Require Import namespaces.
From iris.proofmode Require Import base intro_patterns spec_patterns
sel_patterns coq_tactics reduction.
From iris.proofmode Require Export classes notation.
From stdpp Require Import hlist pretty.
Set Default Proof Using "Type".
Export ident.
......
From iris.bi Require Export bi.
From stdpp Require Import namespaces.
From iris.bi Require Export bi.
Set Default Proof Using "Type".
Import bi.
......
From iris.proofmode Require Import coq_tactics environments.
From stdpp Require Export strings.
From iris.proofmode Require Import coq_tactics environments.
Set Default Proof Using "Type".
Delimit Scope proof_scope with env.
......