search

lecopivo / SciLean

Scientific computing in Lean 4
https://lecopivo.github.io/scientific-computing-lean/
Apache License 2.0
327 stars 29 forks source link

Custom rewrite for ftrans and improved ftrans trace #10

Closed lecopivo closed 8 months ago

lecopivo commented 1 year ago

Use custom rewrite functions in ftrans. The main motivation is to have working trace Meta.Tactic.fprop.rewrite/discharge/unify. Currently, ftrans is using simp's rewrite functions thus it is producing Meta.Tactic.simp.rewrite/discharge/unify.

Further advantage will be that we can again introduce rewrite rules guards. For example rule like cderiv.arg_dx.semiAdjoint_rule is problematic as it can apply to itself with g = fun x => x.

lecopivo commented 8 months ago

This is solved by using new fun_trans