Tactics can modify the elaborated types of theorems with let rec

[alexb-harmonic]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Tactics within a proof can change the type of a theorem with let rec in.

Steps to Reproduce

import Mathlib

theorem ohno :
  ¬ ((let rec recur (n : Nat) : List Nat :=
      match n with
      | 0 => [1]
      | (Nat.succ n) => recur n
    recur 0 = [1])) ∧ True := by
        -- sorry
        refine Decidable.byContradiction fun h_contra => ?_
        apply h_contra
        constructor
        intro h
        apply_mod_cast h_contra
        any_goals tauto
        simp

theorem a : False := by
  have := ohno
  simp [ohno.recur] at this

Expected behavior: swapping the "proof" of ohno for "sorry" should not change the type of "ohno",

Actual behavior: when "ohno" is sorried out the type includes ohno.recur (and the following theorem is provable (ie ohno is false)). But when it is not sorried out Lean accepts the proof, which is fairly unintuitive.

on latest, I couldn't get rid of the Mathlib import easily but hopefully this is clear enough

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

It seems rather strange to put a let rec into a type of a theorem. I assume only because humans don't do that doesn't mean we don't have to worry about it…

[alexb-harmonic]

@nomeata I'd be perfectly happy if using let rec in a theorem caused an error, though I am a little worried that the root cause here is something more widespread (do other features make use of lifting mvars that can be assigned later on in elaboration?).

[nomeata]

I just had a brief look. Here is a clue:

/--
error: Failed: `fail` tactic was invoked
⊢ (fun recur => recur 0 = [1]) ?m.1
-/
#guard_msgs in
theorem ohno :
    ((let rec recur (n : Nat) : List Nat :=
      match n with
      | 0 => [1]
      | (Nat.succ n) => recur n
      recur 0 = [1])) := by
  fail

There is a mvar in the goal statement right after by. This shouldn’t be the case for theorem. So maybe that check is running too early or something, and if we fix that, then at least this will just error (with a bad error message…)

We want to see something like

Failed to infer type of theorem `ohno2`

Note: All parameter types and holes (e.g., `_`) in the header of a theorem are resolved before the proof is processed; information from the proof cannot be used to infer what these values should be

---

We reach

def logUnassignedUsingErrorInfos (pendingMVarIds : Array MVarId) (extraMsg? : Option MessageData := none) : TermElabM Bool := do

with the mvar in pendingMVarIds, but then nothing happens? I don’t quite understand the role of

for mvarErrorInfo in (← get).mvarErrorInfos do

and am running out of time for now.

[nomeata]

I also found this code:

/--
Ensures that the of let-rec definition types do not contain functions being defined.
In principle, this test can be improved. We could perform it after we separate the set of functions is strongly connected components.
However, this extra complication doesn't seem worth it.
-/
private def checkLetRecsToLiftTypes (funVars : Array Expr) (letRecsToLift : List LetRecToLift) : TermElabM Unit :=
  letRecsToLift.forM fun toLift =>
    match typeHasRecFun toLift.type funVars letRecsToLift with
    | none        => pure ()
    | some fvarId => do
      let fnName ← getFunName fvarId letRecsToLift
      throwErrorAt toLift.ref "invalid type in `let rec`, it uses `{fnName}` which is being defined simultaneously"

this looks like it would be reasonable to generalize it to forbid using let-rec in the whole recursive group.

[nomeata]

So yeah, maybe easiest to simply forbid let rec in types syntactically?