!4#3107

Stream: mathlib4

[Jeremy Tan]

!4#3107 there are a lot of these errors related to the use of .map i:

[Jeremy Tan]

application type mismatch
  map i
argument
  i
has type
  @RingHom K L NonAssocRing.toNonAssocSemiring NonAssocRing.toNonAssocSemiring : Type (max v w)
but is expected to have type
  @RingHom K L Semiring.toNonAssocSemiring Semiring.toNonAssocSemiring : Type (max v w)

[Jeremy Tan]

How can I fix these errors?

[Moritz Doll]

probably attribute [-instance] Ring.toNonAssocRing

[Jeremy Tan]

What porting note should I add then?

[Eric Wieser]

Lean4#2074 is to blame

[Kevin Buzzard]

That link doesn't work for me. Is it lean4#2074 ? Edit: yes

[Eric Wieser]

More accurately, I think the fact that we worked around 2074 in a previous file is likely the cause, though I'm speculating without having opened Lean

[Jeremy Tan]

At some places after placing attribute [-instance] Ring.toNonAssocRing I'm now getting this error:

application type mismatch
  roots (map i p)
argument
  map i p
has type
  @Polynomial L DivisionSemiring.toSemiring : Type w
but is expected to have type
  @Polynomial L Ring.toSemiring : Type w

Which new line should I put?

[Eric Wieser]

set_option synth.etaExperiment true in might be an easier fix for this file

[Jeremy Tan]

@Eric Wieser Most definitions do get solved by the eta experiment, but splits_of_splits_id actually causes a timeout when eta is enabled

[Jeremy Tan]

