Stream: Is there code for X?

Topic: order on bool

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?

Gabriel Ebner (Jun 14 2020 at 19:29):

Maybe you're thinking of the order on Prop?

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.

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.

Gabriel Ebner (Jun 14 2020 at 19:31):

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

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!

Kevin Buzzard (Jun 14 2020 at 19:34):

My method is more conceptual.

Mario Carneiro (Jun 14 2020 at 19:55):

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

Mario Carneiro (Jun 14 2020 at 19:55):

which should give you at least a total order

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


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