Zulip Chat Archive

Stream: maths

Topic: how to prove simple stuffs


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 19 2019 at 19:28):

import tactic.norm_num

example : 2 * 4 < 9 := by norm_num

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 19 2019 at 19:37):

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

view this post on Zulip Kevin Buzzard (Apr 19 2019 at 19:37):

This is all explained in Theorem Proving In Lean.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 19 2019 at 19:54):

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

view this post on Zulip 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.

view this post on Zulip 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