Zulip Chat Archive

Stream: new members

Topic: How to prove a conditional?

debord (Jan 20 2023 at 03:22):

Hello. I am a noobie mathematician and an even bigger noobie with Lean. I've managed to do all the exercises in the 'Propositions and Proofs' chapter in 'Proving Theorems with Lean 4', apart from the ones that have conditionals in their conclusions. For example

example : (p  q  r)  ((p  q)  (p  r)) :=
  λ hpqr : p  q  r => byCases
    (λ hp : p =>
      have hqr : q  r := hpqr hp
      Or.elim hqr
        (λ hq : q =>
          /- I wish I could use "hp hq" here but I seem to be confused about how lambda works.-/)
        (λ hr : r =>
          /- "hp hr" here I feel like should mean assuming p we can prove q ∨ r, and if r is true then p → r is true. Then I could use Or.intro to prove the final statement.-/))
    (λ hnp : ¬p =>

is my current best attempt at one of them. Lambda's are explained as a kind of "conditional introduction" in the text, and as with the other introduction rules I would think you could then prove a conditional with it, but that seems not to be the case, or at least I'm thinking about it wrongly. Could I have at least some hint to what I should be doing to complete these?
I'm also having a very tough time figuring out how to prove the simple ¬(p → q) → p. ¬(p → q) is equivalent to (p → q) → False, and I certainly can see informally why ¬(p → q) → p is the case, ¬(p → q) being true means that p is true while q is false, so therefore p is true, but I am having a hard time figuring out how to articulate this notion of conditionals in lean. What am I missing?
Thanks for your time.

Bulhwi Cha (Jan 20 2023 at 04:45):

Can you prove the following examples?

open Classical
variable (p q : Prop)

example (hp : p) (hq : q) : p  q :=

example (hnp : ¬p) : p  q :=

example : ¬(p  q)  p :=
  λ hnpq : ¬(p  q) => byCases
    (λ hp : p => sorry)
    (λ hnp : ¬p =>
      have hpq : p  q := sorry


debord (Jan 20 2023 at 06:21):

Okay I think I'm starting to see it now then. The way to do what I'm trying to do is to make a proof that the assumption is false and then use absurd to prove any arbitrary q including whatever my goal is. This logic was pretty shocking to me but I suppose it is a natural consequence of the principle of explosion. I need more practice to get used to it, thank you for the demonstration Bulhwi.

Last updated: Dec 20 2023 at 11:08 UTC