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: Dec 20 2023 at 11:08 UTC