coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] cleaning up after 'field'

From: Michael Shulman <shulman AT sandiego.edu>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] cleaning up after 'field'
Date: Thu, 5 Nov 2015 09:14:16 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=viritrilbia AT gmail.com; spf=Pass smtp.mailfrom=viritrilbia AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f44.google.com
Ironport-phdr: 9a23:n0qdAx0j7VSYqsVOsmDT+DRfVm0co7zxezQtwd8ZsegQK/ad9pjvdHbS+e9qxAeQG96LtrQf1qGN7OjJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6PyZ/qnLvts7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JsKWqLjOq88ULZwDTI8Mmlz6teh/U3IShLK7X8BWE0XlABJCk7L9kepcI32t37ft+F90SSedfb2ULQxUDLqu7xrVRvtgSEvLDc//GDahcs2ga5G9kHy7ydjypLZNdnGfMF1ebnQKIsX

Thanks, that does work in this case if the field is R. But it would
be nice to have one that works for an arbitrary field too.

On Thu, Nov 5, 2015 at 9:06 AM, Frédéric Besson
<frederic.besson AT inria.fr>
wrote:
>
>> On 05 Nov 2015, at 17:59, Michael Shulman
>> <shulman AT sandiego.edu>
>> wrote:
>>
>> Is there a standard tactic that can automatically solve the non-zero
>> conditions left over by "field", at least in simple cases? E.g. if
>> the condition is "x - 1 != 0" and we have "x != 1" as a hypothesis?
> If this linear arithmetics over R, you can try lra.
>
> Best,
> —
> Frédéric

[Coq-Club] cleaning up after 'field', Michael Shulman, 11/05/2015
- Re: [Coq-Club] cleaning up after 'field', Frédéric Besson, 11/05/2015
- Message not available
  - Re: [Coq-Club] cleaning up after 'field', Michael Shulman, 11/05/2015