Commit 2943146f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris, and remove some stuff that's in Iris now.

parent be74f7c1
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
depends: [
"coq-iris" { (= "dev.2019-11-21.0.e0d10c05") | (= "dev") }
"coq-iris" { (= "dev.2020-01-23.2.e2f65bbd") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -37,55 +37,3 @@ Ltac properness :=
| |- (_ _)%I (_ _)%I => apply sep_proper
| |- (inv _ _)%I (inv _ _)%I => apply (contractive_proper _)
end.
Section big_opm.
Context `{Countable K} {A : ofeT}.
Context `{Monoid M o}.
Infix "`o`" := o (at level 50, left associativity).
Implicit Types m : gmap K A.
Implicit Types f g : K A M.
Global Instance big_opM_ne2 n `{Proper _ (dist n ==> dist n ==> dist n) o} :
Proper (pointwise_relation _ (dist n ==> dist n) ==> dist n ==> dist n)
(big_opM o (K:=K) (A:=A)).
Proof.
intros f g Hf m1.
induction m1 as [|i x m Hnone IH] using map_ind.
{ intros m2 Hm2. rewrite big_opM_empty.
induction m2 as [|j y m2 ? IH2] using map_ind.
- by rewrite big_opM_empty.
- exfalso.
specialize (Hm2 j). revert Hm2.
rewrite lookup_insert lookup_empty /=. by inversion 1. }
intros m2 Hm2.
assert (is_Some (m2 !! i)) as [y Hy].
{ specialize (Hm2 i). revert Hm2. rewrite lookup_insert=>Hm2.
destruct (m2 !! i); first naive_solver.
inversion Hm2. }
replace m2 with (<[i:=y]>(delete i m2)).
- rewrite !big_opM_insert // /=; last by apply lookup_delete.
f_equiv.
+ apply Hf. specialize (Hm2 i). revert Hm2.
rewrite Hy lookup_insert //. by inversion 1.
+ apply IH=> j.
destruct (decide (j = i)) as [->|?].
* by rewrite lookup_delete Hnone.
* rewrite lookup_delete_ne//. specialize (Hm2 j).
revert Hm2. by rewrite lookup_insert_ne.
- rewrite insert_delete insert_id //.
Qed.
End big_opm.
(** todo move somewhere *)
Instance map_zip_with_ne {K} {A B C : ofeT} (f : A B C)
`{Countable K} `{!EqDecision K} n :
Proper (dist n ==> dist n ==> dist n) f
Proper (dist n ==> dist n ==> dist n)
(@map_zip_with (gmap K) _ _ _ _ f).
Proof.
intros Hf m1 m2 Hm2 m1' m2' Hm2' i.
rewrite !map_lookup_zip_with. f_equiv =>//.
intros x1 x2 Hx2. f_equiv =>//.
intros y1 y2 Hy2. repeat f_equiv =>//.
Qed.
......@@ -186,16 +186,7 @@ Section env_typed.
Global Instance env_ltyped2_ne n :
Proper (dist n ==> (=) ==> dist n) env_ltyped2.
Proof.
intros Γ Γ' HΓ ? vvs ->.
rewrite /env_ltyped2 /big_sepM2.
f_equiv.
- f_equiv.
split;
intros Hvvs x; specialize (HΓ x); rewrite -(Hvvs x);
by apply (is_Some_ne n).
- apply big_opM_ne2; first apply _.
+ by intros x A B ->.
+ apply map_zip_with_ne=>//. apply _.
intros Γ Γ' HΓ ? vvs ->. apply big_sepM2_ne_2; [done..|solve_proper].
Qed.
Global Instance env_ltyped2_proper :
......
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