fix: fin bug in to_additive

[fpvandoorn]

• The to_additive heuristic was ported wrong (a conjunction in Lean 3 was ported to a disjunction in Lean 4)
  • I had to add a check to take care that heuristic doesn't treat (fun x => α) (n + 1) as a type that depends on Nat. This was causing at least one error.
• Also re-add some simple debug tracing in applyReplacementFun (with dbg_trace, since it's a pure function).
• In a future PR I will speed-up additiveTestAux, since it's currently still exponentially slower than necessary (though usually applied to only small terms).

---

[gebner]

I don't think it's a good idea to use dbg_trace for logging. It doesn't use MessageData, and the output is not interleaved with the other trace messages (dbg_trace just prints things to stdout).

We should either put this function in CoreM or leave out the logging.

[fpvandoorn]

Putting this function in CoreM would require generalizing memoFix to monads (which is used in Lean.Expr.replaceRec), so that it memoizes the output value of a monad application. I don't know if that is doable, and more specifically, I don't know how to do that.

I find the dbg_trace useful when debugging, and they will only ever fire with trace.to_additive_detail set to true, which almost nobody ever does (and never happens on the master branch of mathlib). That said, if you think this bad, I'll remove the dbg_trace (I could also put them behind a new option to_additive_debug).

[gebner]

Ah, I didn't realize it was only set with to_additive_detail. I still don't think it's a good solution, but at least it's contained.

[fpvandoorn]

I was very confused when merging this with master, since git would remove all my changes.
Apparently what happened is that this PR was already merged to master as a part of #1848. (cc @jcommelin @joneugster)

[fpvandoorn]

I will close this PR now

@gebner I will still change the dbg_trace to whatever you prefer, see above.

[joneugster]

I was very confused when merging this with master, since git would remove all my changes.
Apparently what happened is that this PR was already merged to master as a part of #1848. (cc @jcommelin @joneugster)

Looks like #1848 has been merged while still having a "Blocked-by-other-PR" label.