Feedback on some exercises

Stream: lean4

[James Sully]

Hi! I'm working through the exercises from chapter 3 of Theorem Proving in Lean 4.

I've done about a third of them, and I'm looking for some general feedback on style that I might be able to incorporate into later solutions. Would anyone be willing to give me a quick code review? I'd greatly appreciate it. Here are my solutions so far.

In particular I'm looking for feedback on

• code neatness
• making things more idiomatic
• variable naming
• succinctness
• places I can use show, have, suffices to make things more readable - I don't feel like I have a good intuition for how/where to use them, or when to use have vs let

[James Sully]

nitpicks especially welcome

[Eric Wieser]

or when to use have vs let

The general rule is "use have for proofs, use let for data"

[Eric Wieser]

In your code you don't have any data, so you don't need let at all

[James Sully]

Thank you, noted

[Bulhwi Cha]

De Morgan's law 1:

(show ¬p from λ hp => h_n_pOrq ∘ Or.inl <| hp)
(show ¬q from λ hq => h_n_pOrq ∘ Or.inr <| hq)

Suggestion:

(show ¬p from h_n_pOrq ∘ Or.inl)
(show ¬q from h_n_pOrq ∘ Or.inr)

[Bulhwi Cha]

¬(p ∧ q) → ¬p ∨ ¬q (classical):

have ifNotP := show ¬p → ¬p ∨ ¬q from
  λ hnp => Or.inl hnp

Suggestion:

have ifNotP := show ¬p → ¬p ∨ ¬q from Or.inl

[Bulhwi Cha]

(p → q) → (¬p ∨ q) (classical):

(show p  → ¬p ∨ q from λ hp  => Or.inr (hpq hp))
(show ¬p → ¬p ∨ q from λ hnp => Or.inl hnp)

Suggestion:

(show  p → ¬p ∨ q from λ hp => Or.inr (hpq hp))
(show ¬p → ¬p ∨ q from Or.inl)