order on options

Stream: general

[Simon Hudon]

Is there an instance of decidable_linear_order on option in Mathlib or core? I can't find one

[Kenny Lau]

maybe with_bot has an order

[Simon Hudon]

Yes, it does, thanks! Now I'm stuck for a new reason: I don't have a decidable linear order for name (from the tactics). I think I'll need to write some of those orders myself

[Mario Carneiro]

There is an order on name, but it is meta and not an instance

[Kenny Lau]

does it need to be meta?

[Mario Carneiro]

no

[Simon Hudon]

Actually, I only need a decidable relation, not an order

[Mario Carneiro]

it has that already

[Mario Carneiro]

meta instance : decidable_rel name.lt :=
λ a b, ordering.decidable_eq _ _

meta instance : has_lt name :=
⟨name.lt⟩

[Mario Carneiro]

also relevant

/- Both cmp and lex_cmp are total orders, but lex_cmp implements a lexicographical order. -/
meta constant name.cmp : name → name → ordering
meta constant name.lex_cmp : name → name → ordering

[Simon Hudon]

The issue is that the order relation and its decidability for has_bot are wrapped up in order instances

[Mario Carneiro]

I guess we could generalize the definitions to has_le from has_le and has_lt from has_lt, without committing to any order properties

[Simon Hudon]

Exactly

[Mario Carneiro]

An easy fix is

meta instance : decidable_linear_order name :=
by refine {lt := (<), le := \lam a b, \neg b < a, ..}; exact undefined

[Simon Hudon]

That's evil

[Kenny Lau]

how exactly is undefined defined?

[Mario Carneiro]

undefined := undefined, effectively

[Kenny Lau]

then how does VM know what to do with #eval unchecked_cast?

[Mario Carneiro]

it's not really, because this causes loops instead of an error

[Simon Hudon]

@Mario Carneiro you may have a different opinion if you knew that this is for a mathlib PR

[Mario Carneiro]

name is basically meta. If a proof gets in your way, kill it

[Mario Carneiro]

As long as it's actually true

[Mario Carneiro]

or close enough to true that it doesn't matter

[Mario Carneiro]

We could write name.lt non-meta, but I would want to see what is the performance hit first

[Simon Hudon]

or close enough to true that it doesn't matter

I'm hesitant to agree because I see the type class constraint as a way the type system tells you to make sure you're satisfying assumptions and warning you when you break those assumptions. You write undefined and you lose all that information. Or rather, the type system tells you "all the assumptions are satisfied, no worries" when it might not be the case

[Mario Carneiro]

This is true, but meta code doesn't have these guarantees anyway, except in a vague sense

[Mario Carneiro]

A proof in meta land means something between "nothing at all" and "probably true"

[Simon Hudon]

As a comparison, that used to be my opinion of software testing until I started grading software assignment of students who often didn't bother testing. Yes, tested software is still imperfect but untested is so much worse

[Mario Carneiro]

right, which is why a meta proof can mean "probably true": the user had to make a conscious choice to either prove it or stub it out

[Mario Carneiro]

I liken it to the "preconditions" requirements in programs in Haskell or Java. It says "don't fail this requirement or else" and no compile or run time checking

[Mario Carneiro]

If you pass an order that is not linear to a function expecting one in the type, it's your fault if it breaks

[Simon Hudon]

I think comparing it the a quickcheck property would be closer to the truth, when you decide to write them, they nudge you in the right direction