Zulip Chat Archive

Stream: general

Topic: Why does `field_simp` leave this as the goal?

Keefer Rowan (Jun 03 2020 at 12:56):

Applying field_simp * to the somewhat complicated expression (where we have (innerc y y).re \ne 0 in the local context):

((innerc y y).re)⁻¹ * innerc x y * (((innerc y y).re)⁻¹ * innerc x y) * (innerc y y).re =
    ((innerc y y).re)⁻¹ * innerc x y * innerc x y

leaves the almost solved goal:

(innerc x y).abs * (innerc x y).abs * (innerc y y).re * (innerc y y).re =
    (innerc x y).abs * (innerc x y).abs * ((innerc y y).re * (innerc y y).re)

A few call to mul_assoc would solve the goal, but for some reason field_simp doesn't finish it. ring does the trick from here, but I'm wondering why field_simp can't just finish it off.

Note that everything has type R\mathbb{R}.

Sebastien Gouezel (Jun 03 2020 at 13:12):

The goal of field_simp is to clear off denominators, so that ring can finish it. So the standard invocation is really field_simp [h], ring.

Bryan Gin-ge Chen (Jun 03 2020 at 13:15):

The fact that field_simp should be used as preparation for ring is mentioned in tactic#field_simp and the docstring, but maybe it needs more emphasis?

Keefer Rowan (Jun 03 2020 at 13:17):

@Bryan Gin-ge Chen Looking at it now, it's pretty well emphasized. I just didn't look at it well enough.

Yury G. Kudryashov (Jun 04 2020 at 04:20):

BTW, can we reassign @[simp] tags so that simp works as field_simp?

Johan Commelin (Jun 04 2020 at 04:47):

I think we can, why not?

Last updated: Aug 03 2023 at 10:10 UTC