Feedback wanted on Hamming implmentation

Stream: maths

[Wrenna Robson]

As I've mentioned before, I've been working on an implementation of Hamming spaces (that is, spaces equipped with the Hamming metric/norm if appropriate). While it is possible to construct this using the L_1 norm and discrete metric, that isn't desirable for a number of reasons - you can define the metric much more generally, for instance, and in many ways the fact that it is integer-valued is significant: it also means it's naturally computable.

Here's what I have so far:
https://gist.github.com/linesthatinterlace/9d13f7f13a9779e5986db573753741f7

I think this is nearing a PR, probably going under computability though I'm not sure about that. Some of the notions in computability (languages, encoding) are close to but not the same as notions in coding theory (which is the thing I'm really aiming to formalise some results for).

I do have some issues. I've mentioned these in the file (and in previous messages) but to summarise:

• The lack of a "normed monoid" structure seems related to the fact that I seem to get odd possible-diamond related problems when defining a module structure for the Hamming space when the base space has monoid instances.
• "normed space" is not the appropriate notion for unifying module and metric behaviour here, but there are true results about the way they interact - e.g. ham_dist_smul_le in my file - that I can't seem to capture in any existing structure.
• Side point - the fact that there's no way of defining a norm on a non-commutative group feels very odd. This only slightly impacts this work but I did encounter it.
• I'm not sure if "integer-valued metrics" could do with their own definition, or if the type of the return values a metric/norm should be part of its type a la valuation, but the Hamming distance is just one of a number of metric or metric-like operations from computer science which are topologically equivalent to the discrete metric but which are nevertheless of significance.

I would be interested in thoughts in these issues or others relating to the code I've posted above.

[Riccardo Brasca]

Can you please open a WIP or RFC pull request? Don't worry if it's not done yet!

[Riccardo Brasca]

I am teaching a course about linear codes, so I am definitely interested in having this in Lean

[Wrenna Robson]

Ah, I can do! I thought it was good practice to ask for a bit of feedback before making a larger PR.

[Wrenna Robson]

What do I do to mark it WIP/RFC?

[Yaël Dillies]

There are WIP and RFC labels.

[Wrenna Robson]

bingo, ta.

[Wrenna Robson]

Right, here we go.

[Wrenna Robson]

https://github.com/leanprover-community/mathlib/pull/14739

[Wrenna Robson]

Riccardo, I would be super interesting in discussing what the definition of linear codes should be as I've been mulling a few options, but that's outside the scope of this.