order on bool

Stream: Is there code for X?

[Rob Lewis]

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]

Maybe you're thinking of the order on Prop?

[Rob Lewis]

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]

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

[Gabriel Ebner]

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

[Rob Lewis]

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]

My method is more conceptual.

[Mario Carneiro]

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

[Mario Carneiro]

which should give you at least a total order

[Rob Lewis]

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]

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.