coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Valentin Robert <valentin.robert.42 AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Tactics to manipulate real arithmetic (w/o solving)
Date: Mon, 13 Mar 2017 23:28:11 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=valentin.robert.42 AT gmail.com; spf=Pass smtp.mailfrom=valentin.robert.42 AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f53.google.com
Ironport-phdr: 9a23:8L1P1R/u05o7G/9uRHKM819IXTAuvvDOBiVQ1KB90+4cTK2v8tzYMVDF4r011RmSDNidtq8P0rGe8/i5HzdfsdDZ6DFKWacPfiFGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkImbtjyT8TZiN3y3OSv8bXSZR9JjXyze/k6eB6xtEDastQcqYpkMKc4jBXT9ChmYeNTkF1hIV+Vgxf6rv239pN572wEpfsl+shcUKO8ZaMyQKZESmh8G28w7czv8xLESF3ctTMnTmwKn08QUED+5xbgU8Kpvw==

Hello,

Are there any existing techniques to either:

1) allow rewriting with equations/inequations where the term to be rewritten is not immediately found, but can be isolated:

Require Import Reals.

Example e1 (a b c d e : R) (H : c * a = d) : a * b * c = e.

(* super_rewrite with H, to obtain something like (d * b = e) or (b * d = e) *)

2) allow solving simple (i.e., reflexive up-to permutations/simplifications/...) existentially-quantified equations:

Example e2 (a b c : R) : exists (x : R), a * b * c = b * x * a.

(* figure out that you should instantiate x with c *)

Thanks,

- Valentin

[Coq-Club] Tactics to manipulate real arithmetic (w/o solving), Valentin Robert, 03/14/2017
- Re: [Coq-Club] Tactics to manipulate real arithmetic (w/o solving), Guillaume Melquiond, 03/14/2017
- Re: [Coq-Club] Tactics to manipulate real arithmetic (w/o solving), Laurent Thery, 03/15/2017