# Zulip Chat Archive

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