Commit b5f04f02 authored by MEVEL Glen's avatar MEVEL Glen

update to Coq 8.9.1 and Iris dev version

parent 945a2737
## Requirements
The project is known to compile with:
* Coq 8.8.2
* coq-iris dev.2018-11-01.3.19aae59a (development version of Iris)
* Coq 8.9.1
* coq-iris dev.2019-09-20.0.b958d569 (development version of Iris)
* coq-tlc 20181116 (for the proof of union-find)
As those dependencies (especially Iris) often make breaking changes,
......@@ -28,19 +28,19 @@ _If opam is already installed:_ Create a new switch for the project:
opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam install -j4 -v coq.8.8.2
opam install -j4 -v coq.8.9.1
If you want to use CoqIDE (a graphical, interactive toplevel for Coq), install
it as well:
# NOTE: this version of CoqIDE is only available if using opam 2.x
opam install coqide.8.8.2
opam install coqide.8.9.1
### Step 3: Install a development version of Iris
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
opam update
opam pin add coq-iris -k version dev.2018-11-01.3.19aae59a
opam pin add coq-iris -k version dev.2019-09-20.0.b958d569
(This will also install `coq-stdpp`, another Coq library made available through
the same repo.)
......@@ -57,7 +57,7 @@ available through an opam package in the Coq repository (added earlier).
Alternatively, TLC can be installed from source:
git clone 'https://gitlab.inria.fr/charguer/tlc'
( cd tlc && git checkout a7c9f61 )
( cd tlc && git checkout 4d7f23ce )
opam pin add coq-tlc -k path ./tlc
## Compiling
......
From iris Require Export algebra.auth base_logic.lib.own proofmode.tactics.
From iris Require Export algebra.auth algebra.excl base_logic.lib.own proofmode.tactics.
Notation "'●mnat' n" := (Auth (A:=mnat) (Excl' n%nat) ε) (at level 20).
Notation "'◯mnat' n" := (Auth (A:=mnat) None n%nat) (at level 20).
Notation "'●mnat' n" := (auth_auth (A:=mnatUR) 1%Qp n%nat) (at level 20).
Notation "'◯mnat' n" := (auth_frag (A:=mnatUR) n%nat) (at level 20).
Section Auth_mnat.
......@@ -12,7 +12,9 @@ Section Auth_mnat.
Lemma auth_mnat_alloc (n : mnat) :
(|==> γ, own γ (mnat n) own γ (mnat n))%I.
Proof.
by iMod (own_alloc (mnat n mnat n)) as (γ) "[? ?]" ; auto with iFrame.
iMod (own_alloc (mnat n mnat n)) as (γ) "[? ?]".
- by apply auth_both_valid_2.
- by auto with iFrame.
Qed.
Global Arguments auth_mnat_alloc _%nat.
......@@ -22,7 +24,7 @@ Section Auth_mnat.
(n m)%nat.
Proof.
iIntros "H● H◯".
iDestruct (own_valid_2 with "H● H◯") as % [[k ->] _] % auth_valid_discrete_2.
iDestruct (own_valid_2 with "H● H◯") as % [[k ->] _] % auth_both_valid.
iPureIntro. apply Max.le_max_l.
Qed.
......@@ -81,4 +83,4 @@ Section Auth_mnat.
Qed.
Global Arguments auth_mnat_update_incr' _ (_ _ _)%nat_scope.
End Auth_mnat.
\ No newline at end of file
End Auth_mnat.
......@@ -2,8 +2,8 @@ From iris Require Export algebra.auth base_logic.lib.own proofmode.tactics.
Notation "'●nat' n" := (Auth (A:=nat) (Excl' n%nat) ε) (at level 20).
Notation "'◯nat' n" := (Auth (A:=nat) None n%nat) (at level 20).
Notation "'●nat' n" := (auth_auth (A:=natUR) 1%Qp n%nat) (at level 20).
Notation "'◯nat' n" := (auth_frag (A:=natUR) n%nat) (at level 20).
Section Auth_nat.
......@@ -12,7 +12,9 @@ Section Auth_nat.
Lemma auth_nat_alloc (n : nat) :
(|==> γ, own γ (nat n) own γ (nat n))%I.
Proof.
by iMod (own_alloc (nat n nat n)) as (γ) "[? ?]" ; auto with iFrame.
iMod (own_alloc (nat n nat n)) as (γ) "[? ?]".
- by apply auth_both_valid_2.
- by auto with iFrame.
Qed.
Lemma own_auth_nat_le (γ : gname) (m n : nat) :
......@@ -22,7 +24,7 @@ Section Auth_nat.
Proof.
iIntros "H● H◯".
by iDestruct (own_valid_2 with "H● H◯")
as % [?%nat_le_sum _] % auth_valid_discrete_2.
as % [?%nat_le_sum _] % auth_both_valid.
Qed.
Lemma own_auth_nat_weaken (γ : gname) (n n : nat) :
......
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris.proofmode Require Import coq_tactics.
From iris.base_logic Require Import invariants.
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris_time Require Import Auth_nat Auth_mnat Misc Reduction Tactics.
From iris_time Require Export Translation Simulation.
From iris.proofmode Require Import coq_tactics.
Implicit Type e : expr.
Implicit Type v : val.
Implicit Type σ : state.
......@@ -39,7 +38,7 @@ Definition TCTR_interface `{irisG heap_lang Σ, Tick}
(|={}=> TR 0%nat)
(* ∗ (|={⊤}=> TRdup 0%nat) *)
m n, TR (m + n)%nat (TR m TR n)
m n, TRdup (m `max` n) (TRdup m TRdup n)
m n, TRdup (m `max` n)%nat (TRdup m TRdup n)
(* ∗ (TR max_tr ={⊤}=∗ False) *)
(TRdup max_tr ={}= False)
( v n, {{{ TC 1%nat TRdup n }}} tick v {{{ RET v ; TR 1%nat TRdup (n+1)%nat }}})
......@@ -284,7 +283,7 @@ Section Definitions.
iDestruct (own_auth_nat_le with "Hγ1● Hγ1◯") as %I'.
iDestruct (auth_mnat_update_read_auth with "Hγ2●") as ">[Hγ2● Hγ2◯]".
iAssert (TR n TRdup n)%I with "[$Hγ1◯ Hγ2◯]" as "$". {
rewrite (_ : (max_tr-1-m)%nat = (max_tr-1-m)%nat `max` n) ; last lia.
rewrite (_ : (max_tr-1-m) = (max_tr-1-m) `max` n)%nat ; last lia.
iDestruct "Hγ2◯" as "[_ $]".
}
iApply "InvClose". auto with iFrame.
......@@ -581,7 +580,7 @@ Section Simulation.
Qed.
Local Lemma simulation_exec_failure_now n t1 σ1 t2 σ2 :
nsteps erased_step (S n) (t1, σ1) (t2, σ2)
relations.nsteps erased_step (S n) (t1, σ1) (t2, σ2)
e1, e1 t1
¬ safe «e1» S«σ1, 0».
Proof.
......@@ -594,7 +593,7 @@ Section Simulation.
Lemma simulation_exec_failure m n e1 σ1 t2 σ2 :
σ2 !! = None
nsteps erased_step (m + S n) ([e1], σ1) (t2, σ2)
relations.nsteps erased_step (m + S n) ([e1], σ1) (t2, σ2)
¬ safe «e1» S«σ1, m».
Proof.
intros H Hnsteps.
......@@ -642,7 +641,7 @@ Section Soundness.
useTC = true
σ2 !! = None
safe «e» S«σ, m»
nsteps erased_step n ([e], σ) (t2, σ2)
relations.nsteps erased_step n ([e], σ) (t2, σ2)
(n m)%nat.
Proof.
intros HuseTC Hfresh Hsafe Hnsteps.
......@@ -836,7 +835,7 @@ Section Soundness.
iMod (own_alloc ( to_gen_heap (<[ := #M]> σ') to_gen_heap {[ := #M]}))
as (h) "[Hh● Hℓ◯]".
{
apply auth_valid_discrete_2 ; split.
apply auth_both_valid ; split.
- rewrite - insert_delete ; set σ'' := delete σ'.
unfold to_gen_heap ; rewrite 2! fmap_insert fmap_empty insert_empty.
exists (to_gen_heap σ'').
......@@ -844,6 +843,9 @@ Section Soundness.
rewrite lookup_fmap ; apply fmap_None, lookup_delete.
- apply to_gen_heap_valid.
}
(* allocate the meta-heap: *)
iMod (own_alloc ( to_gen_meta )) as (γmeta) "H" ;
first by apply auth_auth_valid, to_gen_meta_valid.
(* allocate the ghost state associated with ℓ: *)
iAssert (|==> γ,
(if useTC then own γ ( M) else True)
......@@ -859,7 +861,7 @@ Section Soundness.
iMod (auth_nat_alloc (max_tr-1-M)) as (γ1) "[Hγ1● _]".
iMod (auth_mnat_alloc (max_tr-1-M)) as (γ2) "[Hγ2● _]".
(* packing all those bits, build the heap instance necessary to use time credits: *)
pose (Build_tctrHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ _ _ _ h)) _ _ _ _ γ γ1 γ2 _)
pose (Build_tctrHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ _ _ _ _ _ h γmeta)) _ _ _ _ γ γ1 γ2 _)
as HtcHeapG.
(* create the invariant: *)
iAssert (|={}=> TCTR_invariant max_tr)%I with "[Hℓ◯ Hγ● Hγ1● Hγ2●]" as "> Hinv".
......@@ -872,8 +874,9 @@ Section Soundness.
}
iIntros (?) "!>".
(* finally, use the user-given specification: *)
iExists (λ σ _, gen_heap_ctx σ). iFrame "Hh●".
iApply (Hspec $ HtcHeapG with "Hinv Hγ◯") ; auto.
iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I). iSplitL "H Hh●".
- iExists . auto with iFrame.
- iApply (Hspec $ HtcHeapG with "Hinv Hγ◯") ; auto.
Qed.
(* the final soundness theorem. *)
......
......@@ -425,7 +425,7 @@ Section Soundness.
iMod (own_alloc ( to_gen_heap (<[ := #k]> σ') to_gen_heap {[ := #k]}))
as (h) "[Hh● Hℓ◯]".
{
apply auth_valid_discrete_2 ; split.
apply auth_both_valid ; split.
- rewrite - insert_delete ; set σ'' := delete σ'.
unfold to_gen_heap ; rewrite 2! fmap_insert fmap_empty insert_empty.
exists (to_gen_heap σ'').
......@@ -433,10 +433,13 @@ Section Soundness.
rewrite lookup_fmap ; apply fmap_None, lookup_delete.
- apply to_gen_heap_valid.
}
(* allocate the meta-heap: *)
iMod (own_alloc ( to_gen_meta )) as (γmeta) "H" ;
first by apply auth_auth_valid, to_gen_meta_valid.
(* allocate the ghost state associated with ℓ: *)
iMod (auth_nat_alloc k) as (γ) "[Hγ● Hγ◯]".
(* packing all those bits, build the heap instance necessary to use time credits: *)
pose (Build_timeCreditHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ _ _ _ h)) _ _ γ)
pose (Build_timeCreditHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ _ _ _ _ _ h γmeta)) _ _ γ)
as HtcHeapG.
(* create the invariant: *)
iAssert (|={}=> TC_invariant)%I with "[Hℓ◯ Hγ●]" as "> Hinv".
......@@ -449,9 +452,10 @@ Section Soundness.
}
iIntros (?) "!>".
(* finally, use the user-given specification: *)
iExists (λ σ _, gen_heap_ctx σ). iFrame "Hh●".
iDestruct (own_auth_nat_weaken _ _ _ Ik with "Hγ◯") as "Hγ◯".
iApply (Hspec with "Hinv Hγ◯") ; auto.
iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I). iSplitL "H Hh●".
- iExists . auto with iFrame.
- iDestruct (own_auth_nat_weaken _ _ _ Ik with "Hγ◯") as "Hγ◯".
iApply (Hspec with "Hinv Hγ◯") ; auto.
Qed.
Theorem spec_tctranslation__adequate_and_bounded {Σ} m φ e :
......@@ -529,7 +533,7 @@ Section Tactics.
envs_entails Δ (WP fill K (App tick v) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq => HsubsetE ???? Hentails''.
rewrite envs_lookup_persistent_sound // intuitionistically_elim. apply wand_elim_r'.
rewrite envs_lookup_intuitionistic_sound // intuitionistically_elim. apply wand_elim_r'.
rewrite -wp_bind.
eapply wand_apply ; first by (iIntros "HTC1 HΦ #Htick" ; iApply (tick_spec with "Htick HTC1 HΦ")).
rewrite into_laterN_env_sound -later_sep /=. apply later_mono.
......
......@@ -234,13 +234,12 @@ Lemma gen_heap_ctx_mapsto {Σ : gFunctors} {Hgen : gen_heapG loc val Σ} (σ : s
l v' -
v = v'.
Proof.
iIntros (Hσ) "Hheap Hl".
rewrite /gen_heap_ctx /=.
iIntros (Hσ) "Hheap Hl". iDestruct "Hheap" as (hmeta) "(_ & Hheap & _)".
unfold mapsto ; destruct mapsto_aux as [_->] ; rewrite /mapsto_def /=.
iDestruct (own_valid_2 with "Hheap Hl") as %H.
iPureIntro.
assert (CmraDiscrete (gen_heapUR loc val)) as Hdiscrete by apply _.
apply ((auth_valid_discrete_2 (H:=Hdiscrete))) in H as [H _].
apply auth_both_valid in H as [H _].
apply gen_heap_singleton_included in H.
pose proof (eq_stepl Hσ H) as E. by injection E.
Qed.
......@@ -257,7 +256,7 @@ Proof.
intros Hspec Hloc HtcPreG σ1 t2 σ2 z Hsteps.
(* apply the invariance result. *)
apply (wp_invariance Σ _ NotStuck «e» S«σ1,m» T«t2» S«σ2,z») ; simpl ; last assumption.
intros HinvG κs κs'.
intros HinvG κs(*κs'*).
(* … now we have to prove a WP for some state interpretation, for which
* we settle the needed invariant TC_invariant. *)
set σ' := S«σ1».
......@@ -265,7 +264,7 @@ Proof.
iMod (own_alloc ( to_gen_heap (<[ := #m]> σ') to_gen_heap {[ := #m]}))
as (h) "[Hh● Hℓ◯]".
{
apply auth_valid_discrete_2 ; split.
apply auth_both_valid ; split.
- rewrite - insert_delete ; set σ'' := delete σ'.
unfold to_gen_heap ; rewrite 2! fmap_insert fmap_empty insert_empty.
exists (to_gen_heap σ'').
......@@ -273,11 +272,14 @@ Proof.
rewrite lookup_fmap ; apply fmap_None, lookup_delete.
- apply to_gen_heap_valid.
}
(* allocate the meta-heap: *)
iMod (own_alloc ( to_gen_meta )) as (γmeta) "H" ;
first by apply auth_auth_valid, to_gen_meta_valid.
(* allocate the ghost state associated with ℓ: *)
iMod (auth_nat_alloc m) as (γ) "[Hγ● Hγ◯]".
(* packing all those bits, build the heap instance necessary to use time credits: *)
destruct HtcPreG as [[HinvPreG [HgenHeapPreInG]] HinG] ; simpl ; clear HinvPreG.
pose (Build_timeCreditHeapG Σ (HeapG Σ HinvG (GenHeapG _ _ Σ _ _ HgenHeapPreInG h)) HinG _ γ)
pose (Build_timeCreditHeapG Σ (HeapG Σ HinvG (GenHeapG _ _ Σ _ _ _ _ _ h γmeta)) HinG _ γ)
as HtcHeapG.
(* create the invariant: *)
iAssert (|={}=> TC_invariant)%I with "[Hℓ◯ Hγ●]" as "> #Hinv".
......@@ -289,11 +291,13 @@ Proof.
by iFrame.
}
(* finally, use the user-given specification: *)
iModIntro. iExists (λ σ _ _, gen_heap_ctx σ), (λ _, True)%I. iFrame "Hh●".
iModIntro.
iExists (λ σ _ _, gen_heap_ctx σ), (λ _, True%I). iSplitL "H Hh●" ;
first by (iExists ; auto with iFrame).
iSplitL ; first (iApply (Hspec with "Hinv Hγ◯") ; auto).
(* it remains to prove that the interpretation of the final state, along
* with the invariant, implies the inequality… *)
iIntros "Hheap2".
iIntros "Hheap2". iExists _.
(* open the invariant: *)
iInv timeCreditN as (m') ">[Hc Hγ●]" "InvClose".
(* derive that z = m' (that is, the relative integer is in fact a natural integer): *)
......
......@@ -34,7 +34,7 @@ Definition TR_interface `{irisG heap_lang Σ, Tick}
(|={}=> TR 0%nat)
(* ∗ (|={⊤}=> TRdup 0%nat) *)
m n, TR (m + n)%nat (TR m TR n)
m n, TRdup (m `max` n) (TRdup m TRdup n)
m n, TRdup (m `max` n)%nat (TRdup m TRdup n)
(* ∗ (TR nmax ={⊤}=∗ False) *)
(TRdup nmax ={}= False)
( v n, {{{ TRdup n }}} tick v {{{ RET v ; TR 1%nat TRdup (n+1)%nat }}})
......@@ -206,7 +206,7 @@ Section TickSpec.
iDestruct (own_auth_nat_le with "Hγ1● Hγ1◯") as %In.
iDestruct (auth_mnat_update_read_auth with "Hγ2●") as ">[Hγ2● Hγ2◯]".
iAssert (TR n TRdup n)%I with "[$Hγ1◯ Hγ2◯]" as "$". {
rewrite (_ : m = m `max` n) ; last lia.
rewrite (_ : m = m `max` n)%nat ; last lia.
iDestruct "Hγ2◯" as "[_ $]".
}
iApply "InvClose". auto with iFrame.
......@@ -322,7 +322,7 @@ Section Soundness.
iMod (own_alloc ( to_gen_heap (<[ := #(nmax-1)%nat]> σ') to_gen_heap {[ := #(nmax-1)%nat]}))
as (h) "[Hh● Hℓ◯]".
{
apply auth_valid_discrete_2 ; split.
apply auth_both_valid ; split.
- rewrite - insert_delete ; set σ'' := delete σ'.
unfold to_gen_heap ; rewrite 2! fmap_insert fmap_empty insert_empty.
exists (to_gen_heap σ'').
......@@ -330,11 +330,14 @@ Section Soundness.
rewrite lookup_fmap ; apply fmap_None, lookup_delete.
- apply to_gen_heap_valid.
}
(* allocate the meta-heap: *)
iMod (own_alloc ( to_gen_meta )) as (γmeta) "H" ;
first by apply auth_auth_valid, to_gen_meta_valid.
(* allocate the ghost state associated with ℓ: *)
iMod (auth_nat_alloc 0) as (γ1) "[Hγ1● _]".
iMod (auth_mnat_alloc 0) as (γ2) "[Hγ2● _]".
(* packing all those bits, build the heap instance necessary to use time receipts: *)
pose (Build_timeReceiptHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ _ _ _ h)) _ _ _ γ1 γ2)
pose (Build_timeReceiptHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ _ _ _ _ _ h γmeta)) _ _ _ γ1 γ2)
as HtrHeapG.
(* create the invariant: *)
iAssert (|={}=> TR_invariant nmax)%I with "[Hℓ◯ Hγ1● Hγ2●]" as "> Hinv".
......@@ -347,8 +350,9 @@ Section Soundness.
}
iModIntro.
(* finally, use the user-given specification: *)
iExists (λ σ _, gen_heap_ctx σ). iFrame "Hh●".
iApply (Hspec with "Hinv") ; auto.
iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I). iSplitL "H Hh●".
- iExists . auto with iFrame.
- iApply (Hspec with "Hinv") ; auto.
Qed.
Theorem spec_trtranslation__nadequate {Σ} nmax φ e :
......
......@@ -20,6 +20,6 @@ Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
iMod (gen_heap_init σ) as (?) "Hh".
iModIntro.
iExists (λ σ κs, (gen_heap_ctx σ)%I). iFrame.
iExists (λ σ κs, (gen_heap_ctx σ)%I), (λ _, True%I). iFrame.
iApply (Hwp (HeapG _ _ _)).
Qed.
......@@ -365,8 +365,8 @@ Proof. refine (inj_countable of_val to_val _); auto using to_of_val. Qed.
Global Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
Global Instance expr_inhabited : Inhabited expr := populate (Val inhabitant).
Canonical Structure valC := leibnizC val.
Canonical Structure exprC := leibnizC expr.
Canonical Structure valC := leibnizO val.
Canonical Structure exprC := leibnizO expr.
(** Evaluation contexts *)
Inductive ectx_item :=
......
......@@ -167,7 +167,7 @@ Proof.
iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by auto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
iMod (@gen_heap_alloc with "Hσ") as "(Hσ & Hl & _)"; first done.
iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
......
......@@ -225,7 +225,7 @@ End heap.
Tactic Notation "wp_apply" open_constr(lem) :=
wp_pures;
iPoseProofCore lem as false true (fun H =>
iPoseProofCore lem as false (fun H =>
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
reshape_expr false e ltac:(fun K e' =>
......
......@@ -803,7 +803,7 @@ Proof using.
assert (z' = R y). { symmetry. eapply is_repr_incl_R; eauto. } subst z'.
forwards IH' : IH HI HM HB'; [math|done|].
iCombine "TCd TC" as "TC".
math_rewrite (11 * S d' + 6 = 11 * d' + 11 + 6)%nat.
math_rewrite (11 * S d' + 6 = 11 * d' + 11 + 6)%nat ; first by lia.
iDestruct "TC" as "[TCd TC]".
wp_apply (IH' with "[//] [$HM $TCd]").
iIntros (M') "[HM' hM']". iDestruct "hM'" as %HM'. wp_tick_let.
......@@ -830,7 +830,7 @@ Proof using.
iDestruct "UF" as (F K M HI HM) "(HM & TC2 & TR)".
forwards* (d&F'&HC&HP): amortized_cost_of_iterated_path_compression_simplified x.
iCombine "TC1 TC2" as "TC".
rewrite [TC (_ + _)](TC_weaken _ (11*Phi D F' K + (11 * d + 11))%nat); [|math].
rewrite [TC (_ + _)](TC_weaken _ (11*Phi D F' K + (11 * d + 11))%nat); [|lia].
iDestruct "TC" as "[TC1 TC2]".
iApply (find_spec_inductive with "[//] [$TC2 $HM]")=>//.
iIntros "!>" (M') "[HM' %]". iApply "HΦ".
......@@ -852,7 +852,8 @@ Theorem get_spec : forall D R V x, x \in D ->
{{{ RET V x; UF D R V }}}.
Proof using.
introv Dx. iIntros "#?" (Φ) "!# [UF TC] HΦ".
math_rewrite (22 * alpha (card D) + 57 = 22 * alpha (card D) + 44 + 13)%nat.
math_rewrite (22 * alpha (card D) + 57 = 22 * alpha (card D) + 44 + 13)%nat ;
first by lia.
iDestruct "TC" as "[TC1 TC2]".
wp_tick_rec.
wp_apply (find_spec with "[//] [$TC1 $UF]")=>//.
......@@ -884,7 +885,8 @@ Theorem set_spec : forall D R V x v,
{{{ RET #(); UF D R (update1 V R x «v»%V) }}}.
Proof using.
introv Dx. iIntros "#?" (Φ) "!# [UF TC] HΦ".
math_rewrite (22 * alpha (card D) + 62 = 22 * alpha (card D) + 44 + 18)%nat.
math_rewrite (22 * alpha (card D) + 62 = 22 * alpha (card D) + 44 + 18)%nat ;
first by lia.
iDestruct "TC" as "[TC1 TC2]".
wp_tick_rec. wp_tick_let. wp_apply (find_spec with "[//] [$TC1 $UF]")=>//.
iIntros "UF". wp_tick_let. iDestruct "UF" as (F K M HI HM) "[HM TC]".
......@@ -917,7 +919,8 @@ Theorem eq_spec : forall D R V x y,
Proof using.
introv Dx Dy. iIntros "#?" (Φ) "!# [UF TC] HΦ".
math_rewrite (44 * alpha (card D) + 92 =
(22 * alpha (card D) + 44) + (22 * alpha (card D) + 44) + 4)%nat.
(22 * alpha (card D) + 44) + (22 * alpha (card D) + 44) + 4)%nat ;
first by lia.
iDestruct "TC" as "[[TC1 TC2] TC3]".
wp_tick_rec. wp_tick_let.
wp_apply (find_spec with "[//] [$TC1 $UF]")=>//. iIntros "UF".
......@@ -1072,7 +1075,8 @@ Theorem union_spec : forall D R V x y,
Proof using.
introv Hnmax Dx Dy.
math_rewrite (44 * alpha (card D) + 152 =
(22 * alpha (card D) + 44) + (22 * alpha (card D) + 44) + 61 + 3)%nat.
(22 * alpha (card D) + 44) + (22 * alpha (card D) + 44) + 61 + 3)%nat ;
first by lia.
iIntros "#?" (Φ) "!# [UF [[[TC1 TC2] TC3] TC4]] HΦ".
wp_tick_rec. wp_tick_let.
wp_apply (find_spec with "[//] [$TC1 $UF]")=>//. iIntros "UF".
......
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