The Coq mailing list

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

Thanks, that was quite helpful.

(I didn't realize you could pass arguments to field_simplify and the manual only seems to specify the possibility for one of the three field tactics: https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.field-simplify) 

(It's also a bit of a shame that it only takes equalities without preconditions, which limits its use in this instance.)

Unfortunately, I've run into some issues which you can see in the following example:

```

Require Import Reals.

Open Scope R_scope.
Notation "√ x" := (sqrt x) (at level 0) : R_scope.

Lemma pow2_sqrt : forall x:R, 0 <= x -> (√ x) ^ 2 = x.
Proof. intros; simpl; rewrite Rmult_1_r, sqrt_def; auto. Qed.

Lemma sqrt_inv : forall (r : R), 0 < r -> √ (/ r) = (/ √ r)%R.
Proof.
  intros.
  replace (/r)%R with (1/r)%R.
  rewrite sqrt_div_alt, sqrt_1;trivial.
  unfold Rdiv. rewrite Rmult_1_l. easy.
  unfold Rdiv. rewrite Rmult_1_l. easy.
Qed.  

Lemma Rle_0_2 : 0 <= 2. Proof. left. apply Rlt_0_2. Qed.

Lemma test : 1 / √ 2 = / √ (/ 2) * (/ 2 * 1).

Proof.

Try 1: field [(pow2_sqrt 2 Rle_0_2) (sqrt_inv 2 Rlt_0_2)]. (* fails with "Tactic failure: not a valid field equation" *)

Try 2: field_simplify [(pow2_sqrt 2 Rle_0_2) (sqrt_inv 2 Rlt_0_2)]. (* Some progress, but I don't expect much since it doesn't handle inverses *) 

Try 3: 

field_simplify_eq [(pow2_sqrt 2 Rle_0_2) (sqrt_inv 2 Rlt_0_2)]. (* Gets us to: 2 * / √ (2) = √ (2) *)

field_simplify_eq [(pow2_sqrt 2 Rle_0_2) (sqrt_inv 2 Rlt_0_2)]. (*Second execution returns 2 = 2 *)

```

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`.)

(Also, if I call field_simplify with on 2=2, I get 2/1/1 = 2/1/1, which is kind of strange.)

Thanks,

Robert

On Wed, Jun 5, 2019 at 4:06 AM Laurent Thery <Laurent.Thery AT inria.fr> wrote:

>> Is there any tactic that is like field_simplify but can deal with roots?
>> (Are there any tactics to deal  with roots?) If not, any thoughts on how
>> difficult it would be to extend field_simplify to handle roots?
>
> an easy hack that could be enough in simple cases would be to do
> some preprocessing before calling field_simplify
>  renaming in the goal first (sqrt x) by y an then x by y^2.

Here is an example:

Require Import Reals.
Open Scope R_scope.

Lemma Rr x : 0 <= x -> x = sqrt x ^ 2.
Proof. now intros x0; simpl; rewrite -> Rmult_1_r, sqrt_sqrt. Qed.

Goal forall x y, (0 <= x) -> (0 <= y) ->
((sqrt x) + (sqrt y))^2 - x - y = 2 * sqrt x * sqrt y.
Proof.
intros x y H1 H2.
field [(Rr _ H1) (Rr _ H2)].
Qed.