Zulip Chat Archive

Stream: general

Topic: noncomm_ring regression


view this post on Zulip 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.

view this post on Zulip Eric Wieser (Apr 01 2021 at 07:48):

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

view this post on Zulip Eric Wieser (Apr 01 2021 at 07:50):

What's the goal state that noncomm_ring leaves behind?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Eric Wieser (Apr 01 2021 at 07:51):

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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 07:53):

Why did it work before ?? mysteries abound

view this post on Zulip Eric Wieser (Apr 01 2021 at 07:53):

Does abel close that goal in the old commit?

view this post on Zulip Eric Wieser (Apr 01 2021 at 07:54):

(the leftover one, that is)

view this post on Zulip 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.

view this post on Zulip 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?)

view this post on Zulip Eric Wieser (Apr 01 2021 at 08:08):

So then the simp is behaving differently then?

view this post on Zulip 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

view this post on Zulip Eric Wieser (Apr 01 2021 at 08:09):

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

view this post on Zulip 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',

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 08:32):

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

view this post on Zulip Mario Carneiro (Apr 01 2021 at 08:32):

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

view this post on Zulip Mario Carneiro (Apr 01 2021 at 08:33):

a ^ b.succ is not a ring expression

view this post on Zulip Mario Carneiro (Apr 01 2021 at 08:33):

it sounds like you want noncomm_ring_exp

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 08:33):

But it already has

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

view this post on Zulip Mario Carneiro (Apr 01 2021 at 08:34):

yeah, because x ^ 37 is a ring expression

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 08:34):

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

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 08:34):

Great, I'll close the PR.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 01 2021 at 08:42):

I don't think it was ever intended to work

view this post on Zulip Mario Carneiro (Apr 01 2021 at 08:42):

maybe simp did it by accident?

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 08:43):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Apr 01 2021 at 08:53):

Just to pin down the problem


Last updated: May 12 2021 at 04:19 UTC