!4#2850

Stream: mathlib4

[Jeremy Tan]

!4#2850 there are two remaining questions I have with this port.

theorem taylor_coeff (n : ℕ) : (taylor r f).coeff n = (hasseDeriv n f).eval r :=
  show (lcoeff R n).comp (taylor r) f = (leval r).comp (hasseDeriv n) f by
    congr 1; clear! f; ext i

In Lean 3 the tactic state after ext i is

⇑(((lcoeff R n).comp (taylor r)).comp (monomial i)) 1 = ⇑(((leval r).comp (hasse_deriv n)).comp (monomial i)) 1

but in Lean 4 the 1s are inaccessible variables instead, which causes the rest of the proof to fail. What can I do to introduce the 1s?

↑(LinearMap.comp (LinearMap.comp (lcoeff R n) (taylor r)) (monomial i)) x✝ =
  ↑(LinearMap.comp (LinearMap.comp (leval r) (hasseDeriv n)) (monomial i)) x✝

[Jeremy Tan]

And in here, apply_fun fails for being a dependent function even though intuitively it should go through. How can I apply this dependent function to h?

theorem taylor_injective {R} [CommRing R] (r : R) : Function.Injective (taylor r) := by
  intro f g h
  apply_fun (taylor (-r) ·) at h
  simpa only [taylor_apply, comp_assoc, add_comp, X_comp, C_comp, C_neg, neg_add_cancel_right,
    comp_X] using h
#align polynomial.taylor_injective Polynomial.taylor_injective

[Eric Wieser]

It sounds like an ext lemma is being missed

[Eric Wieser]

In Lean 3 you can write ext? to find out which ones are applied

[Eric Wieser]

I think it's something like docs#linear_map.ext_ring

[Eric Wieser]

docs4#LinearMap.ext_ring

[Eric Wieser]

The priority needs raising on that ext lemma, since now the order is by default random instead of by default exactly what we want

[Jeremy Tan]

yeah, apply Polynomial.lhom_ext'; rintro i; apply LinearMap.ext_ring in place of ext i works

[Jireh Loreaux]

Well don't just substitute that, please fix the priority. Then ext should just work

[Jeremy Tan]

how can I get an idea for the right priority to use?

[Jeremy Tan]

I think the default priority is 1000, so would setting it to 1100 be good?

[Jireh Loreaux]

I think the default is 1000, so I've just been setting it at 1001 (or 1002 etc. if necessary).

[Jireh Loreaux]

I'm not too picky, so long as we're going about this the right way.

[Eric Wieser]

I think priority := high is usually the right choice?

[Eric Wieser]

I'm not too picky, so long as we're going about this the right way.

Arguably the right way was the Lean3 behavior...

[Jireh Loreaux]

But that's not available?

[Eric Wieser]

priority := high is, right? But yes, the Lean3 behavior (currently) is not

[Jeremy Tan]

I just set the priority for the offending lemma to 1001. Let's see if it works

[Jireh Loreaux]

Yes, Eric, that's what I meant.

[Eric Wieser]

Jeremy Tan said:

I just set the priority for the offending lemma to 1001. Let's see if it works

@[ext high] is preferred I think

[Jeremy Tan]

changed again to @[ext high]. And what about the dependent function problem later on in the file?

[Jeremy Tan]

@Eric Wieser @[ext high] fails in HasseDeriv.lean

[Eric Wieser]

I would guess that's because someone changed the proof when it stopped working and didn't track down the cause

[Eric Wieser]

Have a look at the diff from mathport in the PR that ported HasseDeriv

[Jeremy Tan]

Yeah, tracking down the offending declaration in HasseDeriv revealed that it could be shortened a bit with the new priority. casavaca rewrote the proof of hasseDeriv_comp in an excessively long-winded way

[Jeremy Tan]

The apply_fun (taylor (-r) ·) at h problem remains

[Eric Wieser]

Can you make a standalone PR that fixes HasseDeriv and the ext priority?

[Eric Wieser]

That way we can prevent other porting PRs running into the same problem

[Eric Wieser]

ext_ring_op should get the same treatment

[Casavaca]

casavaca rewrote the proof of hasseDeriv_comp in an excessively long-winded way

