Stream: new members
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
Johan Commelin (Jul 17 2020 at 17:42):
I think the easy answer is
congr' 1, ring
Johan Commelin (Jul 17 2020 at 17:43):
The hard answer would explain why it doesn't work right away...
Eloi (Jul 17 2020 at 17:44):
thanks, for now it is enough
Johan Commelin (Jul 17 2020 at 17:45):
congr strips away as much as possible from two sides of an
congr' n you can tell it to take
n steps in stripping things away
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