# Zulip Chat Archive

## 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 },
{ 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 (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):

But it already has

```
-- 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 },
{ 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 (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