Proof of not_not_em

Stream: new members

[newptcai]

I saw the following code in Lean

theorem not_not_em (a : Prop) : ¬¬(a ∨ ¬a) :=
  fun h => h (Or.inr (h ∘ Or.inl))

I am confused how can h ∘ Or.inl produce ¬a, which is expected here.

[Niels Voss]

¬a means the same as a -> False. h has type ¬(a ∨ ¬a), which means (a ∨ ¬a) -> False.
h ∘ Or.inl is a function which takes in a proof that a is true, applies Or.inl to get a proof that a ∨ ¬a is true, and then uses h to get a proof of False.
Here's a less concise version of the proof:

theorem not_not_em (a : Prop) : ¬¬(a ∨ ¬a) :=
  fun h : a ∨ ¬a → False =>
    have h₁ : a → False := λ ha => h (Or.inl ha) -- This is the same as `h ∘ Or.inl`
    have h₂ : a ∨ ¬a := Or.inr h₁
    show False from h h₂