Commit a249c071 authored by Robbert Krebbers's avatar Robbert Krebbers

WIP: Bump Iris.

parent 8d8b842a
......@@ -7,5 +7,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris-c-monad"]
depends: [
"coq-iris" { (= "dev.2018-10-11.0.f426901d") | (= "dev") }
"coq-iris" { (= "dev.2018-11-08.2.9eee9408") | (= "dev") }
]
......@@ -10,14 +10,14 @@ From iris_c.lib Require Import mset flock.
Definition a_ret : val := λ: "a" <> <>, "a".
(* (A → M B) → M A → M B *)
Definition a_bind : val := λ: "f" "x" "env" "l",
Definition a_bind : val := λ: "x" "f" "env" "l",
let: "a" := "x" "env" "l" in
"f" "a" "env" "l".
Notation "x ←ᶜ y ;;ᶜ z" :=
(a_bind (λ: x, z) y)%E
(a_bind y (λ: x, z))%E
(at level 100, y at next level, z at level 200, right associativity) : expr_scope.
Notation "x ;;ᶜ z" := (a_bind (λ: <>, z) x)%E
Notation "y ;;ᶜ z" := (a_bind y (λ: <>, z))%E
(at level 100, z at level 200, right associativity) : expr_scope.
(* M A → A *)
......@@ -121,11 +121,13 @@ Section a_wp_rules.
Qed.
Lemma wp_awp_bind R Φ K e :
WP e {{ v, AWP (fill K (of_val v)) @ R {{ Φ }} }} - AWP (fill K e) @ R {{ Φ }}.
WP e {{ v, AWP (fill K (of_val v)) @ R {{ Φ }} }} -
AWP (fill K e) @ R {{ Φ }}.
Proof. by apply: wp_bind. Qed.
Lemma wp_awp_bind_inv R Φ K e :
AWP (fill K e) @ R {{ Φ }} - WP e {{ v, AWP (fill K (of_val v)) @ R {{ Φ }} }}.
AWP (fill K e) @ R {{ Φ }} -
WP e {{ v, AWP (fill K (of_val v)) @ R {{ Φ }} }}.
Proof. by apply: wp_bind_inv. Qed.
Lemma awp_insert_res e Φ R1 R2 :
......@@ -181,37 +183,34 @@ Section a_wp_rules.
Lemma awp_ret e R Φ :
WP e {{ Φ }} - AWP (a_ret e) @ R {{ Φ }}.
Proof.
iIntros "Hwp". rewrite /awp /a_ret /=. wp_apply (wp_wand with "Hwp").
iIntros (v) "HΦ". wp_lam.
iIntros (γ env l I) "#Hlock Hres #Heq". do 2 wp_lam. iFrame.
iIntros "Hwp". rewrite /awp /=. wp_apply (wp_wand with "Hwp").
iIntros (v) "HΦ". wp_lam. wp_pures.
iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures. iFrame.
Qed.
Lemma awp_bind (f e : expr) R Φ :
AsVal f
Lemma awp_bind (f : val) (e : expr) R Φ :
AWP e @ R {{ ev, AWP (f ev) @ R {{ Φ }} }} -
AWP (a_bind f e) @ R {{ Φ }}.
AWP a_bind e f @ R {{ Φ }}.
Proof.
iIntros ([fv <-]) "Hwp". rewrite /awp /a_bind /=.
iIntros "Hwp". rewrite /awp /=.
wp_apply (wp_wand with "Hwp"). iIntros (ev) "Hwp".
wp_lam. wp_lam.
iIntros (γ env l I) "#Hflock Hres #Heq". do 2 wp_lam. wp_bind (ev env l).
wp_lam. wp_pures.
iIntros (γ env l I) "#Hflock Hres #Heq". wp_pures. wp_bind (ev env l).
iApply (wp_wand with "[Hwp Hres]"). iApply ("Hwp" with "Hflock Hres Heq").
iIntros (w) "[Hwp Hres]". wp_let. wp_apply (wp_wand with "Hwp").
iIntros (v) "H". iApply ("H" with "Hflock Hres Heq").
Qed.
Lemma awp_atomic (e : expr) (ev : val) R Φ :
IntoVal e ev
Lemma awp_atomic (ev : val) R Φ :
(R - R', R' AWP ev #() @ R' {{ w, R' - R Φ w }}) -
AWP a_atomic e @ R {{ Φ }}.
AWP a_atomic ev @ R {{ Φ }}.
Proof.
iIntros (<-) "Hwp". rewrite /awp /a_atomic /=. wp_lam.
iIntros (γ env l I) "#Hlock1 Hres #Heq1". do 2 wp_let.
iIntros "Hwp". rewrite /awp /=. wp_lam. wp_pures.
iIntros (γ env l I) "#Hlock1 Hres #Heq1". wp_pures.
wp_apply (acquire_cancel_spec with "[$]").
iIntros "[HI Hcl]". iRewrite "Heq1" in "HI".
iDestruct "HI" as "[Henv HR]".
iDestruct ("Hwp" with "HR") as (Q) "[HQ Hwp]".
wp_seq.
wp_apply (newlock_cancel_spec amonadN); first done.
iIntros (k γ') "#Hlock2".
iMod (flock_res_single_alloc _ (dom (gset prop_id) I) _ _ (env_inv env Q)%I
......@@ -232,27 +231,26 @@ Section a_wp_rules.
iMod ("Hcl" with "[HR Henv]") as "[Hflocked Hres]".
{ iNext. iRewrite "Heq1". iFrame. }
wp_apply (release_cancel_spec with "[$Hlock1 $Hflocked]").
iIntros "_". wp_seq. iFrame.
iIntros "_". wp_pures. iFrame.
Qed.
Lemma awp_atomic_env (e : expr) (ev : val) R Φ :
IntoVal e ev
Lemma awp_atomic_env (ev : val) R Φ :
( env, env_inv env - R -
WP ev env {{ w, (env_inv env R Φ w) }}) -
AWP a_atomic_env e @ R {{ Φ }}.
AWP a_atomic_env ev @ R {{ Φ }}.
Proof.
iIntros (<-) "Hwp". rewrite /awp /a_atomic_env /=. wp_lam.
iIntros (γ env l I) "#Hlock Hres #Heq". do 2 wp_lam.
iIntros "Hwp". rewrite /awp /=. wp_lam. wp_pures.
iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures.
wp_apply (acquire_cancel_spec with "[$]").
iIntros "[HI Hcl]". iRewrite "Heq" in "HI".
iDestruct "HI" as "[Henv HR]".
iDestruct ("Hwp" with "Henv HR") as "Hwp".
wp_seq. wp_apply (wp_wand with "Hwp").
iIntros (w) "[Henv [HR HΦ]]". wp_let.
wp_apply (wp_wand with "Hwp").
iIntros (w) "[Henv [HR HΦ]]". wp_pures.
iRewrite "Heq" in "Hcl".
iMod ("Hcl" with "[$HR $Henv]") as "[Hflocked Hres]".
wp_apply (release_cancel_spec with "[$Hlock $Hflocked]").
iIntros "_". wp_seq. iFrame.
iIntros "_". wp_pures. iFrame.
Qed.
Lemma awp_par (Ψ1 Ψ2 : val iProp Σ) e1 e2 R (Φ : val iProp Σ) :
......@@ -261,12 +259,12 @@ Section a_wp_rules.
( w1 w2, Ψ1 w1 - Ψ2 w2 - Φ (w1,w2)%V) -
AWP e1 ||| e2 @ R {{ Φ }}.
Proof.
iIntros "Hwp1 Hwp2 HΦ". rewrite /a_par /awp /=.
iIntros "Hwp1 Hwp2 HΦ". rewrite /awp /=.
wp_apply (wp_wand with "Hwp2").
iIntros (ev2) "Hwp2".
wp_apply (wp_wand with "Hwp1").
iIntros (ev1) "Hwp1". do 2 wp_lam.
iIntros (γ env l I) "#Hlock Hres #Heq". do 2 wp_lam.
iIntros (ev1) "Hwp1". wp_lam. wp_pures.
iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures.
pose (I' := fmap (λ x, (x.1, (x.2/2)%Qp)) I).
iAssert (flock_resources γ I' flock_resources γ I')%I with "[Hres]" as "[Hres1 Hres2]".
{ rewrite /flock_resources -big_sepM_sepM.
......@@ -294,12 +292,11 @@ End a_wp_rules.
Section a_wp_run.
Context `{heapG Σ, flockG Σ, spawnG Σ, locking_heapPreG Σ}.
Lemma awp_run (e : expr) R Φ :
AsVal e
R - ( `{amonadG Σ}, AWP e @ R {{ w, R ={}= Φ w }}) -
WP a_run e {{ Φ }}.
Lemma awp_run (ev : val) R Φ :
R - ( `{amonadG Σ}, AWP ev @ R {{ w, R ={}= Φ w }}) -
WP a_run ev {{ Φ }}.
Proof.
iIntros ([ev <-]) "HR Hwp". rewrite /awp /a_run /=. wp_let.
iIntros "HR Hwp". rewrite /awp /=. wp_lam.
wp_bind (mset_create #()). iApply mset_create_spec; first done.
iNext. iIntros (env) "Henv". wp_let.
iMod locking_heap_init as (?) "Hσ".
......
......@@ -64,22 +64,36 @@ Tactic Notation "awp_pure" open_constr(efoc) :=
|apply _ (* PureExec *)
|try fast_done (* The pure condition for PureExec *)
|apply _ (* IntoLaters *)
|simpl_subst
|simpl
])
|| fail "awp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
| _ => fail "awp_pure: not an 'awp'"
end.
(* See Iris for documentation on this tactic *)
Ltac awp_pures :=
iStartProof;
repeat (awp_pure _; []). (* The `;[]` makes sure that no side-condition
magically spawns. *)
Tactic Notation "awp_rec" :=
let H := fresh in
assert (H := AsRecV_recv_locked);
awp_pure (App _ _);
clear H.
Tactic Notation "awp_if" := awp_pure (If _ _ _).
Tactic Notation "awp_if_true" := awp_pure (If (Lit (LitBool true)) _ _).
Tactic Notation "awp_if_false" := awp_pure (If (Lit (LitBool false)) _ _).
Tactic Notation "awp_if_true" := awp_pure (If (LitV (LitBool true)) _ _).
Tactic Notation "awp_if_false" := awp_pure (If (LitV (LitBool false)) _ _).
Tactic Notation "awp_unop" := awp_pure (UnOp _ _).
Tactic Notation "awp_binop" := awp_pure (BinOp _ _ _).
Tactic Notation "awp_op" := awp_unop || awp_binop.
Tactic Notation "awp_rec" := awp_pure (App _ _).
Tactic Notation "awp_lam" := awp_rec.
Tactic Notation "awp_let" := awp_lam.
Tactic Notation "awp_seq" := awp_lam.
Tactic Notation "awp_proj" := awp_pure (Fst _) || awp_pure (Snd _).
Tactic Notation "awp_case" := awp_pure (Case _ _ _).
Tactic Notation "awp_match" := awp_case; awp_let.
Tactic Notation "awp_inj" := awp_pure (InjL _) || wp_pure (InjR _).
Tactic Notation "awp_pair" := awp_pure (Pair _ _).
Tactic Notation "awp_closure" := awp_pure (Rec _ _ _).
This diff is collapsed.
......@@ -75,7 +75,7 @@ Section proof.
Proof.
iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
wp_apply (try_acquire_spec with "Hl"). iIntros ([]).
- iIntros "[Hlked HR]". iMod ("HΦ" with "[$Hlked $HR]"). wp_if. done.
- iIntros "[Hlked HR]". iMod ("HΦ" with "[$Hlked $HR]"). by wp_pures.
- iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
Qed.
......@@ -83,8 +83,8 @@ Section proof.
{{{ is_lock γ lk R locked γ R }}} release lk {{{ RET #(); True }}}.
Proof.
iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
iDestruct "Hlock" as (l ->) "#Hinv".
rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
iDestruct "Hlock" as (l ->) "#Hinv". wp_lam.
iInv N as (b) "[Hl _]" "Hclose".
wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
Qed.
End proof.
......
......@@ -45,7 +45,7 @@ Section test.
s1 C #0 - l C #1 - s2 C #0 -
AWP ♯ₗs1 = ∗ᶜ ♯ₗl ; ∗ᶜ ♯ₗs1 + 42 @ R {{ _, s1 C #1 l C #1 }}.
Proof.
iIntros "Hs1 Hl Hs2". vcg_solver. iModIntro.
iIntros "Hs1 Hl Hs2". vcg_solver.
rewrite Qp_half_half. eauto with iFrame.
Qed.
......@@ -118,7 +118,7 @@ Section test.
l C #0 -
AWP ♯ₗl = 2 ; 1 + (♯ₗl = 1) {{ _, l C[LLvl] #1 }}.
Proof.
iIntros "Hl". vcg_solver. iModIntro. eauto with iFrame.
iIntros "Hl". vcg_solver. eauto with iFrame.
Qed.
Lemma test_seq4 l k :
......@@ -128,7 +128,7 @@ Section test.
{{ v, v = #4 l C[LLvl] #1 k C[LLvl] #1 }}.
Proof.
iIntros "Hl Hk".
vcg_solver. iModIntro. by eauto with iFrame.
vcg_solver. by eauto with iFrame.
Qed.
Definition stupid (l : cloc) : expr :=
a_store (♯ₗ l) ( 1); a_ret #0.
......@@ -175,11 +175,10 @@ Section test.
l C #1 -
AWP while (∗ᶜ ♯ₗl < 2) { ♯ₗl = 1 } @ R {{ _, True }}.
Proof.
iIntros "Hl".
iLöb as "IH".
iApply a_while_spec'. iNext.
iIntros "Hl". iApply a_while_spec.
iLöb as "IH". iApply a_whileV_spec. iNext.
vcg_solver. rewrite Qp_half_half. iIntros "Hl".
iLeft. iSplitR; eauto.
iLeft. iSplitR; eauto. iModIntro.
vcg_solver. iIntros "Hl". iModIntro. by iApply "IH".
Qed.
End test.
......@@ -30,8 +30,8 @@ Section factorial_spec.
AWP factorial_body #n (cloc_to_val c) (cloc_to_val r) @ R
{{ _, c C #n r C #(fact n) }}.
Proof.
iIntros "(Hk & Hc & Hr)". do 3 awp_lam.
iLöb as "IH" forall (n k) "Hk Hc Hr". iApply a_while_spec'. iNext.
iIntros "(Hk & Hc & Hr)". awp_lam. awp_pures.
iLöb as "IH" forall (n k) "Hk Hc Hr". iApply a_whileV_spec. iNext.
vcg_solver. rewrite Qp_half_half. iIntros "Hr Hc".
case_bool_decide.
+ iLeft. iSplit; eauto.
......
This diff is collapsed.
......@@ -275,7 +275,7 @@ Section denv_spec.
iApply (big_sepL_impl (λ _ _, True)%I); first by rewrite big_sepL_True.
iAlways. iIntros (? dio Hk) "_ %".
destruct dio; eauto.
apply denv_singleton_lookup in Hk as [? ->]. omega.
apply denv_singleton_lookup in Hk as [? ->]. lia.
- iIntros "[$ _]".
Qed.
......@@ -299,11 +299,11 @@ Section denv_spec.
* iIntros "[H1 H2]".
rewrite /denv_interp_aux. simpl. iDestruct "H1" as "[$ H1]".
iDestruct ("IHm" $! i (k+1)%nat with "[H1 H2]") as "H".
{ assert ((k + 1 + i)%nat = (k + S i)%nat) as -> by omega. iFrame "H2".
{ assert ((k + 1 + i)%nat = (k + S i)%nat) as -> by lia. iFrame "H2".
iApply (big_sepL_mono with "H1"). intros n y ?. simpl.
assert ((k + 1 + n)%nat = (k + S n)%nat) as -> by omega. done. }
assert ((k + 1 + n)%nat = (k + S n)%nat) as -> by lia. done. }
iApply (big_sepL_mono with "H"). intros n y ?. simpl.
assert ((k + 1 + n)%nat = (k + S n)%nat) as -> by omega. done.
assert ((k + 1 + n)%nat = (k + S n)%nat) as -> by lia. done.
+ destruct i as [|i].
* iIntros "[H1 H2]".
rewrite /denv_interp_aux. simpl.
......@@ -311,11 +311,11 @@ Section denv_spec.
* iIntros "[H1 H2]".
rewrite /denv_interp_aux. simpl. iDestruct "H1" as "[$ H1]".
iDestruct ("IHm" $! i (k+1)%nat with "[H1 H2]") as "H".
{ assert ((k + 1 + i)%nat = (k + S i)%nat) as -> by omega. iFrame "H2".
{ assert ((k + 1 + i)%nat = (k + S i)%nat) as -> by lia. iFrame "H2".
iApply (big_sepL_mono with "H1"). intros n y ?. simpl.
assert ((k + 1 + n)%nat = (k + S n)%nat) as -> by omega. done. }
assert ((k + 1 + n)%nat = (k + S n)%nat) as -> by lia. done. }
iApply (big_sepL_mono with "H"). intros n y ?. simpl.
assert ((k + 1 + n)%nat = (k + S n)%nat) as -> by omega. done.
assert ((k + 1 + n)%nat = (k + S n)%nat) as -> by lia. done.
Qed.
Lemma denv_insert_interp E m i x q dv :
......@@ -335,22 +335,22 @@ Section denv_spec.
iSpecialize ("IH1" with "[H1 H2]").
{ iSplitL "H1".
- iApply (big_sepL_mono with "H1"). intros n y ?. simpl.
assert ((k + S n)%nat = ((S k) + n)%nat) as -> by omega. reflexivity.
assert ((k + S n)%nat = ((S k) + n)%nat) as -> by lia. reflexivity.
- iApply (big_sepL_mono with "H2"). intros n y ?. simpl.
assert ((k + S n)%nat = ((S k) + n)%nat) as -> by omega. reflexivity. }
assert ((k + S n)%nat = ((S k) + n)%nat) as -> by lia. reflexivity. }
(* TODO: this can be factored away *)
destruct dio1 as [d1|], dio2 as [d2|]; simpl; iFrame.
+ destruct d1, d2. simpl.
iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
iCombine "Hl1 Hl2" as "$".
iApply (big_sepL_mono with "IH1"). intros n y ?. simpl.
assert ((k + S n)%nat = ((S k) + n)%nat) as -> by omega. done.
assert ((k + S n)%nat = ((S k) + n)%nat) as -> by lia. done.
+ iApply (big_sepL_mono with "IH1"). intros n y ?. simpl.
assert ((k + S n)%nat = ((S k) + n)%nat) as -> by omega. done.
assert ((k + S n)%nat = ((S k) + n)%nat) as -> by lia. done.
+ iApply (big_sepL_mono with "IH1"). intros n y ?. simpl.
assert ((k + S n)%nat = ((S k) + n)%nat) as -> by omega. done.
assert ((k + S n)%nat = ((S k) + n)%nat) as -> by lia. done.
+ iApply (big_sepL_mono with "IH1"). intros n y ?. simpl.
assert ((k + S n)%nat = ((S k) + n)%nat) as -> by omega. done.
assert ((k + S n)%nat = ((S k) + n)%nat) as -> by lia. done.
Qed.
Lemma denv_merge_interp E m1 m2 :
......@@ -375,13 +375,13 @@ Section denv_spec.
iSpecialize ("IHm" $! _ (k+1)%nat with "[] [Hm]"); eauto.
{ iApply (big_sepL_mono with "Hm").
intros n y ?. simpl.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by omega.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by lia.
done. }
assert ((k+1+i)%nat = (k + S i)%nat) as -> by omega.
assert ((k+1+i)%nat = (k + S i)%nat) as -> by lia.
iDestruct "IHm" as "[H $]".
iApply (big_sepL_mono with "H").
intros n y ?. simpl.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by omega. done.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by lia. done.
Qed.
Lemma denv_delete_frac_interp_aux_flip E i k m m' q dv :
......@@ -400,14 +400,14 @@ Section denv_spec.
as [[[mf q'] dv']|] eqn:Hdenv; simplify_eq/=.
iIntros "[[$ Hmf] Hl]".
iSpecialize ("IHm" $! _ (k+1)%nat with "[] [-]"); eauto.
{ assert ((k+1+i)%nat = (k + S i)%nat) as -> by omega. iFrame "Hl".
{ assert ((k+1+i)%nat = (k + S i)%nat) as -> by lia. iFrame "Hl".
iApply (big_sepL_mono with "Hmf").
intros n y ?. simpl.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by omega.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by lia.
done. }
iApply (big_sepL_mono with "IHm").
intros n y ?. simpl.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by omega. done.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by lia. done.
Qed.
Lemma denv_delete_frac_interp E i m m' q dv :
......@@ -437,13 +437,13 @@ Section denv_spec.
iSpecialize ("IHm" $! i (k+1)%nat with "[] [Hm]"); eauto.
* iApply (big_sepL_mono with "Hm").
intros n y ?. simpl.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by omega.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by lia.
done.
* assert ((k+1+i)%nat = (k + S i)%nat) as -> by omega.
* assert ((k+1+i)%nat = (k + S i)%nat) as -> by lia.
iDestruct "IHm" as "[H $]".
iApply (big_sepL_mono with "H").
intros n y ?. simpl.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by omega. done.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by lia. done.
Qed.
Lemma denv_delete_full_interp_aux_flip E i k m m' q dv :
......@@ -462,14 +462,14 @@ Section denv_spec.
as [[[mf q'] dv']|] eqn:Hdenv; simplify_eq/=.
iIntros "[[$ Hm] Hl]".
iSpecialize ("IHm" $! i (k+1)%nat with "[] [-]"); eauto.
* assert ((k+1+i)%nat = (k + S i)%nat) as -> by omega. iFrame "Hl".
* assert ((k+1+i)%nat = (k + S i)%nat) as -> by lia. iFrame "Hl".
iApply (big_sepL_mono with "Hm").
intros n y ?. simpl.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by omega.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by lia.
done.
* iApply (big_sepL_mono with "IHm").
intros n y ?. simpl.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by omega. done.
assert ((k+1+n)%nat = (k + S n)%nat) as -> by lia. done.
Qed.
Lemma denv_delete_full_interp E i m m' dv :
......@@ -834,9 +834,9 @@ Section denv_spec.
denv_wf_len E (denv_merge m1 m2).
Proof.
rewrite /denv_wf_len. bool_decide_unfold.
revert m1 m2. induction E; destruct m1, m2; try naive_solver omega.
revert m1 m2. induction E; destruct m1, m2; try naive_solver lia.
simpl. intros.
apply le_n_S. eapply IHE; omega.
apply le_n_S. eapply IHE; lia.
Qed.
Lemma denv_wf_merge E m1 m2 :
......@@ -869,8 +869,8 @@ Section denv_spec.
denv_wf_len E m denv_wf_len E (denv_unlock m).
Proof.
rewrite /denv_wf_len. bool_decide_unfold.
revert m; induction E; destruct m; try naive_solver omega.
simpl. intros. apply le_n_S. eapply IHE. omega.
revert m; induction E; destruct m; try naive_solver lia.
simpl. intros. apply le_n_S. eapply IHE. lia.
Qed.
Lemma denv_wf_unlock E m :
......@@ -936,7 +936,7 @@ Section denv_spec.
Proof.
rewrite /denv_wf_len.
intros ? ?%denv_delete_frac_len.
bool_decide_unfold. omega.
bool_decide_unfold. lia.
Qed.
Lemma denv_wf_len_delete_full_aux E i m m' q dv :
......@@ -945,7 +945,7 @@ Section denv_spec.
Proof.
rewrite /denv_wf_len.
intros ? ?%denv_delete_full_len.
bool_decide_unfold. omega.
bool_decide_unfold. lia.
Qed.
Lemma denv_delete_frac_idx i m m' q dv :
......@@ -1026,15 +1026,15 @@ Section denv_spec.
split_and; bool_decide_unfold;
eauto using denv_wf_val_singleton.
rewrite denv_singleton_length.
apply lookup_lt_is_Some in Hi. omega.
apply lookup_lt_is_Some in Hi. lia.
Qed.
Lemma denv_insert_length i x q dv m:
length (denv_insert i x q dv m) = max (S i) (length m).
Proof.
revert m. induction i as [|i']=>m.
+ destruct m as [|dio m]; simpl. omega.
destruct dio as [[]|]; naive_solver omega.
+ destruct m as [|dio m]; simpl. lia.
destruct dio as [[]|]; naive_solver lia.
+ destruct m as [|dio m]; cbn-[max].
* rewrite denv_singleton_length. lia.
* rewrite -Nat.succ_max_distr. f_equal.
......@@ -1216,7 +1216,7 @@ Section denv_spec.
apply denv_wf_insert; eauto.
{ rewrite /dloc_wf. bool_decide_unfold.
apply lookup_lt_is_Some. rewrite app_length /=.
omega. }
lia. }
by eapply denv_wf_mono.
Qed.
End denv_spec.
......@@ -100,7 +100,7 @@ Section tactics.
E = penv_to_known_locs Γls
ListOfMapsto Γls E m
IntoDCExpr E e de
dcexpr_wf [] E de
dcexpr_wf E de
denv_wf (penv_to_known_locs Γls) m
envs_entails (Envs Γp Γs_out c)
(vcg_wp E m de R (λ E m dv,
......@@ -159,7 +159,7 @@ Ltac vcg_solver :=
| apply _ (* Reify the expression *)
| vm_compute[reflexivity]; try done (* Prove that the reified expression is well-formed *)
| done (* Prove that the environment is well-formed *)
| simpl; simpl_subst ].
| simpl ].
Ltac vcg_continue :=
eapply tac_exists_known_locs;
......@@ -168,4 +168,4 @@ Ltac vcg_continue :=
| apply _ (* ListOfMapsto Γls (E_old ++ E_new) ps *)
| apply _ (* IntoDVal (E_old ++ E_new) v dv *)
| done (* ps is well-formed *)
| simpl; simpl_subst ].
| simpl ].
This diff is collapsed.
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