Zulip Chat Archive

Stream: new members

Topic: ring does not fully work inside exp


view this post on Zulip Eloi (Jul 17 2020 at 17:41):

I have found that the ring tactic does not fully work inside exp. I see that it manages to do something so I wonder if it is possible to improve it to solve this kind of goals?

import data.complex.basic
import data.real.pi
open real
open complex


example (z t: ): (2: ) * pi * I * (z+1) * t  = (2: ) * pi * I * t + 2 * pi * I * z * t:=
begin
  ring,
end

example (z t: ): exp ( (2: ) * pi * I * (z+1) * t ) = exp ( (2: ) * pi * I * t + 2 * pi * I * z * t ):=
  begin
    ring,
   -- ⊢ exp ((2 * t * z + 2 * t) * I * ↑pi) = exp ((2 * z + 2) * t * I * ↑pi)
    sorry
  end

view this post on Zulip Johan Commelin (Jul 17 2020 at 17:42):

I think the easy answer is congr' 1, ring

view this post on Zulip Johan Commelin (Jul 17 2020 at 17:43):

The hard answer would explain why it doesn't work right away...

view this post on Zulip Eloi (Jul 17 2020 at 17:44):

thanks, for now it is enough

view this post on Zulip Johan Commelin (Jul 17 2020 at 17:45):

congr strips away as much as possible from two sides of an =. With congr' n you can tell it to take n steps in stripping things away

view this post on Zulip Alex J. Best (Jul 17 2020 at 17:47):

My guess is that ring picks different variable orderings when trying to normalize the LHS and RHS so they don't end up matching, does that sound plausible to a ring expert ?


Last updated: May 14 2021 at 03:27 UTC