Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Any tactic or automation for orders?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Any tactic or automation for orders?


Chronological Thread 
  • From: Cao Qinxiang <caoqinxiang AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Any tactic or automation for orders?
  • Date: Wed, 24 Jul 2019 23:52:05 +0800
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=caoqinxiang AT gmail.com; spf=Pass smtp.mailfrom=caoqinxiang AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi1-f174.google.com
  • Ironport-phdr: 9a23:zqTOThKwPG4KsVuA2tmcpTZWNBhigK39O0sv0rFitYgRIvTxwZ3uMQTl6Ol3ixeRBMOHsqgC27Kd4/6ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmSSxbalxIRmqognctcgbipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3QqBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4qx2TxDmlToHNyUh8G7JlsNwkKxVoBWkpxNlwo7UZpyeOP5xc67ZeN8XQ3dKUMRMWCxbGo6zYIUPAOgBM+hWrIfzukUAogelCAa2GO/i0CVFimPq0aA41ekqDAHI3BYnH9ILqHnZss/6NKAPWu6uzanIyzrCb/JM1jf754jDbxcsru2WUrJ3aMrRyE8vFgzEjlqKr4zlMCiY1usIs2eB7upgUfijhHIgqwF0uzWiwNonhIfOhoIQ0F/E9CN5zZ46Jd25VE57YcOkH4BKuyGbMIt7RN4pTWJwuCsi1LEKpZq2cDIJxZkn3RLTdv2KfoqS7h7+VuucLjF1j29/dr2lnRa9602gx/X8Vsaq1FZKqTJIktzWuXAM0xzf88+HSvpg8ku41zaDygLe5+5eLUA7kqrbLJEhwroumZYJrUvDGSr2lF33jK+QaEok5vCl5/r7brjivJORNI95hhvjPqkvmMGzG/k0PwoBUmSD/OSzzrzj/Un3QLVQif02l7HUv4zAKsQcv665AglV04ki6xmlCTem388VnXYCLF1feRKHi5LlNE3JIPD9Ffu/mUijkC93x/DaOb3sGonCLn/akLv4Ybl971NcxxEowNBE55NUD6kBL+jpVk/wstzYFB45PBauz+bpEtUunr8ZDGmIG+qSNL7YmV6O/OMmZeeWN6EPvzOoAPEir8fvi284kFkSNf2i1JwOaXaoH/1gLG2WZHPthpEKFmJc7Vl2d/DjlFDXCW0bXH21Ra9pumBiVNCWSLzbT4Xou4SvmT+hF8QPNG9DA1GIV3zvctfcAqZeWGepOsZk1wc8e/2kQo4l2wupsVajmbViJ+vQvCYfsMC6jYUn16jojRg3sAdMIYGd3mWKFT8mm2oJQ3ox3fk6rxUilhGM1q93h/EeHttWtatE
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.


Archive powered by MHonArc 2.6.18.

Top of Page