From f20cae3729e4428c13883b906ec63e2c28dc4995 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 11 Feb 2026 12:49:10 +0100 Subject: [PATCH] fix: no defeq equations for irreducible definitions (#12429) This PR sets the `irreducible` attribute before generating the equations for recursive definitions. This prevents these equations to be marked as `defeq`, which could lead to `simp` generation proofs that do not type check at default transparency. This issue is surfacing more easily since well-founded recursion on `Nat` is implemented with a dedicated fix point operator (#7965). Before that, `WellFounded.fix` was used, which is inherently not reducing, so we did get the desired result even without the explicit reducibility setting. Fixes #12398. --- src/Lean/Elab/PreDefinition/Eqns.lean | 1 + src/Lean/Elab/PreDefinition/Mutual.lean | 22 +++++--- tests/lean/run/issue12398.lean | 70 ++++++++++++++++++++++++ tests/lean/run/structuralEqn6.lean | 2 +- tests/lean/run/wfEqns5.lean | 6 +- tests/pkg/module/Module/Basic.lean | 6 +- tests/pkg/module/Module/ImportedAll.lean | 2 +- tests/pkg/module/Module/NonModule.lean | 2 +- 8 files changed, 95 insertions(+), 16 deletions(-) create mode 100644 tests/lean/run/issue12398.lean diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 8b3ce5fe5b..2165b8c045 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -64,6 +64,7 @@ private partial def mkEqnProof (declName : Name) (type : Expr) : MetaM Expr := d -- Try rfl before deltaLHS to avoid `id` checkpoints in the proof, which would make -- the lemma ineligible for dsimp if (← tryURefl mvarId) then + trace[Elab.definition.eqns] "proved directly by rfl" return ← instantiateMVars main go (← unfoldLHS declName mvarId) diff --git a/src/Lean/Elab/PreDefinition/Mutual.lean b/src/Lean/Elab/PreDefinition/Mutual.lean index 74d64a967b..0e03d63d4a 100644 --- a/src/Lean/Elab/PreDefinition/Mutual.lean +++ b/src/Lean/Elab/PreDefinition/Mutual.lean @@ -57,17 +57,25 @@ def cleanPreDef (preDef : PreDefinition) (cacheProofs := true) : MetaM PreDefini Assign final attributes to the definitions. Assumes the EqnInfos to be already present. -/ def addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit := do + /- + Set irreducibility attribute, unless the user has requested a different setting. + Must appen before `enableRealizationsForConst`, else the equation generation sees + a wrong setting and creates bad `defEq` equations. + -/ + for preDef in preDefs do + unless preDef.modifiers.attrs.any fun a => a.name = `reducible || a.name = `semireducible do + setIrreducibleAttribute preDef.declName + + /- + `enableRealizationsForConst` must happen before `generateEagerEqns` + It must happen in reverse order so that constants realized as part of the first decl + have realizations for the other ones enabled + -/ for preDef in preDefs.reverse do - -- must happen before `generateEagerEqns` - -- must happen in reverse order so that constants realized as part of the first decl - -- have realizations for the other ones enabled enableRealizationsForConst preDef.declName + for preDef in preDefs do generateEagerEqns preDef.declName applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation - -- Unless the user asks for something else, mark the definition as irreducible - unless preDef.modifiers.attrs.any fun a => - a.name = `reducible || a.name = `semireducible do - setIrreducibleAttribute preDef.declName end Lean.Elab.Mutual diff --git a/tests/lean/run/issue12398.lean b/tests/lean/run/issue12398.lean new file mode 100644 index 0000000000..0fab5dab0e --- /dev/null +++ b/tests/lean/run/issue12398.lean @@ -0,0 +1,70 @@ +inductive PFormula (α: Type): Type where + | And: Array (PFormula α) → PFormula α + | Or: Array (PFormula α) → PFormula α + | Not: (PFormula α) → PFormula α + | Atom: α → PFormula α + | FF: PFormula α + | TT: PFormula α + +namespace PFormula + +@[simp] +def is_atom (f: PFormula α): Prop := + match f with + | .Atom _ => True + | _ => False + +-- set_option trace.Elab.definition.eqns true +def is_nnf (f: PFormula α): Prop := + match f with + | .And a | .Or a => all_nnf a + | .Not g => g.is_atom + | .Atom _ | .TT | .FF => True + termination_by sizeOf f +where + all_nnf (a: Array (PFormula α)): Prop := ∀ i, (h: i < a.size) → a[i].is_nnf + termination_by sizeOf a + +-- This is irreducible + +/-- info: @[irreducible] def PFormula.is_nnf : {α : Type} → PFormula α → Prop -/ +#guard_msgs in +#print sig is_nnf + +-- So this should not be defeq! + +/-- info: theorem PFormula.is_nnf.eq_4 : ∀ {α : Type} (a : α), (Atom a).is_nnf = True -/ +#guard_msgs(pass trace, all) in +#print sig is_nnf.eq_4 + +-- If we try to prove it manually, it the irreducibility of `is_nnf` prevents that: +theorem eq_4 : ∀ {α : Type} (a : α), (Atom a).is_nnf = True := by + intros + fail_if_success rfl -- Should not work + apply is_nnf.eq_4 + + +def to_nnf (f: PFormula α): PFormula α := + match f with + | .And a => And (a.mapFinIdx (fun i _ _ => a[i].to_nnf)) + | .Or a => Or (a.mapFinIdx (fun i _ _ => a[i].to_nnf)) + | .Not g => + match g with + | .And a => Or (a.mapFinIdx + (fun i _ _ => + have : sizeOf a[i] < sizeOf a := by simp + (Not a[i]).to_nnf)) + | .Or a => And (a.mapFinIdx + (fun i _ _ => + have : sizeOf a[i] < sizeOf a := by simp + (Not a[i]).to_nnf)) + | .Not h => h.to_nnf + | .Atom x => Not (.Atom x) + | .TT => .FF + | .FF => .TT + | g => g + +theorem test: (TT: PFormula α).Not.to_nnf.is_nnf := by + simp [is_nnf, to_nnf] + +end PFormula diff --git a/tests/lean/run/structuralEqn6.lean b/tests/lean/run/structuralEqn6.lean index e88de20d03..1acb9df7b5 100644 --- a/tests/lean/run/structuralEqn6.lean +++ b/tests/lean/run/structuralEqn6.lean @@ -80,7 +80,7 @@ info: equations: theorem trailingZeros2'.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (hk_2 : i.natAbs ≤ k_2 + 1), trailingZeros2'.aux k_2.succ i hi hk_2 acc = if h : i % 2 = 0 then trailingZeros2'.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc -@[defeq] theorem trailingZeros2'.aux.eq_2 : ∀ (i : Int) (hi : i ≠ 0) (acc : Nat) (hk_2 : i.natAbs ≤ 0), +theorem trailingZeros2'.aux.eq_2 : ∀ (i : Int) (hi : i ≠ 0) (acc : Nat) (hk_2 : i.natAbs ≤ 0), trailingZeros2'.aux 0 i hi hk_2 acc = acc -/ #guard_msgs(pass trace, all) in diff --git a/tests/lean/run/wfEqns5.lean b/tests/lean/run/wfEqns5.lean index 245b3cf62a..824f980835 100644 --- a/tests/lean/run/wfEqns5.lean +++ b/tests/lean/run/wfEqns5.lean @@ -6,7 +6,7 @@ termination_by n => n /-- info: equations: -@[defeq] theorem foo.eq_1 : foo 0 0 = 0 +theorem foo.eq_1 : foo 0 0 = 0 theorem foo.eq_2 : ∀ (x : Nat), (x = 0 → False) → foo 0 x = x theorem foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x -/ @@ -53,7 +53,7 @@ termination_by n => n /-- info: equations: -@[defeq] theorem bar.eq_1 : ∀ (x : Nat), +theorem bar.eq_1 : ∀ (x : Nat), bar 0 x = match x with | 0 => 0 @@ -120,7 +120,7 @@ termination_by n => n /-- info: equations: -@[defeq] theorem Structural.bar.eq_1 : ∀ (x : Nat), +theorem Structural.bar.eq_1 : ∀ (x : Nat), bar 0 x = match x with | 0 => 0 diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean index 6c80be11cf..2c70fd421f 100644 --- a/tests/pkg/module/Module/Basic.lean +++ b/tests/pkg/module/Module/Basic.lean @@ -259,7 +259,7 @@ info: private theorem f_struct.eq_unfold : f_struct = fun x => -/ #guard_msgs(pass trace, all) in #print sig f_struct.eq_unfold -/-- info: @[defeq] private theorem f_wfrec.eq_1 : ∀ (x : Nat), f_wfrec 0 x = x -/ +/-- info: private theorem f_wfrec.eq_1 : ∀ (x : Nat), f_wfrec 0 x = x -/ #guard_msgs(pass trace, all) in #print sig f_wfrec.eq_1 /-- @@ -279,7 +279,7 @@ info: private theorem f_wfrec.eq_unfold : f_wfrec = fun x x_1 => -/ #guard_msgs in #print sig f_wfrec.eq_unfold -/-- info: @[defeq] theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/ +/-- info: theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/ #guard_msgs in #print sig f_exp_wfrec.eq_1 /-- @@ -553,4 +553,4 @@ public structure OpOperand2 where public def func (ctx : Nat) (operand : OpOperand2) : Nat := match operand.nextUse with | none => ctx - | some nextPtr => ctx + | some _nextPtr => ctx diff --git a/tests/pkg/module/Module/ImportedAll.lean b/tests/pkg/module/Module/ImportedAll.lean index 6bc963e9ed..21edf1bfde 100644 --- a/tests/pkg/module/Module/ImportedAll.lean +++ b/tests/pkg/module/Module/ImportedAll.lean @@ -105,7 +105,7 @@ info: theorem f_wfrec.induct_unfolding : ∀ (motive : Nat → Nat → Nat → P -/ #guard_msgs(pass trace, all) in #print sig f_wfrec.induct_unfolding -/-- info: @[defeq] theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/ +/-- info: theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/ #guard_msgs in #print sig f_exp_wfrec.eq_1 /-- diff --git a/tests/pkg/module/Module/NonModule.lean b/tests/pkg/module/Module/NonModule.lean index 5e2bb12dd6..48bfa62e2b 100644 --- a/tests/pkg/module/Module/NonModule.lean +++ b/tests/pkg/module/Module/NonModule.lean @@ -54,7 +54,7 @@ info: theorem f_wfrec.induct_unfolding : ∀ (motive : Nat → Nat → Nat → P -/ #guard_msgs(pass trace, all) in #print sig f_wfrec.induct_unfolding -/-- info: @[defeq] theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/ +/-- info: theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/ #guard_msgs(pass trace, all) in #print sig f_exp_wfrec.eq_1