spurious `unusedHavesSuffices` linter error?

Stream: std4

[Kevin Buzzard]

Am I right in that xgcd_aux_rec can just be marked with nolint unusedHavesSuffices and this is a spurious error? The have in xgcdAux is necessary in general but perhaps not in the application?

import Std.Tactic.Lint

open Nat

def xgcdAux : Nat → Int → Int → Nat → Int → Int → Nat × Int × Int
  | 0, _, _, r', s', t' => (r', s', t')
  | succ k, s, t, r', s', t' =>
    have : r' % succ k < succ k := mod_lt _ <| (succ_pos _)
    let q := r' / succ k
    xgcdAux (r' % succ k) (s' - q * s) (t' - q * t) (succ k) s t

theorem xgcd_aux_rec {r s t r' s' t'} (h : 0 < r) :
    xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t := by
  cases r with
  | zero => exact absurd h (Nat.lt_irrefl _)
  | succ k =>
      simp only [xgcdAux]
      rfl

#lint
/-
/- The `unusedHavesSuffices` linter reports:
THE FOLLOWING DECLARATIONS HAVE INEFFECTUAL TERM MODE HAVE/SUFFICES BLOCKS. In the case of `have` this is a term of the form `have h := foo, bar` where `bar` does not refer to `foo`. Such statements have no effect on the generated proof, and can just be replaced by `bar`, in addition to being ineffectual, they may make unnecessary assumptions in proofs appear as if they are used. For `suffices` this is a term of the form `suffices h : foo, proof_of_goal, proof_of_foo` where `proof_of_goal` does not refer to `foo`. Such statements have no effect on the generated proof, and can just be replaced by `proof_of_goal`, in addition to being ineffectual, they may make unnecessary assumptions in proofs appear as if they are used.  -/
#check @xgcd_aux_rec /- unnecessary have this : r' % succ k < succ k -/
-/

[Shreyas Srinivas]

Hello everyone, to add some context:
This is basically the only thing holding up data.nat.bits at the moment

[Shreyas Srinivas]

This in turn opens up the possibility of finishing data.nat.even_odd_rec

[Mario Carneiro]

You can add an equation lemma for xgcdAux that does not contain the rogue have

[Kevin Buzzard]

Indeed

theorem xgcdAux_zero : xgcdAux 0 s t r' s' t' = (r', s', t') := rfl
theorem xgcdAux_succ : xgcdAux (succ k) s t r' s' t' =
  xgcdAux (r' % succ k) (s' - q * s) (t' - q * t) (succ k) s t := rfl

theorem xgcd_aux_rec {r s t r' s' t'} (h : 0 < r) :
    xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t := by
  cases r with
  | zero => exact absurd h (Nat.lt_irrefl _)
  | succ k =>
      rw [xgcdAux_succ]

#lint

now works. Thanks!

[Scott Morrison]

@Kevin Buzzard, did this get PR'd somewhere? We need it on two branches.

[Kevin Buzzard]

No sorry! I've done nothing, but hopefully it's clear how to proceed in this case. I've not looked at @Shreyas Srinivas 's issue.

[Mario Carneiro]

This can also be reported to core, the equation compiler generator should try to remove these unused haves

[Scott Morrison]

I don't even know where you pulled your code from, @Kevin Buzzard. Is it a version of the code in EuclideanDomain.defs, specialised to Int/Nat?

[Kevin Buzzard]

This was a question posted by someone in another thread, which I was trying to solve.

[Mario Carneiro]

it looks like data.int.gcd to me

[Kevin Buzzard]

Here is Riccardo's question

[Kevin Buzzard]

Here is Shreyas' question but I didn't follow that one up.

[Scott Morrison]

Ah, I see. I was starting from Shreyas' question, which is not from data.int.gcd.

[Scott Morrison]

That one is probably being caused by the nolints on

 ["unusedHavesSuffices", "EuclideanDomain.xgcdAux_rec"],
 ["unusedHavesSuffices", "EuclideanDomain.xgcd_zero_left"]

but where the have term is leaking through and being detected by the linter again later.

[Scott Morrison]

In that case I feel like the linter is wrong, as the have there is being used to prove termination.

[Scott Morrison]

I can work around that lint by using decreasing_by (exact mod_lt _ _hr) instead of a have term. Not sure, @Mario Carneiro, if you'd like an issue opened on the linter for this.

[Mario Carneiro]

yes I was going to suggest that as well

[Mario Carneiro]

it's a bit more awkward in general since you get called in who knows what context

[Mario Carneiro]

I don't think the linter can do much about it, it is very far from having enough information to understand the situation

[Scott Morrison]

We're going to need to be very cautious about nolinting unusedHavesSuffices, given that it can cause linter problems with downstream declarations that use the nolinted one.

[Scott Morrison]

But I've just removed the only ones in nolints.json, so we're good for now.

[Patrick Massot]

Is this worth a mention in the porting wiki?

[Scott Morrison]

Given we only had one such nolint, and it's now gone, I'm not sure it's worth taking up the bandwidth in the wiki. Searching for unusedHavesSuffices on zulip will find this thread.

[Riccardo Brasca]

Kevin Buzzard said:

Indeed

theorem xgcdAux_zero : xgcdAux 0 s t r' s' t' = (r', s', t') := rfl
theorem xgcdAux_succ : xgcdAux (succ k) s t r' s' t' =
  xgcdAux (r' % succ k) (s' - q * s) (t' - q * t) (succ k) s t := rfl

theorem xgcd_aux_rec {r s t r' s' t'} (h : 0 < r) :
    xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t := by
  cases r with
  | zero => exact absurd h (Nat.lt_irrefl _)
  | succ k =>
      rw [xgcdAux_succ]

#lint

now works. Thanks!

Where did you write this proof? rfl doesn't work for me to prove xgcdAux_succ.

[Riccardo Brasca]

In any case I still have the linter error in 981.

[Kevin Buzzard]

I wrote it in your branch IIRC. I'll try again.

[Kevin Buzzard]

Oh there is a chance I wrote it just in core Lean when I was trying to minimise.

[Kevin Buzzard]

yeah I can't reproduce -- maybe it didn't work at all :-/

[Kevin Buzzard]

oh lol those are autoImplicit qs!

[Kevin Buzzard]

theorem xgcdAux_succ : xgcdAux (succ k) s t r' s' t' =
  xgcdAux (r' % succ k) (s' - (r' / succ k) * s) (t' - (r' / succ k) * t) (succ k) s t := rfl

works. autoImplicit is a constant source of confusing errors as well as being sometimes wonderful.

[Kevin Buzzard]

theorem gcd_a_zero_right {s : ℕ} (h : s ≠ 0) : gcdA s 0 = 1 := by
  unfold gcdA xgcd
  induction s
  · exact absurd rfl h
  · simp [xgcdAux_succ]

lints. I'll fix the errors and push.

[Riccardo Brasca]

Thanks!

[Kevin Buzzard]

Ok pushed. Hopefully there'll be a green tick in 10 minutes or so...