noncomm_ring regression

Stream: general

[Yakov Pechersky]

This somewhat #mwe shows a regression at having the noncomm_ring no longer discharge the goal. The offending commit is 5f1b4500f21b62968aad9bd939625cdf2b2372a6, on generalizing to nonassociative monoids @Eric Wieser .

import data.matrix.basic
import tactic.noncomm_ring

open_locale big_operators

example {R n : Type*} [comm_ring R] [fintype n] [decidable_eq n] : true :=
begin
  have hr : ∀ m (x : matrix n n R), 1 - x ^ m = (1 - x) * ∑ i in finset.range m, x ^ i,
    { intros m x,
      induction m with m hm,
      { simp },
      { rw [finset.sum_range_succ, mul_add, ←hm],
        noncomm_ring } },
  trivial
end

I found this issue by first being flagged by Rob's auto-update script for a personal repo, and the following up with a

❯ git bisect start
❯ git bisect bad master
❯ git bisect good e5c112d6d70f18efbbbda43535d0d86db12c03f6
❯ git bisect run sh -c "leanproject get-c; lean --make src/noncomm_ring_test.lean"

For some reason, I was unable to minimize the example to just the 1 - x ^ m.succ = (1 - x) * x ^ m + (1 - x ^ m) statement in the goal, then noncomm_ring doesn't close that no matter what commit I'm on.

[Eric Wieser]

It's a shame there wasn't a test for this. tactic#noncomm_ring for reference

[Eric Wieser]

What's the goal state that noncomm_ring leaves behind?

[Yakov Pechersky]

I don't understand why for an earlier commit (let's say e5c112d6d70f18efbbbda43535d0d86db12c03f6) the example is fine, but something like

example {R n : Type*} [comm_ring R] [fintype n] [decidable_eq n] (m : ℕ) (x : matrix n n R) :
  1 - x ^ m.succ = (1 - x) * x ^ m + (1 - x ^ m) :=
begin
  noncomm_ring
end

is not.

[Yakov Pechersky]

In the new commit, the left over goal is

(-1) •ℤ x ^ m.succ + 1 = 1 + (-1) •ℤ (x * x ^ m)

[Eric Wieser]

src#tactic.interactive.noncomm_ring knows nothing about pow it seems

[Yakov Pechersky]

example {R n : Type*} [comm_ring R] [fintype n] [decidable_eq n] : true :=
begin
  have hr : ∀ m (x : matrix n n R), 1 - x ^ m = (1 - x) * ∑ i in finset.range m, x ^ i,
    { intros m x,
      induction m with m hm,
      { simp },
      { rw [finset.sum_range_succ, mul_add, ←hm, pow_succ],
        noncomm_ring } },
  trivial
end

works in the new commit

[Yakov Pechersky]

Why did it work before ?? mysteries abound

[Eric Wieser]

Does abel close that goal in the old commit?

[Eric Wieser]

(the leftover one, that is)

[Yakov Pechersky]

All abel does (at the e5c112) commit to the (-1) •ℤ x ^ m.succ + 1 = 1 + (-1) •ℤ (x * x ^ m) goal is change some universes around.

[Yakov Pechersky]

(Relatedly, is there a way to check if the target is pp-equal to some other target?)

[Eric Wieser]

So then the simp is behaving differently then?

[Yakov Pechersky]

I guess I can do this:

open tactic tactic.interactive

meta def tactic.interactive.guard_change (tac : itactic) : tactic unit := do
  t ← target,
  tac,
  t' ← target,
  tactic.success_if_fail (unify t t')

example {R n : Type*} [comm_ring R] [fintype n] [decidable_eq n] (m : ℕ) (x : matrix n n R) :
  (-1) •ℤ x ^ m.succ + 1 = 1 + (-1) •ℤ (x * x ^ m) :=
begin
  guard_change { abel }, -- fails because abel didn't do anything special
  sorry
end

[Eric Wieser]

(I'm shocked at how trivial the implementation of noncomm_ring is)

[Yakov Pechersky]

I propose the following change to noncomm_ring:

             -- Expand powers to numerals.
-             pow_bit0, pow_bit1, pow_one,
+             pow_bit0, pow_bit1, pow_one, pow_succ, ←pow_succ',

[Yakov Pechersky]

Which will solve the issue, but I'll still be puzzled why that commit broke it in the first place.

[Mario Carneiro]

why not just rewrite with pow_succ? I don't think noncomm_ring supports a ^ b.succ

[Yakov Pechersky]

With #6990 it will, commuting multiplications to the left.

[Mario Carneiro]

I'm not a fan of heuristic extensions to tactics with a well defined scope

[Mario Carneiro]

a ^ b.succ is not a ring expression

[Mario Carneiro]

it sounds like you want noncomm_ring_exp

[Yakov Pechersky]

But it already has

             -- Expand powers to numerals.
             pow_bit0, pow_bit1, pow_one,

[Mario Carneiro]

yeah, because x ^ 37 is a ring expression

[Yakov Pechersky]

Feature creep? Of course, I can include pow_succ in my actual rewrite before noncomm_ring.

[Yakov Pechersky]

Great, I'll close the PR.

[Yakov Pechersky]

@Mario Carneiro do you have an idea what could have caused the regression in the first place?

[Mario Carneiro]

I don't think it was ever intended to work

[Mario Carneiro]

maybe simp did it by accident?

[Yakov Pechersky]

simp only took care of some pow_succ term that is no longer defeq?

[Mario Carneiro]

oh, if it was a change to defeq then it might also be abel when it tries to unify the two normalized expressions using refl

[Yakov Pechersky]

Here is the old commit example file. The first two examples are not solved by noncomm_ring but the third one somehow is

import data.matrix.basic
import tactic.noncomm_ring

open_locale big_operators

variables {K ι : Type*} [comm_ring K] [fintype ι] [decidable_eq ι] (m : ℕ) (A : matrix ι ι K)

example : 1 - A ^ m.succ = (1 - A) * A ^ m + (1 - A ^ m) := by noncomm_ring
example : 1 - A ^ m.succ = A ^ m * 1 - A ^ m * A + (1 - A ^ m) := by noncomm_ring

example (m : ℕ) (A : matrix ι ι K) : 1 - A ^ m = (1 - A) * (∑ i in finset.range m, A ^ i) :=
begin
  induction m with m hm,
  { simp },
  { rw [finset.sum_range_succ, mul_add, ←hm],
    -- goal is 1 - A ^ m.succ = (1 - A) * A ^ m + (1 - A ^ m) which is the same as first example
    noncomm_ring } -- somehow this doesn't fail here
end

[Eric Wieser]

Can you replace noncomm_ring with it's implementation (simp only [...] followed by abel), and prune the simp only to the minimum required?

[Eric Wieser]

Just to pin down the problem