Commit 0e53b389 authored by Ralf Jung's avatar Ralf Jung

keep more instances local

parent d3aefed0
......@@ -88,7 +88,6 @@ theories/heap_lang/lifting.v
theories/heap_lang/notation.v
theories/heap_lang/proofmode.v
theories/heap_lang/adequacy.v
theories/heap_lang/total_adequacy.v
theories/heap_lang/proph_map.v
theories/heap_lang/lib/spawn.v
theories/heap_lang/lib/par.v
......
......@@ -23,6 +23,7 @@ Class savedAnythingG (Σ : gFunctors) (F : cFunctor) := SavedAnythingG {
savedAnythingG_contractive : cFunctorContractive F;
savedAnythingG_subG : subG (savedAnythingΣ F) Σ
}.
(** Assumption constructor *)
Global Instance subG_savedAnythingG (F : cFunctor) `{!cFunctorContractive F} Σ :
subG (savedAnythingΣ F) Σ savedAnythingG Σ F.
Proof. solve_inG. Qed.
......
From iris.program_logic Require Export weakestpre adequacy.
From iris.program_logic Require Export weakestpre adequacy total_adequacy.
From iris.algebra Require Import auth.
From iris.heap_lang Require Import proofmode notation proph_map.
From iris.proofmode Require Import tactics.
......@@ -8,11 +8,11 @@ Set Default Proof Using "Type".
Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val; proph_mapΣ proph_id val].
Notation heapPreG Σ := (subG heapΣ Σ).
(** Instances for sub-libraries *)
Instance heap_preG_iris Σ : heapPreG Σ invPreG Σ.
Local Instance heap_preG_iris Σ : heapPreG Σ invPreG Σ.
Proof. solve_inG. Qed.
Instance heap_preG_heap Σ : heapPreG Σ gen_heapPreG loc val Σ.
Local Instance heap_preG_heap Σ : heapPreG Σ gen_heapPreG loc val Σ.
Proof. solve_inG. Qed.
Instance heap_preG_proph Σ : heapPreG Σ proph_mapPreG proph_id val Σ.
Local Instance heap_preG_proph Σ : heapPreG Σ proph_mapPreG proph_id val Σ.
Proof. solve_inG. Qed.
Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
......@@ -26,3 +26,17 @@ Proof.
iExists (λ σ κs, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I). iFrame.
iApply (Hwp (HeapG _ _ _ _)).
Qed.
Definition heap_total Σ `{heapPreG Σ} s e σ φ :
( `{heapG Σ}, WP e @ s; [{ v, ⌜φ v }]%I)
sn erased_step ([e], σ).
Proof.
intros Hwp; eapply (twp_total _ _); iIntros (?) "".
iMod (gen_heap_init σ.(heap)) as (?) "Hh".
iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
iModIntro.
iExists
(λ σ κs _, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I),
(λ _, True%I); iFrame.
iApply (Hwp (HeapG _ _ _ _)).
Qed.
......@@ -8,6 +8,7 @@ From iris.proofmode Require Import tactics.
From stdpp Require Import fin_maps.
Set Default Proof Using "Type".
(** See [adequacy.v] for the functor list and init lemma *)
Class heapG Σ := HeapG {
heapG_invG : invG Σ;
heapG_gen_heapG :> gen_heapG loc val Σ;
......
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 σ φ :
( `{heapG Σ}, WP e @ s; [{ v, ⌜φ v }]%I)
sn erased_step ([e], σ).
Proof.
intros Hwp; eapply (twp_total _ _); iIntros (?) "".
iMod (gen_heap_init σ.(heap)) as (?) "Hh".
iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
iModIntro.
iExists
(λ σ κs _, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I),
(λ _, True%I); iFrame.
iApply (Hwp (HeapG _ _ _ _)).
Qed.
......@@ -10,7 +10,7 @@ Definition ownPΣ (Λ : language) : gFunctors :=
#[GFunctor (authR (optionUR (exclR (stateC Λ)))); invΣ].
Notation ownPPreG Λ Σ := (subG (ownPΣ Λ) Σ).
(** Instances for sub-libraries *)
Instance ownPPreG_iris Λ Σ : ownPPreG Λ Σ invPreG Σ.
Local Instance ownPPreG_iris Λ Σ : ownPPreG Λ Σ invPreG Σ.
Proof. solve_inG. Qed.
(** Instance for [own] *)
Local Hint Extern 10 (inG _ _) => solve_inG_with id ownPΣ : typeclass_instances.
......
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