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

@@ -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)

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

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

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

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

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

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
 
 /--

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