# Zulip Chat Archive

## Stream: new members

### Topic: dec_trivial in classical

#### 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

#### Kevin Buzzard (Apr 12 2020 at 08:35):

oh wow I thought this stuff had been solved.

#### 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

#### 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

#### Mario Carneiro (Apr 12 2020 at 08:36):

`classical`

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

#### Kevin Buzzard (Apr 12 2020 at 08:38):

Could `classical`

instead do what `open_locale classical`

does?

#### 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

#### 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

#### Mario Carneiro (Apr 12 2020 at 08:40):

but maybe `open_locale classical`

just sets some precedences and those might be doable

#### Alex Zhang (Jun 23 2021 at 04:21):

Kevin Buzzard said:

`import tactic /-! -/ open_locale classical example : nat.coprime 127 128 := by exact dec_trivial`

Oh I see. This works

It seems to me that this does not work. It reports an error:

```
exact tactic failed, type mismatch, given expression has type
true
but is expected to have type
as_true (127.coprime 128)
state:
⊢ as_true (127.coprime 128)
state:
⊢ 127.coprime 128
```

```
import tactic
open_locale classical
example : nat.coprime 127 128 :=
by exact dec_trivial
```

#### Mario Carneiro (Jun 23 2021 at 05:06):

this is an old thread, things have changed since last april

#### Mario Carneiro (Jun 23 2021 at 05:06):

in particular, I think the issue this is hitting is that definitions by well founded recursion no longer compute in the kernel, and `gcd`

is defined by well founded recursion

#### Alex Zhang (Jun 23 2021 at 06:15):

Uhmmm, then are we still able to close the goal `example : nat.coprime 127 128 :=`

by a dec related tactic (or by any other convenient way)?

#### Mario Carneiro (Jun 23 2021 at 08:32):

Yes, using a `norm_num`

plugin I just implemented in #8053:

```
example : nat.coprime 127 128 := by norm_num
```

#### Kevin Buzzard (Jun 23 2021 at 08:34):

Alternatively you could prove `nat.coprime n (n+1)`

for all n. Alternatively you could write down two integers x and y (found e.g. using a computer algebra system, although probably not in this case) such that 127x+128y=1 and then use a lemma in the library showing that this guarantees gcd=1.

#### Mario Carneiro (Jun 23 2021 at 08:34):

That latter option is in fact what the tactic does

#### Mario Carneiro (Jun 23 2021 at 08:35):

the proof that the gcd/coprime fact is correct doesn't use the euclidean algorithm

#### Kevin Buzzard (Jun 23 2021 at 08:36):

right, the algorithm "is" finding x and y.

#### Mario Carneiro (Jun 23 2021 at 08:36):

the "computer algebra system" here is using `#eval`

with the extended euclidean algorithm to get x and y

#### Kevin Buzzard (Jun 23 2021 at 08:37):

Oh interesting! So the tactic uses `#eval`

and then comes up with a proof that the kernel accepts!

#### Mario Carneiro (Jun 23 2021 at 08:38):

writing norm_num plugins is always fun because you end up with algorithms that look nothing like what you find in the books

#### Kevin Buzzard (Jun 23 2021 at 08:38):

I guess I saw this phenomenon in Chris' MSc thesis -- he implemented an algorithm in group theory, didn't formally prove it worked, but then just passed the proofs it discovered to the kernel and the kernel was happy.

#### Alex Zhang (Jun 24 2021 at 03:46):

Mario Carneiro said:

Yes, using a

`norm_num`

plugin I just implemented in #8053:`example : nat.coprime 127 128 := by norm_num`

How can I update my mathlib?

#### Kevin Buzzard (Jun 24 2021 at 07:42):

Are you working on mathlib directly or in another project which depends on mathlib as a dependency?

#### Eric Wieser (Jun 24 2021 at 07:57):

#8053 hasn't yet been merged anyway

#### Kevin Buzzard (Jun 24 2021 at 07:59):

Alex could still use the branch Mario made

#### Alex Zhang (Jun 24 2021 at 08:03):

Kevin Buzzard said:

Are you working on mathlib directly or in another project which depends on mathlib as a dependency?

I am in the second case.

#### Kevin Buzzard (Jun 24 2021 at 08:28):

Well then if you want Mario's changes *NOW* before they have even been merged to master, then probably the simplest way is to just edit the `leanpkg.toml`

of your project manually. Assuming your toml says

```
lean_version = "leanprover-community/lean:3.30.0"
```

then it will be as simple as changing the `rev =`

bit of the `mathlib = ...`

line to the commit corresponding to Mario's PR, and then running `leanproject get-mathlib-cache`

(or `leanproject get-m`

if you want to type less) and then `leanproject build`

to rebuild your project.

If you are happy to wait until it's merged to master, then any time after that's happened you can type `leanproject up`

and you'll have the latest version.

#### Mario Carneiro (Jun 24 2021 at 13:03):

You can also copy the contents of the PR file (it's a pure addition) to some file in your repo

Last updated: Dec 20 2023 at 11:08 UTC