rests-on-unproved

A Lean theorem whose proof reads a declaration that is not proved.

Group: Lean proofs
Runs: On by default
Level: warning
Reads: Every file
Fix: None: a proof is the author's to write

Why

The theorem's own proof may be sound, but it reads a declaration, directly or through others, that takes a proof on trust, as unchecked-proof reports, so what it proves is no more than what that declaration assumes. Names resolve among the constants the project's Lean files declare, through namespaces and open commands; a constant of a library outside them is taken as proved. The finding lists the declarations it reads through.

The fix, as Ur suggests it: prove the declaration it rests on, or prove the theorem without it.

For agents

Before citing a lemma in a Lean proof, check that the lemma is proved, and prove it first if it is not.

Example

Ledger.lean

def balance (entries : List Int) : Int :=
  entries.foldl (· + ·) 0

theorem balance_append (xs ys : List Int) :
    balance (xs ++ ys) = balance xs + balance ys := by
  sorry

Statement.lean

import Ledger

theorem balance_after_deposit (entries : List Int) (amount : Int) :
    balance (entries ++ [amount]) = balance entries + balance [amount] :=
  balance_append entries [amount]

What Ur prints

$ ur lint --rule rests-on-unproved
warning[rests-on-unproved]: theorem `balance_after_deposit` rests on `balance_append`, which uses `sorry`
  --> ./Statement.lean:3:1-5 theorem `balance_after_deposit`
  = step 1: ./Ledger.lean:4:1-6 theorem `balance_append`
  = step 2: ./Ledger.lean:6:3 `sorry`
  = hint: prove the declaration it rests on, or prove the theorem without it
0 clone classes and 1 proof finding in 2 files
Lean proofs: 0 of 2 theorems proved (0%), 1 unproved, 1 resting on unproved ones

Try it in the playground →