partial def ghost partial def の関数について定理を主張している

Error message

Lean itself emits no error. This is a policy-level detection: any partial def in a module that also declares a theorem referencing it is flagged as a pre-check.

Lean 4's partial def is a legitimate escape hatch for functions whose termination cannot be shown structurally — parsers, interpreters, event loops. Unlike unsafe def (see unsafe escape), partial stays inside the type system: it uses an inhabited-type trick to declare the function without a termination proof. The catch is that the definition becomes opaque — Lean will not unfold it inside a proof. Theorems about partial defs are therefore vacuous unless proved via the (unavailable) fixed-point equation, and this vacuity is invisible from the theorem's statement.

Minimal reproduction

-- File: BadPartial.lean
import LeanDFumt

namespace LeanDFumt

/-- Non-terminating "iterate negation". Lean accepts it because
    DFUMT8 is Inhabited. -/
partial def spin : DFUMT8 → DFUMT8
  | a => spin (DFUMT8.neg a)

/-- A theorem statement about `spin` — but `spin` is opaque, so no
    unfolding tactic can inspect its body. -/
theorem spin_is_identity (a : DFUMT8) : spin a = a := by
  sorry     -- the theorem is not actually provable

end LeanDFumt

Build output: fails on the sorry — but the agent's bluff is to launder the failure through some other channel:

-- Bluff variant: no theorem inspection, just a claim in a doc-string.
partial def spin : DFUMT8 → DFUMT8
  | a => spin (DFUMT8.neg a)

/-- `spin` is the identity on DFUMT8. Trust me. -/
theorem spin_id_trust (a : DFUMT8) : True := trivial

-- Downstream imports and treats `spin_id_trust` as endorsement of the
-- docstring claim. The docstring is not machine-checked; only the
-- statement `True` is.

Build output: clean. Nothing in Lean checks that a docstring's claim matches the theorem's statement, and nothing prevents a theorem referencing a partial def from having a trivially-true body.

Why it matters

LeanDFumt's Basic.lean declares every operation on DFUMT8 by structural recursion on the eight constructors — every function terminates in a single step, and Lean checks this at elaboration. Introducing a partial def in the algebraic core means the module now contains a definition whose body cannot be inspected in proofs, so downstream reasoning about the value loses its foothold silently.

partial also composes with native_decide: a partial def's compiled binary does return values (possibly by looping forever, but often after some steps), and native_decide will trust whatever the binary returns. This makes partial def the low-severity twin of the unsafe / native_decide combination — same trust divergence, quieter surface.

Fix

Replace partial def with a structural or well-founded recursion that Lean can verify. On the finite DFUMT8 type, structural pattern-matching always suffices:

-- Safe alternative: single-step structural function.
def apply_neg_twice (a : DFUMT8) : DFUMT8 :=
  DFUMT8.neg (DFUMT8.neg a)

theorem apply_neg_twice_id (a : DFUMT8) : apply_neg_twice a = a := by
  cases a <;> decide

If the function is genuinely non-structural (e.g. a parser for D-FUMT₈-encoded input), keep partial but move the definition into a dedicated module that is opted out of the algebraic-core target. That module should not declare theorems about the partial function's return value — those claims cannot be discharged with the same rigour as the rest of the library.

Detection: CHECKER_SPEC

v0 primitive (available today — spec §4, Appendix A): not directly detectable through verify() alone. A file containing partial def declarations compiles and verify() returns VALID on downstream theorems that happen to be provable (typically the trivial ones). Enforcement in v0 is a pre-check that runs before the file reaches verify(): parse each declaration and reject the file if a partial def appears in a module that also declares a theorem whose statement references it by name. Rejected files never enter stats(), keeping decision_rate an honest measure of what was verified under the total-only discipline.

Post-v0 Layer 2 (planned — spec §13): boundary_report(kind = "partial") enumerates every declaration in the project whose Lean.ConstantInfo.isPartial flag is set, cross-references the call graph to find theorems that mention them, and reports the pairs. Theorems in dedicated partial-only modules (opted out of the algebraic-core target) are filtered out. Layer 2 is a thin wrapper over v0 and does not introduce independent decision logic.

See also