Zulip Chat Archive

Stream: triage

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


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Sebastien Gouezel (Mar 31 2021 at 15:03):

I think silly_fixed is a good idea, yes.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 31 2021 at 15:19):

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

view this post on Zulip Mario Carneiro (Mar 31 2021 at 15:20):

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

view this post on Zulip Eric Wieser (Mar 31 2021 at 15:22):

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

view this post on Zulip Eric Wieser (Mar 31 2021 at 15:22):

Because update_zero.equations._eqn_1 is the bad lemma

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Mar 31 2021 at 15:29):

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

view this post on Zulip Eric Wieser (Mar 31 2021 at 15:30):

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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Mar 31 2021 at 15:49):

I would use [decidable_eq α] in the definition of update_zero.

view this post on Zulip Eric Wieser (Mar 31 2021 at 15:53):

But you wouldn't add such an argument for finsum, right?

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 31 2021 at 16:15):

That is, have rw my_def mean rw my_def.equation.my_eqn_lemma

view this post on Zulip 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".

view this post on Zulip Yury G. Kudryashov (Mar 31 2021 at 20:14):

But probably Mario is right about update_zero too.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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