From ecff9b3d1f60143f807f3401703d1ae84d9dec34 Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Mon, 24 Feb 2020 11:08:25 +0100
Subject: [PATCH] `wsat` notes.
---
theories/base_logic/lib/wsat.v | 10 ++++++++--
1 file changed, 8 insertions(+), 2 deletions(-)
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 80202624a..a675d227b 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -113,8 +113,14 @@ Proof.
rewrite -own_op own_valid auth_both_validI /=. iIntros "[_ [#HI #HvI]]".
iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI.
iSpecialize ("HI" $! i). iSpecialize ("HvI" $! i).
- (*rewrite lookup_fmap lookup_op lookup_singleton bi.option_equivI.*)
- rewrite lookup_fmap (lookup_op (A:=agreeR (laterO (iPrePropO Σ)))).
+ Fail rewrite lookup_fmap lookup_op lookup_singleton bi.option_equivI.
+ rewrite lookup_fmap.
+ Set Typeclasses Debug. Fail rewrite lookup_op. Unset Typeclasses Debug.
+ (* Failed TC search for `(ElemOf ?T (agreeR (laterO (iPrePropO
+ Σ))))`. The [singletonM] on the LHS of the [̧(⋅)] we want to rewrite
+ has [A := agree (later (ofe_car (iPrePropO Σ)))], not [agreeR ...].
+ *)
+ rewrite (lookup_op (A:=agreeR (laterO (iPrePropO Σ)))).
rewrite lookup_singleton bi.option_equivI.
case: (I !! i)=> [Q|] /=; [|case: (I' !! i)=> [Q'|] /=; by iExFalso].
iExists Q; iSplit; first done.
--
GitLab