Zulip Chat Archive

Stream: new members

Topic: Tactics


view this post on Zulip Brandon B (Apr 26 2020 at 05:19):

I'm not fully grasping what the tactics are doing in this proof. I've written a comment that is how I'm thinking of it on paper but not sure if that's correct.

        theorem even_plus_even2 {a b : nat}
            (h1 : is_even a) (h2 : is_even b) : is_even (a + b) :=
                match h1, h2 with
                    w1, hw1, w2, hw2 := w1 + w2, by rw [hw1, hw2, mul_add]
                end
        /-
        ∃ w1, a = 2 * w1
        w1 : ℕ
        hw1 : a = 2 * w1
        ∃ w2, b = 2 * w2
        w2 : ℕ
        hw2 : b = 2 * w2
        w1 = a/2, w2 = b/2
        w1 + w2 = a/2 + b/2
        a + b = 2 * (w1 + w2)
        -/

view this post on Zulip Mario Carneiro (Apr 26 2020 at 05:35):

This proof looks okay (but you didn't provide a MWE). What error do you get?

view this post on Zulip Mario Carneiro (Apr 26 2020 at 05:37):

Or is the proof correct and you don't understand how it works?

view this post on Zulip Brandon B (Apr 26 2020 at 05:38):

The proof is correct I'm just trying to understand what's going on under the hood

view this post on Zulip Mario Carneiro (Apr 26 2020 at 05:38):

Actually there aren't really any tactics in this proof except rw. The match is pattern matching on h1 and h2, which are existential statements once you unfold the definition of is_even, to produce w1 and hw1 : a = 2 * w1 and similarly for w2

view this post on Zulip Brandon B (Apr 26 2020 at 05:39):

yeah I understand match I just dont fully understand the ,by rw [hw1, hw2, mul_add]

view this post on Zulip Mario Carneiro (Apr 26 2020 at 05:39):

The right hand side is similarly building an existential proof saying w1 + w2 suffices, and so the by rw proof needs to prove a + b = 2 * (w1 + w2)

view this post on Zulip Mario Carneiro (Apr 26 2020 at 05:40):

Then the rewrites respectively change the goal to 2 * w1 + b = 2 * (w1 + w2) and 2 * w1 + 2 * w2 = 2 * (w1 + w2), and the final mul_add rewrites the right hand side to 2 * w1 + 2 * w2 = 2 * w1 + 2 * w2. Since this is true by reflexivity it closes the goal

view this post on Zulip Mario Carneiro (Apr 26 2020 at 05:40):

At least, that's what the lean in my head would do, since that's not an MWE I can't test it

view this post on Zulip Brandon B (Apr 26 2020 at 05:42):

Ohhh that makes sense, thanks!

view this post on Zulip Brandon B (Apr 26 2020 at 05:42):

So rewrite is a substitution rule

view this post on Zulip Frank Dai (Apr 26 2020 at 05:42):

you can also expand by rw [a, b, c] into begin rw a, rw b, rw c, end and step through it

theorem even_plus_even2 {a b : nat}
    (h1 : is_even a) (h2 : is_even b) : is_even (a + b) :=
        match h1, h2 with
            w1, hw1, w2, hw2 := w1 + w2, begin
              rw hw1,
              rw hw2,
              rw mul_add,
              end
        end
 ```

view this post on Zulip Mario Carneiro (Apr 26 2020 at 05:43):

You should be able to step through it even if it is in rw [a,b,c] form

view this post on Zulip Mario Carneiro (Apr 26 2020 at 05:43):

this is one of the special privileges of the rw tactic

view this post on Zulip Brandon B (Apr 26 2020 at 05:46):

How does mul_add know to apply to the right hand side of the equation?

view this post on Zulip Brandon B (Apr 26 2020 at 05:47):

rw is rewriting terms on the LHS but mul_add works on the RHS.

view this post on Zulip Brandon B (Apr 26 2020 at 05:47):

⊢ 2 * w1 + 2 * w2 = 2 * (w1 + w2)

view this post on Zulip Mario Carneiro (Apr 26 2020 at 05:50):

rw will try to find the LHS of the input theorem anywhere in the goal, including on the RHS of the equality if the goal happens to be an equality

view this post on Zulip Mario Carneiro (Apr 26 2020 at 05:51):

If you used mul_add the other way around, that is rw <- mul_add, then it would try to find a * b + a * c somewhere in the goal instead. In this case it would still succeed, rewriting the LHS and resulting in 2 * (w1 + w2) = 2 * (w1 + w2) which is also reflexivity

view this post on Zulip Brandon B (Apr 26 2020 at 05:55):

When we use tactics, what exactly is happening? Is it replacing the tactic command with lambda expressions under-the-hood? Doesn't everything ultimately need to be reduced to lambda expressions for type checking?

view this post on Zulip Bryan Gin-ge Chen (Apr 26 2020 at 06:06):

Did you look at the sources we linked here when you asked this previously?

view this post on Zulip Brandon Brown (Apr 26 2020 at 06:10):

Yes, but I have zero background in functional programming. I know Python and R and Java and C. So a "proof state" doesn't make sense to me in the first place. I am sort of learning how to prove basic things but I'm frustrated I don't know what's going on at the computer science level.

view this post on Zulip Mario Carneiro (Apr 26 2020 at 06:10):

Behind the scenes Lean is building a term which has holes, metavariables, in it

view this post on Zulip Mario Carneiro (Apr 26 2020 at 06:11):

as you use more tactics these holes get filled with more terms with holes until eventually the holes go away

view this post on Zulip Mario Carneiro (Apr 26 2020 at 06:11):

each hole is marked with the type that is expected at that position, and that's the goal state that you see

view this post on Zulip Mario Carneiro (Apr 26 2020 at 06:12):

It's very much like writing term mode proofs using _

view this post on Zulip Brandon Brown (Apr 26 2020 at 06:12):

So in principle there is a way to mechanistically translate a proof written using tactics into a term mode proof?

view this post on Zulip Brandon Brown (Apr 26 2020 at 06:13):

And get one ugly lambda expression at the other end

view this post on Zulip Kenny Lau (Apr 26 2020 at 06:13):

#print

view this post on Zulip Mario Carneiro (Apr 26 2020 at 06:14):

See also the thread here

view this post on Zulip Kenny Lau (Apr 26 2020 at 06:14):

treat tactics as little C++ programs that help you write term mode proofs

view this post on Zulip Brandon Brown (Apr 26 2020 at 06:15):

Ohh, ok #print is exactly what I wanted to know

view this post on Zulip Mario Carneiro (Apr 26 2020 at 06:15):

the lean kernel only knows term proofs, so tactics have to run to produce a term proof before the theorem can be accepted

view this post on Zulip Mario Carneiro (Apr 26 2020 at 06:16):

these proofs are stored and #print recalls them

view this post on Zulip Bryan Gin-ge Chen (Apr 26 2020 at 06:17):

#print is mentioned early on in the Tactics chapter of TPiL.

view this post on Zulip Brandon Brown (Apr 26 2020 at 06:17):

I see - starting to make a lot more sense. I just couldnt understand why there seemed to be two completely different languages in the same language

view this post on Zulip Mario Carneiro (Apr 26 2020 at 06:17):

They call it metaprogramming because you are writing a program (tactic) to build a program (term)

view this post on Zulip Brandon Brown (Apr 26 2020 at 06:22):

Ahh, your answer there about filling holes is very lucid, thanks

view this post on Zulip Brandon Brown (Apr 26 2020 at 06:24):

Thanks for bearing with me - I'm actually a medical doctor just trying to learn more math so I have very little background in all of this

view this post on Zulip Bryan Gin-ge Chen (Apr 26 2020 at 06:29):

Feel free to keep asking questions! There aren't very many introductory sources so most of us have been learning here.


Last updated: May 13 2021 at 06:15 UTC