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