Moved connective notation to BI.

Added ⁺T for ra_pos T and eliminated BI.pres since I'd rather see ⁺res than BI.pres.

Bound mask_scope to type mask.

This gets rid of an unnecessary proof obligation for wpF.

(I've seen ↓a before for validity, …)

introduce notation to provide "pres" existential witnesses by giving the missing proof. (This is a natural candidate for more ltac magic, to solve these obligations automatically... actually, why can't eauto do that?)

Simplified adv, defining it with ownL.

Proof of concept for a friendly interface that (if it works) lets the user
set up an invariant and prove view shifts and atomic triples for primitive
reductions, rather than work in the model. (It should work, but I have to
merge my two proofs to make sure.)

add first version of RA (resource algebra): validity is a decidable predicate, rather than hard-coded into the type structure

create iris_meta file for meta-theorems (adequacy, lifting lemmas). formulate two of our four lifting lemmas.