Commit a9db2f6b authored by Michael Sammler's avatar Michael Sammler

update iris dependency

parent dc744bb2
......@@ -17,7 +17,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
depends: [
"coq" { (>= "8.12.0" & < "8.13~") }
"coq-iris" { (= "dev.2020-10-01.3.8f6c063a") | (= "dev") }
"coq-iris" { (= "dev.2020-11-12.3.126531ec") | (= "dev") }
"dune" {>= "2.7.0"}
"cerberus" {= "~dev"}
"cmdliner" {>= "1.0.4"}
......
......@@ -66,21 +66,6 @@ Lemma entails_eq {PROP : bi} (P1 P2 : PROP) :
P1 = P2 P1 - P2.
Proof. move => ->. reflexivity. Qed.
Section theorems.
Context `{FinMapDom K M D}.
Lemma dom_list_to_map {A} (l : list (K * A)) :
dom D (list_to_map (M:=M A) l) list_to_set l.*1.
Proof using Type*.
elim: l => /=. { by apply dom_empty. }
move => ? l <-. by apply dom_insert.
Qed.
Lemma dom_list_to_map_L {A} (l : list (K * A)) `{!LeibnizEquiv D}:
dom D (list_to_map (M:=M A) l) = list_to_set l.*1.
Proof using Type*. unfold_leibniz. apply: dom_list_to_map. Qed.
End theorems.
Section list_to_map.
Context `{FinMap K M}.
......@@ -585,3 +570,14 @@ Qed.
Lemma if_bool_decide_eq_branches {A} P `{!Decision P} (x : A) :
(if bool_decide P then x else x) = x.
Proof. by case_bool_decide. Qed.
(* from https://mattermost.mpi-sws.org/iris/pl/dcktjjjpsiycmrieyh74bzoagr *)
Ltac solve_sep_entails :=
try (apply equiv_spec; split);
iIntros;
repeat iMatchHyp (fun H P =>
lazymatch P with
| (_ _)%I => iDestruct H as "[??]"
| ( _, _)%I => iDestruct H as (?) "?"
end);
eauto with iFrame.
From stdpp Require Import coPset.
From iris.algebra Require Import big_op gmap frac agree.
From iris.algebra Require Import csum excl auth cmra_big_op numbers.
From iris.bi Require Import fractional tactics.
From iris.bi Require Import fractional.
From iris.base_logic Require Export lib.own.
From iris.proofmode Require Export tactics.
From refinedc.lang Require Export lang.
......@@ -226,7 +226,8 @@ Section allocs.
Proof.
move: a1 a2 => ? ?. rewrite allocs_entry_eq /allocs_entry_def.
iIntros "H1 H2". iCombine "H1 H2" as "H".
by iDestruct (own_valid with "H") as %H%singleton_valid%to_agree_op_inv_L.
iDestruct (own_valid with "H") as %Hvalid.
by move: Hvalid => /auth_frag_valid/singleton_valid/to_agree_op_inv_L.
Qed.
Lemma allocs_alloc ub id a :
......@@ -363,10 +364,7 @@ Section heap.
Lemma heap_mapsto_nil l q:
l {q} [] loc_in_bounds l 0.
Proof.
rewrite heap_mapsto_eq/heap_mapsto_def /=.
apply equiv_spec. split; solve_sep_entails.
Qed.
Proof. rewrite heap_mapsto_eq/heap_mapsto_def /=. solve_sep_entails. Qed.
Lemma heap_mapsto_cons_mbyte l b v q:
l {q} (b::v) heap_mapsto_mbyte l q b loc_in_bounds l 1 (l + 1) {q} v.
......@@ -374,8 +372,8 @@ Section heap.
rewrite heap_mapsto_eq/heap_mapsto_def /= shift_loc_0. setoid_rewrite shift_loc_assoc.
have Hn:( n, Z.of_nat (S n) = 1 + n) by lia. setoid_rewrite Hn.
have ->:( n, S n = 1 + n)%nat by lia.
rewrite -loc_in_bounds_split. have <- : (1 = 1%nat) by lia.
apply equiv_spec. split; solve_sep_entails.
rewrite -loc_in_bounds_split.
solve_sep_entails.
Qed.
Lemma heap_mapsto_cons l b v q:
......@@ -383,7 +381,7 @@ Section heap.
Proof.
rewrite heap_mapsto_cons_mbyte !assoc. f_equiv.
rewrite heap_mapsto_eq/heap_mapsto_def /= shift_loc_0.
apply equiv_spec. split; solve_sep_entails.
solve_sep_entails.
Qed.
Lemma heap_mapsto_app l v1 v2 q:
......
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