Zulip Chat Archive

Stream: general

Topic: Interval simp normal forms

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.

Patrick Massot (Jul 28 2020 at 17:04):

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

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

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?

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: Dec 20 2023 at 11:08 UTC