Ring tactic on `(n+1)^2=n^2+2n+1`

Stream: mathlib4

[Kaiyu Yang]

Hi,

I found that the ring tactic can prove

import Mathlib.Tactic.Ring

open Nat

example (n : Nat) : (n + 1) ^ 2 = n ^ 2 + 2 * n + 1 := by
  ring

but cannot prove

import Mathlib.Tactic.Ring

open Nat

example (n : Nat) : (succ n) ^ 2 = n ^ 2 + 2 * n + 1 := by
  ring  -- failed

Is that expected? What would be a workaround? Thank you!

[Joël Riou]

Just do simp only [succ_eq_add_one] before ring.

[Damiano Testa]

This came up before: ring does not support Nat.succ, except that in some cases defeq with n + 1 gets in the way and makes ring work!

[Kaiyu Yang]

Ah, I see. Thanks a lot! I'm actually quite surprised that basic facts such as succ_eq_add_one is not supported by ring nor tagged by @[simp].

[Kaiyu Yang]

As related question, it can prove

import Mathlib.Tactic.Ring

open Nat

example (n : Nat) : 2 * n + 3 + (n + 1) ^ 2 - 1  = (n + 1 + 1) ^ 2 - 1 := by
  ring

but cannot prove

import Mathlib.Tactic.Ring

open Nat

example (n : Nat) : 2 * n + 3 + ((n + 1) ^ 2 - 1)  = (n + 1 + 1) ^ 2 - 1 := by
  ring  -- failed

[Patrick Massot]

Nat subtraction is a nightmare, you should try really hard to avoid it.

[Ruben Van de Velde]

Presumably in the first case it'll normalize the additions within the outer natural subtraction and that finishes the proof. Does it tell you to use ring_nf?

[Kaiyu Yang]

Does it tell you to use ring_nf?

Yes, it does.

[Kaiyu Yang]

Nat subtraction is a nightmare, you should try really hard to avoid it.

I changed the Nat in the second example to ℤ and it worked. :rolling_on_the_floor_laughing:

[Kevin Buzzard]

succ is not part of the structure of a ring, so why should ring know about it? The same comment holds for subtraction of naturals. That has nothing to do with rings!

[Heather Macbeth]

I hope we will soon decide on how to make a standard induction tactic for mathlib which invokes "0" and "n + 1", so that no one in mathlib ever encounters "succ" at all.

[Kaiyu Yang]

@Kevin Buzzard That makes sense. I'm wondering if there is a tactic in Lean/mathlib that can automate this kind of trivial calculations even if they do not fall into the responsibility of ring.

[Patrick Massot]

Kevin Buzzard said:

succ is not part of the structure of a ring, so why should ring know about it? The same comment holds for subtraction of naturals. That has nothing to do with rings!

This is a bit subtle, so I will try to explain Kevin's comment a bit more. As explained at the beginning of the ring section in MIL, the ring tactic is doubly misnamed: it should be called commsemiring since it assumes commutativity and works in semirings. However, Kaiyu's goal does not follow from the axioms of semirings, it requires knowing something special about Nat since the subtraction operation simply does not appear at all in the definition of semirings.

[Adam Topaz]

Heather Macbeth said:

I hope we will soon decide on how to make a standard induction tactic for mathlib which invokes "0" and "n + 1", so that no one in mathlib ever encounters "succ" at all.

I wonder whether we can add support for tagging induction lemmas as "default" and have the usual induction tactic use the default lemma by default. Either that or we could make the @[match_pattern] attribute more flexible/powerful.

[Patrick Massot]

Adam, this already exists, but tagging the nice induction principle for Nat breaks cases.

[Patrick Massot]

This has been discussed many times.

[Patrick Massot]

For instance the first search result is https://leanprover.zulipchat.com/#narrow/stream/187764-Lean-for-teaching/topic/An.20exercise.20using.20induction/near/370365516

[Adam Topaz]

Ah I didn't know that the eliminator attribute had this behavior.

[Adam Topaz]

That's not the only issue, it seems. It seems that adding such an eliminator also breaks the ability to write structured proofs with induction. I can't get any permutation of (n+1), succ n, whatever, to work in the following example:

import Mathlib.Tactic

@[eliminator]
theorem Nat.rec' {motive : Nat → Sort u}
    (zero : motive 0) (add_one : (n : Nat) → motive n → motive (n + 1)) (t : Nat) :
    motive t :=
  Nat.rec zero add_one t

example (P : Nat → Prop) : P n := by
  induction n with
  | zero => sorry
  | succ n ih => sorry

The only thing I can get to work is the following:

example (P : Nat → Prop) : P n := by
  induction n with
    | zero => sorry
    | _ n ih => sorry

[Joachim Breitner]

Why not

import Mathlib.Tactic

