We never make canonical instances of them.

With Coq master, we otherwise fail to infer instances with subG_savedAnythingΣ, which leads to goals like

> looking for (subG
>                       (@savedAnythingΣ (@ofe_funCF val (fun _ : val => laterCF idCF))
>                          ?cFunctorContractive0) Σ)

This is a follow up of !248.

Joseph Tassarotti authored 5 years ago and Robbert Krebbers committed 5 years ago

Also fixes pre-existing bug in iCombine error messages.

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.

This proof also more easily scales to other recursive types, like
trees etc.

Notably, `big_andL_andL` and `big_andL_and` where a ⊣⊢ and ⊢ version
of the same lemma. I favored the `big_opL_op` naming scheme.

This comment wasn't updated after
866cad62.