Commit 64101a38 authored by Michael Sammler's avatar Michael Sammler
Browse files

update iris

parent e85e4ffc
Pipeline #48638 passed with stage
in 22 minutes and 52 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-10.0.5d80dfef") | (= "dev") }
"coq-iris" { (= "dev.2021-06-12.0.3cb65333") | (= "dev") }
"dune" {>= "2.7.0"}
"cerberus" {= "~dev"}
"cmdliner" {>= "1.0.4"}
......
......@@ -378,7 +378,7 @@ Proof. elim: l y => //=. Qed.
Lemma list_lookup_length_default_last {A} (x : A) (l : list A) :
(x :: l) !! length l = Some (default x (last l)).
Proof. elim: l x => //= a l IH x. rewrite IH. f_equal. destruct l => //. apply default_last_cons. Qed.
Proof. elim: l x => //= a l IH x. rewrite IH. f_equal. destruct l => //=. apply default_last_cons. Qed.
Reserved Notation "'[∧' 'map]' k ↦ x ∈ m , P"
......
......@@ -36,7 +36,7 @@ Section tyfold.
iDestruct "Htys" as "[H1 Hty2]". iDestruct "H1" as (l1 l2 ??) "H1". simplify_eq.
iExists l2. rewrite tyexists_eq. iExists ls. rewrite tyexists_eq. iSplit => //.
iSplitL "H1" => //=. rewrite /tyown_constraint. iSplit => //. iFrame.
iStopProof. f_equiv. destruct ls =>//. by apply default_last_cons.
iStopProof. f_equiv. destruct ls =>//=. by apply default_last_cons.
Qed.
Global Instance simplify_hyp_place_tyfold_optional_inst l β ls tys b:
SimplifyHypPlace l β (ls @ tyfold tys b) (Some 50%N) :=
......@@ -56,7 +56,7 @@ Section tyfold.
iIntros "HT". iExists _. iFrame. iDestruct 1 as (l2 ls2 ->) "[Hl [% [Htys Hb]]]".
iSplit => /=. by iPureIntro; f_equal. iFrame.
iSplitR "Hb"; first by eauto with iFrame.
iStopProof. f_equiv. destruct ls2 =>//. by apply default_last_cons.
iStopProof. f_equiv. destruct ls2 =>//=. by apply default_last_cons.
Qed.
Global Instance simplify_goal_place_tyfold_cons_inst l β ls ty tys b:
SimplifyGoalPlace l β (ls @ tyfold (ty :: tys) b) (Some 0%N) :=
......
Supports Markdown
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