Zulip Chat Archive

Stream: new members

Topic: dec_trivial in classical


view this post on Zulip Kenny Lau (Apr 12 2020 at 08:34):

how to make dec_trivial work when I have an instance of all propositions decidable? MWE:

import tactic

example : nat.coprime 127 128 :=
by classical; exact dec_trivial

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 08:35):

oh wow I thought this stuff had been solved.

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 08:35):

import tactic

/-! -/
open_locale classical

example : nat.coprime 127 128 :=
by exact dec_trivial

Oh I see. This works

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 08:36):

The classical tactic adds _inst : Π (a : Prop), decidable a to the type class inference system but ideally it would add it with priority 10

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:36):

classical puts decidability in your context, and I think that gets maximum precedence

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 08:38):

Could classical instead do what open_locale classical does?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:39):

I don't think so? Changing declarations in the environment in the middle of a proof is kind of weird

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:40):

Certainly it can't do everything that open_locale can do because open_locale runs in the parser monad and hence has the ability to inject commands into the file that tactics can't do

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:40):

but maybe open_locale classical just sets some precedences and those might be doable


Last updated: May 10 2021 at 00:31 UTC