From eed2dc1df57c6b2494d2461b27a78f4ea6be62a3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 22 Feb 2016 20:36:22 +0100
Subject: [PATCH] hide which exact functors the barrier needs

---
 barrier/barrier.v   |  3 +++
 barrier/client.v    |  3 +--
 prelude/functions.v | 31 ++++++++++++++++++++++++++-----
 3 files changed, 30 insertions(+), 7 deletions(-)

diff --git a/barrier/barrier.v b/barrier/barrier.v
index 77ace3112..e7b305102 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -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).
diff --git a/barrier/client.v b/barrier/client.v
index d6717de0a..8ad1d8f26 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -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 }}.
diff --git a/prelude/functions.v b/prelude/functions.v
index 193c37659..d0205d343 100644
--- a/prelude/functions.v
+++ b/prelude/functions.v
@@ -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.
-- 
GitLab