## Stream: new members

### Topic: Tactics

#### 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)
-/


#### Mario Carneiro (Apr 26 2020 at 05:35):

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

#### Mario Carneiro (Apr 26 2020 at 05:37):

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

#### 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

#### 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

#### Brandon B (Apr 26 2020 at 05:39):

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

#### 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)

#### 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

#### 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

#### Brandon B (Apr 26 2020 at 05:42):

Ohhh that makes sense, thanks!

#### Brandon B (Apr 26 2020 at 05:42):

So rewrite is a substitution rule

#### 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,
end⟩
end



#### 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

#### Mario Carneiro (Apr 26 2020 at 05:43):

this is one of the special privileges of the rw tactic

#### Brandon B (Apr 26 2020 at 05:46):

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

#### Brandon B (Apr 26 2020 at 05:47):

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

#### Brandon B (Apr 26 2020 at 05:47):

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

#### 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

#### 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

#### 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?

#### Bryan Gin-ge Chen (Apr 26 2020 at 06:06):

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

#### 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.

#### Mario Carneiro (Apr 26 2020 at 06:10):

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

#### 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

#### 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

#### Mario Carneiro (Apr 26 2020 at 06:12):

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

#### 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?

#### Brandon Brown (Apr 26 2020 at 06:13):

And get one ugly lambda expression at the other end

#### Kenny Lau (Apr 26 2020 at 06:13):

#print

#### Kenny Lau (Apr 26 2020 at 06:14):

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

#### Brandon Brown (Apr 26 2020 at 06:15):

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

#### 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

#### Mario Carneiro (Apr 26 2020 at 06:16):

these proofs are stored and #print recalls them

#### Bryan Gin-ge Chen (Apr 26 2020 at 06:17):

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

#### 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

#### Mario Carneiro (Apr 26 2020 at 06:17):

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