[Merged by Bors] - feat(data/fin): add some lemmas about coercions

[jsm28]

Two of these lemmas allow norm_cast to work with inequalities
involving fin values converted to ℕ. The rest are for simplifying
expressions where coercions are used to convert from ℕ to fin, in
cases where an inequality means those coercions do not in fact change
the value.

There are very few lemmas relating to coercions from ℕ to fin in
mathlib at present; the lemma of_nat_eq_coe (and val_add on which it
depends, and a few similarly trivial lemmas alongside val_add) is
moved from data.zmod.basic to fin.basic for use in proving the other
lemmas, while the nat lemma add_mod is moved to data.nat.basic for use
in the proof of of_nat_eq_coe, and mul_mod is moved alongside it as
suggested in review. These lemmas were found useful in formalising
solutions to an olympiad problem, see
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Some.20olympiad.20formalisations,
and seem more generally relevant than to just that particular problem.

TO CONTRIBUTORS:

Please include a summary of the changes made in this PR above "TO CONTRIBUTORS:", as that text will become the commit message. You are also encouraged to append the following co-authorship template if you'd like to acknowledge suggestions / commits made by other users:

Co-authored-by: name name@example.com

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• for tactics:
  • added or adapted documentation in the tactic doc entries
  • write an example of use of the new feature in test/tactics.lean or another test file
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

If you're confused by comments on your PR like bors r+ or bors d+, please see our notes on bors for information on our merging workflow.

[bryangingechen]

Is there a reason to use nat.succ n instead of n+1? I noticed that the rest of the file uses the latter.

[jsm28]

Only that the definition of of_nat (in the core Lean library) uses it. All my uses of these lemmas work unchanged with n+1 used in place of nat.succ n, if this is a matter of the core library using a style that's not preferred for this mathlib code and n+1 is preferred in mathlib.

[bryangingechen]

It may not matter a lot in practice, since n.succ and n+1 are definitionally equal, thus generally Lean is able to automatically convert between the two as needed. I think we try to keep things consistent for those odd cases where it can't, and I believe we've decided to prefer n+1 in mathlib. See e.g. #2067 (comment).

[jsm28]

Now changed to use n + 1.

[bryangingechen]

The PR looks good to me. I think some of these should be made @[simp], but I'm not 100% sure, so I'll let someone else comment on that.

Thanks for this and the previous contribution! I'll send you an invite so that you can create new branches in this repo and make PRs from them. This is preferred since that way github will display status icons that tell us at a glance whether your PRs build + lint successfully.

[gebner]

I'm not 100% sure these are correct simp lemmas. Write #lint at the end of the file, it will tell you if these should not be marked as simp lemmas.

[jsm28]

Those simp lemmas all passed #lint, so applied the suggested changes.

[urkud]

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bryangingechen]

The build failed on linting some of the simp lemmas: https://github.com/leanprover-community/mathlib/runs/618907915#step:14:68

bors r-

[bors]

Canceled.

[jsm28]

I interpret that lint failure as indicating that the presence of of_nat_eq_coe (in data.zmod.basic) means all these lemmas should actually be expressed in terms of coercions from ℕ to fin, and in general any proofs working with such conversions should prefer to express them in terms of those coercions rather than in terms of of_nat. Thus I've rephrased all the new lemmas (not just the simp ones) accordingly, removing the of_nat_one lemma and no longer marking of_nat_zero as a simp lemma. Proving some of the lemmas in their new form uses of_nat_eq_coe. To avoid circular imports, data.fin cannot import data.zmod.basic, so of_nat_eq_coe needed to move to data.fin (which seems to me to be a better place for it anyway); the proof uses val_add, which is also moved, and nat.add_mod, which needs to move from data.nat.modeq to data.nat.basic (thus getting a different proof that's usable in that context) to be usable from data.fin.

[bryangingechen]

bors try

[bors]

try

Build succeeded:

• Build mathlib

[bryangingechen]

Should some of the other fin-related lemmas be moved to data.fin as well?

[jsm28]

I've moved the trivial lemmas val_mul, one_val and zero_val that seem reasonably to go along with val_add. The rest look more specific to how fin is being used to set up zmod n.

[jcommelin]

Thanks for these PRs! It's much appreciated that you try to fill in these holes. It seems like you jumped into a messy import tangle... I'm sorry. But overall this PR looks good to me. We could try to split some of the longer .basic files, so that we can put things in the logical place without creating circular deps. But that would be work for a follow-up PR, so don't worry about it now.

[jcommelin]

LGTM

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib