Commit 98ecdc91 authored by Michael Sammler's avatar Michael Sammler
Browse files

update iris

parent 5d1b43a8
Pipeline #48910 passed with stage
in 21 minutes and 33 seconds
......@@ -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.2021-06-12.0.3cb65333") | (= "dev") }
"coq-iris" { (= "dev.2021-06-18.1.bd9d16c9") | (= "dev") }
"dune" {>= "2.7.0"}
"cerberus" {= "~dev"}
"cmdliner" {>= "1.0.4"}
......
......@@ -539,7 +539,7 @@ Section heap.
rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /= Z.add_0_r.
etrans. { apply (IH (a + 1)). move => a' Ha'. apply Hfree => /=. lia. }
rewrite -insert_singleton_op; last first.
{ rewrite -equiv_None big_opL_commute equiv_None big_opL_None=> l' v' ?.
{ rewrite -None_equiv_eq big_opL_commute None_equiv_eq big_opL_None=> l' v' ?.
rewrite lookup_singleton_None. lia. }
rewrite /heap_alloc /heap_update -/heap_update.
rewrite to_heapUR_insert. setoid_rewrite Z.add_assoc.
......
......@@ -47,8 +47,8 @@ Section function.
iPureIntro. apply: Forall2_same_length_lookup_2. { rewrite -Hlen. symmetry. by apply: length_proper. }
move => i ty [??] Haty Harg.
move: Hatys => /list_equiv_lookup Hatys.
have := Hatys i. rewrite Haty => /(equiv_Some_inv_r' _ _)[? [? [?->?]]].
by apply: (Hall _ _ (_, _)).
have := Hatys i. rewrite Haty => /(Some_equiv_eq _ _)[? [? [?<-?]]].
by apply: (Hall _ _ (_, _)).
}
iIntros "!>" (lsa lsv) "[Hv Ha] %". rewrite -HPa.
have [|lsa' Hlsa]:= vec_cast _ lsa (length (fp_atys (fp1 x))). { by rewrite Hatys. }
......@@ -57,8 +57,8 @@ Section function.
iFrame. iApply (big_sepL2_impl' with "Hv") => //. by rewrite Hatys.
move: Hatys => /list_equiv_lookup Hatys.
iIntros "!>" (k ????? Haty2 ? Haty1) "?".
have := Hatys k. rewrite Haty1 Haty2=> /(equiv_Some_inv_r' _ _)[? [? [Heql ??]]].
rewrite Heql. by simplify_eq.
have := Hatys k. rewrite Haty1 Haty2=> /(Some_equiv_eq _ _)[?[? [Heql ? ?]]].
rewrite -Heql. by simplify_eq.
}
iApply "HT". by rewrite -Hlsa.
- rewrite /typed_stmt_post_cond. iIntros (v).
......
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