`LT` instance for Option is unused/not useful to have at this kind of base level.

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The file Init/Data/Option/Basic.lean contains a function Option.lt, an instance of LT for Option A inherited from a LT A, and a decidability instance for that relation.

The definition that it uses is one which sets none < some a and some a < some b just when a < b. This is a perfectly sane definition, but making this choice at such a low-level seems counter-intuitive to me. Different libraries might want to choose different definitions for LT on Option. Back in Mathlib 4 land, WitBot A and WithTop A are synonyms for Option that are based off this ordering and the obvious dual one. The base Option type having a LT instance as a core feature of lean4 - when as far as I can see this isn't used anywhere - removes the ability of downstream projects like std4 or mathlib4 to make different choices.

Context

I was doing some work in Mathlib4 and I used < in some statements about Option, It worked (because the instance is defined), and some stuff is RFL-true and so it wasn't until substantially later that I realised that this instance wasn't particular doing what I had expected and didn't have any nice API. I discussed this in a Zulip thread here: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Preorder.20on.20Option

I think downstream in Mathlib4 (or maybe std4 but I am not as sure how to contribute to that) we should add an instance, but in the context of this project I think it should simply be removed - it isn't useful and it creates footguns like what happened to me.

Steps to Reproduce

1. Write down the following code:

example {A : Type*} [LT A] {a : A} : (none : Option A) < some a := sorry` 

2. The code is trivially true (I think trivial works as a proof through I am not sure.)
3. And this typechecks.

Expected behavior:
I would expect the default behaviour of LT on Option to be either:
a) LT is not defined, and so this shouldn't typecheck/synthesise a correct instance.
b) An instance is defined, and in it, this is not a true statement. Why should none < some a be true, and some a < none not? You don't have to make a choice.

Actual behavior:
A choice is made: this statement is true.

Versions

4.30
Windows 11 running Ubuntu WSL2

Additional Information

None.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reading Init/Data/Option/Basic.lean, focusing on Option.lt, the LT instance, and its decidability instance. Search the Lean 4 sources for uses of these definitions and compare them with the minimal Option example in the issue. Done means the chosen treatment of LT for Option is implemented consistently without leaving unintended users or regressions.