dec_trivial on `nat` vs `int`

Stream: general

[Michael Stoll]

Why does the first example below work and the second does not?

import tactic
import data.zmod.basic

open zmod

def χ₄ : (zmod 4) →*₀ ℤ :=
{ to_fun := (![0,1,0,-1] : (zmod 4 → ℤ)),
  map_zero' := rfl, map_one' := rfl, map_mul' := by dec_trivial }

example : ∀ (m : ℕ), 0 ≤ m → m < 4 → χ₄ m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1 :=
  dec_trivial

example : ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1 :=
  dec_trivial
-- failed to synthesize type class instance for
-- ⊢ decidable (∀ (m : ℤ), 0 ≤ m → m < 4 → ⇑χ₄ ↑m = ite (m % 2 = 0) 0 (ite (m = 1) 1 (-1)))

[Eric Rodriguez]

there is docs#nat.decidable_lo_hi, but not an int version (as far as I can tell)

[Michael Stoll]

docs#int.decidable_le_lt ?

[Reid Barton]

You probably don't have it imported

[Michael Stoll]

I don't think it is obvious that one needs to import precisely that...

[Reid Barton]

Certainly not!

[Reid Barton]

This is an issue that Lean/mathlib doesn't really attempt to solve, beyond "well statistically you're likely to import most things transitively anyways"

[Michael Stoll]

... and import all more or less immediately gives a timeout...

[Mario Carneiro]

it shouldn't, if you have mathlib compiled

[Mario Carneiro]

unless the file you are working on is in mathlib

[Michael Stoll]

OK; I'll try import all again in the future (when not working on a mathlib file).

[Mario Carneiro]

a more realistic approach is when you want to find something, grep the sources for files that talk about the constants you are working with and import them

[Mario Carneiro]

and also be aware that the behavior of dec_trivial and by simp depends on your imports

[Michael Stoll]

In the case at hand, I'd first have to know that I'm looking for int.decidable_le_lt (and not lo_hi as for nat) ...
You have to know something about how the whole decidability business works behind the scenes.

[Eric Rodriguez]

and to find that, I had to #print the proof, turn on pp.implicit, and dig...

[Eric Rodriguez]

it'd be nice to be able to tell what instances dec_trivial uses sometimes

[Eric Rodriguez]

like squeeze_dec_trivial

[Mario Carneiro]

Michael Stoll said:

In the case at hand, I'd first have to know that I'm looking for int.decidable_le_lt (and not lo_hi as for nat) ...
You have to know something about how the whole decidability business works behind the scenes.

No, you don't need to know or reference the names of instances in the vast majority of cases, you only need to know the statements and a vague idea of what files to find them in

[Mario Carneiro]

you do need to know something about how decidability instances work to expect that ∀ (m : ℤ), 0 ≤ m → m < 4 → ... is going to be solved in the first place (decidability instances generally don't exist for statements with quantifiers except in specific cases), and the fact that it's a bounded quantifier over int suggests to look in int files

[Mario Carneiro]

or just import them indiscriminately and see if it fixes the issue

[Eric Wieser]

Michael Stoll said:

In the case at hand, I'd first have to know that I'm looking for int.decidable_le_lt (and not lo_hi as for nat) ...
You have to know something about how the whole decidability business works behind the scenes.

I think a PR to rename the nat one to le_lt would probably be accepted; generally consistent names are good to have, it's just hard to notice when we introduce inconsistent ones.

[Mario Carneiro]

especially for instances because they are rarely referred to by name

[Mario Carneiro]

(bounded quantifier instances have to be named because the default name would be something like decidable.forall and there would be lots of name clashes for that)

[Eric Wieser]

(does the instance naming actually know about forall?)

[Mario Carneiro]

true, it would probably be decidable.Pi or something even more vague

[Mario Carneiro]

as a matter of fact it is pi.decidable

[Kevin Buzzard]

Michael Stoll said:

OK; I'll try import all again in the future (when not working on a mathlib file).

I tell my undergraduates to start every file with import tactic and this empirically seems to import all the tactics they'll ever use, plus enough of mathlib to make basic stuff work, whilst not importing enough to make library_search unusable -- however I guess you just gave a counterexample to the claim that this should be enough :-/