Skip to content
Snippets Groups Projects
Commit 151d4e46 authored by Hai Dang's avatar Hai Dang
Browse files

bump iris

parent 2c54350f
No related branches found
No related tags found
No related merge requests found
...@@ -7,7 +7,7 @@ synopsis: "The Coq artifact for 'Stacked Borrows'" ...@@ -7,7 +7,7 @@ synopsis: "The Coq artifact for 'Stacked Borrows'"
build: [make "-j%{jobs}%"] build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
depends: [ depends: [
"coq-iris" { (= "dev.2019-08-29.2.b75bb397") | (= "dev") } "coq-iris" { (= "dev.2019-09-19.3.aa7871c7") | (= "dev") }
"coq-paco" { (= "3.0.0") } "coq-paco" { (= "3.0.0") }
"coq-equations" { (= "1.2~beta+8.8") | (= "1.2~beta+8.9") } "coq-equations" { (= "1.2~beta+8.8") | (= "1.2~beta+8.9") }
] ]
...@@ -249,13 +249,13 @@ Equations read_mem (l: loc) (n: nat) h: option value := ...@@ -249,13 +249,13 @@ Equations read_mem (l: loc) (n: nat) h: option value :=
Definition fresh_block (h : mem) : block := Definition fresh_block (h : mem) : block :=
let loclst : list loc := elements (dom (gset loc) h) in let loclst : list loc := elements (dom (gset loc) h) in
let blockset : gset block := foldr (λ l, ({[l.1]} )) loclst in let blockset : gset block := foldr (λ l, ({[l.1]} .)) loclst in
fresh blockset. fresh blockset.
Lemma is_fresh_block h i : (fresh_block h,i) dom (gset loc) h. Lemma is_fresh_block h i : (fresh_block h,i) dom (gset loc) h.
Proof. Proof.
assert ( l (ls: list loc) (X : gset block), assert ( l (ls: list loc) (X : gset block),
l ls l.1 foldr (λ l, ({[l.1]} )) X ls) as help. l ls l.1 foldr (λ l, ({[l.1]} .)) X ls) as help.
{ induction 1; set_solver. } { induction 1; set_solver. }
rewrite /fresh_block /shift /= -elem_of_elements. rewrite /fresh_block /shift /= -elem_of_elements.
move=> /(help _ _ ) /=. apply is_fresh. move=> /(help _ _ ) /=. apply is_fresh.
......
...@@ -102,11 +102,11 @@ Instance nat_sqsubseteq : SqSubsetEq nat := le. ...@@ -102,11 +102,11 @@ Instance nat_sqsubseteq : SqSubsetEq nat := le.
Instance nat_sqsubseteq_po : @PartialOrder nat () := _. Instance nat_sqsubseteq_po : @PartialOrder nat () := _.
Instance elem_of_list_suffix_proper {A : Type} (x:A) : Instance elem_of_list_suffix_proper {A : Type} (x:A) :
Proper ((suffix) ==> impl) (x ). Proper ((suffix) ==> impl) (x .).
Proof. intros l1 l2 [? ->] ?. rewrite elem_of_app. by right. Qed. Proof. intros l1 l2 [? ->] ?. rewrite elem_of_app. by right. Qed.
Instance elem_of_list_sublist_proper {A : Type} (x:A) : Instance elem_of_list_sublist_proper {A : Type} (x:A) :
Proper ((sublist) ==> impl) (x ). Proper ((sublist) ==> impl) (x .).
Proof. Proof.
intros l1 l2 SUB. induction SUB; [done|..]. intros l1 l2 SUB. induction SUB; [done|..].
- rewrite 2!elem_of_cons. intros []; [by left|right; auto]. - rewrite 2!elem_of_cons. intros []; [by left|right; auto].
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment