# Zulip Chat Archive

## Stream: triage

### Topic: PR #6485: Add a linter for incorrectly used decidable arg...

#### Random Issue Bot (Mar 31 2021 at 14:24):

Today I chose PR 6485 for discussion!

**Add a linter for incorrectly used decidable arguments**

Created by @Eric Wieser (@eric-wieser) on 2021-02-28

Labels: WIP

Is this PR still relevant? Any recent updates? Anyone making progress?

#### Eric Wieser (Mar 31 2021 at 14:38):

The linter works, but "Yury's rule of thumb" seems to lead to some unpleasant conclusions. Consider the following lemma:

```
lemma silly (n : nat) : (if n = 0 then 0 else n * n) = n * n := by split_ifs; simp[*]
```

This lemma includes a docs#nat.decidable_eq term in its theorem statement, which means it can't be used to rewrite a goal containing an `if`

that uses docs#classical.dec_eq. The solution to this is to instead write this lemma

```
lemma silly_fixed (n : nat) [decidable (n = 0)] : (if n = 0 then 0 else n * n) = n * n := by split_ifs; simp[*]
```

This will make the statement of some lemmas significantly harder to read. Are we ok with this?

#### Kevin Buzzard (Mar 31 2021 at 14:40):

I don't know what Yury thinks, but I think my rule of thumb would be not to apply Yury's rule of thumb in situations like that where there is already a constructive decidable instance in core.

#### Eric Wieser (Mar 31 2021 at 14:49):

Here's a case where the difference matters:

```
open_locale classical
/-- This definition is in a classical module, so we don't care about decidability. -/
noncomputable def update_zero {α : Type*} [semiring α] (f : α → α) : α → α := function.update f 0 0
example (n : nat) : update_zero (λ n : ℕ, n * n) n = n * n := begin
rw [update_zero, function.update_apply],
rw silly, -- fails. `rw silly_fixed` works
end
```

#### Sebastien Gouezel (Mar 31 2021 at 15:03):

I think `silly_fixed`

is a good idea, yes.

#### Eric Wieser (Mar 31 2021 at 15:11):

The CI logs suggest there are 363 lemmas which need a `[decidable_eq ℕ]`

argument added like this.

#### Mario Carneiro (Mar 31 2021 at 15:18):

I think this is not a good idea. We should try to avoid `classical.dec_eq`

being used to prove `decidable_eq nat`

instead

#### Eric Wieser (Mar 31 2021 at 15:19):

Here's a full list of the arguments we'd have to add. Things like `[decidable false]`

seem particularly nonsensical.

#### Mario Carneiro (Mar 31 2021 at 15:19):

The only way that would happen is if you substitute into a lemma about general alpha, where the decidability proof used `classical.dec_eq`

; but then that lemma is already violating yury's rule

#### Eric Wieser (Mar 31 2021 at 15:19):

So the violation in the example above is that I unfolded `update_zero`

?

#### Mario Carneiro (Mar 31 2021 at 15:20):

right; there should be a "definitional lemma" for it instead, which takes an arbitrary instance

#### Eric Wieser (Mar 31 2021 at 15:22):

But essentially what we're saying then is that the equation compiler itself is broken?

#### Eric Wieser (Mar 31 2021 at 15:22):

Because `update_zero.equations._eqn_1`

is the bad lemma

#### Anne Baanen (Mar 31 2021 at 15:25):

This seems like a task for `@[simps]`

. Would it be hard to teach it to generalize over subsingleton instances according to Yury's rule?

#### Eric Wieser (Mar 31 2021 at 15:29):

"generalizing over subsingleton instances" is the task that leads to inserting (arguable) nonsense like `[decidable false]`

#### Eric Wieser (Mar 31 2021 at 15:30):

It sounds like Mario is arguing that only the classical instances should be generalized

#### Eric Wieser (Mar 31 2021 at 15:31):

Which I think is a valid argument iff there are no other diamonds that can occur for `decidable`

#### Yury G. Kudryashov (Mar 31 2021 at 15:49):

I would use `[decidable_eq α]`

in the definition of `update_zero`

.

#### Eric Wieser (Mar 31 2021 at 15:53):

But you wouldn't add such an argument for `finsum`

, right?

#### Mario Carneiro (Mar 31 2021 at 15:54):

I think it is okay for `update_zero`

to have classical stuff internally, since the type of `update_zero`

does not require any decidability

#### Mario Carneiro (Mar 31 2021 at 15:54):

You might want a version with `decidable_eq A`

if you intend to use it in computational contexts, like the finset ops, but otherwise this is analogous to definitions on `finsupp`

or `finsum`

that are "explicitly classicalized"

#### Mario Carneiro (Mar 31 2021 at 15:57):

Eric Wieser said:

Because

`update_zero.equations._eqn_1`

is the bad lemma

True, but this lemma is only as important as you make it. You can write your own equation lemma and use it instead of the built in one - the equation compiler "gets it right" only about 70-80% of the time, so manual equation lemmas are quite common

#### Eric Wieser (Mar 31 2021 at 16:14):

It would be nice if there were some way to register your own lemmas as an equation lemma, so that there was no way to end up using the bad one

#### Eric Wieser (Mar 31 2021 at 16:15):

That is, have `rw my_def`

mean `rw my_def.equation.my_eqn_lemma`

#### Yury G. Kudryashov (Mar 31 2021 at 20:14):

For me difference between `update_zero`

and `finprod`

is that `finprod`

is irreducible which means "don't unfold, use API".

#### Yury G. Kudryashov (Mar 31 2021 at 20:14):

But probably Mario is right about `update_zero`

too.

#### Eric Wieser (Mar 31 2021 at 20:22):

So your rule would be, the API around `finprod`

should always accept a decidable argument rather than finding one from the environment?

#### Mario Carneiro (Mar 31 2021 at 20:25):

It should take a decidable argument in any lemma that requires decidability in the statement. Many theorems about `finprod`

won't need this, specifically *because* `finprod`

itself doesn't take a decidability argument

#### Mario Carneiro (Mar 31 2021 at 20:26):

So for example if you have `foo x := if p x then 0 else 1`

then the theorem `foo x = if p x then 0 else 1`

will need `decidable (p x)`

but `p x -> foo x = 0`

and `not (p x) -> foo x = 1`

will not

Last updated: May 09 2021 at 16:20 UTC