how to prove simple stuffs

Stream: maths

[Truong Nguyen]

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]

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]

import tactic.norm_num

example : 2 * 4 < 9 := by norm_num

[Truong Nguyen]

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]

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]

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

[Kevin Buzzard]

This is all explained in Theorem Proving In Lean.

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

import tactic.interactive

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

These tactics are not explained in TPIL though.

[Truong Nguyen]

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