The Coq mailing list

[Cao Qinxiang <caoqinxiang AT gmail.com>]

Dear Vincent and Frédéric,

Thank you very much! It works now.

Best,

Qinxiang Cao

Shanghai Jiao Tong University, John Hopcroft Center

Room 1110-2, SJTUSE Building

800 Dongchuan Road, Shanghai, China, 200240

On Thu, Jul 25, 2019 at 12:03 AM Frédéric Besson <frederic.besson AT inria.fr> wrote:

Hello,

For Q, you need to Require Import Lqa.
This may be a bit puzzling but it defines a lra tactic working for Q.

Best,


On Wed, 2019-07-24 at 23:52 +0800, Cao Qinxiang wrote:
> Dear Vincent,
>
> The following file does not work:
>
> > Require Import Psatz.
> > Require Import QArith.
> > Require Import Lra.
> > Local Open Scope Q.
> > Goal forall a b: Q, a <= b <= a -> a == b.
> > intros.
> > lra.
>
> It says:
>
> > In nested Ltac calls to "lra" and "lra_R (tactic)", last call
> > failed.
> > Tactic failure:  Cannot find witness.
>
> I currently use Coq 8.9.0 on Windows. Shall I try another version?
>
> Qinxiang Cao
> Shanghai Jiao Tong University, John Hopcroft Center
> Room 1110-2, SJTUSE Building
> 800 Dongchuan Road, Shanghai, China, 200240
>
>
>
> On Wed, Jul 24, 2019 at 11:40 PM Vincent Laporte <
> vincent.laporte AT gmail.com> wrote:
> > Hello,
> >
> > The “lra” tactic can solve this goal:
> >
> > https://coq.github.io/doc/v8.9/refman/addendum/micromega.html#lra-a-decision-procedure-for-linear-real-and-rational-arithmetic
> >
> > Cheers,
> > --
> > Vincent.
> >