Topic: unsafe mode for simp
Yury G. Kudryashov (Aug 02 2020 at 20:33):
It would be nice to have an "unsafe mode" for
simp. In this mode it should apply some lemmas even if it can't prove all the prerequisites (and add new goals like
rw does). Probably we need some syntax to mark those arguments that "unsafe simp" should assume to be true.
- If I simplify an expression with division, then probably all assumptions "denominator is nonzero" hold true.
- If I argue about integrals, then most probably all functions are measurable and integrable.
- If I want to prove
continuous (f + g), then most probably I want to prove both
Sebastien Gouezel (Aug 02 2020 at 21:45):
See the discussion on
auto at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/golfing.20.60Ico.60.20union/near/205010470, and in particular the discussion of
Last updated: May 14 2021 at 07:19 UTC