Skip to content
Snippets Groups Projects
Commit ecff9b3d authored by David Swasey's avatar David Swasey
Browse files

`wsat` notes.

parent dedbd2c0
Branches ci/ralf/retime
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/base_logic/lib/wsat.v
+ 8
− 2
View file @ ecff9b3d
...@@ -113,8 +113,14 @@ Proof. ...@@ -113,8 +113,14 @@ Proof.
rewrite -own_op own_valid auth_both_validI /=. iIntros "[_ [#HI #HvI]]". rewrite -own_op own_valid auth_both_validI /=. iIntros "[_ [#HI #HvI]]".
iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI. iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI.
iSpecialize ("HI" $! i). iSpecialize ("HvI" $! i). iSpecialize ("HI" $! i). iSpecialize ("HvI" $! i).
(*rewrite lookup_fmap lookup_op lookup_singleton bi.option_equivI.*) Fail rewrite lookup_fmap lookup_op lookup_singleton bi.option_equivI.
rewrite lookup_fmap (lookup_op (A:=agreeR (laterO (iPrePropO Σ)))). 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. rewrite lookup_singleton bi.option_equivI.
case: (I !! i)=> [Q|] /=; [|case: (I' !! i)=> [Q'|] /=; by iExFalso]. case: (I !! i)=> [Q|] /=; [|case: (I' !! i)=> [Q'|] /=; by iExFalso].
iExists Q; iSplit; first done. iExists Q; iSplit; first done.
......
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