Zulip Chat Archive

Stream: general

Topic: classical tactic and linear orders


view this post on Zulip Patrick Massot (Apr 15 2020 at 15:16):

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?

view this post on Zulip Simon Hudon (Apr 15 2020 at 15:28):

Can you show your code?

view this post on Zulip Sebastien Gouezel (Apr 15 2020 at 15:31):

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

view this post on Zulip Patrick Massot (Apr 15 2020 at 15:32):

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

view this post on Zulip Simon Hudon (Apr 15 2020 at 15:38):

classical only adds decidable_prop to the local set of instances.

view this post on Zulip Mario Carneiro (Apr 15 2020 at 15:38):

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

view this post on Zulip Reid Barton (Apr 15 2020 at 15:39):

The problem is DLO extends LO

view this post on Zulip Simon Hudon (Apr 15 2020 at 15:40):

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

view this post on Zulip Simon Hudon (Apr 15 2020 at 15:41):

I mean in general, with the rest of the library

view this post on Zulip Reid Barton (Apr 15 2020 at 15:43):

I don't know.

view this post on Zulip Simon Hudon (Apr 15 2020 at 15:45):

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

view this post on Zulip Mario Carneiro (Apr 15 2020 at 15:57):

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

view this post on Zulip Simon Hudon (Apr 15 2020 at 15:59):

That's true, that would be simple enough.


Last updated: May 08 2021 at 04:14 UTC