## 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 $\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: Dec 20 2023 at 11:08 UTC