Is there code to apply ring in an equation

Stream: Is there code for X?

[Shi You]

example (h1: x - 1 = 1 - x): x = 1 :=
begin
  have h2 : x = 1 - x + 1, from by exact eq_add_of_sub_eq h1,
  have h3 : x = 2 - x, from by sorry,

In the code above, I am looking for a tactic or a combination of tactics to get h3 checked.

[Kevin Buzzard]

Can you post fully working code? The way to fill in the sorry might depend on the type of x. If I post your code into VS Code I get an error about not knowing what x is. #mwe

[Kevin Buzzard]

if you want a guess, try have h3 : x = 2 - x, convert h2, ring,

[Kevin Buzzard]

But linarith might just solve this goal instantly without h2 or h3, depending on the type of x.

[Kevin Buzzard]

or maybe omega. I need more clues.

[Shi You]

Here is the full code

example (h1: x - 1 = 1 - x): x = 1 :=
begin
  have h2 : x = 1 - x + 1, from by exact eq_add_of_sub_eq h1,
  have h3 : x = 2 - x, from by rw [h2, ring],
  have h4 : 2 * x = 2, from by sorry,
  show x = 1, from sorry
end

[Kevin Buzzard]

That's not the full code because if I post that into VS Code I get an error saying that Lean doesn't know what x is. Read this link #mwe

[Shi You]

x is rational

[Shi You]

import data.rat.basic
import tactic.ring

variable (x : ℚ)

[Kevin Buzzard]

Then my guess earlier works, right?

[Shi You]

Yes, thx

[Kevin Buzzard]

ring can only prove results of the form X = Y when X and Y simplify to the same thing. It can't prove results of the form "if f(A,B)=0 then g(A,B)=0". Here you're lucky that we can use convert.

[Shi You]

what about checking h4 from h3. I guess there should be a tactic handling equation manipulation.

[Kevin Buzzard]

linarith proves the main goal immediately, you don't need any of this stuff

[Kevin Buzzard]

It might also prove your subgoals

[Kevin Buzzard]

I'm not at lean right now but my guess is have h3 : x = 2 - x, conv_lhs {rw h2}, ring would also work

[Shi You]

Thx, that's very helpful

[Kevin Buzzard]

If linarith doesn't give you h4 from h3 then you could rewrite the theorem that says 2*x=x+x -- you can look up its name with library_search. After you've rewritten that, you can use library_search again to deduce x+x=2 from x=2-x, this is bound to be a special case of a result in the library

[Shi You]

It checks everything indeed