The Coq mailing list

[Robert Rand <rrand AT seas.upenn.edu>]

But doesn't it know that /y = x by my second hint? It's not clear to me if I'd need to keep adding more hints specific to the equation, or if there's some sufficient subset for equations with multiplication and division of sqrt2. 

On Thu, Jun 6, 2019, 12:56 PM Laurent Thery <Laurent.Thery AT inria.fr> wrote:

On 6/6/19 6:36 PM, Robert Rand wrote:
>
> Any idea what's going on with field_simplify_eq and if there's anything
> I can do besides wrap it in a repeat? (And likewise for field, with the
> alternative being said repeat followed by `field`.)

Ok the field works by abstracting away the goal
things that it does not know becomes variables:
in your example : sqrt(2) becomes x and sqrt(/2) becomes y
so it is missing that x * y = 1

If you add it it works.

Lemma test : 1 / √ 2 - / √ (/ 2) * (/ 2 * 1)  = 0.
Proof.
intros.
assert (H : 0 <= 2) by admit.
assert (H2 : sqrt 2 * sqrt (/ 2) = 1) by admit.
field [(pow2_sqrt _ H) H2].
Qed.