Zulip Chat Archive

Stream: Is there code for X?

Topic: order on bool


view this post on Zulip Rob Lewis (Jun 14 2020 at 19:28):

I feel like this has been asked here before but I can't find it. Is there anywhere we define an order on bool?

view this post on Zulip Gabriel Ebner (Jun 14 2020 at 19:29):

Maybe you're thinking of the order on Prop?

view this post on Zulip Rob Lewis (Jun 14 2020 at 19:31):

There's that too, but it won't help me with what I need. I'm just surprised the library seems to have no instances that give bool has_lt.

view this post on Zulip Kevin Buzzard (Jun 14 2020 at 19:31):

Because Prop = bool, you can probably use one of Scott's tactics to infer an order on bool.

view this post on Zulip Gabriel Ebner (Jun 14 2020 at 19:31):

We have complete_boolean_algebra, but neither Prop nor bool is one.

view this post on Zulip Rob Lewis (Jun 14 2020 at 19:33):

Kevin Buzzard said:

Because Prop = bool, you can probably use one of Scott's tactics to infer an order on bool.

Yes, this is clearly more direct than the one line direct definition!

view this post on Zulip Kevin Buzzard (Jun 14 2020 at 19:34):

My method is more conceptual.

view this post on Zulip Mario Carneiro (Jun 14 2020 at 19:55):

If you use boole you can define it via pullback from nat

view this post on Zulip Mario Carneiro (Jun 14 2020 at 19:55):

which should give you at least a total order

view this post on Zulip Rob Lewis (Jun 14 2020 at 20:14):

Or I'll just add this instance, because this is just a distraction from what I'm really trying to do...

import tactic.interactive

instance : decidable_linear_order bool :=
by refine_struct { lt := λ a b, a = ff  b = tt, le := λ a b, a = ff  b = tt };
   apply_instance <|> exact dec_trivial

view this post on Zulip Scott Morrison (Jun 15 2020 at 01:01):

I dimly remember trying to add it at some point (when I did something about lexicographic orderings)? I agree for tactic writing this ordering is super useful to have available, so I'm all for it.


Last updated: May 07 2021 at 19:12 UTC