More consistent naming for `auth`.

Merged Robbert Krebbers requested to merge robbert/auth_consistency_fixes into master

This MR is a follow up on the renamings performed (implicitly) as part of !215 (merged). This MR makes the following changes:

  • auth_both_frac_valid and auth_both_valid are now of the same shape as auth_both_frac_validN and auth_both_validN. That is, both are now biimplications.
  • The left-to-right direction of auth_both_frac_valid and auth_both_valid only holds in case the camera is discrete. The right-to-left versions for non-discrete cameras are suffixed _2, the convention that we use throughout the development.
  • Change the direction of lemmas like auth_frag_valid and auth_auth_valid so that it's consistent with the other lemmas. I.e. make sure that the ◯ and ● are always on the LHS of the biimplication.
Edited by Robbert Krebbers

Merge request reports