## Stream: new members

### Topic: ring does not fully work inside exp

#### 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 =. With 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