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

Stream: triage

[Random Issue Bot]

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]

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]

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]

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]

I think silly_fixed is a good idea, yes.

[Eric Wieser]

The CI logs suggest there are 363 lemmas which need a [decidable_eq ℕ] argument added like this.

[Mario Carneiro]

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]

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

[decidable ((∃ (x : ℝ), x ∈ S) ∧ ∃ (x : ℝ), ∀ (y : ℝ), y ∈ S → y ≤ x)]
[decidable (0 < n)]
[decidable (0 < y)]
[decidable (2 ∣ n)]
[decidable (_ = _)]
[decidable (_ ∈ _)]
[decidable (_ ≤ _)]
[decidable (a = 0 ∨ b = 0)]
[decidable (a = a')]
[decidable (a ∈ f.support)]
[decidable (a' = a)]
[decidable (a.val ≤ n / 2)]
[decidable (b < a)]
[decidable (b ∣ a + 1)]
[decidable (bitvec.add_lsb x b % 2 = 1)]
[decidable (c ≤ a % c + b % c)]
[decidable (d.support.sum (λ (i : σ), ⇑d i) = n)]
[decidable (e₂ = 0)]
[decidable (f.same_cycle x y)]
[decidable (finsupp.single i 1 = m)]
[decidable (finsupp.single i k = m)]
[decidable (fintype.card K - 1 ∣ i)]
[decidable (i = f.nat_degree)]
[decidable (k = 0 ∧ n = 0)]
[decidable (m = finsupp.single s n)]
[decidable (n % 2 = 1)]
[decidable (n < L.length)]
[decidable (n = finsupp.single s 1)]
[decidable (ordnode.delta * ls < rs)]
[decidable (ordnode.delta * rs < ls)]
[decidable (p a)]
[decidable (p ∣ n)]
[decidable (p ∧ q)]
[decidable (p ∨ q)]
[decidable (roption.of_option o).dom]
[decidable (roption.some 0).dom]
[decidable (roption.some a).dom]
[decidable (s ∈ m.support)]
[decidable (x = 0 ∧ y < 0)]
[decidable (x' ≠ x)]
[decidable (x.dom ∧ y.dom)]
[decidable (x.val ≤ n / 2)]
[decidable (y < 0)]
[decidable (¬p)]
[decidable (¬P)]
[decidable (↑m % ↑k = 0)]
[decidable (∀ (a : α) (h : a ∈ s), (λ (i : α) (H : i ∈ s), p i) a h)]
[decidable (∀ (n : ℕ) (h : n ≤ N), (λ (k : ℕ) (H : k ≤ N), has_edist.edist (e (N + 1)) x < has_edist.edist (e k) x) n h)]
[decidable (∃ (a : α), f a = b)]
[decidable (∃ (x : ℝ), x ∈ S)]
[decidable (∃ (x : ℝ), ∀ (y : ℝ), y ∈ S → y ≤ x)]
[decidable false]
[decidable roption.none.dom]
[decidable true]
[decidable x.dom]
[decidable y.dom]
[decidable ↑n.dom]
[decidable_eq ((unit ⊕ l) ⊕ l)]
[decidable_eq (_ × _)]
[decidable_eq (_ ⊕ _)]
[decidable_eq (dihedral n)]
[decidable_eq (finset α)]
[decidable_eq (lucas_lehmer.X (lucas_lehmer.q (p' + 2)))]
[decidable_eq (option nnreal)]
[decidable_eq (option α)]
[decidable_eq (quotient (sym2.rel.setoid V))]
[decidable_eq (quotient R)]
[decidable_eq (unit ⊕ l ⊕ l)]
[decidable_eq (unit ⊕ l)]
[decidable_eq (units (lucas_lehmer.X (lucas_lehmer.q (p' + 2))))]
[decidable_eq (units (zmod p))]
[decidable_eq (zmod n)]
[decidable_eq (zmod p)]
[decidable_eq (α →₀ ℕ)]
[decidable_eq (Π (a : α), (λ (a : α), δ a) a)]
[decidable_eq (Π (a_1 : α), a_1 ∈ has_insert.insert a s → (λ (a : α), δ a) a_1)]
[decidable_eq (σ →₀ ℕ)]
[decidable_eq (ℕ →₀ F)]
[decidable_eq (ℕ →₀ R)]
[decidable_eq (ℕ →₀ α)]
[decidable_eq bool]
[decidable_eq category_theory.limits.walking_pair]
[decidable_eq G.dart]
[decidable_eq onote]
[decidable_eq punit]
[decidable_eq turing.partrec_to_TM2.K']
[decidable_eq {x // (λ (x : associates α), irreducible x) x}]
[decidable_eq {x // (λ (x : M), x ∈ set.range b) x}]
[decidable_eq {x // (λ (x : M₁), x ∈ set.range v₁) x}]
[decidable_eq {x // (λ (x : α), p x) x}]
[decidable_eq {x // (λ (x : α), x ∈ has_insert.insert a s) x}]
[decidable_eq {x // (λ (x : α), x ∈ multiset.ndinsert a s) x}]
[decidable_eq {x // (λ (x : α), ¬p x) x}]
[decidable_eq {x // (λ (x : ι), p x) x}]
[decidable_eq {x // (λ (x : ℕ), nat.prime x) x}]
[decidable_eq {x // (λ (x : ℕ), x < 0) x}]
[decidable_eq {x // (λ (x : ℕ), x < 1) x}]
[decidable_eq {x // (λ (x : ℕ), x < 2) x}]
[decidable_eq {x // (λ (x : ℕ), x < 3) x}]
[decidable_eq {x // (λ (x : ℕ), x < c.blocks_fun (c.index j)) x}]
[decidable_eq {x // (λ (x : ℕ), x < c.length) x}]
[decidable_eq {x // (λ (x : ℕ), x < k) x}]
[decidable_eq {x // (λ (x : ℕ), x < l) x}]
[decidable_eq {x // (λ (x : ℕ), x < m) x}]
[decidable_eq {x // (λ (x : ℕ), x < n + 1) x}]
[decidable_eq {x // (λ (x : ℕ), x < n + 2 + 1) x}]
[decidable_eq {x // (λ (x : ℕ), x < n + 2) x}]
[decidable_eq {x // (λ (x : ℕ), x < n + 3) x}]
[decidable_eq {x // (λ (x : ℕ), x < n) x}]
[decidable_eq {x // (λ (x : ℕ), x < n.succ) x}]
[decidable_eq {x // (λ (x : ℝ), 0 ≤ x) x}]
[decidable_eq α]
[decidable_eq ℂ]
[decidable_eq ℕ]
[decidable_eq ℤ]
[decidable_pred (G.common_neighbors v w)]
[decidable_pred odd]
[decidable_pred set.univ]
[decidable_pred squarefree]
[decidable_pred {a : composition (n + 2) | (λ (c : composition (n + 2)), 1 < c.length) a}]
[decidable_pred {a : composition n | (λ (c : composition n), 1 < c.length) a}]
[decidable_pred {a : α | (λ (a : α), ↥((⇑f a).is_some)) a}]
[decidable_pred {a : α | (λ (x : α), p x) a}]
[decidable_pred {a : β | (λ (b : β), ↥((⇑(f.symm) b).is_some)) a}]
[decidable_pred ↑(subgroup.gpowers a)]
[decidable_rel (complete_graph V).adj]
[decidable_rel (sym2.rel V)]
[decidable_rel f.same_cycle]
[decidable_rel has_dvd.dvd]
[decidable_rel has_le.le]
[decidable_rel has_lt.lt]
[decidable_rel setoid.r]

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Eric Wieser]

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

[Eric Wieser]

Because update_zero.equations._eqn_1 is the bad lemma

[Anne Baanen]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Yury G. Kudryashov]

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

[Eric Wieser]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Yury G. Kudryashov]

For me difference between update_zero and finprod is that finprod is irreducible which means "don't unfold, use API".

[Yury G. Kudryashov]

But probably Mario is right about update_zero too.

[Eric Wieser]

So your rule would be, the API around finprod should always accept a decidable argument rather than finding one from the environment?

[Mario Carneiro]

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]

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

[Random Issue Bot]

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?

[Random Issue Bot]

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?

[Random Issue Bot]

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?

[Random Issue Bot]

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?