Commit d3aefed0 authored by Ralf Jung's avatar Ralf Jung

tweak comment, reduce diff

parent 1b1818d5
......@@ -6,7 +6,6 @@ From iris.heap_lang.lib Require Import par.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Module Import one_shot.
Definition one_shot_example : val := λ: <>,
let: "x" := ref NONE in (
(* tryset *) (λ: "n",
......@@ -98,7 +97,6 @@ Proof.
- iIntros "!# _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
Qed.
End proof.
End one_shot.
(* Have a client with a closed proof. *)
Definition client : expr :=
......
......@@ -69,7 +69,7 @@ Section to_gen_heap.
Proof. by rewrite /to_gen_heap fmap_delete. Qed.
End to_gen_heap.
Lemma gen_heap_init {L V : Type} `{Countable L, !gen_heapPreG L V Σ} σ :
Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
(|==> _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
Proof.
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
......
......@@ -69,8 +69,6 @@ Coercion gFunctors.singleton : gFunctor >-> gFunctors.
Notation "#[ ]" := gFunctors.nil (format "#[ ]").
Notation "#[ Σ1 ; .. ; Σn ]" :=
(gFunctors.app Σ1 .. (gFunctors.app Σn gFunctors.nil) ..).
(** Avoid unnecessary [app]s, to make [subG_const_inG] more useful. *)
Notation "#[ Σ ]" := (gFunctors.singleton Σ).
(** * Subfunctors *)
......
......@@ -5,17 +5,15 @@ Set Default Proof Using "Type".
Import uPred.
(** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
[Σ]. This class is similar to the [subG] class, but written down in terms of
individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
needed because Coq is otherwise unable to solve type class constraints due to
higher-order unification problems.
The class will be used by definitions that might work with higher-order
ghost state, such sa [own] below. "Normal" libraries should just work
with [subG] instead.
You should never assume this class, because it is very easy to accidentally
introduce inconsistent assumptions by assuming [inG]. When you are working with
higher-order ghost state, you might have to add a new instance of this class,
but that's all. *)
[Σ]. This class is similar to the [subG] class, but written down in terms of
individual CMRAs instead of (lists of) CMRA *functors*. This additional
class is needed because Coq is otherwise unable to solve type class
constraints due to higher-order unification problems.
You should never assume this class, because it is very easy to accidentally
introduce inconsistent assumptions by assuming [inG]. See [IrisProofs.md]
for how to manage library assumptions.
*)
Class inG (Σ : gFunctors) (A : cmraT) :=
InG { inG_id : gid Σ; inG_prf : A = Σ inG_id (iPreProp Σ) }.
Hint Mode inG - ! : typeclass_instances.
......@@ -24,7 +22,7 @@ Arguments inG_id {_ _} _.
Lemma subG_inG Σ (F : gFunctor) : subG F Σ inG Σ (F (iPreProp Σ)).
Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
(** [solve_inG_with proj someΣ] expetcs [someΣ] to be defined as [#[ F1; F2;
(** [solve_inG_with proj someΣ] expects [someΣ] to be defined as [#[ F1; F2;
...]] and [proj] to be some projection from a typeclass that ends in [subG
Σ someΣ]. It expects the goal to be [inG (Fn (iPreProp Σ)) Σ] for one of
the [Fn], and will turn the goal into [subG Σ someΣ], and then apply [proj].
......
......@@ -32,7 +32,7 @@ Definition saved_anything_own `{!savedAnythingG Σ F}
(γ : gname) (x : F (iProp Σ)) : iProp Σ :=
own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
Typeclasses Opaque saved_anything_own.
Instance: Params (@saved_anything_own) 5 := {}.
Instance: Params (@saved_anything_own) 4 := {}.
Section saved_anything.
Context `{!savedAnythingG Σ F}.
......@@ -43,9 +43,9 @@ Section saved_anything.
Persistent (saved_anything_own γ x).
Proof. rewrite /saved_anything_own; apply _. Qed.
Global Instance saved_anything_ne γ : NonExpansive (saved_anything_own (F:=F) γ).
Global Instance saved_anything_ne γ : NonExpansive (saved_anything_own γ).
Proof. solve_proper. Qed.
Global Instance saved_anything_proper γ : Proper (() ==> ()) (saved_anything_own (F:=F) γ).
Global Instance saved_anything_proper γ : Proper (() ==> ()) (saved_anything_own γ).
Proof. solve_proper. Qed.
Lemma saved_anything_alloc_strong x (G : gset gname) :
......
......@@ -4,7 +4,6 @@ From iris.algebra Require Import gmap auth agree gset coPset.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
(** All definitions in this file are internal to [fancy_updates] with the
exception of what's in the [invG] module. The module [invG] is thus exported in
[fancy_updates], which [wsat] is only imported. *)
......@@ -33,7 +32,6 @@ Local Hint Extern 10 (inG _ _) => solve_inG_with inv_preG_subG invΣ : typeclass
Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) :=
to_agree (Next (iProp_unfold P)).
Definition ownI `{invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
own invariant_name ( {[ i := invariant_unfold P ]}).
Arguments ownI {_ _} _ _%I.
......
......@@ -19,7 +19,7 @@ Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
( `{heapG Σ}, WP e @ s; {{ v, ⌜φ v }}%I)
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy Σ _). iIntros (??) "".
intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
iMod (gen_heap_init σ.(heap)) as (?) "Hh".
iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
iModIntro.
......
......@@ -4,7 +4,7 @@ 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 σ φ :
Definition heap_total Σ `{heapPreG Σ} s e σ φ :
( `{heapG Σ}, WP e @ s; [{ v, ⌜φ v }]%I)
sn erased_step ([e], σ).
Proof.
......
......@@ -33,7 +33,7 @@ Proof.
Qed.
Section adequacy.
Context `{!irisG Λ Σ}.
Context `{irisG Λ Σ}.
Implicit Types e : expr Λ.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ iProp Σ.
......@@ -173,7 +173,7 @@ Proof.
Qed.
End adequacy.
Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} s e σ φ :
Theorem wp_strong_adequacy Σ Λ `{invPreG Σ} s e σ φ :
( `{Hinv : invG Σ} κs,
(|={}=>
(stateI : state Λ list (observation Λ) nat iProp Σ)
......@@ -198,7 +198,7 @@ Proof.
iApply (@wptp_safe _ _ (IrisG _ _ Hinv stateI fork_post) with "[Hσ] Hwp"); eauto.
Qed.
Theorem wp_adequacy Σ Λ `{!invPreG Σ} s e σ φ :
Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ :
( `{Hinv : invG Σ} κs,
(|={}=> stateI : state Λ list (observation Λ) iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ κs _, stateI σ κs) (λ _, True%I) in
......@@ -212,7 +212,7 @@ Proof.
iIntros "_". by iApply fupd_mask_weaken.
Qed.
Theorem wp_strong_all_adequacy Σ Λ `{!invPreG Σ} s e σ1 v vs σ2 φ :
Theorem wp_strong_all_adequacy Σ Λ `{invPreG Σ} s e σ1 v vs σ2 φ :
( `{Hinv : invG Σ} κs,
(|={}=>
(stateI : state Λ list (observation Λ) nat iProp Σ)
......@@ -232,7 +232,7 @@ Proof.
with "[Hσ] [Hwp]"); eauto. by rewrite right_id_L.
Qed.
Theorem wp_invariance Σ Λ `{!invPreG Σ} s e σ1 t2 σ2 φ :
Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
( `{Hinv : invG Σ} κs κs',
(|={}=>
(stateI : state Λ list (observation Λ) nat iProp Σ)
......@@ -253,7 +253,7 @@ Qed.
(* An equivalent version that does not require finding [fupd_intro_mask'], but
can be confusing to use. *)
Corollary wp_invariance' Σ Λ `{!invPreG Σ} s e σ1 t2 σ2 φ :
Corollary wp_invariance' Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
( `{Hinv : invG Σ} κs κs',
(|={}=>
(stateI : state Λ list (observation Λ) nat iProp Σ)
......
......@@ -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 Σ.
Instance ownPPreG_iris Λ Σ : ownPPreG Λ Σ invPreG Σ.
Proof. solve_inG. Qed.
(** Instance for [own] *)
Local Hint Extern 10 (inG _ _) => solve_inG_with id ownPΣ : typeclass_instances.
......
......@@ -114,7 +114,7 @@ Proof.
Qed.
End adequacy.
Theorem twp_total Σ Λ `{!invPreG Σ} s e σ Φ :
Theorem twp_total Σ Λ `{invPreG Σ} s e σ Φ :
( `{Hinv : invG Σ},
(|={}=>
(stateI : state Λ list (observation Λ) nat iProp Σ)
......
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