rw + apply_instance

Stream: general

[Eric Rodriguez]

it'd be nice if there was a version of rw that ran apply_instance on every class argument created during its execution; for example, consider this as to why it's useful (it's not minimal, but I'm sure that everyone here has seen this behaviour and knows what I mean):

lemma is_root_of_unity_iff {n : ℕ+} {R : Type*} [comm_ring R] [is_domain R] (ζ : R) :
  ζ ^ (n : ℕ) = 1 ↔ ∃ i ∈ (n : ℕ).divisors, (cyclotomic i R).is_root ζ :=
by rw [←mem_nth_roots n.pos, nth_roots, mem_roots $ X_pow_sub_C_ne_zero n.pos _,
       C_1, ←prod_cyclotomic_eq_X_pow_sub_one n.pos, is_root_prod]; apply_instance

[Eric Rodriguez]

it's not too annoying in this case but in long proofs it can really clog up the proof state and lead to awkward things like any_goals { apply_instance }, or even swap { ... }, swap ... if it's too slow

[Eric Rodriguez]

would this be easy to make for someone with low meta knowledge?

[Kevin Buzzard]

My experience with this issue is that apply_instance does get tried, but sometimes it's tried too early.

[Eric Rodriguez]

I think it's when you have terms like mem_nth_roots n.pos, whose signatures look something like {R} [... R] ... (h : 0 < n), so the elaborator gets confused about the terms, and is only resolved when it unifies with the expression you are rewriting; and then it's too late for inference to kick in

[Alex J. Best]

Just hypothesizing here but could this be resolved by reordering the arguments for the lemma being rewritten?

[Eric Rodriguez]

I think so, but this requires a massive change in how mathlib works because it means you have to take pretty much all types out of variables statements, and put them after hypotheses. (e.g. for mem_nth_roots you'd need a signature like {n : ℕ} (h : 0 < n) {R : Type*} [comm_ring R] ...)

[Alex J. Best]

Well if it actually worked and was useful we could try some metaprogramming magic to generate reordered declarations automatically, or make rw try to do such reordering automatically?

[Eric Wieser]

Can we verify that this actually helps by making a local copy of the one offending lemma before exploring this rabbit hole?

[Alex J. Best]

Yeah it doesn't help sadly

[Alex J. Best]

What does help is making R explicit, even if its not specified explicitly in the rw

[Alex J. Best]

import ring_theory.polynomial.cyclotomic

open polynomial
lemma puff_the_magic_lemma {n : ℕ} (hn : 0 < n) (R : Type*) {x a : R} [comm_ring R] [is_domain R] :
  x ∈ nth_roots n a↔ x ^ n = a:= mem_nth_roots hn
lemma is_root_of_unity_iff {n : ℕ+} {R : Type*} [comm_ring R] [is_domain R] (ζ : R) :
  ζ ^ (n : ℕ) = 1 ↔ ∃ i ∈ (n : ℕ).divisors, (cyclotomic i R).is_root ζ :=
begin
  rw [← puff_the_magic_lemma n.pos, nth_roots, mem_roots $ X_pow_sub_C_ne_zero n.pos _,
  -- rw [←mem_nth_roots n.pos, nth_roots, mem_roots $ X_pow_sub_C_ne_zero n.pos _,
       C_1, ←prod_cyclotomic_eq_X_pow_sub_one n.pos],
  sorry,
  apply_instance,
  apply_instance,
end

[Alex J. Best]

Here puff the magic lemma is the same as docs#mem_nth_roots apart from argument order and explicitness of R. rwing with puff doesn't produce a side goal where the original does

[Eric Rodriguez]

⦃⦄ binders on R work too... I'm now more confused than I was before, ngl

[Eric Rodriguez]

Actually, I guess it prevents it from elaborating further till we know what R is, and then rw's internal stuff can do the work

[Alex J. Best]

I don't think I've ever seen those binders on a type before! Whats the thinking behind using those rather than round?

[Eric Wieser]

They're usually used on the RHS of :=, like in src#function.injective

[Eric Rodriguez]

Because I still don't have to state it, but lean won't evaluate it until I go to the rhs of it :) I think it's a clever solution, but going to test it for a bit first and see how it works out

[Alex J. Best]

When would you have to state it though? If you are only ever doing rw with that lemma still?

[Eric Rodriguez]

Maybe you'll want to do .mp or something on the lemma? Not sure...

[Eric Rodriguez]

Ahh, it doesn't even work if you want to do .mp; you'll get told that ∀ {{R}} ... doesn't have mp. Shame :/