Is there a more Lean-y approach to coercions?

Stream: Analysis I

[Dan Abramov]

We've discussed it briefly in other threads but I'm still running into difficulties with coercions between Object, ℕ, custom Nat, and the Subtype machinery.

To give you a few examples, in image_f_3_4_2, after simp my goal becomes

x : nat.toSubtype
h : (↑x : Object) = 2
⊢ 2 * (nat_equiv.symm : Nat.toSubtype → ℕ) x = 4

So we have a statement that ((x: nat): Object) = (ofNat(2): Object) and we want to show that 2 * ((x: Nat): ℕ) = (4: ℕ). That's pretty hard to think about when you don't quite have the right lemmas.

Then further on in preimage_f_3_4_2, after simps we have

x : nat.toSubtype
h : 2 * nat_equiv.symm x = 4
⊢ ↑x = 2

So we need to turn (2:ℕ) * ((x: Nat): ℕ) = (4:ℕ) into ((x: Nat): Object) = (ofNat(2): Object).

And then we have a bunch of lemmas in 3.1 that try to do some of these conversions, but whenever a particular exercise (or a particular "path" through an exercise) doesn't hit the happy path, it really sucks the joy out of doing the exercises — and I'm not sure how much it is actually teaching.

I'm wondering if there is a more systematic way to approach this problem. I would take as a given that we want to preserve the current hierarchy (and all the types). It's casts themselves that feel dubious to me.

I'd like to know, in particular, if there is a way to:

• (a) Either leverage more Lean/Mathlib machinery (like norm_cast?) to take care of these more automatically

• (b) Or to be more strategic about the choice of simp lemmas so that they reliably eliminate the patterns the reader is likely to encounter

Re (a), I just don't have enough Lean background to know whether this would significantly improve on the problem or not.

Re (b), I'm wondering if there's some systematic way to deal with "three types" (e.g. to enumerate each permutation of nesting, or to only write lemmas of certain signatures — like "double elimination"). Intuitively it feels like there must be some way to "work how Lean wants us to" rather than fight against it, and that maybe we're missing some discipline in how the simp lemmas are chosen.

If someone has ideas, the relevant definitions are mostly here: https://github.com/teorth/analysis/blob/5cacd4af98b4c3b02e75df1f4c0961c80b7e6569/analysis/Analysis/Section_3_1.lean#L621-L674

If you want to playtest a change to how they work, you can use https://github.com/rkirov/analysis or https://github.com/gaearon/analysis-solutions (and other forks). I'm also happy to playtest ideas myself if someone can suggest what concrete things to try.

Thank you!

[Dan Abramov]

It's also possible that this is just "how it is" and I need to bite the bullet and embrace individual tedious one-off conversions.

[Kevin Buzzard]

It seems to me that if users are getting into this kind of mess because of Object and nat.toSubtype then a (bespoke?) tactic is needed which just does "get me out of this mess please".

[Terence Tao]

In this particular case, a new @[simp] lemma that ((x:nat):Object) = (ofNat(n):Object) is equivalent to x = ofNat(n) may resolve the problem (this is a slight variant of the existing @[simp] lemma SetTheory.Set.nat_coe_eq_iff, which unfortunately doesn't quite apply in this context). I'm not 100% sure how norm_cast actually works but perhaps such lemmas could also be tagged @[norm_cast]?

[Dan Abramov]

Okay, I couldn't get this lemma to work but I figured a slightly different one that does. Folded that into https://github.com/teorth/analysis/pull/191. Maybe that's enough but I'll keep poking later to see if something can be simplified.