leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.64k stars 416 forks source link

cases/induction does not connect reverted variables in info tree #2873

Open sven-manthe opened 11 months ago

sven-manthe commented 11 months ago

Prerequisites

Description

In some cases, the linter.unusedVariables yields false positives for variables used only in inductions.

Context

This was discussed in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Possible.20linter.2EunusedVariables.20bug

Steps to Reproduce

example (P : Unit → Prop) (H : P () → True) (x : Unit) (h : P x) : True := by
  let h' := h
  cases x
  exact H h'

Expected behavior: No warning occurs.

Actual behavior: The message "unused variable h' [linter.unusedVariables]" is shown.

Versions

Lean (version 4.3.0-rc1, commit baa4b68a7192, Release) Manjaro Linux 23.0

Kha commented 11 months ago

Must be a general info tree issue image

Kha commented 11 months ago

I think we're still missing a tactic version of #1396

Seasawher commented 11 months ago

I have encountered a similar false positive warning.

This is the MWE to reproduce the bug.

variable (α : Type)

def sample (n : Nat) : Nat :=
  match h : n with
  | 0 => 0
  | m + 1 => m + sample (m / 2)
  decreasing_by
    simp [h]
    simp_wf
    exact Nat.lt_of_le_of_lt (Nat.div_le_self _ _) (Nat.lt_succ_self _)

related : https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/False.20Positive.20Warning.3A.20.60linter.2EunusedVariables.60

kim-em commented 11 months ago

@Seasawher, I think this is an independent issue, that nothing is checking for usages in a decreasing_by clause. Could you open your example as a separate issue?

Seasawher commented 11 months ago

done #2920