## Stream: general

### Topic: noncomm_ring regression

#### Yakov Pechersky (Apr 01 2021 at 05:33):

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 },
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 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 (Apr 01 2021 at 07:48):

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

#### Eric Wieser (Apr 01 2021 at 07:50):

What's the goal state that noncomm_ring leaves behind?

#### Yakov Pechersky (Apr 01 2021 at 07:50):

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 (Apr 01 2021 at 07:51):

In the new commit, the left over goal is

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


#### Eric Wieser (Apr 01 2021 at 07:51):

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

#### Yakov Pechersky (Apr 01 2021 at 07:52):

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 (Apr 01 2021 at 07:53):

Why did it work before ?? mysteries abound

#### Eric Wieser (Apr 01 2021 at 07:53):

Does abel close that goal in the old commit?

#### Eric Wieser (Apr 01 2021 at 07:54):

(the leftover one, that is)

#### Yakov Pechersky (Apr 01 2021 at 08:04):

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 (Apr 01 2021 at 08:06):

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

#### Eric Wieser (Apr 01 2021 at 08:08):

So then the simp is behaving differently then?

#### Yakov Pechersky (Apr 01 2021 at 08:09):

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 (Apr 01 2021 at 08:09):

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

#### Yakov Pechersky (Apr 01 2021 at 08:16):

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 (Apr 01 2021 at 08:20):

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

#### Mario Carneiro (Apr 01 2021 at 08:31):

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

#### Yakov Pechersky (Apr 01 2021 at 08:32):

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

#### Mario Carneiro (Apr 01 2021 at 08:32):

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

#### Mario Carneiro (Apr 01 2021 at 08:33):

a ^ b.succ is not a ring expression

#### Mario Carneiro (Apr 01 2021 at 08:33):

it sounds like you want noncomm_ring_exp

#### Yakov Pechersky (Apr 01 2021 at 08:33):

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


#### Mario Carneiro (Apr 01 2021 at 08:34):

yeah, because x ^ 37 is a ring expression

#### Yakov Pechersky (Apr 01 2021 at 08:34):

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

#### Yakov Pechersky (Apr 01 2021 at 08:34):

Great, I'll close the PR.

#### Yakov Pechersky (Apr 01 2021 at 08:40):

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

#### Mario Carneiro (Apr 01 2021 at 08:42):

I don't think it was ever intended to work

#### Mario Carneiro (Apr 01 2021 at 08:42):

maybe simp did it by accident?

#### Yakov Pechersky (Apr 01 2021 at 08:43):

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

#### Mario Carneiro (Apr 01 2021 at 08:44):

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 (Apr 01 2021 at 08:52):

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 },
-- 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 (Apr 01 2021 at 08:53):

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 (Apr 01 2021 at 08:53):

Just to pin down the problem

Last updated: May 12 2021 at 04:19 UTC