rename elem_of_equiv_L -> set_eq, and set_equiv_spec_L -> set_eq_subseteq

This hopefully makes the lemmas easier to find.

mapset_eq is an internal lemma, that should not be used. The lemma that you want is elem_of_equiv_L. That said, that lemma is not easy to find...

added 19 commits

• ae119f28...c5676b11 - 18 commits from branch master
• 6c8f86aa - rename elem_of_equiv_L -> set_eq, and set_equiv_spec_L -> set_eq_subseteq

Compare with previous version

changed title from add gset_eq to rename elem_of_equiv_L -> set_eq, and set_equiv_spec_L -> set_eq_subseteq

changed the description

resolved all threads

added 1 commit

• 88815fc7 - rename elem_of_equiv -> set_equiv and set_equiv_spec -> set_equiv_subseteq,...

Compare with previous version

added 31 commits

• 88815fc7...1f7d13f3 - 29 commits from branch master
• cb566d43 - rename elem_of_equiv_L -> set_eq, and set_equiv_spec_L -> set_eq_subseteq
• ea3cdadb - rename elem_of_equiv -> set_equiv and set_equiv_spec -> set_equiv_subseteq,...

Compare with previous version

added 1 commit

• 4cb9449b - rename elem_of_equiv -> set_equiv and set_equiv_spec -> set_equiv_subseteq,...

Compare with previous version

@robbertkrebbers I think this is ready to be merged.

Related to the set_{eq,equiv}_subseteq lemmas, there's also https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/bi/interface.v#L281

Can we come up with some scheme to also make the naming of that lemma consistent?

We decided there are 4 renames we should do based in naming schemes we uncovered in this MR:

• Rename equiv_spec in Iris iris!628 (merged)
• Forall_Forall2 should get a _diag !223 (merged)
• The _11/_12 lemmas should be renamed to _1_1/_1_2. !222 (merged)
• We should add _instance suffixes to some TC instnaces to make room for using e.g. frac_op as a lemma name, and document this. iris!629 (merged)

mentioned in merge request iris!628 (merged)

resolved all threads

added 9 commits

• 4cb9449b...889d99ae - 8 commits from branch master
• 609a8918 - rename elem_of_equiv -> set_equiv and set_equiv_spec -> set_equiv_subseteq,...

Compare with previous version

It seems like there are MRs for all remaining tasks. Feel free to merge this MR once you have time to update reverse dependencies.

added 7 commits

• 609a8918...c7f299a5 - 6 commits from branch master
• 46cc81ad - rename elem_of_equiv -> set_equiv and set_equiv_spec -> set_equiv_subseteq,...

Compare with previous version

merged

mentioned in commit 58c0e8cb

@iris-users this renames some lemmas about set equality/equivalence:

- Rename set equality and equivalence lemmas:
  `elem_of_equiv_L` → `set_eq`,
  `set_equiv_spec_L` → `set_eq_subseteq`,
  `elem_of_equiv` → `set_equiv`,
  `set_equiv_spec` → `set_equiv_subseteq`.