eq.subst vs. ▸

Stream: general

[Junyan Xu]

▸ is simply the notation for docs#eq.subst, but I've found it sometimes less powerful, e.g. The two subst here cannot be replaced by ▸. Why is this, and is it possible to make them equally powerful? This is desirable since h ▸ is shorter than h.subst; it's less a problem for h.symm ▸ vs. h.substr since they have equal length (but a pair of parentheses may be eliminable using h.symm ▸), though it will be another story if we introduce a notation for eq.substr ...

[Kevin Buzzard]

Huh, yeah that's pretty weird. Note that eq.subst h ... also doesn't work (even though h.subst does).

[Kevin Buzzard]

Here's the issue on master and I've no doubt that it can be minimised a lot more:

import field_theory.splitting_field

variables {K : Type} [field K] (i : K →+* K)

open_locale polynomial

open polynomial

lemma roots_ne_zero_of_splits {f : K[X]} (hs : splits i f) (hf0 : nat_degree f ≠ 0) :
  (f.map i).roots ≠ 0 :=
begin
  obtain ⟨x, hx⟩ := exists_root_of_splits i hs (λ h, hf0 $ nat_degree_eq_of_degree_eq_some h),
  intro h, -- h : (map i f).roots = 0
  rw ← eval_map at hx,
--  cases eq.subst h ((mem_roots _).2 hx), -- fails
  cases h.subst ((mem_roots _).2 hx), -- works
  exact map_ne_zero (λ h, (h.subst hf0) rfl)
end

[Yaël Dillies]

I'm pretty sure this is the result of elab_as_eliminator. I'm not certain we want to get the two to do the same thing because if I remember correctly I sometimes reached the opposite situation, so it's nice to have both options available.

[Junyan Xu]

Interesting, I didn't know elab_as_eliminator has to do with dot notation.

[Yaël Dillies]

Dot notation in general messes up with elaboration, so dot notation has to do with elab_as_eliminator to the extent that both change elaboration. As a result, I'm not sure the difference in behavior is intended.

[Peter Nelson]

I’ve run into this problem too - I am not sure that having both options available is a great solution, since it is rather opaque when one works over the other. I don’t understand what fixing this would entail, though.