unknown tactic

Stream: lean4

[Floris van Doorn]

The code

example : True := by nope

produces the error unknown tactic. How hard would it be to print the error unknown tactic 'nope'?

I had some people using suggest (my alias for library_search) and they got the unknown tactic error. I realize only a few hours later that this error was because the sugges tactic is an unknown tactic, and the suggest tactic was still running.

[Mario Carneiro]

should be easy, the unknown tactic tactic is an ident parser

[Patrick Massot]

I agree that Floris' suggestion will already be a great improvement but it would also be nice to fix the underlying problem that this error message shouldn't stay like this. I noticed this is indeed very confusing.

[Mario Carneiro]

I'm confused what distinction you are making. Floris's suggestion is to improve the error message, no?

[Mario Carneiro]

or do you think the behavior needs to change more radically?

[Floris van Doorn]

Patrick, are you saying that the unknown tactic error message should disappear when suggest is running. I'm not sure if that is good. I definitely want to see the goal view while Lean is running.

[Patrick Massot]

I want to see the goal but not the unknown tactic error

[Kevin Buzzard]

One could imagine that the error is cleared when the next key is pressed. In Lean 3 you used to see weird errors like unknown import data.real.basi which were confusing when in the file you've clearly typed data.real.basic.

[Patrick Massot]

Yes exactly. Here the outdated error stays on display for a very long time because Lean is working on something else.

[Mario Carneiro]

Kevin Buzzard said:

One could imagine that the error is cleared when the next key is pressed. In Lean 3 you used to see weird errors like unknown import data.real.basi which were confusing when in the file you've clearly typed data.real.basic.

This is annoying though because while you are typing you see no information, rather than an unbroken (if delayed) infoview

[Mario Carneiro]

I would much rather have it hold the last message if it has nothing useful to display, possibly with a spinner or something to indicate it is out of date

[Mario Carneiro]

this is especially important if you are typing something based on the goal view (e.g. the type of a hypothesis), since you might forget what it was halfway through typing

[Julian Berman]

Couldn't that be mitigated by various long-running things sending more LSP diagnostics themselves, just not error ones?

[Julian Berman]

E.g. the Processing... LSP info diagnostic messages -- or tactic specific ones saying suggest is searching through lemmas or whatever that gets sent on start and cleared when it's done

[Floris van Doorn]

Mario Carneiro said:

I would much rather have it hold the last message if it has nothing useful to display, possibly with a spinner or something to indicate it is out of date

A visual indication on all outdated message would also be very helpful! With "outdated message" I mean here any message that is produced by a line in the "yellow bar zone" (i.e. that will be recompiled without any additional keystrokes). I think this should include the goal view, assuming the visual indication is not too obtrusive.

[Sebastian Ullrich]

Good point with the yellow bar, that should mean it's implementable in the extension without touching core

[Young]

import Mathlib.RingTheory.Polynomial.RationalRoot
import Mathlib.Algebra.Polynomial.Degree.Definitions
import Mathlib.Algebra.Polynomial.RingDivision
import Mathlib.Tactic.Linarith
import Init.SimpLemmas
import Init.Data.NeZero

open Polynomial

-- Define the polynomial f(x) = x^3 - 3x + 1
noncomputable def f : ℤ[X] := X^3 - 3 * X + 1

-- Prove that f(x) is irreducible over ℚ
theorem f_irreducible : Irreducible f := by

  -- Assume f is reducible, i.e., f = g * h, where g and h are polynomials
  intro h_red  -- Assume f is reducible, i.e., f = g * h
  obtain ⟨g, h, h_eq⟩ := h_red  -- Extract g and h from the assumption

  -- Analyze the degrees of g and h next
  have hg_deg : degree g < degree f := by
    rw [degree_mul] at h_red;
    exact lt_of_le_of_ne (degree_nonneg _) (mul_ne_zero h_red.1 h_red.2);

  -- Discuss the degree of g by cases
  cases' Nat.eq_zero_or_pos (degree g) with **g_zero** g_pos
  { -- Case 1: The degree of g is 0, i.e., g is a constant
    rw [degree_eq_zero] at g_zero
    -- Since g is a constant and f is a cubic polynomial, f cannot be reducible
    simp [f] at h_red
    linarith
  };
  { -- Case 2: The degree of g is greater than 0
    -- The degree of g is less than the degree of f (which is 3), so g cannot be a unit
    exact lt_of_le_of_ne (degree_nonneg _) (mul_ne_zero h_red.1 h_red.2)
  }

