Zulip Chat Archive

Stream: general

Topic: Interval simp normal forms


view this post on Zulip Patrick Massot (Jul 28 2020 at 17:03):

Should we have lemmas like:

@[simp] lemma Ici_def (x) : {t | x \le t} = Ici x := rfl

The point is the simp attribute. My goal is to have simp getting of as many interval manipulation as possible, including topological operation (like closure, interior and frontiers) of intervals.

view this post on Zulip Patrick Massot (Jul 28 2020 at 17:04):

And sometimes things are blocked because and interval is not written using I..

view this post on Zulip Anatole Dedecker (Jul 28 2020 at 19:28):

I totally second this. I'm still new to mathlib, but intervals are really frustrating : most useful lemmas are already there, but having to invoke them manually is quite annoying

view this post on Zulip Johan Commelin (Jul 28 2020 at 20:36):

Maybe one of the trickier but also most important enhancements would be the "simp procs" for simp?

view this post on Zulip Johan Commelin (Jul 28 2020 at 20:37):

It seems that this is necessary to bridge the step from a ≤ b to a < b in the hypothesis. (Currently simp won't trigger if you don't get the hyps exactly right...)


Last updated: May 17 2021 at 20:14 UTC