Commit 97f38310 authored by Ralf Jung's avatar Ralf Jung

update dependencies; fix for vdash changes

parent 5fd586f6
......@@ -10,6 +10,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris_time" ]
depends: [
"coq-iris" { (= "dev.2020-02-23.1.802035a5") | (= "dev") }
"coq-iris" { (= "dev.2020-03-18.1.ad3a71bf") | (= "dev") }
"coq-tlc" { (= "20181116") | (= "dev") }
]
......@@ -11,7 +11,7 @@ Section Auth_mnat.
Context `{inG Σ (authR mnatUR)}.
Lemma auth_mnat_alloc (n : mnat) :
(|==> γ, own γ (mnat n) own γ (mnat n))%I.
|==> γ, own γ (mnat n) own γ (mnat n).
Proof.
iMod (own_alloc (mnat n mnat n)) as (γ) "[? ?]".
- by apply auth_both_valid_2.
......
......@@ -11,7 +11,7 @@ Section Auth_nat.
Context `{inG Σ (authR natUR)}.
Lemma auth_nat_alloc (n : nat) :
(|==> γ, own γ (nat n) own γ (nat n))%I.
|==> γ, own γ (nat n) own γ (nat n).
Proof.
iMod (own_alloc (nat n nat n)) as (γ) "[? ?]".
- by apply auth_both_valid_2.
......@@ -66,4 +66,4 @@ Section Auth_nat.
apply auth_update, nat_local_update. lia.
Qed.
End Auth_nat.
\ No newline at end of file
End Auth_nat.
......@@ -290,7 +290,7 @@ Section Definitions.
Qed.
Theorem loop_spec s E (Φ : val iProp Σ) :
WP loop #() @ s ; E {{ Φ }}%I.
WP loop #() @ s ; E {{ Φ }}.
Proof.
iLöb as "IH". wp_rec. iExact "IH".
Qed.
......@@ -949,4 +949,4 @@ Section Soundness.
by apply closure_free_predicate.
Qed.
End Soundness.
\ No newline at end of file
End Soundness.
......@@ -31,7 +31,7 @@ Fixpoint is_list_tr `{timeCreditHeapG Σ} (l : list Z) (v : val) : iProp Σ :=
end%I.
(* some proofs: *)
Lemma is_list_translation `{!timeCreditHeapG Σ} l v :
(is_list l v - is_list l v v = «v»%V)%I.
is_list l v - is_list l v v = «v»%V.
Proof.
iIntros "Hl".
destruct l as [|x l] ; simpl.
......@@ -42,7 +42,7 @@ Proof.
+ done.
Qed.
Lemma is_list_tr_translation `{!timeCreditHeapG Σ} l v :
(is_list_tr l v - is_list_tr l v v = «v»%V)%I.
is_list_tr l v - is_list_tr l v v = «v»%V.
Proof.
iIntros "Hl".
destruct l as [|x l] ; simpl.
......@@ -53,7 +53,7 @@ Proof.
+ done.
Qed.
Lemma is_list_tr_is_list_translation `{!timeCreditHeapG Σ} l v :
(is_list_tr l v is_list l «v»%V)%I.
is_list_tr l v is_list l «v»%V.
Proof.
iSplit ; iIntros "Hl".
{
......
......@@ -212,7 +212,7 @@ Section TickSpec.
Qed.
Theorem loop_spec s E (Φ : val iProp Σ) :
WP loop #() @ s ; E {{ Φ }}%I.
WP loop #() @ s ; E {{ Φ }}.
Proof.
iLöb as "IH". wp_rec. iExact "IH".
Qed.
......
......@@ -14,7 +14,7 @@ Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
Proof. solve_inG. Qed.
Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
( `{heapG Σ}, WP e @ s; {{ v, ⌜φ v }}%I)
( `{heapG Σ}, WP e @ s; {{ v, ⌜φ v }})
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
......
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