Idiomatic notation for interval comparison

Stream: maths

[Geoffrey Irving]

Say I have an Interval type representing intervals of real numbers. I’d like to define a partial order on Interval where < or <= are true if we know that the approximated real numbers satisfy that comparison. For example, we’d have [0,1] <= [1,2].

The problem is that then <= is not reflexive: it is not the case that [a,b] <= [a,b] unless a = b. As far as I can tell, this means I can’t register any instances for this order, even though it has some nice properties (transitivity, antisymmetry).

What’s the best way to proceed in terms of idiomatic use of mathlib? Should I just define < and <= and prove Interval.le_trans and such without trying to link into the instance hierarchy?

[Violeta Hernández]

You could register the unbundled versions docs#IsTrans and docs#IsAntisymm

[Violeta Hernández]

Of course, these are significantly less useful.

[Violeta Hernández]

A simpler idea might be to just make the relation reflexive, and prove theorems about x ≤ y with the hypothesis x ≠ y whenever needed.

[Violeta Hernández]

So, x < y

[Geoffrey Irving]

Yep, both of those make sense. Though it feels like they’re less good than Interval.le_trans, alas, so I may just do the non-instance thing.

[Eric Wieser]

You should definitely do the instance thing, but also having the non-instance lemmas for convenience is fine too