Make validy lemmas for `excl_auth` and `(u)frac_auth` more consistent with `auth`.
- Make validy lemmas for
excl_auth
more consistent withauth
.- Rename
excl_auth_frag_validN_op_1_l
intoexcl_auth_frag_op_validN
andexcl_auth_frag_valid_op_1_l
intoexcl_auth_frag_op_valid
(similar toauth_auth_op_valid
), and make them bi-implications. - Add
excl_auth_auth_op_validN
andexcl_auth_auth_op_valid
.
- Rename
- Make validy lemmas for
(u)frac_auth
more consistent withauth
.- Remove unidirectional lemmas with
1
fractionfrac_auth_frag_validN_op_1_l
andfrac_auth_frag_valid_op_1_l
- Add
frac_auth_frag_op_validN
andfrac_auth_frag_op_valid
, which are bi-implications with arbitrary fractions. - Add
ufrac_auth_frag_op_validN
andufrac_auth_frag_op_valid
.
- Remove unidirectional lemmas with
I think the old names were a consequence of porting lemmas like:
Lemma frac_auth_frag_validN_op_1_l n q a b : ✓{n} (◯F{1} a ⋅ ◯F{q} b) → False.
Edited by Robbert Krebbers