Zulip Chat Archive

Stream: general

Topic: unsafe mode for simp


view this post on Zulip 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.

Examples:

  • 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 continuous f and continuous g.

view this post on Zulip 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 intro.


Last updated: May 14 2021 at 07:19 UTC