Zulip Chat Archive

Stream: new members

Topic: Need help with trivial identity


Noob (May 13 2020 at 13:56):

Hi,
Can't figure out how to get p cancelled in the proof of the left side of the iff:

 example : ¬(p  q)  ¬p  ¬q :=
    iff.intro
      (λ h : ¬(p  q),
        λ (hp : p),
        have hpq : p  q, from or.inl hp,
        show ¬p  ¬ q, from false.elim (h hpq))
      (λ hnp, hnq,
        λ hpq,
          or.elim hpq
            (λ hp, hnp hp)
            (λ hq, hnq hq))

Lean complains that the left side has type
¬(p ∨ q) → p → ¬p ∧ ¬q
but is expected to have type
¬(p ∨ q) → ¬p ∧ ¬q
which makes sense.
Could someone give me a hint?

Kenny Lau (May 13 2020 at 13:57):

write down a proof in maths first

Bryan Gin-ge Chen (May 13 2020 at 14:05):

Note that you can solve these by (almost mindlessly) chasing the type errors at underscores. Here are the first few steps which should get you back on the right track:

 example : ¬(p  q)  ¬p  ¬q :=
    iff.intro
      (λ h : ¬(p  q),
        _
      (λ hnp, hnq,
        λ hpq,
          or.elim hpq
            (λ hp, hnp hp)
            (λ hq, hnq hq))
 example : ¬(p  q)  ¬p  ¬q :=
    iff.intro
      (λ h : ¬(p  q),
        and.intro _ _
      (λ hnp, hnq,
        λ hpq,
          or.elim hpq
            (λ hp, hnp hp)
            (λ hq, hnq hq))
 example : ¬(p  q)  ¬p  ¬q :=
    iff.intro
      (λ h : ¬(p  q),
        and.intro (λ hp, _) (λ hq, _))
      (λ hnp, hnq,
        λ hpq,
          or.elim hpq
            (λ hp, hnp hp)
            (λ hq, hnq hq))

etc.

Noob (May 13 2020 at 14:21):

@Bryan Gin-ge Chen, this is extremely helpful and exactly the kind of advice I was looking for. Thanks a lot!

Kevin Buzzard (May 13 2020 at 14:23):

@Noob this video might help. This is what Bryan is referring to when he talks about chasing type errors at underscores. The link points to the start of the term mode proof; the first half of the video is a tactic mode proof.

Noob (May 13 2020 at 14:57):

@Kevin Buzzard, the video is really helpful. The only feature I'm not familiar with (apart from how to use tactics) is the $ operator, but you explain it along the way. I think the term mode is not more intimidating (you need to know less to use it) if you use formatting similar to what you used in the tactics mode.

Noob (May 13 2020 at 15:21):

@Kevin Buzzard, I think having type annotations on hypotheses might make the proof easier to follow for beginners, but maybe it's just my bias as a programmer.


Last updated: Dec 20 2023 at 11:08 UTC