classical tactic and linear orders

Stream: general

[Patrick Massot]

Is it a bug in the classical tactic that Lean still complains it can't find a decidable_linear_order instance even after calling classical?

[Simon Hudon]

Can you show your code?

[Sebastien Gouezel]

The standard way is letI := classical.DLO γ.

[Patrick Massot]

Yes, I know the standard way, but I thought classical would take care of that.

[Simon Hudon]

classical only adds decidable_prop to the local set of instances.

[Mario Carneiro]

Unfortunately not; we could have an instance that derives DLO from LO but it would loop

[Reid Barton]

The problem is DLO extends LO

[Simon Hudon]

would it be better if LO was an argument of DLO?

[Simon Hudon]

I mean in general, with the rest of the library

[Reid Barton]

I don't know.

[Simon Hudon]

If we compare with is_lawful_functor, DLO doesn't add propositional fields but it is a subsingleton

[Mario Carneiro]

I suppose that since classical is a tactic, it can do some intelligent things here. In particular, it can look for linear_order foo things in the local context and add letI := classical.DLO foo as necessary

[Simon Hudon]

That's true, that would be simple enough.