Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Daniel Fabian (May 11 2020 at 19:14):

I did mention #tpil

view this post on Zulip Daniel Fabian (May 11 2020 at 19:14):

sorry for the noob questions, btw

view this post on Zulip Jalex Stark (May 11 2020 at 19:15):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Daniel Fabian (May 11 2020 at 19:16):

got a github repo or something?

view this post on Zulip Kevin Buzzard (May 11 2020 at 19:17):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (May 11 2020 at 19:19):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 11 2020 at 19:36):

What is MSRC?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 11 2020 at 19:41):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Daniel Fabian (May 11 2020 at 19:51):

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

view this post on Zulip Kevin Buzzard (May 11 2020 at 20:07):

Wow so linarith does equalities as well as inequalities?

view this post on Zulip 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