[Merged by Bors] - feat(field_theory/intermediate_field): generalize algebra instances

[Vierkantor]

The algebra and is_scalar_tower instances for intermediate_field are (again) as general as those for subalgebra.

---

[bors]

✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

bors d+

[Vierkantor]

Looks like the timeout is due to a bad, but terminating, interaction with the instance [h : fact (p.splits (algebra_map F E))] : algebra p.splitting_field E. Giving that instance a lower priority makes the failing lemma a lot faster again.

[Vierkantor]

I don't really understand what is going on. The issue is that typeclass search gets stuck when it makes a wrong turn at gal.is_scalar_tower. But there should be nothing that can cause a loop there, since there are no is_scalar_tower in its (transitive) assumptions. Instead it keeps on starting a search for a fact (p.splits (algebra_map F E)) instance.

Here's some test code. Above two examples that should, and do, fail fast. Then the problem where Lean gets stuck.

def should_fail_fast1 (α : p.splitting_field) : is_scalar_tower F p.splitting_field p.splitting_field :=
@gal.is_scalar_tower _ _ p p.splitting_field _ _ _  -- failed to synthesize class instance

def should_fail_fast2 : fact
  (@splits F p.splitting_field _inst_1 (@splitting_field.field F _inst_1 p)
    (@algebra_map F p.splitting_field
      (@comm_ring.to_comm_semiring F (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
      (@ring.to_semiring p.splitting_field
        (@division_ring.to_ring p.splitting_field
          (@field.to_division_ring p.splitting_field (@splitting_field.field F _inst_1 p))))
      (@splitting_field.algebra F _inst_1 p))
p) := infer_instance -- failed to synthesize class instance

def should_work_but_loops (α : p.splitting_field) : is_scalar_tower F F⟮α⟯ p.splitting_field :=
@@intermediate_field.is_scalar_tower_mid _ _ _ _ _ _ _ (@gal.is_scalar_tower _ _ p p.splitting_field _ _ _)
-- timeout, keeps trying to find the above instance

[Vierkantor]

Ah nevermind, there's another similar failure, this case for @is_scalar_tower F ↥(solvable_by_rad F E ) ↥(solvable_by_rad F E)...

[Vierkantor]

Ah this is bad, even the following times out:

example (S : intermediate_field K L) (T : intermediate_field K S) : is_scalar_tower K T S := infer_instance

[jcommelin]

Sorry, I was away for a couple of days. Is there some zulip discussion about this problem?

[Vierkantor]

Yes: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Forever.20inferring.20the.20same.20instance

The issue seems to have been resolved by providing a shortcut, which @eric-wieser seems to agree with.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests