# Zulip Chat Archive

## Stream: new members

### Topic: How to move things to the other side of the equation?

#### Daniel Fabian (May 11 2020 at 18:58):

Sorry if this sounds a lot like my question around algebraic transformations. I'm basically struggling and wonder if I'm just approaching it wrong. This is the example. Is there a much better way to write this proof?

```
import tactic
lemma df : (∀ f : ℤ → ℤ, (∀ a b : ℤ, f(2 * a) + 2 * f(b) = f(f(a + b))) → (∀ a b k l, 2 * (f(l - a) - f(l - b)) = f(2 * (b + k)) - f(2 * (a + k)))) :=
begin
intros f h,
intros,
have lhs : f (2 * (a + k)) + 2 * f (l - a) = f (f (k + l)), by { rw h, ring },
have rhs : f (2 * (b + k)) + 2 * f (l - b) = f (f (k + l)), by { rw h, ring },
rw ← lhs at rhs,
apply eq_add_of_sub_eq,
have : 2 * (f (l - a) - f (l - b)) = 2 * f(l - a) - 2 * f(l - b), by rw mul_sub_left_distrib,
rw this,
rw sub_right_comm,
symmetry,
apply eq_sub_of_add_eq,
convert rhs,
ring,
end
```

Up to `rw ← lhs at rhs`

, this is more or less what you'd do on paper. After that it becomes painful and I wonder if there's a better way. I read the whole theorem proving in Lean book and I never found a better.

On paper, you'd just shift the terms from one half of the equation to the other. But the crux is, they aren't rewrites, but completely new separate equations that just happen to be true.

But maybe I'm just doing it wrong trying to use lean as a notebook / CAS when you should only be proving things you've already proved on paper?

#### Jalex Stark (May 11 2020 at 19:09):

First, it took me a while to parse the example. Here's how I would write it:

