Improve the consistency of naming and definitions in Cedar.Data and Cedar.Thm.Data

[emina]

Category

Lean formalization

Describe the feature you'd like to request

We accumulated some redundancies and stylistic inconsistencies across the shared data structure definitions and lemmas. Let's fix these by consolidating the definitions:

Definitions in Cedar.Data:

• Map has both .kvs and .toList, which are synonyms. Drop one.
• The definition of Membership.mem for Maps is inconsistent with contains and find?. Let's make them consistent.
• Set has both .elts and .toList, which are synonyms. Drop one.

Theorems in Cedar.Thm.Data:

• We are inconsistent about when we make arguments to lemmas implicit vs explicit. Let's adopt a consistent style in line with Lean's Std and MathLib: an argument is explicit only when it can't be inferred from the preconditions.
• We are inconsistent about expressing lemmas as a single iff lemma versus two lemmas for both directions. Let's use a single iff lemma when both directions have the same preconditions.
• For theorems that take both a Map and a key (or value or both), consistent ordering of those arguments.
• Rename make_mem_list_mem because mem comes first in the statement of the theorem.

Describe alternatives you've considered

N/A

Additional context

No response

Is this something that you'd be interested in working on?

• 👋 I may be able to implement this feature request
• ⚠️ This feature might incur a breaking change

[cdisselkoen]

Another tiny one: argument order. For theorems that take both a Map and a key (or value or both), consistent ordering of those arguments.

[emina]

Added

Another tiny one: argument order. For theorems that take both a Map and a key (or value or both), consistent ordering of those arguments.

Added to the issue description.

[cdisselkoen]

Another one we discussed: renaming make_mem_list_mem