coes and instances

Stream: general

[Eric Rodriguez]

tl;dr: how do I design an instance such that foo ((x : A) : B) ↔ foo (@coe_trans X A B ... x) and both are seen by typeclass search?

For flt_regular, we made a typeclass ne_zero to carry around the statement of something not being zero in a field/etc. This is usually most helpful when casting to fields. However, in flt-regular, we deal with pnats, and so therefore we often state results with [ne_zero ((n : ℕ) : K)]. However, this is overly verbose, and it would be nice to deal with purely the coe_trans: we attmepted to do this in PR #11715, and it worked fine on the material in mathlib. However, _everything_ in flt-regular broke, so I'm currently reverting the changes in #11760. (I will test this again with flt-regular before merging so that there is no fiasco this time!)

However, it would be nice to not have to write this sort of double coercions. So I was hoping there was some magic that I could write to make these instance results work. I tried reversing the instances from what is currently there, and this almost works, but instead of looking for ne_zero (n : ℕ) en-route to ne_zero ((n : ℕ) : K), it ends up looking for ne_zero (coe_b n). I don't know what coe_b is, and the source didn't prove much more enlightening (docs#coe_b) - it is defeq but not synctactically equal to ↑n, so typeclass search gets stuck and doesn't look further (or maybe it does? the upshot is that the relevant instances are not found). Maybe making it reducible would help here, but I feel like I'm missing the big-picture point - what _is_ coe_b? Why does it hurt us in this way? (see this commit for the issues in trying to use this). Obviously we can't create a loop, so we have to choose one way... how do we tell the TC system that these are equivalent?

I wrote a long writeup about this issue on the flt_regular stream, see there for more details.

cc: @Riccardo Brasca

[Anne Baanen]

The quick answer is: in Lean 3 you cannot have an instance A → B and an instance B → A at the same time. In Lean 4 this is possible, provided the instance created by going A → B → A is syntactically exactly equal to the original instance.

[Eric Rodriguez]

that's exciting for lean4! so the only real solution is to keep the double-coes?

[Anne Baanen]

A solution is to split A into two copies, and only add the implications A → B and B → A', consistently having A as return value and and taking an A' as parameter.

[Anne Baanen]

instead of looking for ne_zero (n : ℕ) en-route to ne_zero ((n : ℕ) : K)

should the first be ne_zero (n : K)?

[Anne Baanen]

I suspect there's no technical reason to use coe_b over writing out has_coe.coe. Have you already tried local attribute [reducible] coe_b at the place you got the errors?

[Anne Baanen]

Do I understand correctly that you want the following to work (cyclotomic/basic.lean:337):

/-- If `is_cyclotomic_extension {n} K L` and `ne_zero (n : K)`, then `L` is the splitting
field of `cyclotomic n K`. -/
lemma splitting_field_cyclotomic : is_splitting_field K L (cyclotomic n K) :=
{ splits := splits_cyclotomic n {n} K L (mem_singleton n),
  adjoin_roots :=
  begin
    rw [← ((iff_adjoin_eq_top {n} K L).1 infer_instance).2],
    letI := classical.dec_eq L,
    obtain ⟨ζ, hζ⟩ := @is_cyclotomic_extension.exists_root {n} K L _ _ _ _ _ (mem_singleton n),
    haveI : ne_zero (n : L) := ne_zero.nat_of_injective (algebra_map K L).injective,
    rw [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ← is_root.def, is_root_cyclotomic_iff] at hζ,
    refine adjoin_roots_cyclotomic_eq_adjoin_nth_roots n hζ
  end }

[Eric Rodriguez]

sorry, I just had some internet issues. yes, exactly, this is what we would like to work

[Anne Baanen]

I think it's best to keep using the double coercions in your parameters, for two reasons: simp-normal form is to have multiple coercions, so it's likely local variables already have this form. Moreover, in this case it's common to have terms of the form ne_zero (coe n : K) where n is a natural number (not a pnat), so we should try to arrange our instances so that this applies easily.

[Anne Baanen]

So make ne_zero.coe_trans the instance and ne_zero.trans a lemma.

[Eric Rodriguez]

I just removed them entirely; I'll try that but still using ↑↑n in most places. I'm also hoping to introduce some random arrow as the specific coe from ℕ+ to ℕ (in a locale), so that at least it's easier to type.

[Eric Rodriguez]

Thanks so much for the advice!