Problem with linter.unusedVariables warnings in a proof

Stream: new members

[Kuba]

Hi! I am new to lean4 and wanted to start by doing some of the exercises from #tpil.

I am currently working my way through chapter 3 and I got stuck a bit on the first example requring classical reasoning:

(p → q ∨ r) → ((p → q) ∨ (p → r))

All the proofs that I was able to come up with end up causing a linter.unusedVariables warning. Here are two examples:
Proof 1 (unused variable in line 4):

example : (p → q ∨ r) → (p → q) ∨ (p → r) :=
    λ h : p → q ∨ r => Or.elim (em q)
        (λ hq : q => Or.inl
            λ hp : p => hq)
        (λ hnq : ¬q => Or.inr
            λ hp : p => Or.elim (h hp)
                (λ hq : q => absurd hq hnq)
                (λ hr : r => hr))

Proof 2 (unused variable in line 6):

example : (p → q ∨ r) → (p → q) ∨ (p → r) :=
    λ h : p → q ∨ r => Or.elim (em (p → q))
        (λ hpq : p → q => Or.inl hpq)
        (λ hnpq : ¬(p → q) => Or.inr
            (λ hp : p => Or.elim (h hp)
                (λ hq : q => absurd (λ hp : p => hq) hnpq)
                (λ hr : r => hr)))

The issue seems to occur whenever I construct a proof of p → q from the proof of q. A similar issue occurs when trying to prove the following simpler example (one of the examples described in the book):

example : p → q → p :=
    λ hp : p => λ hq : q => hp

My questions are:

• Are linter warnings (the unusedVariables one in particular) telling us anything about the correctness of the proof or are they only about coding style?
• How much should I worry about them?
• Is it always possible to avoid them? In particular, can I prove any theorem without introducing unused variables?
• Can I prove the examples above without introducing any unused variables? How?

[Jireh Loreaux]

It's not an issue of correctness, only code style (although sometimes it can help you catch errors when defining things). You can ignore them and get the linter to be quiet by adding an underscore to the start of the variable name.

[Notification Bot]

2 messages were moved here from #new members > Lean as a way to learn proving by Kuba.

[Bulhwi Cha]

open Classical

example : (p → q ∨ r) → (p → q) ∨ (p → r) :=
    λ h : p → q ∨ r => Or.elim (em q)
        (λ hq : q => Or.inl
            λ _hp : p => hq) -- use `_hp` instead of `hp`
        (λ hnq : ¬q => Or.inr
            λ hp : p => Or.elim (h hp)
                (λ hq : q => absurd hq hnq)
                (λ hr : r => hr))

example : (p → q ∨ r) → (p → q) ∨ (p → r) :=
    λ h : p → q ∨ r => Or.elim (em (p → q))
        (λ hpq : p → q => Or.inl hpq)
        (λ hnpq : ¬(p → q) => Or.inr
            (λ hp : p => Or.elim (h hp)
                (λ hq : q => absurd (λ _ : p => hq) hnpq) -- use `_` instead of `hp`
                (λ hr : r => hr)))