(I'm looking through the proof now that I understand the statement)

```
lemma df_rewritten
(f : ℤ → ℤ)
(fun_eq1 : ∀ a b,
f(2 * a) + 2 * f b = (f ∘ f) (a + b)
)
(a b k l : ℤ ) :
2 * (f(l - a) - f(l - b)) = f(2 * (b + k)) - f(2 * (a + k)) :=
begin
apply df, assumption,
end
```

#### Kevin Buzzard (May 11 2020 at 19:11):

Theorem proving in Lean doesn't consider things like `ring`

because it sticks to core lean, not mathlib

#### Jalex Stark (May 11 2020 at 19:14):

Kevin did you post in the wrong thread? (or am i missing context? Daniel does use `ring`

and doesn't mention #tpil)

#### Daniel Fabian (May 11 2020 at 19:14):

I did mention #tpil

#### Daniel Fabian (May 11 2020 at 19:14):

sorry for the noob questions, btw

#### Jalex Stark (May 11 2020 at 19:15):

oof okay I should go back to kindergarten and learn to read

#### Jalex Stark (May 11 2020 at 19:15):

Daniel Fabian said:

sorry for the noob questions, btw

You're in the right stream :) people who don't want to think about such questions hang out elsewhere

#### Kevin Buzzard (May 11 2020 at 19:16):

The book you should be reading is the one that we're currently writing :-) This uses lots of mathlib

#### Daniel Fabian (May 11 2020 at 19:16):

got a github repo or something?

#### Kevin Buzzard (May 11 2020 at 19:17):

https://github.com/leanprover-community/mathematics_in_lean

#### Kevin Buzzard (May 11 2020 at 19:17):

The issue you have run into is that we don't have a Groebner basis tactic in Lean, so you have to learn to work around it.

#### Kevin Buzzard (May 11 2020 at 19:18):

In general if you have a bunch of integers, or elements of any commutative ring, and you know a bunch of relations between them, and you want to deduce another relation, then abstractly you're just asking for a proof that a certain element of a polynomial ring is in a certain ideal (the one generated by the relations)

#### Kevin Buzzard (May 11 2020 at 19:19):

The `ring`

tactic does this in the special case that the ideal is $0$.

#### Kevin Buzzard (May 11 2020 at 19:20):

The trick in general is to spot relations of the form `X = f(A,B,C,..)`

and then eliminate `X`

.

#### Alex J. Best (May 11 2020 at 19:20):

What you are doing can be phrased just as a chain of rewrites, but rewrites that rewrite the equality rather than a single atom

```
lemma df : (∀ f : ℤ → ℤ, (∀ a b : ℤ, f(2 * a) + 2 * f(b) = f(f(a + b))) → (∀ a b k l, 2 * (f(l - a) - f(l - b)) = f(2 * (b + k)) - f(2 * (a + k)))) :=
begin
intros f h,
intros,
have lhs : f (2 * (a + k)) + 2 * f (l - a) = f (f (k + l)), by { rw h, ring },
have rhs : f (2 * (b + k)) + 2 * f (l - b) = f (f (k + l)), by { rw h, ring },
rw ← lhs at rhs,
rw eq_sub_iff_add_eq,
rw mul_sub_left_distrib,
rw sub_add_eq_add_sub,
rw sub_eq_iff_eq_add,
rw rhs,
rw add_comm,
end
```

#### Jalex Stark (May 11 2020 at 19:25):

I like @Alex J. Best's answer better, but here is my attempt at golfing it:

```
import tactic
lemma df_rewritten
(f : ℤ → ℤ)
(fun_eq1 : ∀ a b,
f(2 * a) + 2 * f b = (f ∘ f) (a + b)
)
(a b k l : ℤ ) :
2 * (f(l - a) - f(l - b)) = f(2 * (b + k)) - f(2 * (a + k)) :=
begin
have key : f (2 * (a + k)) + 2 * f (l - a)
= f (2 * (b + k)) + 2 * f (l - b),
{ transitivity f (f (k + l));
{rw fun_eq1, ring},},
rw (eq_sub_of_add_eq key),
ring,
end
```

#### Daniel Fabian (May 11 2020 at 19:25):

Thanks both of you, I'll. Work through the mathlib tutorial then and read the new book.

#### Kevin Buzzard (May 11 2020 at 19:25):

```
import tactic
lemma df (f : ℤ → ℤ) (h : ∀ a b : ℤ, f(2 * a) + 2 * f(b) = f(f(a + b)))
(a b k l : ℤ) : 2 * (f(l - a) - f(l - b)) = f(2 * (b + k)) - f(2 * (a + k)) :=
begin
have h' : ∀ a b : ℤ, f(2 * a) = f(f(a+b)) - 2*f(b),
{ intros A B, rw (h A B).symm, ring},
rw h' (a + k) (l - a),
rw h' (b + k) (l - b),
rw (show (b + k + (l - b)) = k + l, by ring),
rw (show (a + k + (l - a)) = k + l, by ring),
ring,
end
```

I don't use anything apart from `ring`

and eliminating variables.

#### Daniel Fabian (May 11 2020 at 19:30):

Alright, I'll have to get used to that, thanks for the help so far. After a few more times struggling I get the hang of it. And if it goes well, I can give a talk at MSRC ;-). Hopefully we get some more people.

#### Daniel Fabian (May 11 2020 at 19:35):

I also notice you rewrite not by hypotheses but by ad-hoc terms, I need to start doing that, too.

#### Kevin Buzzard (May 11 2020 at 19:36):

I was a bit annoyed that I couldn't finish earlier but I couldn't find a tactic which would simpify x+k+(l-x) to k+l

#### Kevin Buzzard (May 11 2020 at 19:36):

What is MSRC?

#### Daniel Fabian (May 11 2020 at 19:40):

Microsoft Research Cambridge. We often invite speakers but also often hold our own seminars and the likes. I gave a talk about F* not too long ago. At that time, I had tried to use Lean to verify Okasaki's Red-Black-tree insertion algorithm and failed miserably.

It really doesn't do too well for proving properties about programs, the level of automation is just too bad, yet.

So I figured, I'd give Lean another go, this time for math instead.

#### Kevin Buzzard (May 11 2020 at 19:41):

maths automation has been seriously worked on in the past, basically because of the needs of various users

#### Kevin Buzzard (May 11 2020 at 19:41):

You should invite Bhavik and Ed to give talks :-)

#### Patrick Massot (May 11 2020 at 19:42):

```
lemma df : (∀ f : ℤ → ℤ, (∀ a b : ℤ, f(2 * a) + 2 * f(b) = f(f(a + b))) → (∀ a b k l, 2 * (f(l - a) - f(l - b)) = f(2 * (b + k)) - f(2 * (a + k)))) :=
begin
intros f h a b k l,
have lhs : f (2 * (a + k)) + 2 * f (l - a) = f (f (k + l)), by { rw h, ring },
have rhs : f (2 * (b + k)) + 2 * f (l - b) = f (f (k + l)), by { rw h, ring },
linarith,
end
```

#### Patrick Massot (May 11 2020 at 19:42):

I'd be curious to know what you would write on paper. I'm pretty sure you can do the same in Lean.

#### Daniel Fabian (May 11 2020 at 19:46):

why that's neat... The linarith looks really great. This is definitely a lot more powerful than #tpil.

#### Patrick Massot (May 11 2020 at 19:49):

The proof reads: Here are what we want to deduce using `h`

, and then you just stir until cooked (I have no idea how to say that in idiomatic English).

#### Daniel Fabian (May 11 2020 at 19:51):

but that's really what a lot of proving is about... State something useful, rewrite, massage terms for a bit, state something new, massage again, rewrite, done.

#### Daniel Fabian (May 11 2020 at 19:51):

And if the machine can do the massaging, that's just neat

#### Kevin Buzzard (May 11 2020 at 20:07):

Wow so linarith does equalities as well as inequalities?

#### Patrick Massot (May 11 2020 at 20:35):

Daniel Fabian said:

but that's really what a lot of proving is about... State something useful, rewrite, massage terms for a bit, state something new, massage again, rewrite, done.

And if the machine can do the massaging, that's just neat

Yes, this is exactly what I meant

Last updated: May 15 2021 at 23:13 UTC