feat: notations for internalCmraValid, internalEq, internalIncluded

[alvinylt]

Description

Port the notations for internalCmraValid, internalEq, internalIncluded.

Addresses #300 and #234.

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

[markusdemedeiros]

Looks great. I was a little hesitant that there would be situations where the symbols were ambiguous, but I suppose this shows that's not the case--do you agree?

[alvinylt]

Looks great. I was a little hesitant that there would be situations where the symbols were ambiguous, but I suppose this shows that's not the case--do you agree?

We are reusing the symbols ✓ for CMRA.Included and ≼ for CMRA.Valid, but there is no ambiguity as CMRA.Included a b and CMRA.Valid a are of type Prop while internalCmraIncluded a b and internalCmraValid a are of type PROP, so it's not possible that we accidentally use the wrong symbol as it would not be type-correct.

Same for the distinction between internalEq and equivalence.

[markusdemedeiros]

Sounds great. The only overlap would be a BI instance for Prop itself, but perhaps we should cross that bridge when we come to it. If so, a fix would be to put the CMRA and BI notations in different scopes.

Nice work!

[lzy0505]

Great. Only nitpicking

[lzy0505]

Suggested change

	theorem of_pure {A : Type _} [OFE A] {x y : A} : ⌜x ≡ y⌝ ⊢ (iprop(x ≡ y) : PROP) :=
	theorem of_pure {A : Type _} [OFE A] {x y : A} : ⌜x ≡ y⌝ ⊢@{PROP} x ≡ y :=

[lzy0505]

Suggested change

	(∀ x, (f x) ≡ (g x)) ⊢@{PROP} f ≡ g :=
	(∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g :=

[lzy0505]

Suggested change

	CombineSepGives (iOwn γ a1) (iOwn γ a2) iprop(✓ (a1 • a2)) where
	CombineSepGives (iOwn γ a1) (iOwn γ a2) iprop(✓ a1 • a2) where