norm_cast: badly shaped lemma

Stream: mathlib4

[Anatole Dedecker]

The following declaration

@[simp, norm_cast]
theorem coe_to_mul_equiv (f : R ≃+* S) : ⇑(f : R ≃* S) = f :=
  rfl

gives the error norm_cast: badly shaped lemma, rhs can't start with coe
If I understand correcly, the "pure Lean4 solution" would be to write f.toFun instead, but IIUC for FunLike coercions are not syntactically equal to their definition as it is the case with CoeFun (does that sound right?) What is the intended solution here?

[Kevin Buzzard]

Is this a syntactic tautology? Remove the norm_cast attr and lint. If it's a syntactic tautology then we don't want it at all.

[Eric Wieser]

This should be the statement that FunLike.coe f.toMulEquiv = FunLike.coe f

[Eric Wieser]

If the statement is f.toMulEquiv.toFun = f.toFun then there's a problem here, because that is a syntactic tautology

[Eric Wieser]

We probably also need the lemma that saysFunLike.coe (AddEquivClass.coeToAddEquiv f) = FunLike.coe f

[Anatole Dedecker]

Kevin Buzzard said:

Is this a syntactic tautology? Remove the norm_cast attr and lint. If it's a syntactic tautology then we don't want it at all.

In its current form this is not a syntactif tautology

[Kevin Buzzard]

Maybe the intended solution is to figure out why we're not allowed to have this lemma in norm_cast.

[Anatole Dedecker]

Eric Wieser said:

This should be the statement that FunLike.coe f.toMulEquiv = FunLike.coe f

Two things about that:

