From 5d75475553dfdfc6c73bc6d40047be0f1924847d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 25 May 2020 18:21:46 +0200
Subject: [PATCH] rename heap_lang modules

---
 _CoqProject                                   |  4 +-
 tests/atomic.v                                |  1 -
 tests/heap_lang2.v                            |  2 +-
 .../heap_lang/{array.v => derived_laws.v}     | 53 +++++++++++++++++--
 theories/heap_lang/lib/array.v                |  2 +-
 theories/heap_lang/lib/atomic_heap.v          |  6 +--
 theories/heap_lang/lib/lock.v                 |  2 +-
 .../heap_lang/{lifting.v => primitive_laws.v} | 38 +------------
 theories/heap_lang/proofmode.v                |  2 +-
 9 files changed, 60 insertions(+), 50 deletions(-)
 rename theories/heap_lang/{array.v => derived_laws.v} (86%)
 rename theories/heap_lang/{lifting.v => primitive_laws.v} (94%)

diff --git a/_CoqProject b/_CoqProject
index aa95ee163..036d7ec24 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -104,8 +104,8 @@ theories/heap_lang/locations.v
 theories/heap_lang/lang.v
 theories/heap_lang/metatheory.v
 theories/heap_lang/tactics.v
-theories/heap_lang/lifting.v
-theories/heap_lang/array.v
+theories/heap_lang/primitive_laws.v
+theories/heap_lang/derived_laws.v
 theories/heap_lang/notation.v
 theories/heap_lang/proofmode.v
 theories/heap_lang/adequacy.v
diff --git a/tests/atomic.v b/tests/atomic.v
index 7e9ed0726..f9881ffcd 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -1,6 +1,5 @@
 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".
 
diff --git a/tests/heap_lang2.v b/tests/heap_lang2.v
index 85dcae1bc..4ec6061cc 100644
--- a/tests/heap_lang2.v
+++ b/tests/heap_lang2.v
@@ -1,7 +1,7 @@
 (* Test yet another way of importing heap_lang modules that used to break
 printing *)
 From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Export lifting notation.
+From iris.heap_lang Require Export primitive_laws notation.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
diff --git a/theories/heap_lang/array.v b/theories/heap_lang/derived_laws.v
similarity index 86%
rename from theories/heap_lang/array.v
rename to theories/heap_lang/derived_laws.v
index 43879b05b..704c18a8e 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/derived_laws.v
@@ -1,13 +1,19 @@
+(** This file extens the HeapLang program logic with some derived laws about
+arrays and prophecies.
+
+For more array operations, see [heap_lang.lib.array].
+*)
+
 From stdpp Require Import fin_maps.
 From iris.bi Require Import lib.fractional.
 From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Export lifting.
+From iris.program_logic Require Import ectx_lifting.
+From iris.heap_lang Require Export primitive_laws.
 From iris.heap_lang Require Import tactics notation.
 Set Default Proof Using "Type".
 
-(** This file defines the [array] connective, a version of [mapsto] that works
-with lists of values. It also contains array versions of the basic heap
-operations of HeapLang. *)
+(** The [array] connective is a version of [mapsto] that works
+with lists of values. *)
 
 Definition array `{!heapG Σ} (l : loc) (q : Qp) (vs : list val) : iProp Σ :=
   ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦{q} v)%I.
@@ -317,6 +323,45 @@ Proof.
   iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
   iApply (twp_faa_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
 Qed.
+
+(** Derived prophecy laws *)
+
+(** Lemmas for some particular expression inside the [Resolve]. *)
+Lemma wp_resolve_proph s E (p : proph_id) (pvs : list (val * val)) v :
+  {{{ proph p pvs }}}
+    ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
+  {{{ pvs', RET (LitV LitUnit); ⌜pvs = (LitV LitUnit, v)::pvs'⌝ ∗ proph p pvs' }}}.
+Proof.
+  iIntros (Φ) "Hp HΦ". iApply (wp_resolve with "Hp"); first done.
+  iApply wp_pure_step_later=> //=. iApply wp_value.
+  iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame.
+Qed.
+
+Lemma wp_resolve_cmpxchg_suc s E l (p : proph_id) (pvs : list (val * val)) v1 v2 v :
+  vals_compare_safe v1 v1 →
+  {{{ proph p pvs ∗ ▷ l ↦ v1 }}}
+    Resolve (CmpXchg #l v1 v2) #p v @ s; E
+  {{{ RET (v1, #true) ; ∃ pvs', ⌜pvs = ((v1, #true)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦ v2 }}}.
+Proof.
+  iIntros (Hcmp Φ) "[Hp Hl] HΦ".
+  iApply (wp_resolve with "Hp"); first done.
+  assert (val_is_unboxed v1) as Hv1; first by destruct Hcmp.
+  iApply (wp_cmpxchg_suc with "Hl"); [done..|]. iIntros "!> Hl".
+  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
+Qed.
+
+Lemma wp_resolve_cmpxchg_fail s E l (p : proph_id) (pvs : list (val * val)) q v' v1 v2 v :
+  v' ≠ v1 → vals_compare_safe v' v1 →
+  {{{ proph p pvs ∗ ▷ l ↦{q} v' }}}
+    Resolve (CmpXchg #l v1 v2) #p v @ s; E
+  {{{ RET (v', #false) ; ∃ pvs', ⌜pvs = ((v', #false)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦{q} v' }}}.
+Proof.
+  iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
+  iApply (wp_resolve with "Hp"); first done.
+  iApply (wp_cmpxchg_fail with "Hl"); [done..|]. iIntros "!> Hl".
+  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
+Qed.
+
 End lifting.
 
 Typeclasses Opaque array.
diff --git a/theories/heap_lang/lib/array.v b/theories/heap_lang/lib/array.v
index 364c806d4..0de0570c0 100644
--- a/theories/heap_lang/lib/array.v
+++ b/theories/heap_lang/lib/array.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Export lang array.
+From iris.heap_lang Require Export derived_laws.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
diff --git a/theories/heap_lang/lib/atomic_heap.v b/theories/heap_lang/lib/atomic_heap.v
index 6a762620f..bdbc37838 100644
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/theories/heap_lang/lib/atomic_heap.v
@@ -1,8 +1,8 @@
 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.
+From iris.heap_lang Require Export derived_laws.
+From iris.heap_lang Require Import notation proofmode.
 Set Default Proof Using "Type".
 
 (** A general logically atomic interface for a heap. *)
@@ -149,4 +149,4 @@ Definition primitive_atomic_heap `{!heapG Σ} : atomic_heap Σ :=
      load_spec := primitive_load_spec;
      store_spec := primitive_store_spec;
      cmpxchg_spec := primitive_cmpxchg_spec;
