Commit eaf63996 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make sure that anonymous hypotheses do not use some random old name.

parent 93ddf981
...@@ -104,7 +104,7 @@ Qed. ...@@ -104,7 +104,7 @@ Qed.
Lemma ownI_open i P : wsat ownI i P ownE {[i]} wsat P ownD {[i]}. Lemma ownI_open i P : wsat ownI i P ownE {[i]} wsat P ownD {[i]}.
Proof. Proof.
rewrite /ownI /wsat -!lock. rewrite /ownI /wsat -!lock.
iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]". iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[Hw 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. iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
- iSplitR "HQ"; last by iNext; iRewrite -"HPQ". - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
...@@ -115,7 +115,7 @@ Qed. ...@@ -115,7 +115,7 @@ Qed.
Lemma ownI_close i P : wsat ownI i P P ownD {[i]} wsat ownE {[i]}. Lemma ownI_close i P : wsat ownI i P P ownD {[i]} wsat ownE {[i]}.
Proof. Proof.
rewrite /ownI /wsat -!lock. rewrite /ownI /wsat -!lock.
iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]". iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[Hw 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 (big_opM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
- iDestruct (ownD_singleton_twice with "[$]") as %[]. - iDestruct (ownD_singleton_twice with "[$]") as %[].
...@@ -128,7 +128,7 @@ Lemma ownI_alloc φ P : ...@@ -128,7 +128,7 @@ Lemma ownI_alloc φ P :
wsat P == i, ⌜φ i wsat ownI i P. wsat P == i, ⌜φ i wsat ownI i P.
Proof. Proof.
iIntros (Hfresh) "[Hw HP]". rewrite /wsat -!lock. iIntros (Hfresh) "[Hw HP]". rewrite /wsat -!lock.
iDestruct "Hw" as (I) "[? HI]". iDestruct "Hw" as (I) "[Hw HI]".
iMod (own_unit (gset_disjUR positive) disabled_name) as "HE". iMod (own_unit (gset_disjUR positive) disabled_name) as "HE".
iMod (own_updateP with "[$]") as "HE". iMod (own_updateP with "[$]") as "HE".
{ apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None φ i)). { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None φ i)).
...@@ -150,7 +150,7 @@ Lemma ownI_alloc_open φ P : ...@@ -150,7 +150,7 @@ Lemma ownI_alloc_open φ P :
( E : gset positive, i, i E φ i) ( E : gset positive, i, i E φ i)
wsat == i, ⌜φ i (ownE {[i]} - wsat) ownI i P ownD {[i]}. wsat == i, ⌜φ i (ownE {[i]} - wsat) ownI i P ownD {[i]}.
Proof. Proof.
iIntros (Hfresh) "Hw". rewrite /wsat -!lock. iDestruct "Hw" as (I) "[? HI]". iIntros (Hfresh) "Hw". rewrite /wsat -!lock. iDestruct "Hw" as (I) "[Hw HI]".
iMod (own_unit (gset_disjUR positive) disabled_name) as "HD". iMod (own_unit (gset_disjUR positive) disabled_name) as "HD".
iMod (own_updateP with "[$]") as "HD". iMod (own_updateP with "[$]") as "HD".
{ apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None φ i)). { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None φ i)).
......
...@@ -153,7 +153,7 @@ Section proof. ...@@ -153,7 +153,7 @@ Section proof.
wp_store. wp_store.
iDestruct (own_valid_2 with "Hauth Hγo") as iDestruct (own_valid_2 with "Hauth Hγo") as
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2. %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
iDestruct "Haown" as "[[Hγo' _]|?]". iDestruct "Haown" as "[[Hγo' _]|Haown]".
{ iDestruct (own_valid_2 with "Hγo Hγo'") as %[[] ?]. } { iDestruct (own_valid_2 with "Hγo Hγo'") as %[[] ?]. }
iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]". iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
{ apply auth_update, prod_local_update_1. { apply auth_update, prod_local_update_1.
......
...@@ -858,7 +858,11 @@ Tactic Notation "iModCore" constr(H) := ...@@ -858,7 +858,11 @@ Tactic Notation "iModCore" constr(H) :=
Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) := Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
let rec go Hz pat := let rec go Hz pat :=
lazymatch pat with lazymatch pat with
| IAnom => idtac | IAnom =>
lazymatch Hz with
| IAnon _ => idtac
| INamed ?Hz => let Hz' := iFresh in iRename Hz into Hz'
end
| IDrop => iClearHyp Hz | IDrop => iClearHyp Hz
| IFrame => iFrameHyp Hz | IFrame => iFrameHyp Hz
| IIdent ?y => iRename Hz into y | IIdent ?y => iRename Hz into y
......
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