The bold part is told "unknown tactic" by Lean Infoview

[Shreyas Srinivas]

Does it work with import Mathlib.Tactic instead of import Mathlib.Tactic.Linarith

[Shreyas Srinivas]

#min_imports doesn't work very well with tactics

[Shreyas Srinivas]

Also please use code quotes for pasting lean code in zulip

[Young]

No, Mathlib.Tactic does not work : (@Shreyas Srinivas

[Shreyas Srinivas]

I think you are using math quotes. For multiline code snippets, the correct approach is #backticks

[Damiano Testa]

Are you thinking of the cases' tactic, rather than cases?

[Young]

Thanks, the code quotes have been corrected.

[Damiano Testa]

I think that this is an issue of a flawed cases syntax that mangles all errors. The source of the issue is that the initial intro does not work. However, cases masks it. If you use cases', you will see that Lean is unhappy about the final ,. Removing that, shows that the proof never really started.

[Young]

Maybe I did write it terribly... How can I fix it? By start over or make minor changes?

[Damiano Testa]

I think that an important first step is to have an informal proof of the statement. I cannot really follow the informal argument that you have in mind from the comments to the code: can you explain how you would like to prove that f is irreducible?

[Young]

1. Assume is Reducible

intro h_red  -- Assume f is reducible, i.e., f = g * h
obtain ⟨g, h, h_eq⟩ := h_red  -- Extract g and h from the assumption

• intro h_red: Introduces the assumption h_red, which states that f(x) is reducible. That is, there exist polynomials g and h such that f=g⋅h.
• obtain ⟨g, h, h_eq⟩ := h_red: Deconstructs the assumption h_red into the polynomials g and h, and the equation f=g⋅h.

2. Analyze the Degrees of and

have hg_deg : degree g < degree f := by
  rw [degree_mul] at h_red;
  exact lt_of_le_of_ne (degree_nonneg _) (mul_ne_zero h_red.1 h_red.2);

• degree_mul: A theorem about polynomial multiplication that tells us that degree(f)≥degree(g)+degree(h).
• degree_nonneg _: Ensures that the degrees of g and f are non-negative.
• mul_ne_zero h_red.1 h_red.2: Ensures that both g and h are non-zero polynomials, i.e., their degrees are strictly greater than 0.

This step concludes that degree(g)<degree(f), i.e., the degree of g is strictly less than the degree of f.

3. Case Analysis on the Degree of

cases' Nat.eq_zero_or_pos (degree g) with g_zero g_pos
{ -- Case 1: The degree of g is 0, i.e., g is a constant
  rw [degree_eq_zero] at g_zero
  -- Since g is a constant and f is a cubic polynomial, f cannot be reducible
  simp [f] at h_red
  linarith
};
{ -- Case 2: The degree of g is greater than 0
  -- The degree of g is less than the degree of f (which is 3), so g cannot be a unit
  exact lt_of_le_of_ne (degree_nonneg _) (mul_ne_zero h_red.1 h_red.2)
}

Here, we perform a case analysis on the degree of g.

Case 1: degree(g)=0 (i.e., g is a constant)

• rw [degree_eq_zero] at g_zero: Uses degree_eq_zero to apply the assumption that g has degree 0, meaning g is a constant.
• simp [f] at h_red: Simplifies f=g⋅h using the fact that f is a cubic polynomial.
• linarith: This tactic is used to solve linear inequalities, which will lead to a contradiction since f is cubic, but g is constant. Thus, f cannot be reducible.

Case 2: degree(g)>0

• exact lt_of_le_of_ne (degree_nonneg _) (mul_ne_zero h_red.1 h_red.2): In this case, degree(g) is less than degree(f), but since both g and h are non-zero polynomials, neither g nor h can be units. This implies g cannot be a unit, leading to a contradiction because f would then have to factor into polynomials of lower degree.

[Ruben Van de Velde]

Does the proof work now?

[Damiano Testa]

I don't think that this argument is correct: it does not seem to deal correctly with the case in which a factor has degree 0, for instance.

[Young]

The proof does not work now...

[Young]

@Damiano Testa Maybe you are right, degree(0)=-∞. I have ignored that.

[Damiano Testa]

I was referring to the case in which a factor has degree equal to 0, so is a (non-zero) constant.

[Damiano Testa]

The Lean sketch and the comments do not argue in any way anything close to Gauss' lemma.