mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
73640d3758
This PR fixes `@[implicit_reducible]` on well-founded recursive definitions. `addPreDefAttributes` sets WF-recursive definitions as `@[irreducible]` by default, skipping this only when the user explicitly wrote `@[reducible]` or `@[semireducible]`. It was missing `@[instance_reducible]` and `@[implicit_reducible]`, causing those attributes to be silently overridden. Add `instance_reducible` and `implicit_reducible` to the check in `src/Lean/Elab/PreDefinition/Mutual.lean` that guards against overriding user-specified reducibility attributes, and add regression tests in `tests/elab/wfirred.lean`. ## Example ```lean -- Before fix: printed @[irreducible] def f : List Nat → Nat -- After fix: printed @[implicit_reducible] def f : List Nat → Nat @[instance_reducible] def f : ∀ _l : List Nat, Nat | [] => 0 | [_x] => 1 | x :: y :: l => if h : x = y then f (x :: l) else f l + 2 termination_by l => sizeOf l #print sig f ``` Fixes #12775 --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: nomeata <148037+nomeata@users.noreply.github.com>
134 lines
2.4 KiB
Lean4
134 lines
2.4 KiB
Lean4
/-!
|
|
Tests that definitions by well-founded recursion (not on Nat) are irreducible.
|
|
-/
|
|
|
|
set_option pp.mvars false
|
|
|
|
def foo : Nat → Nat → Nat
|
|
| 0, m => m
|
|
| n+1, m => foo n (m + n)
|
|
termination_by n m => (n, m)
|
|
|
|
/--
|
|
error: Type mismatch
|
|
rfl
|
|
has type
|
|
?_ = ?_
|
|
but is expected to have type
|
|
foo 0 m = m
|
|
-/
|
|
#guard_msgs in
|
|
example : foo 0 m = m := rfl
|
|
|
|
/--
|
|
error: Type mismatch
|
|
rfl
|
|
has type
|
|
?_ = ?_
|
|
but is expected to have type
|
|
foo (n + 1) m = foo n (m + n)
|
|
-/
|
|
#guard_msgs in
|
|
example : foo (n+1) m = foo n (m + n) := rfl
|
|
|
|
-- also for closed terms
|
|
/--
|
|
error: Tactic `rfl` failed: The left-hand side
|
|
foo 0 0
|
|
is not definitionally equal to the right-hand side
|
|
0
|
|
|
|
⊢ foo 0 0 = 0
|
|
-/
|
|
#guard_msgs in
|
|
example : foo 0 0 = 0 := by rfl
|
|
|
|
section Unsealed
|
|
|
|
unseal foo
|
|
|
|
-- unsealing works, but does not have the desired effect
|
|
|
|
/--
|
|
error: Type mismatch
|
|
rfl
|
|
has type
|
|
?_ = ?_
|
|
but is expected to have type
|
|
foo 0 0 = 0
|
|
-/
|
|
#guard_msgs in
|
|
example : foo 0 0 = 0 := rfl
|
|
|
|
/--
|
|
error: Type mismatch
|
|
rfl
|
|
has type
|
|
?_ = ?_
|
|
but is expected to have type
|
|
foo (n + 1) m = foo n (n + m)
|
|
-/
|
|
#guard_msgs in
|
|
example : foo (n+1) m = foo n (n +m ):= rfl
|
|
|
|
end Unsealed
|
|
|
|
--should be sealed again here
|
|
|
|
/--
|
|
error: Type mismatch
|
|
rfl
|
|
has type
|
|
?_ = ?_
|
|
but is expected to have type
|
|
foo 0 m = m
|
|
-/
|
|
#guard_msgs in
|
|
example : foo 0 m = m := rfl
|
|
|
|
def bar : Nat → Nat → Nat
|
|
| 0, m => m
|
|
| n+1, m => bar n (m + n)
|
|
termination_by n m => (n, m)
|
|
|
|
-- Once unsealed, the full internals are visible. This allows one to prove, for example
|
|
-- an equality like the following
|
|
|
|
/--
|
|
error: Type mismatch
|
|
rfl
|
|
has type
|
|
?_ = ?_
|
|
but is expected to have type
|
|
foo = bar
|
|
-/
|
|
#guard_msgs in
|
|
example : foo = bar := rfl
|
|
|
|
unseal foo bar in
|
|
example : foo = bar := rfl
|
|
|
|
/-!
|
|
Tests that reducibility attributes set by the user are preserved for WF-recursive functions.
|
|
In particular, `@[instance_reducible]` (alias for `@[implicit_reducible]`) should not be
|
|
overridden by the default `@[irreducible]` that WF recursion sets. See issue #7082.
|
|
-/
|
|
|
|
@[instance_reducible] def baz : Nat → Nat → Nat
|
|
| 0, m => m
|
|
| n+1, m => baz n (m + n)
|
|
termination_by n m => (n, m)
|
|
|
|
/-- info: @[implicit_reducible] def baz : Nat → Nat → Nat -/
|
|
#guard_msgs in
|
|
#print sig baz
|
|
|
|
@[implicit_reducible] def qux : Nat → Nat → Nat
|
|
| 0, m => m
|
|
| n+1, m => qux n (m + n)
|
|
termination_by n m => (n, m)
|
|
|
|
/-- info: @[implicit_reducible] def qux : Nat → Nat → Nat -/
|
|
#guard_msgs in
|
|
#print sig qux
|