type error in ring tactic

Stream: general

[Anne Baanen]

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]

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

[Anne Baanen]

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]

that's because norm_num calls simp

[Anne Baanen]

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]

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]

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

[Anne Baanen]

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]

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]

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]

I pushed a fix for this to the PR

[Anne Baanen]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Anne Baanen]

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

[Anne Baanen]

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]

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]

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

[Rob Lewis]

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

[Anne Baanen]

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

[Anne Baanen]

Thanks for the fix!