Commit eed2dc1d authored by Ralf Jung's avatar Ralf Jung

hide which exact functors the barrier needs

parent 1c4b9888
Pipeline #72 passed with stage
......@@ -126,6 +126,9 @@ End barrier_proto.
the module into our namespaces. But Coq doesn't seem to support that...?? *)
Import barrier_proto.
(* The functors we need. *)
Definition barrierFs := stsF sts `::` agreeF `::` pnil.
(** Now we come to the Iris part of the proof. *)
Section proof.
Context {Σ : iFunctorG} (N : namespace).
......
......@@ -28,8 +28,7 @@ Section client.
End client.
Section ClosedProofs.
Definition Σ : iFunctorG := agreeF .:: constF (stsRA barrier_proto.sts) .:: heapF
.:: (λ _, constF unitRA) : iFunctorG.
Definition Σ : iFunctorG := heapF .:: barrierFs .++ endF.
Notation iProp := (iPropG heap_lang Σ).
Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
......
......@@ -31,20 +31,41 @@ Section functions.
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 Definition fn_mcons {T : Type} (ts : list T) (f : nat T) : nat T :=
fold_right fn_cons f ts.
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 : list T) f :
(ts1 ++ ts2) .++ f = ts1 .++ (ts2 .++ f).
Polymorphic Lemma fn_mcons_app {T : Type} (ts1 ts2 : plist T) f :
(ts1 `++` ts2) .++ f = ts1 .++ (ts2 .++ f).
Proof.
unfold fn_mcons. rewrite fold_right_app. done.
induction ts1; simpl; eauto. congruence.
Qed.
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