## 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