Failure to find a proof of persistence
Version of Iris: dev.2019-07-01.1.6e79f000
Typeclass search fails when trying to prove that a particular statement is persistent.
In resource algebra
authR (prodUR
(prodUR
(optionUR (exclR unitO))
(optionUR (exclR unitO)))
(optionUR (agreeR (boolO))))
proof of
Persistent (own γ (◯((None, None), Some (to_agree true))))
fails with
Proof search failed without reaching its limit.
if performed with typeclasses eauto 10
. It similarly doesn't work with apply _
.
The statement is actually persistent, as shown by Jonas Kastberg:
Proof.
apply own_core_persistent.
apply auth_frag_core_id.
apply pair_core_id; typeclasses eauto.
Qed.
Minimal (non-)working example: https://pastebin.com/T7zhm9Zu