How to replace `induction'` and `norm_num`?

Stream: mathlib4

[Nick Adfor]

We all know that Mathlib code should use #min_imports to keep imports minimal. However, since I have been using Aristotle to help me with proofs, the code it generates includes induction' and norm_num, which cause the code to fail after #min_imports. I have checked some Mathlib files and noticed that they do not seem to use induction' or norm_num. What should I do in this case? Is this an issue with the design of induction', norm_num, or #min_imports? Should I avoid using these when preparing a PR for Mathlib?

The code is as follows. I want to PR to Mathlib/Combinatorics/SimpleGraph/Bipartite
bipartite_iff_all_cycles_even

The discussion on the code is here #mathlib4 > Formalizing Graph Theory - The Odd Cycle Theorem in Lean

[Ruben Van de Velde]

It's an issue with #min_imports in the sense that it doesn't look at the tactics used in the proof script, but just at the proof terms that are generated

[Ruben Van de Velde]

In any case, code for mathlib should not use induction'

[Ruben Van de Velde]

Also, someone was working on a new shake tool. I'm not sure if that handles the issue better

[Nick Adfor]

I'll try to check shake later. And the question now becomes how to replace induction' and norm_num (as the topic theme). As these are tactic design so not easy to find using something like norm_num? just like aesop?

[Nick Adfor]

But here Kim said forbid shake
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib.20has.20moved.20to.20the.20new.20module.20system

[Kyle Miller]

Why are you wanting to avoid norm_num? It's used a couple thousand times in Mathlib — it hasn't been deprecated, has it?

[Ruben Van de Velde]

No, you're absolutely welcome to use norm_num. It's just induction' that needs to be replaced by induction

[Kyle Miller]

For how to replace induction', here's an example:

      induction' p with u v pᵥ _ ih <;> simp_all +decide

becomes

      induction p with simp_all +decide
      | nil => sorry
      | cons h p ih => sorry

Note that I didn't try to copy the variable names in the cons case, since they don't seem to make any sense. The ih variable in induction' is not the induction hypothesis...

Also note that this is not acceptable for mathlib, since simp_all +decide counts as a non-terminal simp.

[Kyle Miller]

I'm looking at even_length_iff_even_bypass_length by the way.

[Kyle Miller]

(All the uses of ‹G.Walk pᵥ _› in the proof are indicating that the variable naming has gone wrong.)

[Nick Adfor]

Kyle Miller said:

(All the uses of ‹G.Walk pᵥ _› in the proof are indicating that the variable naming has gone wrong.)

I do wonder why in induction', ‹G.Walk pᵥ _› can be used but in induction it cannot be used.

[Nick Adfor]

I try to fix for a while and here's more problem. First as mentioned about norm_num, I'm really confused about why here it cannot use. But one can see what happed after #min_imports here

[Nick Adfor]

And about induction', it permits me using ‹G.Walk pᵥ _› but in induction one cannot use (it may be because of cutting variable u, v and p_v). If just fix it by replacement, some implict parts will show error (like grind, it is totally an implict one) see here

[Nick Adfor]

The conflict between Aristotle AI's unconventional style (such as leaving aesop and simp_all open) and Mathlib's standard conventions has been discussed in a previous post by Aristotle, though a satisfactory solution remains elusive. A new issue has now arisen concerning min_imports: Is there a way to add additional imports to permit the use of induction'?

[Jakob von Raumer]

Yes. Add the file where induction' is defined as import.

[Nick Adfor]

Jakob von Raumer said:

Yes. Add the file where induction' is defined as import.

It is import Mathlib.Tactic.Cases. Maybe we should try to find out why #min_imports cannot show it...

[Nick Adfor]

(deleted)

[Kyle Miller]

Nick_adfor said:

Kyle Miller said:

(All the uses of ‹G.Walk pᵥ _› in the proof are indicating that the variable naming has gone wrong.)

I do wonder why in induction', ‹G.Walk pᵥ _› can be used but in induction it cannot be used.

I didn't preserve the variable names in induction — I left this to you to work out, since the names that were already there did not correspond to their meaning (e.g. ih usually refers to an induction hypothesis). Fixing variable names like these is a requirement for passing Mathlib code review.

Nick_adfor said:

First as mentioned about norm_num, I'm really confused about why here it cannot use.

Ruben explained it well enough: #min_imports has limitations. This does not mean norm_num cannot be used in Mathlib.

[Nick Adfor]

#33257

[Nick Adfor]

Kyle Miller said:

Ruben explained it well enough: #min_imports has limitations. This does not mean norm_num cannot be used in Mathlib.

For induction', one needs import Mathlib.Tactic.Cases.
For norm_num, one needs import Mathlib.Tactic.NormNum.