## Stream: maths

### Topic: how to prove simple stuffs

#### Truong Nguyen (Apr 19 2019 at 19:27):

Hi everyone,
I am quite new to lean, I want to prove some stuff like these:
3 < 7,
2 * 4 < 9

or some other logical statement:
p /\ q <-> q /\ p,
or
p /\ q -> p

Do you know a good way to prove these stuffs?

#### Kevin Buzzard (Apr 19 2019 at 19:27):

For numerical stuff, you can use norm_num. For logic, you should read Theorem Proving In Lean, which covers all this stuff in great detail.

#### Kevin Buzzard (Apr 19 2019 at 19:28):

import tactic.norm_num

example : 2 * 4 < 9 := by norm_num


#### Truong Nguyen (Apr 19 2019 at 19:35):

Thanks, I read the Theorem Proving in Lean. So for logical statement, we have to do it manually, by applying: iff.mp, iff.mpr and so on.
No, faster way, right?

#### Kevin Buzzard (Apr 19 2019 at 19:36):

There are super-short ways to do it in term mode, and super-clear ways to do it in tactic mode. But to understand what's going on, you have to read Theorem Proving In Lean.

#### Kevin Buzzard (Apr 19 2019 at 19:37):

example (p q : Prop) : p ∧ q ↔ q ∧ p := ⟨λ ⟨hp, hq⟩, ⟨hq, hp⟩, λ ⟨hq, hp⟩, ⟨hp, hq⟩⟩


#### Kevin Buzzard (Apr 19 2019 at 19:37):

This is all explained in Theorem Proving In Lean.

#### Kevin Buzzard (Apr 19 2019 at 19:39):

example (p q : Prop) : p ∧ q ↔ q ∧ p :=
begin
split,
{ intro hpq,
cases hpq with hp hq,
split,
exact hq,
exact hp
},
{ intro hqp,
cases hqp with hq hp,
split,
exact hp,
exact hq
}
end


This is also all explained in Theorem Proving In Lean. They spend a lot of time on basic logic stuff like this!

#### Kevin Buzzard (Apr 19 2019 at 19:41):

Chapter 5 is on tactic mode and in my mind tactic mode is the best place to start, although I have a more mathematical background than the computer science users of the software, who prefer term mode.

#### Patrick Massot (Apr 19 2019 at 19:54):

I'm not sure I understand the question. There are magic tactic that will prove such a goal in one line, but this won't teach you much

#### Kevin Buzzard (Apr 19 2019 at 19:54):

Oh yeah that's true; you can solve it all using heavy machinery :D

#### Kevin Buzzard (Apr 19 2019 at 19:55):

import tactic.interactive

example (p q : Prop) : p ∧ q ↔ q ∧ p := by tauto


These tactics are not explained in TPIL though.

#### Truong Nguyen (Apr 20 2019 at 16:26):

Thank you,
I know the way that is presented in chapter 5. It is useful to know 'tauto'.

Last updated: May 11 2021 at 15:12 UTC