Zulip Chat Archive

Stream: general

Topic: eq.subst vs. ▸


Junyan Xu (Jun 22 2022 at 06:34):

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 (Jun 22 2022 at 07:54):

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

Kevin Buzzard (Jun 22 2022 at 07:58):

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 (Jun 22 2022 at 09:00):

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 (Jun 22 2022 at 09:07):

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

Yaël Dillies (Jun 22 2022 at 10:44):

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 (Jun 22 2022 at 11:04):

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.


Last updated: Dec 20 2023 at 11:08 UTC