Commit 13dc3369 authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Jacques-Henri Jourdan

Explicitly unfold some definitions.

These unfolds kind of make sense, and I was quite surprised that
it used to work before. However, when changing to primitive
records, these unfolds are actually needed.
parent f2eaf912
......@@ -39,7 +39,7 @@ Section proofs.
Proof. rewrite /cinv; apply _. Qed.
Global Instance cinv_own_fractionnal γ : Fractional (cinv_own γ).
Proof. intros ??. by rewrite -own_op. Qed.
Proof. intros ??. by rewrite /cinv_own -own_op. Qed.
Global Instance cinv_own_as_fractionnal γ q :
AsFractional (cinv_own γ q) (cinv_own γ) q.
Proof. split. done. apply _. Qed.
......@@ -87,7 +87,7 @@ Section gen_heap.
Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
Global Instance mapsto_fractional l v : Fractional (λ q, l {q} v)%I.
intros p q. by rewrite mapsto_eq -own_op -auth_frag_op
intros p q. by rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op
op_singleton pair_op agree_idemp.
Global Instance mapsto_as_fractional l q v :
......@@ -97,7 +97,7 @@ Section gen_heap.
Lemma mapsto_agree l q1 q2 v1 v2 : l {q1} v1 - l {q2} v2 - v1 = v2.
apply wand_intro_r.
rewrite mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid.
f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op.
by intros [_ ?%agree_op_invL'].
......@@ -37,7 +37,8 @@ Section saved_prop.
saved_prop_own γ x - saved_prop_own γ y - (x y).
apply wand_intro_r.
rewrite -own_op own_valid agree_validI agree_equivI later_equivI.
rewrite /saved_prop_own -own_op own_valid agree_validI agree_equivI.
rewrite later_equivI.
set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
assert ( z, G2 (G1 z) z) as help.
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment