Unexpected errors

Stream: general

[Chris Hughes]

Just finished proving this theorem about roots of polynomials, but I'm getting the following errors and I don't understand why

unexpected occurrence of recursive function
univariate_poly.lean:574:18: warning
definition 'roots_aux' was incorrectly marked as noncomputable

It clearly should be marked as noncomputable, and I have no idea what `unexpected occurence of recursive function means

noncomputable def roots_aux : Π {p : polynomial α} (hp : p ≠ 0),
  {s : finset α // s.card ≤ degree p ∧ ∀ x, root p x ↔ x ∈ s}
| p :=
λ hp, @dite (∃ x, root p x) (classical.prop_decidable _)
  {s : finset α // s.card ≤ degree p ∧ ∀ x, root p x ↔ x ∈ s}
  (λ h, let ⟨x, hx⟩ := classical.indefinite_description _ h in
  have hpd : 0 < degree p := nat.pos_of_ne_zero
    (λ h, begin
      rw [eq_C_of_degree_eq_zero h, root, eval_C] at hx,
      have h1 : p (degree p) ≠ 0 := leading_coeff_ne_zero hp,
      rw h at h1,
      contradiction,
    end),
  have hd0 : div_by_monic p (monic_X_sub_C x) ≠ 0 :=
    λ h, by have := mul_div_eq_iff_root.2 hx;
      simp * at *,
  have wf : degree (div_by_monic p _) < degree p :=
    degree_div_by_monic_lt _ (monic_X_sub_C x)
    ((degree_X_sub_C x).symm ▸ nat.succ_pos _) hpd,
  let ⟨t, htd, htr⟩ := @roots_aux (div_by_monic p (monic_X_sub_C x)) hd0 in
  ⟨insert x t, calc (insert x t).card ≤ t.card + 1 : finset.card_insert_le _ _
    ... ≤ degree (div_by_monic p (monic_X_sub_C x)) + 1 : nat.succ_le_succ htd
    ... ≤ _ : nat.succ_le_of_lt wf,
  begin
    assume y,
    rw [mem_insert, ← htr, eq_comm, ← root_X_sub_C],
    conv {to_lhs, rw ← mul_div_eq_iff_root.2 hx},
    exact ⟨root_or_root_of_root_mul, λ h, or.cases_on h (root_mul_right_of_root _) (root_mul_left_of_root _)⟩
  end⟩)
  (λ h, ⟨∅, nat.zero_le _, by finish⟩)
using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf degree⟩]}

The full file is here https://github.com/dorhinj/leanstuff/blob/master/univariate_poly.lean

[Kenny Lau]

it happens with equation compilers

[Kenny Lau]

since they provide you with the theorem you're trying to prove, in case you want to do recursion

[Kenny Lau]

but some tactics touch every local hypothesis

[Kenny Lau]

Suspects I spot: contradiction, simp * at *

[Kenny Lau]

the latter has a higher chance of being the perpetrator

[Chris Hughes]

I don't think it's that or it would have asked me to prove something. I replaced both of those with admit and I still get the error.

[Kenny Lau]

how did you define polynomial?

[Kenny Lau]

can you prove strong induction?

[Chris Hughes]

polynomial is ℕ →₀ α. I have proved and defined stuff in this manner before. I have just rewritten this function using well_founded.fix, and it works, but it would be nice to know what's going on.

[Kenny Lau]

[Mario Carneiro]

noooo lean memes

[Andrew Ashworth]

I wouldn't feel bad about directly using well_founded.fix... the using_well_founded tactic is undocumented and hard to debug unless you know what's going on behind the scenes

[Mario Carneiro]

I don't think this should be a problematic definition, but I can't run it as is

[Andrew Ashworth]

(but maybe I'm just bad at Lean)

[Mario Carneiro]

(it's not actually a tactic, it's a keyword)

[Andrew Ashworth]

(shows how much I've used it... I needed wf recursion a few months ago and struggled with well_founded.fix, and since it worked, never bothered to figure out using_well_founded)

[Mario Carneiro]

the offending tactic is by finish at the end

[Kenny Lau]

I must be blind

[Mario Carneiro]

use by clear roots_aux; finish instead

[Mario Carneiro]

I found it by just replacing things by sorry until the error went away