diff --git a/algebra/cofe.v b/algebra/cofe.v index 3fd8a65e4cee2510b8e2c6e1665fc90787a08d0f..ddf170fe7b5cace107f407599078039a67e0ef7c 100644 --- a/algebra/cofe.v +++ b/algebra/cofe.v @@ -347,6 +347,9 @@ Structure cFunctor := CFunctor { Existing Instance cFunctor_ne. Instance: Params (@cFunctor_map) 5. +Delimit Scope cFunctor_scope with CF. +Bind Scope cFunctor_scope with cFunctor. + Class cFunctorContractive (F : cFunctor) := cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2). @@ -412,6 +415,7 @@ Proof. apply cofe_morC_map_ne; apply cFunctor_contractive=>i ?; split; by apply Hfg. Qed. + (** Discrete cofe *) Section discrete_cofe. Context `{Equiv A, @Equivalence A (≡)}. @@ -518,3 +522,10 @@ Proof. intros A1 A2 B1 B2 n fg fg' Hfg. apply laterC_map_contractive => i ?. by apply cFunctor_ne, Hfg. Qed. + +(** Notation for writing functors *) +Notation "∙" := idCF : cFunctor_scope. +Notation "F1 -n> F2" := (cofe_morCF F1%CF F2%CF) : cFunctor_scope. +Notation "( F1 , F2 , .. , Fn )" := (prodCF .. (prodCF F1%CF F2%CF) .. Fn%CF) : cFunctor_scope. +Notation "▶ F" := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope. +Coercion constCF : cofeT >-> cFunctor. diff --git a/heap_lang/lang.v b/heap_lang/lang.v index c127e0e94e5992dfe3bf1ccedd99484a568bfc37..bc135938a1e132b19348af4eb94dd39325ccb0e7 100644 --- a/heap_lang/lang.v +++ b/heap_lang/lang.v @@ -20,7 +20,7 @@ Inductive binder := BAnon | BNamed : string → binder. Definition cons_binder (mx : binder) (X : list string) : list string := match mx with BAnon => X | BNamed x => x :: X end. Infix ":b:" := cons_binder (at level 60, right associativity). -Delimit Scope binder_scope with binder. +Delimit Scope binder_scope with bind. Bind Scope binder_scope with binder. Instance binder_dec_eq (x1 x2 : binder) : Decision (x1 = x2). Proof. solve_decision. Defined. diff --git a/program_logic/model.v b/program_logic/model.v index d9ad12adbf0179493d6aca3292a35811282be753..fa422c026b75b4a320aaa9a0b507bfd9bcc9d278 100644 --- a/program_logic/model.v +++ b/program_logic/model.v @@ -34,7 +34,7 @@ End iProp_solution_sig. Module Export iProp_solution : iProp_solution_sig. Definition iProp_result (Λ : language) (Σ : iFunctor) : - solution (uPredCF (resRF Λ (laterCF idCF) Σ)) := solver.result _. + solution (uPredCF (resRF Λ (▶ ∙) Σ)) := solver.result _. Definition iPreProp (Λ : language) (Σ : iFunctor) : cofeT := iProp_result Λ Σ. Definition iGst (Λ : language) (Σ : iFunctor) : cmraT := Σ (iPreProp Λ Σ). diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v index 5298742ffdc90837e5680608fc88905c84f51534..5e41b83a7cecced7a7b684b8672a6108237cfdf3 100644 --- a/program_logic/saved_prop.v +++ b/program_logic/saved_prop.v @@ -5,7 +5,7 @@ Import uPred. Class savedPropG (Λ : language) (Σ : gFunctors) (F : cFunctor) := saved_prop_inG :> inG Λ Σ (agreeR (laterC (F (iPreProp Λ (globalF Σ))))). Definition savedPropGF (F : cFunctor) : gFunctor := - GFunctor (agreeRF (laterCF F)). + GFunctor (agreeRF (▶ F)). Instance inGF_savedPropG `{inGF Λ Σ (savedPropGF F)} : savedPropG Λ Σ F. Proof. apply: inGF_inG. Qed. diff --git a/program_logic/tests.v b/program_logic/tests.v index ceb9e9dff0ba0a0de48177d87f7c64d6caecd286..0a5ca9fdbd04b28b8ab8a43915b3cd6e4ae5cc38 100644 --- a/program_logic/tests.v +++ b/program_logic/tests.v @@ -9,7 +9,7 @@ End ModelTest. Module SavedPropTest. (* Test if we can really go "crazy higher order" *) Section sec. - Definition F := (cofe_morCF idCF idCF). + Definition F : cFunctor := ( ∙ -n> ∙ ). Definition Σ : gFunctors := #[ savedPropGF F ]. Context {Λ : language}. Notation iProp := (iPropG Λ Σ).