Commit c390d512 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Clean up Imports so that the ={E}=★ notation is displayed properly.

parent dfa9e843
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
......
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang.lib.barrier Require Export barrier.
From iris.prelude Require Import functions. From iris.prelude Require Import functions.
From iris.algebra Require Import upred_big_op. From iris.algebra Require Import upred_big_op.
From iris.program_logic Require Import saved_prop sts. From iris.program_logic Require Import saved_prop sts.
From iris.heap_lang Require Import proofmode. From iris.heap_lang Require Import proofmode.
From iris.heap_lang.lib.barrier Require Export barrier.
From iris.heap_lang.lib.barrier Require Import protocol. From iris.heap_lang.lib.barrier Require Import protocol.
(** The CMRAs we need. *) (** The CMRAs we need. *)
......
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.proofmode Require Import invariants tactics. From iris.proofmode Require Import invariants tactics.
From iris.program_logic Require Import auth. From iris.program_logic Require Import auth.
......
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.proofmode Require Import invariants tactics. From iris.proofmode Require Import invariants tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
......
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.proofmode Require Import invariants tactics. From iris.proofmode Require Import invariants tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
......
From iris.program_logic Require Export global_functor auth. From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import invariants ghost_ownership. From iris.heap_lang Require Export lang.
From iris.program_logic Require Import auth.
From iris.proofmode Require Import invariants.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import gset. From iris.algebra Require Import gset.
Import uPred. Import uPred.
......
From iris.algebra Require Export auth upred_tactics. From iris.program_logic Require Export pviewshifts.
From iris.algebra Require Export auth.
From iris.algebra Require Import gmap. From iris.algebra Require Import gmap.
From iris.program_logic Require Export invariants ghost_ownership. From iris.proofmode Require Import invariants.
From iris.proofmode Require Import invariants ghost_ownership.
Import uPred. Import uPred.
(* The CMRA we need. *) (* The CMRA we need. *)
......
From iris.algebra Require Import gmap agree upred_big_op. From iris.program_logic Require Export pviewshifts.
From iris.program_logic Require Import auth saved_prop. From iris.algebra Require Import auth gmap agree upred_big_op.
From iris.proofmode Require Import tactics invariants. From iris.proofmode Require Import tactics invariants.
Import uPred. Import uPred.
......
From iris.algebra Require Export sts upred_tactics. From iris.program_logic Require Export pviewshifts.
From iris.program_logic Require Export invariants. From iris.algebra Require Export sts.
From iris.proofmode Require Import invariants. From iris.proofmode Require Import invariants.
Import uPred. Import uPred.
......
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang.lib.barrier Require Import proof. From iris.heap_lang.lib.barrier Require Import proof.
From iris.heap_lang Require Import par. From iris.heap_lang Require Import par.
From iris.program_logic Require Import auth sts saved_prop hoare ownership. From iris.program_logic Require Import auth sts saved_prop hoare ownership.
From iris.heap_lang Require Import proofmode. From iris.heap_lang Require Import proofmode.
Import uPred.
Definition worker (n : Z) : val := Definition worker (n : Z) : val :=
λ: "b" "y", wait "b" ;; !"y" #n. λ: "b" "y", wait "b" ;; !"y" #n.
......
(** This file is essentially a bunch of testcases. *) (** This file is essentially a bunch of testcases. *)
From iris.program_logic Require Import ownership hoare auth. From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.program_logic Require Import ownership hoare.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
Section LangTests. Section LangTests.
......
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.algebra Require Import excl agree csum.
From iris.program_logic Require Import hoare.
From iris.heap_lang.lib.barrier Require Import proof specification. From iris.heap_lang.lib.barrier Require Import proof specification.
From iris.heap_lang Require Import notation par proofmode. From iris.heap_lang Require Import notation par proofmode.
From iris.proofmode Require Import invariants. From iris.proofmode Require Import invariants.
...@@ -54,7 +55,7 @@ Lemma Q_res_join γ : barrier_res γ Ψ1 ★ barrier_res γ Ψ2 ⊢ ▷ barrier_ ...@@ -54,7 +55,7 @@ Lemma Q_res_join γ : barrier_res γ Ψ1 ★ barrier_res γ Ψ2 ⊢ ▷ barrier_
Proof. Proof.
iIntros "[Hγ Hγ']"; iIntros "[Hγ Hγ']";
iDestruct "Hγ" as (x) "[#Hγ Hx]"; iDestruct "Hγ'" as (x') "[#Hγ' Hx']". iDestruct "Hγ" as (x) "[#Hγ Hx]"; iDestruct "Hγ'" as (x') "[#Hγ' Hx']".
iAssert ( (x x'))%I as "Hxx" . iAssert ( (x x'))%I as "Hxx".
{ iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'". { iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
rewrite own_valid csum_validI /= agree_validI agree_equivI uPred.later_equivI /=. rewrite own_valid csum_validI /= agree_validI agree_equivI uPred.later_equivI /=.
rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id. rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id.
......
(** Correctness of in-place list reversal *) (** Correctness of in-place list reversal *)
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Export tactics. From iris.proofmode Require Export tactics.
From iris.program_logic Require Export hoare.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
Section list_reverse. Section list_reverse.
......
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
From iris.algebra Require Import excl dec_agree csum. From iris.algebra Require Import excl dec_agree csum.
From iris.program_logic Require Import hoare.
From iris.heap_lang Require Import assert proofmode notation. From iris.heap_lang Require Import assert proofmode notation.
From iris.proofmode Require Import invariants ghost_ownership. From iris.proofmode Require Import invariants.
Definition one_shot_example : val := λ: <>, Definition one_shot_example : val := λ: <>,
let: "x" := ref NONE in ( let: "x" := ref NONE in (
......
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Export tactics. From iris.proofmode Require Export tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment