Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] field_simplify for radicals

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] field_simplify for radicals


Chronological Thread 
  • From: Robert Rand <rrand AT seas.upenn.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] field_simplify for radicals
  • Date: Thu, 6 Jun 2019 12:36:00 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=rrand AT seas.upenn.edu; spf=Pass smtp.mailfrom=rrand AT seas.upenn.edu; spf=None smtp.helo=postmaster AT mx0b-000c2a01.pphosted.com
  • Ironport-phdr: 9a23:xx003xzExppbWFTXCy+O+j09IxM/srCxBDY+r6Qd1O0fIJqq85mqBkHD//Il1AaPAdyCrasY16GP6/qocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmSexbalvIBi5ogjdudQajZd8Jq0s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlSEKPCM7/m7KkMx9lK1UoByjqBJ/zYDaY5ybOuRica7GZ9wWWXBMU9xNWyBdAI6xaZYEAeobPeZfqonwv0cArRylCgayHuPv1iJDiGPs0q08zusqDAbL3BY6H90UtnTbsc74NLwMXu+v16nE1yjDb+tI1jf77ojEaA4uruyRXb9pd8fa1EchFwTAjlqKqIzlOSuY1uULs2iB7upvT/iji2A9qwx3vzOhxd8sh5HUio8ayV3I7zh1zYc7KNGiVUJ2Yd6pHIFeuiybL4d6XN8uTmVytCs5yrAKo4C3cDQJxZg92hLSafOKfo6V6Rz5TumROy13hHd9dbK/mRmy9U+gx/X5Vsi7zFpFtTNJnsXQunwRyxPf9NKIRudg8ku7wTaPzwDT6uZfIUAoi6XUNoQtzaI3lpoWqUjDHyn2l1vqjKKOa0kp9eul5/76brjnqJKQLZJ4hwH+P6g0lMGyAPw0Mg0UUGia/eS82qfj/Ur8QLhSlP02iLPWsJbHKskAva62HRVa0p055xaiFzepztIYnX8dIF1bZR2HkpDlO0vSL/DgEfe/n1OsnS93yPDBJ73tG4nCLnzekLj6Zrt98E5dyA8rzd9F/Z5UC7cBIOjyWkDrrtDYAAU5YESIxLPsD8w43YcDU0qOBLWYOeXcqwym/OUqdtOLboIPpH7HIv4pr6r0l3Y/lXcGcKCym4YPZXa+WPlqPhPKMjLXnt4dHDJS7UIFR+vwhQjaCGIBVzOJR6s5owoDJse+F46aGNK2jbWamjqjE5tQIG1KFwLUSCa6R8C/Q/4JLRmqDIpkmz0AW6KmTtZ/hwqjvRS81qJqKOyS9yEF58u6iYpFotbLnBR3zgRaSsSQ12bXHzNxjjsCAmduhKslqBQkjE+b0a9jn/FUU9dU4qERXw==

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.



Archive powered by MHonArc 2.6.18.

Top of Page