(I've pushed my latest round of fixes btw)

[Jeremy Tan]

Then there's this error on line 283:

theorem splits_prod_iff {ι : Type u} {s : ι → K[X]} {t : Finset ι} :
    (∀ j ∈ t, s j ≠ 0) → ((∏ x in t, s x).Splits i ↔ ∀ j ∈ t, (s j).Splits i) := by
  refine'
    Finset.induction_on t (fun _ => ⟨fun _ _ h => h.elim, fun _ => splits_one i⟩) -- here
      fun a t hat ih ht => _
  rw [Finset.forall_mem_insert] at ht⊢
  rw [Finset.prod_insert hat, splits_mul_iff i ht.1 (Finset.prod_ne_zero_iff.2 ht.2), ih ht.2]
#align polynomial.splits_prod_iff Polynomial.splits_prod_iff

[Jeremy Tan]

By inspecting the Lean 3 code I know h is of a type x✝ ∈ ∅. This should simplify to False which has elim as a property, but it doesn't simplify

[Jeremy Tan]

oh wait...

[Eric Wieser]

Use set_option synth.etaExperiment true in (note the in) so that you can set it per-decl

[Kevin Buzzard]

Jeremy Tan said:

Eric Wieser Most definitions do get solved by the eta experiment, but splits_of_splits_id actually causes a timeout when eta is enabled

You should only enable it on the declarations where it's necessary. Don't enable it globally.

[Jeremy Tan]

I'm not enabling it globally

[Kevin Buzzard]

Are you saying that you don't know what to do with splits_of_splits_id because you have 0 solutions right now, or are you just remarking the known fact that enabling eta_experiment causes some things to time out?

[Jeremy Tan]

@Kevin Buzzard To put it clearly: as it is in my PR right now, splits_of_splits_id can't synth UniqueFactorizationMonoid K[X] and it doesn't have eta enabled for it. But if I enable eta, it causes

(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

[Jeremy Tan]

exists_root_of_splits' has about the same problem; mem_lift_of_splits_of_roots_mem_range is perhaps the most heinous theorem of all

[Jeremy Tan]

splits_comp_of_splits apparently has an unknown tactic

[Jeremy Tan]

There are also places where I'd like to see in Lean 3, using the Lean Web Editor what a particular _ expands to, particularly in the case where Lean 4 can't infer it. What do I do with that _?

[Jeremy Tan]

Now I have this:

set_option synthInstance.etaExperiment true in -- Porting note: gets around lean4#2074
theorem image_rootSet [Algebra F K] [Algebra F L] {p : F[X]} (h : p.Splits (algebraMap F K))
    (f : K →ₐ[F] L) : f '' p.rootSet K = p.rootSet L := by
  classical
    rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← f.coe_toRingHom]
    rw [← roots_map (↑f) ((splits_id_iff_splits (algebraMap F K)).mpr h)]
    rw [map_map, f.comp_algebra_map, ← root_set]

[Kevin Buzzard]

You can click on a _ in the infoview.

[Kevin Buzzard]

After classical you don't have to indent two (edit: from Eric's reaction apparently I'm wrong? I'm pretty sure you didn't have to indent two in Lean 3)

[Jeremy Tan]

At rw [← roots_map ... I have this error

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  Multiset.map (↑?m.331329) (roots (map (algebraMap F K) p))
i: K →+* L
p: F[X]
h: Splits (algebraMap F K) p
f: K →ₐ[F] L
⊢ ↑(Multiset.toFinset (Multiset.map (↑↑f) (roots (map (algebraMap F K) p)))) = rootSet p L

Why is the system not finding the pattern despite it being there to the human eye?

[Kevin Buzzard]

For the synth, try inserting the line haveI : UniqueFactorizationMonoid K[X] := inferInstance at some point in the proof before the problem.

[Kevin Buzzard]

Another possible approach is to enable eta and also increase heartbeats in the declaration

[Kevin Buzzard]

Why is the system not finding the pattern despite it being there to the human eye?

There can be several reasons for this. Either it doesn't actually match but you can only see this with pp.all true, or the hypotheses of the lemma (e.g. typeclass assumptions) can't be found. Did it work in lean 3, i.e. is this what the porting program is suggesting, or are you going off on a limb trying to fix something?

[Eric Wieser]

Kevin Buzzard said:

After classical you don't have to indent two

I think it might be good practice though, since classical now starts a scope

[Kevin Buzzard]

Did the lean 3 goal have two up-arrows in that failed rewrite? That might be the issue. Try dsimp first or something?

[Matthew Ballard]

Does simp_rw fail also?

[Jeremy Tan]

I'm busy tinkering with heartbeats. They do make the problematic theorems compile...

[Kevin Buzzard]

This might just be the path of least resistance at the end of the day. You are facing issues which are ultimtely going to have to be dealt with by changes in core, so whatever fix you come up with right now may well have to be refactored when MSR have got some momentum going again and start making the fixes to the issues which you and others are currently working around.

[Jeremy Tan]

Matthew Ballard said:

Does simp_rw fail also?

simp_rw does not eliminate the red line beneath but does shrink it to the \u f. The error is replaced with

type mismatch
  f
has type
  K →ₐ[F] L : Type (max v w)
but is expected to have type
  K →+* ?m.346410 : Type (max v ?u.346407)

[Kevin Buzzard]

So was the double up-arrow a coercion from an algebra hom to a ring hom and then to a function?

[Jeremy Tan]

Apparently yes:

F : Type u,
K : Type v,
L : Type w,
_inst_1 : field K,
_inst_2 : field L,
_inst_3 : field F,
_inst_4 : algebra F K,
_inst_5 : algebra F L,
p : F[X],
h : splits (algebra_map F K) p,
f : K →ₐ[F] L
⊢ ↑((multiset.map ⇑↑f (map (algebra_map F K) p).roots).to_finset) = p.root_set L

[Kevin Buzzard]

I don't personally know how to fix this but my impression is that this sort of thing is well-understood now by some people. Learning about how Lean 4 does coercions is high on my list of Lean stuff once I've tamed my non-Lean job list (which is now not being added to nearly as fast because term ended two days ago)

[Kevin Buzzard]

You could probably just change the ⇑↑f to f and this might make the rewrite succeed.

[Matthew Ballard]

If giving lean more time works, then it’s running out of time figuring out and matching up the the types. In a rw, I’ve seen this throw the standard can’t rewrite error in this case.

[Matthew Ballard]

If you trace and profile, you might see what it is spending so much time on.

[Jeremy Tan]

Who exactly are the people at MSR?

[Jeremy Tan]

is it just Leo and Gabriel?

[Jeremy Tan]

Matthew Ballard said:

If you trace and profile, you might see what it is spending so much time on.

how do I trace and profile?

[Matthew Ballard]

set_option trace should give you a menu of options with autocomplete

[Matthew Ballard]

Here most relevant is Meta.synthInstance probably

[Matthew Ballard]

The only profiling option that I am familiar with from an IDE is set_option profiler. There is a build flag for this also, right?

[Kevin Buzzard]

Jeremy Tan said:

is it just Leo and Gabriel?

Right now, yes.

[Matthew Ballard]

You can still end up with output that looks “the same” but where lean says no. Then pp.all might help

[Jeremy Tan]

Kevin Buzzard said:

You could probably just change the ⇑↑f to f and this might make the rewrite succeed.

hmm... that's not working

set_option synthInstance.etaExperiment true in -- Porting note: gets around lean4#2074
theorem image_rootSet [Algebra F K] [Algebra F L] {p : F[X]} (h : p.Splits (algebraMap F K))
    (f : K →ₐ[F] L) : f '' p.rootSet K = p.rootSet L := by
  classical
    rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, ← f.coe_toRingHom]
    change (↑(Multiset.toFinset (Multiset.map f (roots (map (algebraMap F K) p)))) = rootSet p L)
    rw [← roots_map (f) ((splits_id_iff_splits (algebraMap F K)).mpr h)]
    rw [map_map, f.comp_algebra_map, ← root_set]

[Jeremy Tan]

@Kevin Buzzard I'll just push what I have done so far. After the heartbeat fixes, 5 errors remain

[Ruben Van de Velde]

Jeremy Tan said:

By inspecting the Lean 3 code I know h is of a type x✝ ∈ ∅. This should simplify to False which has elim as a property, but it doesn't simplify

I'm not sure if this is the case, but there's at least one case involving x \in empty where a definition changed between lean 3 and lean 4 which means that you now need to insert the relevant not_mem_empty lemma (or whatever it's called) explicitly

[Jeremy Tan]

Ruben Van de Velde said:

Jeremy Tan said:

By inspecting the Lean 3 code I know h is of a type x✝ ∈ ∅. This should simplify to False which has elim as a property, but it doesn't simplify

I'm not sure if this is the case, but there's at least one case involving x \in empty where a definition changed between lean 3 and lean 4 which means that you now need to insert the relevant not_mem_empty lemma (or whatever it's called) explicitly

I already solved that with by simp only [Finset.not_mem_empty] at h

[Jeremy Tan]

Kevin Buzzard said:

You can click on a _ in the infoview.

It's not working in the Lean Web Editor (?)

[Jeremy Tan]

Now trying to fix cases h.subst ((mem_roots _).2 hx) (L196), the first of the 5 remaining errors

[Jeremy Tan]

Well this works:

theorem roots_ne_zero_of_splits' {f : K[X]} (hs : Splits i f) (hf0 : natDegree (f.map i) ≠ 0) :
    (f.map i).roots ≠ 0 :=
  let ⟨x, hx⟩ := exists_root_of_splits' i hs fun h => hf0 <| natDegree_eq_of_degree_eq_some h
  fun h => by
  rw [← eval_map] at hx
  have : f.map i ≠ 0 := by intro; simp_all
  cases h.subst ((mem_roots this).2 hx)

But is there a neater way?

[Jeremy Tan]

But then the error in natDegree_eq_card_roots' is much more complicated, I need help

theorem natDegree_eq_card_roots' {p : K[X]} {i : K →+* L} (hsplit : Splits i p) :
    (p.map i).natDegree = Multiset.card (p.map i).roots := by
  by_cases hp : p.map i = 0
  · rw [hp, natDegree_zero, roots_zero, Multiset.card_zero]
  obtain ⟨q, he, hd, hr⟩ := exists_prod_multiset_X_sub_C_mul (p.map i)
  rw [← splits_id_iff_splits, ← he] at hsplit
  rw [← he] at hp
  have hq : q ≠ 0 := fun h => hp (by rw [h, MulZeroClass.mul_zero])
  rw [← hd, add_right_eq_self]
  by_contra h
  have h' : (map (RingHom.id L) q).natDegree ≠ 0 := by simp [h]
  have := roots_ne_zero_of_splits' (RingHom.id L) (splits_of_splits_mul' _ _ hsplit).2 h'
  · rw [map_id] at this
    exact this hr
  · rw [map_id]
    exact mul_ne_zero monic_prod_multiset_X_sub_C.ne_zero hq

[Jeremy Tan]

Please help me with this PR, my brain is fried