How to move things to the other side of the equation?

Stream: new members

[Daniel Fabian]

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]

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]

Theorem proving in Lean doesn't consider things like ring because it sticks to core lean, not mathlib

[Jalex Stark]

Kevin did you post in the wrong thread? (or am i missing context? Daniel does use ring and doesn't mention #tpil)

[Daniel Fabian]

I did mention #tpil

[Daniel Fabian]

sorry for the noob questions, btw

[Jalex Stark]

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

[Jalex Stark]

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]

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

[Daniel Fabian]

got a github repo or something?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Alex J. Best]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

What is MSRC?

[Daniel Fabian]

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]

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

[Kevin Buzzard]

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

[Patrick Massot]

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]

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]

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

[Patrick Massot]

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]

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]

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

[Kevin Buzzard]

Wow so linarith does equalities as well as inequalities?

[Patrick Massot]

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