Zulip Chat Archive
Stream: mathlib4
Topic: Data.Int.Gcd - NormNum
Riccardo Brasca (Dec 19 2022 at 14:44):
In #981 I am porting data/int/gcd. The only errors left are in the section relative to `NormNum. Can someone who knows tactic writing have a quick look? Thanks!
Heather Macbeth (Dec 19 2022 at 22:11):
This is actually the int.gcd norm_num extension, so I guess it's not surprising that mathport produces garbage. I guess this is a task for @Mario Carneiro ?
Mario Carneiro (Dec 19 2022 at 22:12):
yep, comment the section out completely and leave a TODO
Riccardo Brasca (Dec 20 2022 at 16:37):
There is a linter error I don't understand:
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 @Nat.gcd_b_zero_right /- unnecessary have this : 0 % Nat.succ n✝ < Nat.succ n✝ -/
where gcd_b_zero_right is
@[simp]
theorem gcd_b_zero_right {s : ℕ} (h : s ≠ 0) : gcdB s 0 = 0 := by
unfold gcdB xgcd
induction s
· exact absurd rfl h
· simp [xgcdAux]
There is no have or suffice, so I don't really know what do to.
Kevin Buzzard (Dec 20 2022 at 17:22):
Ha ha, this is quite funny. I think the problem is here:
/-- Helper function for the extended GCD algorithm (`nat.xgcd`). -/
def xgcdAux : ℕ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ
| 0, _, _, r', s', t' => (r', s', t')
| succ k, s, t, r', s', t' =>
have : r' % succ k < succ k := mod_lt _ <| (succ_pos _).gt
let q := r' / succ k
xgcdAux (r' % succ k) (s' - q * s) (t' - q * t) (succ k) s t
There's a have there, which is necessary in general, and is presumably embedded in the term. But sometimes when the definition is being used, in the application the have is not necessary so the linter complains :-)
Shreyas Srinivas (Dec 20 2022 at 17:27):
Kevin Buzzard said:
Ha ha, this is quite funny. I think the problem is here:
/-- Helper function for the extended GCD algorithm (`nat.xgcd`). -/ def xgcdAux : ℕ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ | 0, _, _, r', s', t' => (r', s', t') | succ k, s, t, r', s', t' => have : r' % succ k < succ k := mod_lt _ <| (succ_pos _).gt let q := r' / succ k xgcdAux (r' % succ k) (s' - q * s) (t' - q * t) (succ k) s tThere's a
havethere, which is necessary in general, and is presumably embedded in the term. But sometimes when the definition is being used, in the application thehaveis not necessary so the linter complains :-)
Shreyas Srinivas (Dec 20 2022 at 17:28):
In any case, how do we tell the linter that this is fine?
Kevin Buzzard (Dec 20 2022 at 17:35):
Well you can use the nolint attribute, but it might be worth running the example past the linter experts I guess?
Kevin Buzzard (Dec 20 2022 at 17:36):
Last updated: Dec 20 2023 at 11:08 UTC