Zulip Chat Archive

Stream: new members

Topic: How to do it proprely in lean


T.X. XIA (Mar 02 2022 at 07:10):

Hi. I'm new to lean and am recently reading Theorem Proving in Lean 4.

I was trying to solve the problem in the exercise of Quantifiers and Equality and ended up using three 'byContradiction' in a row.
So I'm wondering is it the right way to do it?

And by the way, I would like to know how can we check out the standard library so as to learn how to use it? I know that there is a manual but, for example, when I wanted to look at what's in the Classical, I couldn't find it in the manual or in VS Code.

example : ( x, p x)  ¬ ( x, ¬ p x) :=
  Iff.intro
    (fun x, hpx h => h x hpx)
    (fun h => byContradiction (fun hne : ¬( x, p x) =>
      have := (fun x => byContradiction (fun hh : ¬¬ p x =>
        have := byContradiction (fun hnpx : ¬ p x => hh hnpx)
        show False from hne x, this
        ))
      absurd this h
    ))

Last updated: Dec 20 2023 at 11:08 UTC