How to do algebraic transformations?

Stream: new members

[Daniel Fabian]

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]

#mwe

[Patrick Massot]

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

[Chris Hughes]

You can use calc or a sequence of have statements.

[Mario Carneiro]

you can also rw at f_lin or simp at f_lin

[Mario Carneiro]

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

[Patrick Massot]

specialize is also useful here

[Daniel Fabian]

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]

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]

@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]

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]

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]

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]

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]

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

[Alex J. Best]

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]

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]

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