Zulip Chat Archive

Stream: general

Topic: type error in ring tactic


Anne Baanen (Oct 15 2019 at 15:03):

I was trying out some edge cases of ring, and the following code failed

  import tactic.ring
  example (n : ℕ) (a : ℤ) : a^(n^0) = a^1 := by ring

with a type error:

error: type mismatch at application
  tactic.ring.subst_into_pow a (n ^ 0) (tactic.ring.horner 1 a 1 0) 1
term
  1
has type
  ℤ
but is expected to have type
  ℕ
⊢ 0 = 1

I think the problem is that ring simplifies n^0 to 1 : ℤ instead of 1 : ℕ. With the variable a : ℕ it works.

Mario Carneiro (Oct 15 2019 at 15:19):

the type error is a problem, but ring isn't supposed to be able to solve this anyway

Anne Baanen (Oct 15 2019 at 15:24):

Yeah, I'm aware that ring doesn't really support this. On the other hand, a^(n^0) = a^1 := by norm_num also works, so it seems reasonable to me that ring shouldn't fail here either.

Mario Carneiro (Oct 15 2019 at 15:25):

that's because norm_num calls simp

Anne Baanen (Oct 28 2019 at 13:32):

I got the same type error again:

import tactic.ring
example (x : ) : x ^ (2 + 2) = x^4 := by ring

I decided to investigate, and it seems to arise from:

meta def eval : expr  ring_m (horner_expr × expr)
...
| e@`(@has_pow.pow _ _ %%P %%e₁ %%e₂) := do
  (e₂', p₂)  eval e₂,

Since eval assumes its argument is of a fixed α (here ), but the exponent is in , we get a type error. One fix is to replace eval with norm_num (which would work, since we don't use the horner_expr data of `e₂'). I just tested this change, and mathlib compiles with the change.

Thoughts?

Reid Barton (Oct 28 2019 at 13:35):

My thought is what about things like a^(n + 1) = a^(1 + n), but now I don't know whether we're outside the scope of what ring is supposed to do

Mario Carneiro (Oct 28 2019 at 13:36):

yeah, those arguments have to be closed numerals so norm_num should work

Anne Baanen (Oct 28 2019 at 13:37):

I'm actually working on a tactic that is designed to deal with expressions like a^(n + 1) = a^(1 + n), so I'm not worried about ring being too powerless :)

Anne Baanen (Oct 28 2019 at 13:42):

I just tested this change, and mathlib compiles with the change.

Hmm, I must have done something wrong when testing it. Now this goal in mathlib/src/data/polynomial.lean:2385:2 isn't solved: (x + y) * (y ^ 2 * z + (x * x ^ n + (↑n + 1) * x ^ n * y)) = x * (x * x ^ n) + ((↑n + 2) * (x * x ^ n) * y + (z * x + (y * z + (↑n + 1) * x ^ n)) * y ^ 2)

Mario Carneiro (Oct 28 2019 at 13:42):

I suppose you could recognize that as a^n * a where a^n is an atom; or you could operate recursively in the argument with a different type (so you could do a ^ (x ^ 2 - y ^ 2) = a ^ ((x + y) * (x - y))

Mario Carneiro (Oct 28 2019 at 13:44):

I pushed a fix for this to the PR

Anne Baanen (Oct 28 2019 at 13:44):

Yeah, changing the type in evaling the exponent seems doable; it's what I do in my new tactic.

Mario Carneiro (Oct 28 2019 at 13:45):

but travis takes just long enough for me to forget that I was compiling before it reports an error

Mario Carneiro (Oct 28 2019 at 13:46):

I think this is going outside ring's intended domain though. If you have a ring equality stuffed in an exponent you should first use congr or other things designed for it

Anne Baanen (Oct 28 2019 at 14:12):

I used norm_num and it seems I get less errors than the Travis build using norm_num.derive.

Anne Baanen (Oct 28 2019 at 14:12):

The difference between tactic.norm_num and tactic.norm_num.derive is that derive supports more expressions, right?

Anne Baanen (Oct 28 2019 at 14:21):

Ah, it's because tactic.norm_num threw an error so the ring tactic went over to simplification mode which just happened to end up with an equality, while tactic.norm_num.derive didn't throw an error and didn't reach the equality immediately

Anne Baanen (Oct 28 2019 at 14:28):

It seems that going to norm_num.derive makes the following not work anymore:

example (a n : ) : a ^ n = a ^ n := by ring

Rob Lewis (Oct 28 2019 at 14:32):

Tim, did you see Mario's PR here? https://github.com/leanprover-community/mathlib/pull/1557

Rob Lewis (Oct 28 2019 at 14:32):

It looks like derive was failing on input that was already a numeral. Mario added derive'.

Anne Baanen (Oct 28 2019 at 14:49):

Aha, I didn't check the other changes in the PR.

Anne Baanen (Oct 28 2019 at 14:49):

Thanks for the fix!


Last updated: Dec 20 2023 at 11:08 UTC