coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Vincent Laporte <vincent.laporte AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Any tactic or automation for orders?
Date: Wed, 24 Jul 2019 15:40:12 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=vincent.laporte AT gmail.com; spf=Pass smtp.mailfrom=vincent.laporte AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f43.google.com
Ironport-phdr: 9a23:ElopIhTrUPmcUqJMXZ9pPisJiNpsv+yvbD5Q0YIujvd0So/mwa6yYBeN2/xhgRfzUJnB7Loc0qyK6vqmCTRLscrJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MQu6oR/Su8UKjodvKak8wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaMDE37XzXitdojK1FvB2huxJxw4nRYI6PNfp+eL7WcdcVSGdFW8pcUTFKDIGhYIsVF+cPPftWoZfzp1UNoxWxCwajC+HzxTJTiX/6wbc33eM9HQzI3gEtGc8FvnTOrNXyMacfSe+6zKjOzTrfcfxW3yv945XOfB87ufGMWqhwcdbPxkIyEA7FkFSQqYr5MDyL0OQNr3KX7+56WuK3jG4nsR1xrSa0y8cjj4nGnIMVylTe+Splx4Y1IMS1RUhmatCqF5tQsjuVN4pwQs46TGFouTo6yr0buZGgZiQKyZMnyhjCYPKEa4iF+gzvWPqVLDtih39oeKiziwis/US90OHxWce53E5XoidLj9XArG4B2hzc58SdV/dw/l2t1SiT2w3Q7OxPPFo6mrDBK5E7x749jpoTvlrHHi/xgEj2ibWZdkQg+uSx5eXneKjqqoaSN4J7hAzyKKsumsu4AeQ3NggBQXKX9vi71L3m5UH5QbNKgeMqkqTBrpzWOcAWqrS6DgJVyIov9QizAyq83NkXk3QLNFdFdwiGj4jtNVHOOvf4DfKnjlSykTdrwezJMaPnApXRNHTDlK3ufa56605G1Ao808tS551RCr4bIfLzXlX9u8DfDh88KwC02froCM1h1oMCXmKCGrOWMKTLsVOR+u0vJ/SMa5QOtTbmK/kl4ubugmUjlV8ce6mpx5oXZ2qiEvRoOUXKKUbr19wGCCIBuhc0ZO3sklyLFzBJNFioWKdp2DA9A4+gEc/nT5iqmqCMlHOlH5tda2ZaTFSFCXDya4isVPIFaSbUKchkxG9XHYO9QpMsgEn9/DTxzKBqe7aFo3FKhdfYzNFwotbru1Qq7zUtVpaS1miMSyd/mWZaH2ZnjpA6mlR0zxK46YY9hvVZEdJJ4PYQC1U1MJfdy6pxDNWgA1ucLOfMc06vR5CdOR90Tt81xIVTMUN0GtHnkQqamiT2WPkakLuEAJFy+aXZjSD8
Openpgp: preference=signencrypt

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.

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Any tactic or automation for orders?, Cao Qinxiang, 07/24/2019
- Re: [Coq-Club] Any tactic or automation for orders?, Vincent Laporte, 07/24/2019
  - Re: [Coq-Club] Any tactic or automation for orders?, Łukasz Czajka, 07/24/2019
  - Re: [Coq-Club] Any tactic or automation for orders?, Cao Qinxiang, 07/24/2019
    - Re: [Coq-Club] Any tactic or automation for orders?, Vincent Laporte, 07/24/2019
    - Re: [Coq-Club] Any tactic or automation for orders?, Frédéric Besson, 07/24/2019
      - Re: [Coq-Club] Any tactic or automation for orders?, Cao Qinxiang, 07/24/2019
        
        Re: [Coq-Club] Any tactic or automation for orders?, Agnishom Chattopadhyay, 07/24/2019
        
        Re: [Coq-Club] Any tactic or automation for orders?, Laurent Thery, 07/24/2019