Commit 6e305349 authored by Ralf Jung's avatar Ralf Jung
Browse files

update dependencies

parent 741d5564
......@@ -9,7 +9,7 @@ synopsis: "Iris with time credits and time credits"
depends: [
"coq" { (>= "8.14" & < "8.15~") | (= "dev") }
"coq-iris" { (= "dev.2021-12-09.1.f52f9f6a") | (= "dev") }
"coq-iris" { (= "dev.2022-05-13.0.a1971471") | (= "dev") }
"coq-tlc" { (= "20210316") }
]
......
......@@ -759,7 +759,7 @@ Section Soundness.
(* (1) adequate result: *)
- intros t2 σ2 v2 Hsteps.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
pose (Build_TickCounter (fresh (dom σ2))) as Hloc.
assert (σ2 !! = None)
by (simpl ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
by eapply adequate_tctranslation__adequate_result.
......@@ -767,7 +767,7 @@ Section Soundness.
- intros t2 σ2 e2 _ Hsteps He2.
(* build a location ℓ which is fresh in e2 and in the domain of σ2: *)
pose (set1 := loc_set_of_expr e2 : gset loc).
pose (set2 := dom (gset loc) σ2 : gset loc).
pose (set2 := dom σ2 : gset loc).
pose (Build_TickCounter (fresh (set1 set2))) as Hloc.
eassert ( set1 set2) as [H1 H2] % not_elem_of_union
by (unfold ; apply is_fresh).
......@@ -780,7 +780,7 @@ Section Soundness.
(* (3) bounded time: *)
- intros t2 σ2 k.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
pose (Build_TickCounter (fresh (dom σ2))) as Hloc.
assert (σ2 !! = None)
by (unfold ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
specialize (Hadq Hloc) as Hsafe % safe_adequate.
......
......@@ -523,7 +523,7 @@ Proof.
(* (1) adequate result: *)
- intros n t2 σ2 v2 Hnsteps Inm.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Hloc := Build_TickCounter (fresh (dom (gset loc) σ2)) : TickCounter).
pose (Hloc := Build_TickCounter (fresh (dom σ2)) : TickCounter).
assert (σ2 !! = None)
by (simpl ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
by eapply adequate_translation__nadequate_result.
......@@ -531,7 +531,7 @@ Proof.
- intros n t2 σ2 e2 _ Hnsteps Inm He2.
(* build a location ℓ which is fresh in e2 and in the domain of σ2: *)
pose (set1 := loc_set_of_expr e2 : gset loc).
pose (set2 := dom (gset loc) σ2 : gset loc).
pose (set2 := dom σ2 : gset loc).
pose (Hloc := Build_TickCounter (fresh (set1 set2)) : TickCounter).
eassert ( set1 set2) as [H1 H2] % not_elem_of_union
by (unfold ; apply is_fresh).
......
......@@ -369,7 +369,7 @@ Section Soundness.
intros Hadq.
intros t2 σ2 k.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
pose (Build_TickCounter (fresh (dom σ2))) as Hloc.
assert (σ2 !! = None)
by (unfold ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
specialize (Hadq Hloc) as Hsafe % safe_adequate.
......
......@@ -170,7 +170,7 @@ Proof.
(* (1) adequate result: *)
- intros t2 σ2 v2 Hsteps.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
pose (Build_TickCounter (fresh (dom σ2))) as Hloc.
assert (σ2 !! = None)
by (simpl ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
by eapply adequate_tctranslation__adequate_result.
......@@ -178,7 +178,7 @@ Proof.
- intros t2 σ2 e2 _ Hsteps He2.
(* build a location ℓ which is fresh in e2 and in the domain of σ2: *)
pose (set1 := loc_set_of_expr e2 : gset loc).
pose (set2 := dom (gset loc) σ2 : gset loc).
pose (set2 := dom σ2 : gset loc).
pose (Build_TickCounter (fresh (set1 set2))) as Hloc.
eassert ( set1 set2) as [H1 H2] % not_elem_of_union
by (unfold ; apply is_fresh).
......@@ -294,7 +294,7 @@ Lemma spec_tctranslation__bounded' {Σ} m ψ e :
Proof.
intros Hspec HtcPreG σ t2 σ2 n Hnsteps.
(* build a location ℓ which is not in the domain of σ2: *)
pose (Build_TickCounter (fresh (dom (gset loc) σ2))) as Hloc.
pose (Build_TickCounter (fresh (dom σ2))) as Hloc.
assert (σ2 !! = None)
by (unfold ; eapply (not_elem_of_dom (D:=gset loc)), is_fresh).
eapply simulation_exec_alt in Hnsteps ; auto.
......
......@@ -604,7 +604,7 @@ Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
Proof. destruct Ki1, Ki2; intros; by simplify_eq. Qed.
Lemma alloc_fresh v σ :
let l := fresh (dom (gset loc) σ) in
let l := fresh (dom σ) in
head_step (Alloc $ Val v) σ [] (Val $ LitV $ LitLoc l) (<[l:=v]> σ) [].
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
......
Supports Markdown
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