@[eliminator]
theorem Nat.rec' {motive : Nat → Sort u}
    (zero : motive 0) (add_one : (n : Nat) → motive n → motive (n + 1)) (t : Nat) :
    motive t :=
  Nat.rec zero add_one t

example (P : Nat → Prop) : P n := by
  induction n
  case zero => sorry
  case add_one n ih => sorry

[Adam Topaz]

Sure, that also works, although it's a bit verbose, and our nice code action for induction doesn't do this by default :)

[Joachim Breitner]

Or

example (P : Nat → Prop) : P n := by
  induction n with
  | zero => sorry
  | add_one n ih => sorry

(not sure if there is a difference between using with and using case; I use the latter usually and am confused that we have both)

[Adam Topaz]

aha!

[Joachim Breitner]

Ah, yes, the code action does something wrong

[Adam Topaz]

case is still useful when there are many cases to consider, whereas I tend to use| when there aren't too many. I think both are useful.

[Adam Topaz]

Ok, so what I said above really is just a bug in the code action.

[Patrick Massot]

See also std4#311

[Joachim Breitner]

Is there a difference beyond minor syntactic variation? Syntax variability means non-uniformity, and that comes at the cost of some amount of confusion. I guess with with there is an error message for missing cases, whereas with case you just have some more goals around.

[Joachim Breitner]

Ah, and there is also induction' … with, doing something different altogether. There must be a reason for having three ways, but what are they?
I also wonder, with name goals, if the code action even needs to be induction-specific. Would a code action that detects that new named goals have created in general not work equally well for induction as well as for many other tactics (e.g. refine)?
(I am derailing this thread, sorry for not starting a new one.)

[Ruben Van de Velde]

induction' exists only to ease the port from lean 3

[Ruben Van de Velde]

(It matches the syntax that lean 3 induction had)

[Joachim Breitner]

That's what I was hoping for. So at least that can eventually be phased out and make space in our brains :-)

[Adam Topaz]

Joachim Breitner said:

and make space in our brains :-)

... I need some more of that :-/

[Adam Topaz]

In any case, I don't think it would be too hard to modify docs#Lean.Meta.getCustomEliminator? and docs#Lean.Meta.CustomEliminator itself to include some isInd : Bool parameter that says whether or not the eliminator is for induction or cases.

[Adam Topaz]

such a flag is already present in the induction and cases tactics themselves.

[Ruben Van de Velde]

I'd say induction with encourages a more "rigid" proof structure. Whether that's good depends on your personal style and the proof at hand

[Joachim Breitner]

You mean it’s more rigid because you *have * to name all the cases, and can’t, for example mix . with case focusing? Or is there some other form of rigidity that I am missing? And maybe more importantly: Is that a form of rigidity that we want for induction specifically, and not for every multi-goal tactic?
(I remember that either Coq or Isabelle had an option that would complain if a tactic would produce multiple subgoals and they were not properly focused with bullets or named caess.)

Reading through the code I see that with | supports a tactic to run first on all cases, and supports running tactics on multiple goals. So that’s presumably some extra power that’s not (easily) available with case.

[Adam Topaz]

I made some changes to a fork of core here: github.com/adamtopaz/lean4
With those changes, the following works:

@[induction_eliminator]
theorem Nat.rec' {motive : Nat → Sort u}
    (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) (t : Nat) :
    motive t :=
  Nat.rec zero succ t

@[cases_eliminator]
theorem Nat.cases' {motive : Nat → Sort u}
    (zero : motive 0) (succ : (n : Nat) → motive (n + 1)) (t : Nat) :
    motive t :=
  Nat.rec zero (fun n _ => succ n) t

example (P : Nat → Prop) : P n := by
  induction n with
  | zero =>
    /-
    P: Nat → Prop
    ⊢ P 0
    -/
    sorry
  | succ n ih =>
    /-
    P: Nat → Prop
    n: Nat
    ih: P n
    ⊢ P (n + 1)
    -/
    sorry

example (P : Nat → Prop) : P n := by
  cases n with
  | zero =>
    /-
    P: Nat → Prop
    ⊢ P 0
    -/
    sorry
  | succ n =>
    /-
    P: Nat → Prop
    n: Nat
    ⊢ P (n + 1)
    -/
    sorry

[Adam Topaz]

(It took more time to figure out how to develop in core than actually making the changes :-/)

[Kevin Buzzard]

When you're developing the very very basic theory of naturals (eg addition!) you really need succ, but beyond a certain point it just gets in the way. This is very cool :-)

[Eric Wieser]

Joachim Breitner said:

Reading through the code I see that with | supports a tactic to run first on all cases,

Can you show an example?

[Joachim Breitner]

Beware, I haven't run the code, just read the docstrings:
https://github.com/leanprover/lean4/blob/170fd845f2ea818bb0c0efc8650f7125371cfc1b/src/Init/Tactics.lean#L539