It's still an improvement. The old proof didn't even get field_simp to work. (https://github.com/leanprover-community/mathlib3port/blob/e3b6a9dcca4b55978e0f5517c4cb0d854115e00f/Mathbin/Data/Polynomial/HasseDeriv.lean#L260) It's true that it can be simplified. But that's not very important.

[Eric Wieser]

What's important is that we re-enable the ext lemma and adjust the proofs that are broken by it. We should prioritize doing that over the rest of !4#2850

[Casavaca]

That's true. I did notice that ext didn't work but I didn't know what to do with it. Now I learned something new.

[Jeremy Tan]

Eric Wieser said:

Can you make a standalone PR that fixes HasseDeriv and the ext priority?

!4#2859

[Jeremy Tan]

the backend changes made in !4#2850 turned out to be enough

[Jeremy Tan]

now that !4#2859 is merged how do I solve the last error?

[Eric Wieser]

I pushed a fix

[Eric Wieser]

Though it's not a particularly nice one

[Eric Wieser]

This seems like a bug in apply_fun, it seems too keen to dismiss (a : R[X]) → (fun x => R[X]) a as a dependent function, when an eta expansion gives R[X] → R[X] which is clearly non-dependent

[Jeremy Tan]

It works by "hiding" the dependent variable r inside a coercion, right?

[Eric Wieser]

I have no idea why that works, it leaves a horrible metavariable in the goal state.

[Eric Wieser]

I pushed a clearer fix that uses replace h := FunLike.congr_arg (taylor (-r)) h instead

[Jeremy Tan]

:+1:

[Scott Morrison]

Eric Wieser said:

This seems like a bug in apply_fun, it seems too keen to dismiss (a : R[X]) → (fun x => R[X]) a as a dependent function, when an eta expansion gives R[X] → R[X] which is clearly non-dependent

If there's a #mwe of this I can take a look; I think I wrote the dependent-function-wrangling in apply_fun.

[Eric Wieser]

Here you go:

import Mathlib.Algebra.Hom.Group
import Mathlib.Tactic.ApplyFun

example (f : ℕ →+ ℕ) (a b : ℕ) (h : a = b) : true := by
  apply_fun f at h
  sorry

[Eric Wieser]

I think any FunLike object would trigger it, if you want to remove the need for groups too

[Kyle Miller]

Here's a mwe with only the ApplyFun import:

import Mathlib.Tactic.ApplyFun

example (f : ℕ ≃ ℕ) (a b : ℕ) (h : a = b) : true := by
  apply_fun f at h
  sorry

[Kyle Miller]

I'm wondering if it would be easier for ApplyFun to get Lean to elaborate f a = f b and then prove it using congr!

[Kyle Miller]

It's a bit ugly (since it sort of reproduces what's already in mkAppN, but those functions are private and not exactly what we'd want), but I got apply_fun to work with anything with a CoeFun instance. Dependent functions too (I wanted to potentially be able to do apply_fun Fintype.card at h). mathlib4#2890 is a WIP -- I haven't looked beyond applyFunHyp, though maybe there's nothing to be done for applyFunTarget.

If you want to work on it or take it over, feel free @Scott Morrison

[Scott Morrison]

Looks very nice!

[Kyle Miller]

The fixes to apply_fun manage to address the apply_fun taylor (-r) at h problem: mathlib4#2925

The tactic now has some extra powers. If you have h : a = b and f a and f b are both expressions that can be elaborated (using the whole elaboration algorithm, including coercions), then it should succeed so long as f a and f b have the same type.

example (f : ℤ ≃ ℤ) (a b : ℕ) (h : a = b) : True := by
  apply_fun f at h
  -- now h : f a = f b with coercions on f, a, and b!

Here's example that almost works but could. If I were to switch mvar.mvarId!.congrN to mvar.mvarId!.congrN! in applyFunHyp then this works too:

import Mathlib.Tactic.ApplyFun
import Mathlib.Data.Fintype.Card

example (α β : Type u) [Fintype α] [Fintype β] (h : α = β) : True := by
  apply_fun Fintype.card at h
  -- now h : Fintype.card α = Fintype.card β

(there are typeclass arguments after the types in Fintype.card). The reason it doesn't work right now is that mvar.mvarId!.congrN doesn't know about Subsingleton.elim.

[Scott Morrison]

So let's do that too?