Commit 50b368c0 authored by Ralf Jung's avatar Ralf Jung

note a few places where we had to use ssreflect to force the use unification algorithm

parent 0a05a8c0
Pipeline #17355 passed with stage
in 14 minutes and 17 seconds
......@@ -134,10 +134,8 @@ Section proph_map.
rewrite proph_eq /proph_def. iIntros "Hp1 Hp2".
iCombine "Hp1 Hp2" as "Hp".
iDestruct (own_valid with "Hp") as %Hp.
(* FIXME: [apply auth_frag_valid in Hp] and
[rewrite ->auth_frag_valid in Hp] both should work but do not. *)
move:Hp. rewrite auth_frag_valid singleton_valid=>Hp.
done.
(* FIXME: FIXME(Coq #6294): needs new unification *)
move:Hp. rewrite auth_frag_valid singleton_valid //.
Qed.
Lemma proph_map_new_proph p ps pvs :
......@@ -169,7 +167,8 @@ Section proph_map.
assert (vs = v :: proph_list_resolves pvs p) as ->.
{ rewrite (Hres p vs HR). simpl. by rewrite decide_True. }
iMod (own_update_2 with "H● Hp") as "[H● H◯]".
{ eapply auth_update. apply: singleton_local_update.
{ (* FIXME: FIXME(Coq #6294): needs new unification *)
eapply auth_update. apply: singleton_local_update.
- by rewrite /to_proph_map lookup_fmap HR.
- by apply (exclusive_local_update _ (Excl (proph_list_resolves pvs p : list (leibnizC V)))). }
rewrite /to_proph_map -fmap_insert.
......
......@@ -60,8 +60,9 @@ Section mono_proof.
wp_cas_suc. iModIntro. iSplitL "Hl Hγ".
{ iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
wp_if. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
iApply (own_mono with "Hγf"). apply: auth_frag_mono.
by apply mnat_included, le_n_S.
iApply (own_mono with "Hγf").
(* FIXME: FIXME(Coq #6294): needs new unification *)
apply: auth_frag_mono. by apply mnat_included, le_n_S.
- wp_cas_fail; first (by intros [= ?%Nat2Z.inj]). iModIntro.
iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
wp_if. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
......
......@@ -118,8 +118,8 @@ Section lifting.
iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs Hstep).
iDestruct "Hσκs" as "Hσ". rewrite /ownP.
iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
{ apply auth_update. apply: option_local_update.
by apply: (exclusive_local_update _ (Excl σ2)). }
{ apply auth_update. apply option_local_update.
by apply (exclusive_local_update _ (Excl σ2)). }
iFrame "Hσ". iApply ("H" with "[]"); eauto with iFrame.
Qed.
......
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