coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Cao Qinxiang <caoqinxiang AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Any tactic or automation for orders?
Date: Wed, 24 Jul 2019 23:32:07 +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-ot1-f49.google.com
Ironport-phdr: 9a23:fulRohKq7p0RVHNVTdmcpTZWNBhigK39O0sv0rFitYgRKv/xwZ3uMQTl6Ol3ixeRBMOHsqgC27Kd4/qocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmSSxbalxIRmqognctdcaipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3QqBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4qx2ThLjlSUJOCMj8GzPhcN+jKxVrhG8qRJh34HZe5uaOOZkc67HYd8WWWhMU8BMXCJBGIO8aI4PAvIfMOlCqIn2ukAArRq4BQijBePg0DlIhnDr1qA9z+suCwbG3BUhH9IIv3XUrc/6NKEdUe2uw6nIyC/Mb/JS2Tvn9IfIdRUhrOiKULltcsTR0VEiGx3ZgliUs4DoPDOY2v4Tv2SG8+ZsT+2ihmohpgpsuDag3N0shZPMho8NylDL6yF5wIEtKN29UkF7YNqkHIJXtyGGKod6W80iTm5stSogxb0Gvpm7fCcOyJs53RLQd/uHc42Q7hLiUuaePyt4iWp7dL6jgxu+60utx+3mWsWqzVpGsjBJn9bIu3wV0hzc8MmHSv9z/ke73jaP0hje5f1eLkAzjKrbKpghw7ExlpUJt0TDETT7mErzjKCMd0Uk/vKk5PjgYrXjvpOcLZN7ihniMqQyncyyGfg3Mg8XX2SC5eu80KDj8lbiTbVRjvw2l7HZv4rAKcQaoK65GQ5V3Zw55xaxFTf1mOgfyHIANRdOfA+Np4nvIVDHZv7iXtmlhFH5uz5sj8nHOK3gC5PCZizImbD4fLBt6kdaxyI8yNle49RfDbRXc6G7YVP4qNGNVkxxCAez2euyUIwghLNbYnqGB+qiCI2XsVKM4bhyceyFZYtQvyqkbvZ5trjhing2nVJbdq6sj8NOOSKIW89+KkDcWkLCx9IIEGMEpA07FbW4h1iLUDoVbHG3DftlumMLTbm+BIKGfbiDxaSb1X7iTJJTb2FCTFuLFCWweg==

Dear Coq Clubbers,

If I want to prove something about rational numbers like:

n: Q

m: Q

H: n <= m <= n

===========

n == m

or something similar about real numbers, or some other order-related stuff, is there any Coq standard library support for that?

I know that "omega" would work for nat or Z. But it does not work for Q.

Thank you very much!

Qinxiang Cao

Shanghai Jiao Tong University, John Hopcroft Center

Room 1110-2, SJTUSE Building

800 Dongchuan Road, Shanghai, China, 200240

[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