# Zulip Chat Archive

## 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, rw mul_add, 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`

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

See also the thread here

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

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

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

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

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