Commit 6c83c489 authored by Robbert Krebbers's avatar Robbert Krebbers

Kill `bi_pow`.

parent f6a4683d
......@@ -126,7 +126,8 @@ Section map.
Lemma par_map_workers_spec γl γ n vmap lk c :
map_spec vmap -
{{{ is_lock N γl lk (map_worker_lock_inv γ c) client γ (:gmultiset A) ^ n }}}
{{{ is_lock N γl lk (map_worker_lock_inv γ c)
[] replicate n (client γ (:gmultiset A)) }}}
par_map_workers #n vmap lk c
{{{ RET #(); True }}}.
Proof.
......
......@@ -20,12 +20,6 @@ Definition client `{contributionG Σ A} (γ : gname) (x : A) : iProp Σ :=
Typeclasses Opaque client.
Instance: Params (@client) 5.
(** MOVE *)
Fixpoint bi_pow {PROP : bi} (n : nat) (P : PROP) : PROP :=
match n with O => emp | S n => P bi_pow n P end%I.
Arguments bi_pow {_} _ _%I.
Notation "P ^ n" := (bi_pow n P) : bi_scope.
Section contribution.
Context `{contributionG Σ A}.
Implicit Types x y : A.
......@@ -140,10 +134,11 @@ Section contribution.
Qed.
(** Derived *)
Lemma contribution_init_pow n : (|==> γ, server γ n ε (client γ ε)^n)%I.
Lemma contribution_init_pow n :
(|==> γ, server γ n ε [] replicate n (client γ ε))%I.
Proof.
iMod (contribution_init) as (γ) "Hs". iExists γ.
iInduction n as [|n] "IH"; first by iFrame.
iInduction n as [|n] "IH"; simpl; first by iFrame.
iMod ("IH" with "Hs") as "[Hs $]". by iApply alloc_client.
Qed.
End contribution.
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