ac9a1cb415
This PR introduces stricter inference for the `@[defeq]` attribute and a companion `@[backward_defeq]` attribute that preserves the pre-PR behavior as an opt-in. ### What changed * `@[defeq]` is now inferred only when the equation holds at `.instances` transparency (the transparency `dsimp` operates at). * `@[backward_defeq]` is the old set: every theorem whose `rfl` proof the legacy inference would have accepted is tagged `@[backward_defeq]`, so `defeq ⊆ backward_defeq` holds by construction. * The option `backward.defeqAttrib.useBackward` (default `false`) makes `dsimp` also use `@[backward_defeq]` theorems, restoring the pre-PR behavior for a specific proof or file. * The option is eqn-affecting: its value at the point of a function's definition is recorded so that the equation lemmas later generated for that function use the same value, regardless of the ambient option at the use site. ### Mathlib adaption A companion adaption branch (`lean-pr-testing-backward-defeq-attrib` on mathlib4) builds cleanly against this PR and passes `lake test` without warnings. Most adaption changes are scoped `set_option backward.defeqAttrib.useBackward true in` additions on the failing declarations; a small number of files needed proof-level edits where the stored form of a `dsimp%`/`@[reassoc]`/`@[elementwise]` /`@[simps]`/`@[to_app]`-generated lemma had drifted under the stricter regime. --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
88 lines
3.2 KiB
Text
88 lines
3.2 KiB
Text
def trailingZeros (i : Int) : Nat :=
|
|
if h : i = 0 then 0 else aux i.natAbs i h (Nat.le_refl _) 0
|
|
where
|
|
aux (k : Nat) (i : Int) (hi : i ≠ 0) (hk : i.natAbs ≤ k) (acc : Nat) : Nat :=
|
|
match k, (by omega : k ≠ 0) with
|
|
| k + 1, _ =>
|
|
if h : i % 2 = 0 then aux k (i / 2) (by omega) (by omega) (acc + 1)
|
|
else acc
|
|
termination_by structural k
|
|
|
|
/--
|
|
info: equations:
|
|
@[backward_defeq] theorem trailingZeros.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (x_1 : k_2 + 1 ≠ 0)
|
|
(hk_2 : i.natAbs ≤ k_2 + 1),
|
|
trailingZeros.aux k_2.succ i hi hk_2 acc = if h : i % 2 = 0 then trailingZeros.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc
|
|
-/
|
|
#guard_msgs(pass trace, all) in
|
|
#print equations trailingZeros.aux
|
|
|
|
|
|
-- set_option trace.Elab.definition.eqns true
|
|
-- set_option trace.split.debug true
|
|
-- set_option trace.Meta.Match.unify true
|
|
|
|
def trailingZeros' (i : Int) : Nat :=
|
|
if h : i = 0 then 0 else aux i.natAbs i h (Nat.le_refl _) 0
|
|
where
|
|
aux (k : Nat) (i : Int) (hi : i ≠ 0) (hk : i.natAbs ≤ k) (acc : Nat) : Nat :=
|
|
match k, (by omega : k ≠ 0) with
|
|
| k + 1, _ =>
|
|
if h : i % 2 = 0 then aux k (i / 2) (by omega) (by omega) (acc + 1)
|
|
else acc
|
|
termination_by k
|
|
|
|
/--
|
|
info: equations:
|
|
theorem trailingZeros'.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (x_1 : k_2 + 1 ≠ 0)
|
|
(hk_2 : i.natAbs ≤ k_2 + 1),
|
|
trailingZeros'.aux k_2.succ i hi hk_2 acc =
|
|
if h : i % 2 = 0 then trailingZeros'.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc
|
|
-/
|
|
#guard_msgs(pass trace, all) in
|
|
#print equations trailingZeros'.aux
|
|
|
|
def trailingZeros2 (i : Int) : Nat :=
|
|
if h : i = 0 then 0 else aux i.natAbs i h (Nat.le_refl _) 0
|
|
where
|
|
aux (k : Nat) (i : Int) (hi : i ≠ 0) (hk : i.natAbs ≤ k) (acc : Nat) : Nat :=
|
|
match k with
|
|
| k + 1 =>
|
|
if h : i % 2 = 0 then aux k (i / 2) (by omega) (by omega) (acc + 1)
|
|
else acc
|
|
| 0 => by omega
|
|
termination_by structural k
|
|
|
|
/--
|
|
info: equations:
|
|
@[backward_defeq] 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
|
|
@[backward_defeq] 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
|
|
#print equations trailingZeros2.aux
|
|
|
|
def trailingZeros2' (i : Int) : Nat :=
|
|
if h : i = 0 then 0 else aux i.natAbs i h (Nat.le_refl _) 0
|
|
where
|
|
aux (k : Nat) (i : Int) (hi : i ≠ 0) (hk : i.natAbs ≤ k) (acc : Nat) : Nat :=
|
|
match k with
|
|
| k + 1 =>
|
|
if h : i % 2 = 0 then aux k (i / 2) (by omega) (by omega) (acc + 1)
|
|
else acc
|
|
| 0 => by omega
|
|
termination_by k
|
|
|
|
/--
|
|
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
|
|
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
|
|
#print equations trailingZeros2'.aux
|