• Robbert Krebbers's avatar
    More consistent naming for `auth`. · 597ec42e
    Robbert Krebbers authored
    This MR is a follow up on the renamings performed (implicitly) as part of
    !215. 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 prefixed `_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.
    597ec42e
boxes.v 13.2 KB