Zulip Chat Archive

Stream: new members

Topic: How to do algebraic transformations?


Daniel Fabian (May 10 2020 at 16:57):

Is there a way to do, what you might call "forward reasoning" in lean? The idea being that maybe I a bunch of fairly complicated expressions and I'd like to manipulate them a bit before they become an instance of the goal.

I've got this state as an example:

f :   ,
h :  (a b : ), f (2 * a) + 2 * f b = f (f (a + b)),
symm :  (a b k l : ), f (2 * (a + k)) + 2 * f (l - a) = f (2 * (b + k)) + 2 * f (l - b),
diff :  (k l : ), 2 * (f k - f l) = f (2 * k) - f (2 * l),
h_f :  (k : ), 2 * f k = f (2 * k) + f 0,
f_lin :  (k : ), 2 * f k = 2 * k * (f 1 - f 0) + f 0,
f₀ : f 0 = 0,
k : 
 f k = k * f 1

f_lin here is in a bad shape, we need to rewrite by f₀, then divide by two and only then does it become a valid instance.

Somehow I find it really hard to manipulate equations, or more precisely, I often find that I'd like to do a bunch of algebraic transforms before things become an instance of the goal.

If I were to do "backwards reasoning", i.e. keep making the goal more and more complicated until it becomes an instance of the hypothesis, then it's quite convenient, but the expressions get worse and worse as opposed to better.

Am I missing something very basic here?

Patrick Massot (May 10 2020 at 17:09):

#mwe

Patrick Massot (May 10 2020 at 17:10):

We can show you how to do what you want, but only with a #mwe

Chris Hughes (May 10 2020 at 17:10):

You can use calc or a sequence of have statements.

Mario Carneiro (May 10 2020 at 17:12):

you can also rw at f_lin or simp at f_lin

Mario Carneiro (May 10 2020 at 17:13):

although you probably want to pick the relevant value for k in the assumption first

Patrick Massot (May 10 2020 at 17:17):

specialize is also useful here

Daniel Fabian (May 10 2020 at 17:18):

here's the example and the proof:

example : ( f :   , ( a b : , f(2 * a) + 2 * f(b) = f(f(a + b)))  ( c : , f c = 0)) :=
begin
    intros f h,
    have f_lin :  k, 2 * f(k) = 2 * k * (f(1) - f(0)) + f(0), sorry,
    have f₀ : f(0) = 0, sorry,
    have f_lin_simp :  k, f(k) = k * f(1),
    {
        intro,
        have f_lin_k := f_lin k,
        rw f₀ at f_lin_k,
        ring at f_lin_k,
        rw sub_zero at f_lin_k,
        apply eq_of_mul_eq_mul_left (show (2 : )  0, by norm_num),
        rwa  mul_assoc,
    },
    sorry
end

Daniel Fabian (May 10 2020 at 17:20):

so here I end up using the at pretty much all the time until only at the very end it becomes a valid instance.

I'm just a bit surprised, because when I do a distinction by cases, generally the goal gets simpler. And in case of algebraic transforms it feels like I have to make the goal more complicated or aim rewrites with at.

Daniel Fabian (May 10 2020 at 17:22):

@Chris Hughes how would I use a sequence of calc? From what I understand it's a chain of equivalences as opposed to a chain of manipulations of the same equation.

Daniel Fabian (May 10 2020 at 17:24):

I think what I'd like to do is effectively change the goal for a hypothesis for a bit until I've modified it and then continue the proof.

Mario Carneiro (May 10 2020 at 17:25):

example : ( f :   , ( a b : , f(2 * a) + 2 * f(b) = f(f(a + b)))  ( c : , f c = 0)) :=
begin
    intros f h,
    have f_lin :  k, 2 * f(k) = 2 * k * (f(1) - f(0)) + f(0), sorry,
    have f₀ : f(0) = 0, sorry,
    simp [f₀, mul_assoc, domain.mul_left_inj (show (2 : )  0, by norm_num)] at f_lin,
    sorry
end

Mario Carneiro (May 10 2020 at 17:29):

I guess I'm still not sure about your question. It's okay to use a bunch of at hyp theorems in a row, but it's definitely preferable to simplify a complicated hypothesis to match a simple goal rather than complexify the goal to match the hypothesis (because there are many ways to complexify you will have to give more information in this second approach)

Patrick Massot (May 10 2020 at 17:35):

If you want the proof to be readable then you can also write something like:

example :  f :   , ( a b : , f(2 * a) + 2 * f(b) = f(f(a + b)))  ( c : , f c = 0) :=
begin
    intros f h,
    have f_lin :  k, 2 * f(k) = 2 * k * (f(1) - f(0)) + f(0), sorry,
    have f₀ : f(0) = 0, sorry,
    replace f_lin :  k, 2 * f(k) = 2 * (k * f(1)),
      by simpa [f₀, mul_assoc] using f_lin,
    replace f_lin :  k, f(k) = k * f(1),
      from λ k, eq_of_mul_eq_mul_left (show (2 : )  0, by norm_num) (f_lin k),
    sorry
end

Patrick Massot (May 10 2020 at 17:36):

Isn't it he same olympiad problem that was already formalized by Kevin and Manuel last summer?

Alex J. Best (May 10 2020 at 17:36):

I'm also not sure exactly what you are looking for but here's a slight variation:

    have f_lin_simp :  k, f(k) = k * f(1),
    {
        intro,
        apply eq_of_mul_eq_mul_left (show (2 : )  0, by norm_num),
        convert f_lin k,
        simp [f₀, mul_assoc],
    },

using convert here to change the goal to "the difference" between the given hypothesis and the goal, then you end up in a state where you just need to simplify the goal, rather than hypotheses.

Daniel Fabian (May 10 2020 at 17:38):

That's possible. I don't really care about formalizing it, but rather figured it might be a nice tutorial project for me to learn lean ;-). Also, lean is definitely better at not making mistakes in rewriting terms than paper :P.

My goal is to use lean to prove various things from the assumption of the Olympiad and explore, not to prove something I know already.

Daniel Fabian (May 10 2020 at 17:39):

@Alex J. Best that's I think very much what I was looking for, thanks!


Last updated: Dec 20 2023 at 11:08 UTC