Commit 457a11d9 authored by Robbert Krebbers's avatar Robbert Krebbers

Move global functor construction to its own file and define notations.

And now the part that I forgot to commit.
parent 3897eaf4
Pipeline #81 passed with stage
......@@ -67,6 +67,7 @@ program_logic/hoare.v
program_logic/language.v
program_logic/tests.v
program_logic/ghost_ownership.v
program_logic/global_functor.v
program_logic/saved_prop.v
program_logic/auth.v
program_logic/sts.v
......
......@@ -125,7 +125,7 @@ End barrier_proto.
Import barrier_proto.
(* The functors we need. *)
Definition barrierGFs := stsGF sts `::` agreeF `::` pnil.
Definition barrierGFs : iFunctors := [stsGF sts; agreeF].
(** Now we come to the Iris part of the proof. *)
Section proof.
......
......@@ -26,7 +26,7 @@ Section client.
End client.
Section ClosedProofs.
Definition Σ : iFunctorG := heapGF .:: barrierGFs .++ endGF.
Definition Σ : iFunctorG := #[ heapGF ; barrierGFs ].
Notation iProp := (iPropG heap_lang Σ).
Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
......
......@@ -76,7 +76,7 @@ Section LiftingTests.
End LiftingTests.
Section ClosedProofs.
Definition Σ : iFunctorG := heapGF .:: endGF.
Definition Σ : iFunctorG := #[ heapGF ].
Notation iProp := (iPropG heap_lang Σ).
Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = '2 }}.
......
......@@ -27,45 +27,4 @@ Section functions.
Lemma fn_lookup_alter_ne (g : T T) (f : A T) a b :
a b alter g a f b = f b.
Proof. unfold alter, fn_alter. by destruct (decide (a = b)). Qed.
End functions.
(** "Cons-ing" of functions from nat to T *)
(* Coq's standard lists are not universe polymorphic. Hence we have to re-define them. Ouch.
TODO: If we decide to end up going with this, we should move this elsewhere. *)
Polymorphic Inductive plist {A : Type} : Type :=
| pnil : plist
| pcons: A plist plist.
Arguments plist : clear implicits.
Polymorphic Fixpoint papp {A : Type} (l1 l2 : plist A) : plist A :=
match l1 with
| pnil => l2
| pcons a l => pcons a (papp l l2)
end.
(* TODO: Notation is totally up for debate. *)
Infix "`::`" := pcons (at level 60, right associativity) : C_scope.
Infix "`++`" := papp (at level 60, right associativity) : C_scope.
Polymorphic Definition fn_cons {T : Type} (t : T) (f: nat T) : nat T :=
λ n, match n with
| O => t
| S n => f n
end.
Polymorphic Fixpoint fn_mcons {T : Type} (ts : plist T) (f : nat T) : nat T :=
match ts with
| pnil => f
| pcons t ts => fn_cons t (fn_mcons ts f)
end.
(* TODO: Notation is totally up for debate. *)
Infix ".::" := fn_cons (at level 60, right associativity) : C_scope.
Infix ".++" := fn_mcons (at level 60, right associativity) : C_scope.
Polymorphic Lemma fn_mcons_app {T : Type} (ts1 ts2 : plist T) f :
(ts1 `++` ts2) .++ f = ts1 .++ (ts2 .++ f).
Proof.
induction ts1; simpl; eauto. congruence.
Qed.
From algebra Require Export auth.
From program_logic Require Export invariants ghost_ownership.
From program_logic Require Export invariants global_functor.
Import uPred.
Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
......
......@@ -6,13 +6,17 @@ Import uPred.
(** Index of a CMRA in the product of global CMRAs. *)
Definition gid := nat.
(** Name of one instance of a particular CMRA in the ghost state. *)
Definition gname := positive.
(** The global CMRA: Indexed product over a gid i to (gname --fin--> Σ i) *)
Definition globalF (Σ : gid iFunctor) : iFunctor :=
iprodF (λ i, mapF gname (Σ i)).
Notation iFunctorG := (gid iFunctor).
Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
Class inG (Λ : language) (Σ : gid iFunctor) (A : cmraT) := InG {
Class inG (Λ : language) (Σ : iFunctorG) (A : cmraT) := InG {
inG_id : gid;
inG_prf : A = Σ inG_id (laterC (iPreProp Λ (globalF Σ)))
}.
......@@ -25,32 +29,6 @@ Instance: Params (@to_globalF) 5.
Instance: Params (@own) 5.
Typeclasses Opaque to_globalF own.
Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
Notation iFunctorG := (gid iFunctor).
(** We need another typeclass to identify the *functor* in the Σ. Basing inG on
the functor breaks badly because Coq is unable to infer the correct
typeclasses, it does not unfold the functor. *)
Class inGF (Λ : language) (Σ : gid iFunctor) (F : iFunctor) := InGF {
inGF_id : gid;
inGF_prf : F = Σ inGF_id;
}.
(* Avoid eager type class search: this line ensures that type class search
is only triggered if the first two arguments of inGF do not contain evars. Since
instance search for [inGF] is restrained, instances should always have [inGF] as
their first argument to avoid loops. For example, the instances [authGF_inGF]
and [auth_identity] otherwise create a cycle that pops up arbitrarily. *)
Hint Mode inGF + + - : typeclass_instances.
Lemma inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (laterC (iPreProp Λ (globalF Σ)))).
Proof. exists inGF_id. by rewrite -inGF_prf. Qed.
Instance inGF_here {Λ Σ} (F: iFunctor) : inGF Λ (F .:: Σ) F.
Proof. by exists 0. Qed.
Instance inGF_further {Λ Σ} (F F': iFunctor) : inGF Λ Σ F inGF Λ (F' .:: Σ) F.
Proof. intros [i ?]. by exists (S i). Qed.
Definition endGF : iFunctorG := const (constF unitRA).
(** Properties about ghost ownership *)
Section global.
Context `{i : inG Λ Σ A}.
......
From algebra Require Export agree.
From program_logic Require Export ghost_ownership.
From program_logic Require Export global_functor.
Import uPred.
Notation savedPropG Λ Σ :=
......
From algebra Require Export sts.
From program_logic Require Export invariants ghost_ownership.
From program_logic Require Export invariants global_functor.
Import uPred.
Class stsG Λ Σ (sts : stsT) := StsG {
......
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