Commit 2026-09-09 00:40 4edb0dba

feat(Tactic/NormNum): run simp's default simprocs inside norm_num (#43003) This PR makes norm_num run simp's default simprocs. norm_num builds its own Simp.Methods rather than going through Simp.mkDefaultMethods, and passes an empty SimprocsArray to Simp.preDefault/Simp.postDefault. Simprocs were only folded into preDefault/postDefault in Lean v4.6.0; in v4.4 and v4.5 those functions had signature (e) (discharge?) and knew nothing about simprocs, and norm_num did not pick them up by any other route either. So no simproc has ever fired inside norm_num, which is surprising given that norm_num is documented as using simp to simplify the goal. The user-visible consequence is that norm_num cannot do arithmetic in any type whose arithmetic is implemented by simprocs rather than by norm_num extensions or simp lemmas. All of the following fail on master and succeed here:

example : (2 : Fin 7) + 6 = 1 := by norm_num
example : (3 : Fin 7) * 5 = 1 := by norm_num
example : (2 : Fin 7) < 5 := by norm_num
example : (⟨3, by omega⟩ : Fin 7) = 3 := by norm_num
example : (5 : UInt8) + 3 = 8 := by norm_num
example : (200 : UInt8) + 100 = 44 := by norm_num
example : (5 : Int8) * 3 = 15 := by norm_num
example : (0xff : BitVec 8) &&& 0x0f = 0x0f := by norm_num

The simproc set is threaded through getSimpContext, deriveSimp and methods, mirroring core's mkSimpContext: plain norm_num gets Simp.getSimprocs, norm_num only gets the empty set exactly as simp only does, and norm_num1 is unaffected since it does not call simp at all. NormNum.discharge keeps its current simproc-free behaviour by default, so reduce_mod_char is unchanged. 🤖 Prepared with Claude Code