• it looks like (f : R ≃* S) is not syntactically equal to f.toMulEquiv (the first one elaborates to a structure declaration, while the second one stays as f.toMulEquiv. Which "normal form" should I choose? I'm tempted to say the second one because it doesn't mess up the infoview, but that means not using coercions to forget structure, which is annoying (or should I setup things differently?)
• in either cases, the fact that there is still a coercion in the rhs makes this unsuitable for norm_cast. IIUC the current status is that norm_cast lemmas have to remove coercions at the start of terms, whereas we have quite a few lemmas in mathlib which only decrease (strictly) the number of coercions. Is this change of behavior intentional?

[Kevin Buzzard]

If whichever normal form we choose is tagged with the coe attribute then the lemma becomes \u \u f = \u f. Are you saying this isn't allowed as a norm_cast lemma?

[Anatole Dedecker]

Thanks Kevin, now I understand the problem better: because the first coercion to MulEquiv was not tagged as coe (in either case), this didn't actually make the number or coercions go down, hence the attribute complaining. If I add the right coe attributes for the goal to look like ↑↑f = ↑f then everything works fine!

[Anatole Dedecker]

I can't tell if the system is getting more subtle (presumably to get more useful), or if I'm just too used to the quirks of Lean3 :sweat_smile:

[Anatole Dedecker]

That said, although tagging RingEquiv.toMulEquiv with coe is easy, I can't make (f : R ≃* S) appear as a coercion, and because everything is syntactically unfolded I'm not sure what I would have to put the attribute on anyway... Any ideas?

[Kevin Buzzard]

Lean 4 is 99% the same as Lean 3 so porting is usually smooth, but in the situations where conventions have changed (and coercion is a great example of this) I think we're still working out how things are going to work -- some lemmas we have about coercions might be useless or may need modification, and it's difficult to know whether what we have will work because we can't test it on mathlib4 because mathlib isn't ported yet.

I think that there is an argument for making three new documents to be hosted somewhere in the porting infrastructure, covering (1) changes in coe and how the new system works (2) what to do when a ported simp proof breaks and (3) how the (proposed) changes in mul_opposite, order_dual etc from a type synonym to a one-field structure will affect the port.

[Riccardo Brasca]

I have the same problem with

@[simp, norm_cast]
theorem Int.coe_nat_pow (n m : ℕ) : ((n ^ m : ℕ) : ℤ) = n ^ m :=

and I don't really understand it...

[Yaël Dillies]

Does this have to do with Int.ofNat vs Nat.cast?

[Riccardo Brasca]

I think so, one is marked @[coe], the other is not.

[Eric Wieser]

Anatole Dedecker said:

it looks like (f : R ≃* S) is not syntactically equal to f.toMulEquiv (the first one elaborates to a structure declaration, while the second one stays as f.toMulEquiv. Which "normal form" should I choose? I'm tempted to say the second one because it doesn't mess up the infoview, but that means not using coercions to forget structure, which is annoying (or should I setup things differently?)

This is the AddEquivClass.coeToAddEquiv function I made up in my comment, and is the coercion define on docs#add_equiv_class that @Yaël Dillies and @Anne Baanen have advocated for in the past (docs#add_equiv.has_coe_t). This coercion is convenient, but it can be tricky to use as a simp-normal form.

[Anatole Dedecker]

Ok so I managed to make it work by extracting the actual coercion from docs4#instCoeTCMulEquiv and tagging it as coe. Is it wrong to have both a CoeTC instance and a @[coe]? It looks like this:

@[to_additive, coe]
def MulEquivClass.toMulEquiv [Mul α] [Mul β] [MulEquivClass F α β] (f : F) : α ≃* β where
  toFun := f
  invFun := EquivLike.inv f
  left_inv := EquivLike.left_inv f
  right_inv := EquivLike.right_inv f
  map_mul' := MulEquivClass.map_mul f

@[to_additive]
instance [Mul α] [Mul β] [MulEquivClass F α β] : CoeTC F (α ≃* β) :=
  ⟨MulEquivClass.toMulEquiv⟩

[Anatole Dedecker]

I guess my question really is: is the right solution to do this or to change something in norm_cast?

[Anatole Dedecker]

If someone wants to play with this, see mathlib4#1077

[Kevin Buzzard]

Riccardo Brasca said:

I have the same problem with

@[simp, norm_cast]
theorem Int.coe_nat_pow (n m : ℕ) : ((n ^ m : ℕ) : ℤ) = n ^ m :=

and I don't really understand it...

@Riccardo Brasca in Lean 4 that lemma is a syntactic tautology, due to differences in parsing.

[Kevin Buzzard]

@[norm_cast]
theorem Int.coe_nat_pow (n m : ℕ) : ((n ^ m : ℕ) : ℤ) = (n : ℤ) ^ m := sorry

[Riccardo Brasca]

Ah that's interesting, thanks!

[Yaël Dillies]

Would then

@[norm_cast]
theorem Int.coe_nat_pow (n m : ℕ) : (n ^ m : ℤ) = (n : ℤ) ^ m := sorry

be the canonical way to write it?

[Riccardo Brasca]

At least this is true but not proved by rfl...

[Moritz Doll]

Kevin Buzzard said:

I think that there is an argument for making three new documents to be hosted somewhere in the porting infrastructure, covering (1) changes in coe and how the new system works (2) what to do when a ported simp proof breaks and (3) how the (proposed) changes in mul_opposite, order_dual etc from a type synonym to a one-field structure will affect the port.

Except for (3) this is in https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki and if there is something missing, then feel free to add it.

[Moritz Doll]

the part about simp should be moved to its own subsection.

[Kevin Buzzard]

Oh thanks! I should get into the habit of looking more at what's there, rather than what was there last time I looked carefully.

[Eric Wieser]

Kevin Buzzard said:

Riccardo Brasca in Lean 4 that lemma is a syntactic tautology, due to differences in parsing.

What are the new parsing rules that are relevant here?

[Kevin Buzzard]

I wrote something about this somewhere, either on Zulip or as an issue, but I can't remember which and I'm at my mother's 80th so can't really look

[Kevin Buzzard]

https://github.com/leanprover/lean4/issues/1915

[Anne Baanen]

In !4#4293, we are running into this error on the coe_C and coe_X lemmas, for example:

theorem coe_C {F : Type u} [Field F] (r : F) : ↑(coeAlgHom F) (↑C r) = ↑HahnSeries.C r

I claim this is a good norm_cast lemma because the right hand side ↑HahnSeries.C r is a bundled function application, which is morally not the same as a cast. Can norm_cast not deal with this?

[Anne Baanen]

Actually, ↑(coeAlgHom F) is suspicious, that should just be a single ↑. Maybe redefining the coercion fixes this?

[Yury G. Kudryashov]

I guess, the problem is that in the LHS the head symbol is not a function marked with @[coe]. Usually, I defined Something.cast and used it for the Coe instance.

[Anne Baanen]

Yep, that fixes coe_C, but coe_X is still complaining:

theorem coe_X {F : Type u} [inst : Field F] : ↑X = ↑(single 1) 1

I suppose the issue is the number of ↑ does not decrease, even though the ↑s are "less big"