Unused arguments and by_cases

Stream: mathlib4

[Mario Carneiro]

that's a bug in the implementation of by_cases

[Yury G. Kudryashov]

I see that by_cases is implemented as dite. I think that if h : p x then (code using h) else (code not using h) in Prop context should report unused variable too.

[Kevin Buzzard]

Well then how the heck am I supposed to prove it without writing noisy code?

[Yury G. Kudryashov]

Just use the negative branch of the argument.

[Notification Bot]

4 messages were moved here from #mathlib4 > Call for help: technical/ organisational debt by Yury G. Kudryashov.

[Yury G. Kudryashov]

The messages above were replies to this message:
Yury G. Kudryashov said:

32. Better support for by_cases (and may be some cases - not sure) in the "unused *" linters. If I run by_cases h : _, but one of the branches doesn't use h, then h is unused. For rcases, see src#iteratedDerivWithin_const_add (going to be fixed in #24227): the 2nd branch doesn't use hxs, but this hxs` isn't marked as unused.

[Mario Carneiro]

Yury G. Kudryashov said:

I see that by_cases is implemented as dite. I think that if h : p x then (code using h) else (code not using h) in Prop context should report unused variable too.

Neither of these are giving me unused variable warnings:

theorem foo (p : Nat → Bool) (h0 : p 0) (x : Nat) : ∃ x, p x :=
  if h : p x then ⟨x, h⟩ else ⟨_, h0⟩

theorem foo' (p : Nat → Bool) (h0 : p 0) (x : Nat) : ∃ x, p x := by
  by_cases h : p x
  · exact ⟨x, h⟩
  · exact ⟨_, h0⟩

I'm testing on 4.19.0-rc3, which I think is the latest version. There was another report about a recent regression on unused variable warnings which could be related?

[Mario Carneiro]

At least the version of the unused variable warning that I wrote is designed to handle this case - if you have multiple variables declared by the same syntax then if any of them is used the unused variable warning on it is suppressed

[Mario Carneiro]

it's been rewritten at least once since then though, and it's possible that some correctness was traded for efficiency

[Yury G. Kudryashov]

This is not a recent regression. This bug was there for quite some time.

[Mario Carneiro]

Can you give a reproduction? As I mentioned, the obvious thing is not a reproducer

[Yury G. Kudryashov]

In what sense your examples aren't reproducers? They don't mark h as unused while they should.

[Yury G. Kudryashov]

I found our previous discussion of this topic: #lean4 > Unused linter with `by_cases`

[Mario Carneiro]

wait, the complaint is that the linter doesn't fire? As I said, this is by design; it would make no sense to call h unused here because it is used and if you change the name of the variable binder then the proof breaks

[Mario Carneiro]

Reading the other thread, the issue isn't so much that h is unused as the whole by_cases is unused (in the sense of the "tactic does nothing" lint)

[Mario Carneiro]

I think this should be done by an entirely different tactic / linter than the unused variables linter

[Yury G. Kudryashov]

I won't enter the argument "should it be a part of the existing linter or a new one?" Let me rephrase my request as "add a linter that catches this anti-pattern".

[Yury G. Kudryashov]

BTW, this is definitely out of scope of the "tactic does nothing" lint, because the call to by_cases modifies the goal. It's closer to "unused have" (but that's not it, because it's not a have or let).

[Jz Pan]

It is just "suboptimal proof"

[Yury G. Kudryashov]

All the "unused ..." linters check for suboptimal proofs.

[Yury G. Kudryashov]

E.g., if one of your assumptions is used in the unneeded branch only, then it's actually an unneeded assumption.

[Robin Arnez]

Well there are reasons for why one might intentionally have it unused in one of the branches (that is, when constructing data), e.g.:

def toFin3? (x : Nat) : Option (Fin 3) :=
  if h : x < 3 then some ⟨x, h⟩ else none

def inverse [Nonempty α] (f : α → β) : β → α := by
  intro x
  by_cases h : ∃ y, f y = x
  · exact h.choose
  · exact Classical.ofNonempty

For Prop goals I would say the tactic is more at fault then the variable (you can also omit the variable name but that won't change whether the by_cases is unused).

[Ruben Van de Velde]

Yes, but Yury explicitly said "in Prop context"

[Kevin Buzzard]

The point (which took me a while to understand) is that if if h : P then <proof using h> else <proof not using h> can always be replaced by <proof not using h>