From c504514596a41587b331c91995d29246de80c530 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Wed, 25 Oct 2017 08:10:06 +0200
Subject: [PATCH] =?UTF-8?q?Make=20`iDestruct=20...=20as=20(cpat)=20"..."`?=
=?UTF-8?q?=20work=20on=20'=E2=8C=9C=CF=86=E2=8C=9D=20=E2=88=A7=20P`=20and?=
=?UTF-8?q?=20`=E2=8C=9C=CF=86=E2=8C=9D=20=E2=88=97=20P`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
The advantage is that we can directly use a Coq introduction pattern
`cpat` to perform actions to the pure assertion. Before, this had
to be done in several steps:
iDestruct ... as "[Htmp ...]"; iDestruct "Htmp" as %cpat.
That is, one had to introduce a temporary name.
I expect this to be quite useful in various developments as many of
e.g. our invariants are written as:
∃ x1 .. x2, ⌜ pure stuff ⌝ ∗ spacial stuff.
---
theories/base_logic/lib/boxes.v | 18 +++++++++---------
theories/base_logic/lib/invariants.v | 4 ++--
theories/base_logic/lib/wsat.v | 4 ++--
theories/heap_lang/lib/spawn.v | 2 +-
theories/heap_lang/lib/spin_lock.v | 4 ++--
theories/heap_lang/lib/ticket_lock.v | 6 +++---
theories/program_logic/adequacy.v | 7 +++----
theories/program_logic/ownp.v | 4 ++--
theories/proofmode/class_instances.v | 13 +++++++++++++
theories/proofmode/classes.v | 27 +++++++++++++++++++++++++++
theories/tests/list_reverse.v | 2 +-
theories/tests/tree_sum.v | 2 +-
12 files changed, 66 insertions(+), 27 deletions(-)
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index d41ce60f..8cf543fd 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -185,7 +185,7 @@ Lemma slice_insert_full E q f P Q :
slice N γ Q ∗ ▷?q box N (<[γ:=true]> f) (Q ∗ P).
Proof.
iIntros (?) "HQ Hbox".
- iMod (slice_insert_empty with "Hbox") as (γ) "(% & #Hslice & Hbox)".
+ iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
iExists γ. iFrame "%#". iMod (slice_fill with "Hslice HQ Hbox"); first done.
by apply lookup_insert. by rewrite insert_insert.
Qed.
@@ -251,11 +251,11 @@ Proof.
iIntros (??) "#HQQ' #Hs Hb". destruct b.
- iMod (slice_delete_full with "Hs Hb") as (P') "(HQ & Heq & Hb)"; try done.
iDestruct ("HQQ'" with "HQ") as "HQ'".
- iMod (slice_insert_full with "HQ' Hb") as (γ') "(% & #Hs' & Hb)"; try done.
+ iMod (slice_insert_full with "HQ' Hb") as (γ' ?) "[#Hs' Hb]"; try done.
iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'".
- iMod (slice_delete_empty with "Hs Hb") as (P') "(Heq & Hb)"; try done.
- iMod (slice_insert_empty with "Hb") as (γ') "(% & #Hs' & Hb)"; try done.
+ iMod (slice_insert_empty with "Hb") as (γ' ?) "[#Hs' Hb]"; try done.
iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'".
Qed.
@@ -268,16 +268,16 @@ Lemma slice_split E q f P Q1 Q2 γ b :
Proof.
iIntros (??) "#Hslice Hbox". destruct b.
- iMod (slice_delete_full with "Hslice Hbox") as (P') "([HQ1 HQ2] & Heq & Hbox)"; try done.
- iMod (slice_insert_full with "HQ1 Hbox") as (γ1) "(% & #Hslice1 & Hbox)"; first done.
- iMod (slice_insert_full with "HQ2 Hbox") as (γ2) "(% & #Hslice2 & Hbox)"; first done.
+ iMod (slice_insert_full with "HQ1 Hbox") as (γ1 ?) "[#Hslice1 Hbox]"; first done.
+ iMod (slice_insert_full with "HQ2 Hbox") as (γ2 ?) "[#Hslice2 Hbox]"; first done.
iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
{ by eapply lookup_insert_None. }
{ by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
- iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
- iMod (slice_insert_empty with "Hbox") as (γ1) "(% & #Hslice1 & Hbox)".
- iMod (slice_insert_empty with "Hbox") as (γ2) "(% & #Hslice2 & Hbox)".
+ iMod (slice_insert_empty with "Hbox") as (γ1 ?) "[#Hslice1 Hbox]".
+ iMod (slice_insert_empty with "Hbox") as (γ2 ?) "[#Hslice2 Hbox]".
iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
{ by eapply lookup_insert_None. }
{ by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
@@ -296,14 +296,14 @@ Proof.
iMod (slice_delete_full with "Hslice2 Hbox") as (P2) "(HQ2 & Heq2 & Hbox)"; first done.
{ by simplify_map_eq. }
iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2)%I with "[$HQ1 $HQ2] Hbox")
- as (γ) "(% & #Hslice & Hbox)"; first done.
+ as (γ ?) "[#Hslice Hbox]"; first done.
iExists γ. iIntros "{$% $#} !>". iNext.
eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
- iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done.
iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done.
{ by simplify_map_eq. }
- iMod (slice_insert_empty with "Hbox") as (γ) "(% & #Hslice & Hbox)".
+ iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
iExists γ. iIntros "{$% $#} !>". iNext.
eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index cadd0c88..467d60e2 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -47,7 +47,7 @@ Lemma inv_alloc N E P : ▷ P ={E}=∗ inv N P.
Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]".
iMod (ownI_alloc (∈ (↑N : coPset)) P with "[$HP $Hw]")
- as (i) "(% & $ & ?)"; auto using fresh_inv_name.
+ as (i ?) "[$ ?]"; auto using fresh_inv_name.
Qed.
Lemma inv_alloc_open N E P :
@@ -55,7 +55,7 @@ Lemma inv_alloc_open N E P :
Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros (Sub) "[Hw HE]".
iMod (ownI_alloc_open (∈ (↑N : coPset)) P with "Hw")
- as (i) "(% & Hw & #Hi & HD)"; auto using fresh_inv_name.
+ as (i ?) "(Hw & #Hi & HD)"; auto using fresh_inv_name.
iAssert (ownE {[i]} ∗ ownE (↑ N ∖ {[i]}) ∗ ownE (E ∖ ↑ N))%I
with "[HE]" as "(HEi & HEN\i & HE\N)".
{ rewrite -?ownE_op; [|set_solver..].
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 3d658b58..b270879e 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -105,7 +105,7 @@ Lemma ownI_open i P : wsat ∗ ownI i P ∗ ownE {[i]} ⊢ wsat ∗ ▷ P ∗ ow
Proof.
rewrite /ownI /wsat -!lock.
iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]".
- iDestruct (invariant_lookup I i P with "[$]") as (Q) "[% #HPQ]".
+ iDestruct (invariant_lookup I i P with "[$]") as (Q ?) "#HPQ".
iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
- iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
iExists I. iFrame "Hw". iApply (big_opM_delete _ _ i); eauto.
@@ -116,7 +116,7 @@ Lemma ownI_close i P : wsat ∗ ownI i P ∗ ▷ P ∗ ownD {[i]} ⊢ wsat ∗ o
Proof.
rewrite /ownI /wsat -!lock.
iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]".
- iDestruct (invariant_lookup with "[$]") as (Q) "[% #HPQ]".
+ iDestruct (invariant_lookup with "[$]") as (Q ?) "#HPQ".
iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
- iDestruct (ownD_singleton_twice with "[$]") as %[].
- iExists I. iFrame "Hw". iApply (big_opM_delete _ _ i); eauto.
diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index 95e104c0..5e5ad25e 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -67,7 +67,7 @@ Proof.
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iMod ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
iModIntro. wp_match. iApply ("IH" with "Hγ [HΦ]"). auto.
- - iDestruct "Hinv" as (v') "[% [HΨ|Hγ']]"; simplify_eq/=.
+ - iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']".
+ iMod ("Hclose" with "[Hl Hγ]"); [iNext; iExists _; iFrame; eauto|].
iModIntro. wp_match. by iApply "HΦ".
+ iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index ea19cf82..007093dc 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -60,7 +60,7 @@ Section proof.
{{{ is_lock γ lk R }}} try_acquire lk
{{{ b, RET #b; if b is true then locked γ ∗ R else True }}}.
Proof.
- iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l) "[% #?]"; subst.
+ iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
wp_rec. iInv N as ([]) "[Hl HR]" "Hclose".
- wp_cas_fail. iMod ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iModIntro. iApply ("HΦ" $! false). done.
@@ -82,7 +82,7 @@ Section proof.
{{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}.
Proof.
iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
- iDestruct "Hlock" as (l) "[% #?]"; subst.
+ iDestruct "Hlock" as (l ->) "#Hinv".
rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
wp_store. iApply "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
Qed.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index a926ab2b..b5c0b735 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -86,7 +86,7 @@ Section proof.
Lemma wait_loop_spec γ lk x R :
{{{ is_lock γ lk R ∗ issued γ x }}} wait_loop #x lk {{{ RET #(); locked γ ∗ R }}}.
Proof.
- iIntros (Φ) "[Hl Ht] HΦ". iDestruct "Hl" as (lo ln) "(% & #?)".
+ iIntros (Φ) "[Hl Ht] HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
iInv N as (o n) "(Hlo & Hln & Ha)" "Hclose".
wp_load. destruct (decide (x = o)) as [->|Hneq].
@@ -108,7 +108,7 @@ Section proof.
Lemma acquire_spec γ lk R :
{{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}}.
Proof.
- iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln) "[% #?]".
+ iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
iLöb as "IH". wp_rec. wp_bind (! _)%E. simplify_eq/=. wp_proj.
iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
wp_load. iMod ("Hclose" with "[Hlo Hln Ha]") as "_".
@@ -139,7 +139,7 @@ Section proof.
Lemma release_spec γ lk R :
{{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}.
Proof.
- iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln) "[% #?]"; subst.
+ iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
iDestruct "Hγ" as (o) "Hγo".
wp_let. wp_proj. wp_proj. wp_bind (! _)%E.
iInv N as (o' n) "(>Hlo & >Hln & >Hauth & Haown)" "Hclose".
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 81488f46..ca566788 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -123,7 +123,7 @@ Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ :
Proof.
intros. rewrite wptp_steps //.
rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono.
- iDestruct 1 as (e2 t2') "(% & (Hw & HE & _) & H & _)"; simplify_eq.
+ iDestruct 1 as (e2 t2' ?) "((Hw & HE & _) & H & _)"; simplify_eq.
iDestruct (wp_value_inv with "H") as "H". rewrite fupd_eq /fupd_def.
iMod ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
Qed.
@@ -143,7 +143,7 @@ Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
Nat.iter (S (S n)) (λ P, |==> ▷ P) ⌜is_Some (to_val e2) ∨ reducible e2 σ2⌝.
Proof.
intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono.
- iDestruct 1 as (e2' t2') "(% & Hw & H & Htp)"; simplify_eq.
+ iDestruct 1 as (e2' t2' ?) "(Hw & H & Htp)"; simplify_eq.
apply elem_of_cons in He2 as [<-|?]; first (iApply wp_safe; by iFrame "Hw H").
iApply wp_safe. iFrame "Hw". by iApply (big_sepL_elem_of with "Htp").
Qed.
@@ -155,8 +155,7 @@ Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 φ Φ :
Proof.
intros ?. rewrite wptp_steps //.
rewrite (Nat_iter_S_r (S n)) !bupd_iter_frame_l. apply bupd_iter_mono.
- iIntros "[Hback H]".
- iDestruct "H" as (e2' t2') "(% & (Hw&HE&Hσ) & _)"; subst.
+ iIntros "[Hback H]". iDestruct "H" as (e2' t2' ->) "[(Hw&HE&Hσ) _]".
rewrite fupd_eq.
iMod ("Hback" with "Hσ [$Hw $HE]") as "> (_ & _ & $)"; auto.
Qed.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index fc96e494..f57fd044 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -89,7 +89,7 @@ Section lifting.
iMod "H" as (σ1) "[Hred _]"; iDestruct "Hred" as %Hred%reducible_not_val.
move: Hred; by rewrite to_of_val.
- iApply wp_lift_step; [done|]; iIntros (σ1) "Hσ".
- iMod "H" as (σ1') "(% & >Hσf & H)". rewrite /ownP.
+ iMod "H" as (σ1' ?) "[>Hσf H]". rewrite /ownP.
iDestruct (own_valid_2 with "Hσ Hσf")
as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
iModIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
@@ -169,7 +169,7 @@ Section ectx_lifting.
⊢ WP e1 @ E {{ Φ }}.
Proof.
iIntros "H". iApply (ownP_lift_step E); try done.
- iMod "H" as (σ1) "(%&Hσ1&Hwp)". iModIntro. iExists σ1.
+ iMod "H" as (σ1 ?) "[Hσ1 Hwp]". iModIntro. iExists σ1.
iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
iApply ("Hwp" with "[]"); eauto.
Qed.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index a55899d0..06331c5d 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -688,6 +688,19 @@ Proof. done. Qed.
Global Instance into_exist_pure {A} (φ : A → Prop) :
@IntoExist M A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
Proof. by rewrite /IntoExist pure_exist. Qed.
+Global Instance into_exist_and_pure P Q φ :
+ IntoPureT P φ → IntoExist (P ∧ Q) (λ _ : φ, Q).
+Proof.
+ intros (φ'&->&?). rewrite /IntoExist (into_pure P).
+ apply pure_elim_l=> Hφ. by rewrite -(exist_intro Hφ).
+Qed.
+Global Instance into_exist_sep_pure P Q φ :
+ IntoPureT P φ → IntoExist (P ∗ Q) (λ _ : φ, Q).
+Proof.
+ intros (φ'&->&?). rewrite /IntoExist (into_pure P).
+ apply pure_elim_sep_l=> Hφ. by rewrite -(exist_intro Hφ).
+Qed.
+
Global Instance into_exist_always {A} P (Φ : A → uPred M) :
IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index ebdb8144..6cabad9a 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -23,6 +23,33 @@ Class IntoPure {M} (P : uPred M) (φ : Prop) := into_pure : P ⊢ ⌜φ⌝.
Arguments into_pure {_} _ _ {_}.
Hint Mode IntoPure + ! - : typeclass_instances.
+(* [IntoPureT] is a variant of [IntoPure] with the argument in [Type] to avoid
+some shortcoming of unification in Coq's type class search. An example where we
+use this workaround is to repair the following instance:
+
+ Global Instance into_exist_and_pure P Q (φ : Prop) :
+ IntoPure P φ → IntoExist (P ∧ Q) (λ _ : φ, Q).
+
+Coq is unable to use this instance: [class_apply] -- which is used by type class
+search -- fails with the error that it cannot unify [Prop] and [Type]. This is
+probably caused because [class_apply] uses an ancient unification algorith. The
+[refine] tactic -- which uses a better unification algorithm -- succeeds to
+apply the above instance.
+
+Since we do not want to define [Hint Extern] declarations using [refine] for
+any instance like [into_exist_and_pure], we factor this out in the class
+[IntoPureT]. This way, we only have to declare a [Hint Extern] using [refine]
+once, and use [IntoPureT] in any instance like [into_exist_and_pure].
+
+TODO: Report this as a Coq bug, or wait for https://github.com/coq/coq/pull/991
+to be finished and merged someday. *)
+Class IntoPureT {M} (P : uPred M) (φ : Type) :=
+ into_pureT : ∃ ψ : Prop, φ = ψ ∧ IntoPure P ψ.
+Lemma into_pureT_hint {M} (P : uPred M) (φ : Prop) : IntoPure P φ → IntoPureT P φ.
+Proof. by exists φ. Qed.
+Hint Extern 0 (IntoPureT _ _) =>
+ notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.
+
Class FromPure {M} (P : uPred M) (φ : Prop) := from_pure : ⌜φ⌝ ⊢ P.
Arguments from_pure {_} _ _ {_}.
Hint Mode FromPure + ! - : typeclass_instances.
diff --git a/theories/tests/list_reverse.v b/theories/tests/list_reverse.v
index 3a042542..3db30108 100644
--- a/theories/tests/list_reverse.v
+++ b/theories/tests/list_reverse.v
@@ -35,7 +35,7 @@ Proof.
iLöb as "IH" forall (hd acc xs ys Φ). wp_rec. wp_let.
destruct xs as [|x xs]; iSimplifyEq.
- wp_match. by iApply "HΦ".
- - iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq.
+ - iDestruct "Hxs" as (l hd' ->) "[Hx Hxs]".
wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store.
iApply ("IH" $! hd' (SOMEV #l) xs (x :: ys) with "Hxs [Hx Hys]"); simpl.
{ iExists l, acc; by iFrame. }
diff --git a/theories/tests/tree_sum.v b/theories/tests/tree_sum.v
index 6ca489c8..d4609d5b 100644
--- a/theories/tests/tree_sum.v
+++ b/theories/tests/tree_sum.v
@@ -45,7 +45,7 @@ Proof.
- iDestruct "Ht" as "%"; subst.
wp_match. wp_load. wp_op. wp_store.
by iApply ("HΦ" with "[$Hl]").
- - iDestruct "Ht" as (ll lr vl vr) "(% & Hll & Htl & Hlr & Htr)"; subst.
+ - iDestruct "Ht" as (ll lr vl vr ->) "(Hll & Htl & Hlr & Htr)".
wp_match. wp_proj. wp_load.
wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
wp_seq. wp_proj. wp_load.
--
GitLab