Commit 08bc474f authored by Dan Frumin's avatar Dan Frumin

Bump iris version

parent 703244e8
......@@ -6,7 +6,7 @@ This version is known to compile with:
- Ssreflect 1.6
- Autosubst branch [coq86-devel](https://github.com/uds-psl/autosubst/tree/coq86-devel)
- std++ version [24aef2fea9481e65d1f6658005ddde25ae9a64ee](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/24aef2fea9481e65d1f6658005ddde25ae9a64ee)
- Iris version [f96a894b14fe7095bb5ac5b937abd31e40316858](https://gitlab.mpi-sws.org/FP/iris-coq/tree/f96a894b14fe7095bb5ac5b937abd31e40316858)
- Iris version [4be0320e9ff9122e90fa5af60e6a02e81eaffa33](https://gitlab.mpi-sws.org/FP/iris-coq/tree/4be0320e9ff9122e90fa5af60e6a02e81eaffa33)
# Compilation
......
......@@ -60,7 +60,7 @@ Definition lookup_binder {A} : Lookup binder A (stringmap A) :=
end.
Lemma dom_insert_binder {A} (m : stringmap A) (i : binder) (x : A) :
dom _ (<[i:=x]> m) = {[i]} dom _ m.
dom stringset (<[i:=x]> m) = {[i]} dom stringset m.
Proof. destruct i; cbn-[union]; unfold_leibniz. set_solver.
apply dom_insert. Qed.
Lemma cons_binder_union (i : binder) (X : stringset) :
......@@ -130,21 +130,6 @@ Proof. destruct i, j; cbn; auto. apply delete_commute. Qed.
Lemma delete_empty_binder {A} (x : binder) :
delete x ( : stringmap A) = .
Proof. destruct x; cbn; eauto. apply delete_empty. Qed.
Lemma delete_singleton_ne_binder {A} (i j : binder) (x : A) :
j i delete i {[j := x]} = {[j := x]}.
Proof.
destruct i,j;cbn; eauto; intros.
- apply delete_empty.
- apply delete_singleton_ne.
intros seq. subst s0. by apply H.
Qed.
Lemma delete_singleton_ne_binder' {A} (i : binder) (j : string) (x : A) :
(BNamed j i) delete i {[j := x]} = {[j := x]}.
Proof.
destruct i; cbn; eauto; intros.
apply delete_singleton_ne.
intros seq. subst s. by apply H.
Qed.
Lemma fmap_insert' {A B} (x : binder) (f : A B) v (vs : stringmap A) :
f <$> <[x:=v]>vs = <[x:=f v]> (f <$> vs).
......
......@@ -371,7 +371,7 @@ Module lang.
Qed.
Lemma alloc_fresh e v σ :
let l := fresh (dom _ σ) in
let l := fresh (dom (gset loc) σ) in
to_val e = Some v head_step (Alloc e) σ (Lit (Loc l)) (<[l:=v]>σ) [].
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
End lang.
......
......@@ -391,10 +391,10 @@ Qed.
Lemma subst_p_rec (x1 x2 : binder) v1 v2 e :
subst_p (<[x1:=v1]>{[x2:=v2]}) e = subst' x2 (of_val v2) (subst' x1 (of_val v1) e).
Proof.
replace (<[x1:=v1]> {[x2 := v2]})
with (<[x1:=v1]>(<[x2 := v2]>)); last first.
{ destruct x1,x2; cbn; eauto. }
rewrite !subst_p_insert.
rewrite subst_p_insert.
replace {[x2 := v2]} with (<[x2 := v2]>( : stringmap val)); last first.
{ by destruct x2; cbn. }
rewrite subst_p_insert.
by rewrite subst_p_empty.
Qed.
......
......@@ -123,7 +123,8 @@ Section Rules_pre.
iDestruct (own_valid_2 with "Howns Hl")
as %[[? [[av [Hav ?]]%equiv_Some_inv_r' Hav']]%singleton_included ?]%auth_valid_discrete_2.
setoid_subst.
apply -> Some_included_total in Hav'.
(* TODO: ask Robbert why did I have to change this *)
apply -> @Some_included_total in Hav'; [| apply _].
move: Hav. rewrite lookup_fmap fmap_Some.
move=> [v' [Hl Hav]]; subst.
apply to_agree_included in Hav'; setoid_subst.
......
......@@ -71,12 +71,12 @@ Section bin_log_related_under_typed_ctx.
iIntros (Δ).
+ iApply (bin_log_related_rec with "[-]"); auto;
rewrite ?cons_binder_union.
replace ({[x]} ({[f]} dom (gset string) _))
with (dom _ (<[x:=τ0]> (<[f:=TArrow τ0 τ2]> Γ'))); last first.
replace ({[x]} ({[f]} dom stringset _))
with (dom stringset (<[x:=τ0]> (<[f:=TArrow τ0 τ2]> Γ'))); last first.
{ by rewrite !dom_insert_binder. }
eapply typed_ctx_closed; eauto.
replace ({[x]} ({[f]} dom (gset string) _))
with (dom _ (<[x:=τ0]> (<[f:=TArrow τ0 τ2]> Γ'))); last first.
with (dom stringset (<[x:=τ0]> (<[f:=TArrow τ0 τ2]> Γ'))); last first.
{ by rewrite !dom_insert_binder. }
eapply typed_ctx_closed; eauto.
iAlways. iApply (IHK with "[Hrel]"); auto.
......
......@@ -582,7 +582,7 @@ Section masked.
- by iApply (bin_log_related_app with "[] []").
- assert (Closed (dom _ Γ) e).
{ apply typed_X_closed in Ht.
pose (K:=(dom_fmap (Autosubst_Classes.subst (ren (+1))) Γ)).
pose (K:=(dom_fmap (Autosubst_Classes.subst (ren (+1))) Γ (D:=stringset))).
fold_leibniz. by rewrite -K. }
iApply bin_log_related_tlam; eauto.
- by iApply bin_log_related_tapp'.
......
......@@ -12,7 +12,7 @@ Section bin_log_def.
Definition interp_env (Γ : stringmap type) (E1 E2 : coPset)
(Δ : listC D) (vvs : stringmap (val * val)) : iProp Σ :=
(dom _ Γ = dom _ vvs
(dom stringset Γ = dom stringset vvs
[ map] x τvv (map_zip Γ vvs), interp E1 E2 (fst τvv) Δ (snd τvv))%I.
Global Instance interp_env_persistent Γ E1 E2 Δ vvs :
......@@ -54,15 +54,16 @@ Section interp_env_facts.
Implicit Types τi : D.
Implicit Types Δ : listC D.
Lemma interp_env_dom Δ Γ E1 E2 vvs : interp_env Γ E1 E2 Δ vvs dom _ Γ = dom _ vvs.
Lemma interp_env_dom Δ Γ E1 E2 vvs :
interp_env Γ E1 E2 Δ vvs dom stringset Γ = dom stringset vvs.
Proof. by iIntros "[% ?]". Qed.
Lemma interp_env_Some_l Δ Γ E1 E2 vvs x τ :
Γ !! x = Some τ interp_env Γ E1 E2 Δ vvs vv, vvs !! x = Some vv interp E1 E2 τ Δ vv.
Proof.
iIntros (Hτ) "[Hdom HΓ]"; iDestruct "Hdom" as %Hdom.
destruct (elem_of_dom vvs x) as [[v Hv] ].
{ rewrite -Hdom. apply elem_of_dom. by exists τ. }
assert (x dom stringset vvs) as [v Hv]%elem_of_dom.
{ rewrite -Hdom. apply elem_of_dom. by eexists τ. }
assert (map_zip Γ vvs !! x = Some (τ, v)) as Hτv.
{ rewrite map_lookup_zip_with.
by rewrite Hτ /= Hv /=. }
......
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