dec_trivial in classical

Stream: new members

[Kenny Lau]

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]

oh wow I thought this stuff had been solved.

[Kevin Buzzard]

import tactic

/-! -/
open_locale classical

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

Oh I see. This works

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Could classical instead do what open_locale classical does?

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Alex Zhang]

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]

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

[Mario Carneiro]

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]

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]

Yes, using a norm_num plugin I just implemented in #8053:

example : nat.coprime 127 128 := by norm_num

[Kevin Buzzard]

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]

That latter option is in fact what the tactic does

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

the "computer algebra system" here is using #eval with the extended euclidean algorithm to get x and y

[Kevin Buzzard]

Oh interesting! So the tactic uses #eval and then comes up with a proof that the kernel accepts!

[Mario Carneiro]

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]

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]

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]

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

[Eric Wieser]

#8053 hasn't yet been merged anyway

[Kevin Buzzard]

Alex could still use the branch Mario made

[Alex Zhang]

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]

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]

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