-     mapsto_agree := lifting.mapsto_agree |}.
+     mapsto_agree := primitive_laws.mapsto_agree |}.
diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v
index 77f57e59b..0430aec74 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -1,5 +1,5 @@
 From iris.base_logic.lib Require Export invariants.
-From iris.heap_lang Require Export lifting notation.
+From iris.heap_lang Require Import primitive_laws notation.
 Set Default Proof Using "Type".
 
 Structure lock Σ `{!heapG Σ} := Lock {
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/primitive_laws.v
similarity index 94%
rename from theories/heap_lang/lifting.v
rename to theories/heap_lang/primitive_laws.v
index 5cb0b0568..9fc1766cf 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/primitive_laws.v
@@ -1,3 +1,5 @@
+(** This file proves the basic laws of the HeapLang program logic. *)
+
 From stdpp Require Import fin_maps.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth gmap.
@@ -611,40 +613,4 @@ Proof.
     iMod "HΦ". iModIntro. by iApply "HΦ".
 Qed.
 
-(** Lemmas for some particular expression inside the [Resolve]. *)
-Lemma wp_resolve_proph s E (p : proph_id) (pvs : list (val * val)) v :
-  {{{ proph p pvs }}}
-    ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
-  {{{ pvs', RET (LitV LitUnit); ⌜pvs = (LitV LitUnit, v)::pvs'⌝ ∗ proph p pvs' }}}.
-Proof.
-  iIntros (Φ) "Hp HΦ". iApply (wp_resolve with "Hp"); first done.
-  iApply wp_pure_step_later=> //=. iApply wp_value.
-  iIntros "!>" (vs') "HEq Hp". iApply "HΦ". iFrame.
-Qed.
-
-Lemma wp_resolve_cmpxchg_suc s E l (p : proph_id) (pvs : list (val * val)) v1 v2 v :
-  vals_compare_safe v1 v1 →
-  {{{ proph p pvs ∗ ▷ l ↦ v1 }}}
-    Resolve (CmpXchg #l v1 v2) #p v @ s; E
-  {{{ RET (v1, #true) ; ∃ pvs', ⌜pvs = ((v1, #true)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦ v2 }}}.
-Proof.
-  iIntros (Hcmp Φ) "[Hp Hl] HΦ".
-  iApply (wp_resolve with "Hp"); first done.
-  assert (val_is_unboxed v1) as Hv1; first by destruct Hcmp.
-  iApply (wp_cmpxchg_suc with "Hl"); [done..|]. iIntros "!> Hl".
-  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
-Qed.
-
-Lemma wp_resolve_cmpxchg_fail s E l (p : proph_id) (pvs : list (val * val)) q v' v1 v2 v :
-  v' ≠ v1 → vals_compare_safe v' v1 →
-  {{{ proph p pvs ∗ ▷ l ↦{q} v' }}}
-    Resolve (CmpXchg #l v1 v2) #p v @ s; E
-  {{{ RET (v', #false) ; ∃ pvs', ⌜pvs = ((v', #false)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦{q} v' }}}.
-Proof.
-  iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
-  iApply (wp_resolve with "Hp"); first done.
-  iApply (wp_cmpxchg_fail with "Hl"); [done..|]. iIntros "!> Hl".
-  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
-Qed.
-
 End lifting.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index dea83e095..28eae1b6f 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import coq_tactics reduction.
 From iris.proofmode Require Export tactics.
 From iris.program_logic Require Import atomic.
-From iris.heap_lang Require Export tactics array.
+From iris.heap_lang Require Export tactics derived_laws.
 From iris.heap_lang Require Import notation.
 Set Default Proof Using "Type".
 Import uPred.
-- 
GitLab