coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Łukasz Czajka <lukaszcz AT mimuw.edu.pl>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Any tactic or automation for orders?
Date: Wed, 24 Jul 2019 17:50:58 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=lukaszcz AT mimuw.edu.pl; spf=Pass smtp.mailfrom=lukaszczz AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f44.google.com
Ironport-phdr: 9a23:CeRE6xQ5MYONWyP5FBYM1qVnI9psv+yvbD5Q0YIujvd0So/mwa6yYRON2/xhgRfzUJnB7Loc0qyK6vqmCTRLscjJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MQu6oR/Su8UKjodvKac8wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaLDMy7n3ZhdJsg6JauBKhpgJww4jIYIGOKfFyerrRcc4GSWZdW8pcUStODJ6hb4sUF+oOI/pXr5XzqVsJqBuxHwisBOXywTNMiXL72ag23uI8Gg/EwQMgBcoDv3varNr3NKkcX+O7wrTWwzrfYP1bwiv96JHSfxw9vf2AQbB9fMzMwkcvDQPFiVCQpJTjMTOI1eQCqXOb7ut4Wu+xim8osQNxoju1ycwxjYTJgp8VylPe+iViwYc6Ody5RVV+Yd6lFZtQqi+bO5FoTcw/XmFkoj46yrkftJO9YSMExpMnxxvFZPyGdYiF+h3jVOeNITd4mXJqY6izhxe18US4xe38V9W00FZXriVeiNXDqncN1xnV58OaSfV95l+s1SiT2w3X8O1JIkA5mbDGJ5Mg37I8jJUevEvFEyTrgkv5lrWWeV8h+uWw6+TofLHmppiEOo9xkA7+M6AultW/AOU2LwQCRmab9Ouz2bH58k35R7JKjvIykqbHqpzVOcMbpquhDw9U1IYs9Qq/Ai+43NgEmXQLNlFIdRKdg4T0OlzCPer0APiwjli0lTdk3fHGPrnvApXXKXjDla/sfbJg605f0gUz1tFe6I5VC7AAO//zVUrxu8bZDh89KQC73+HnCNBl2oMERW2PGrOZML/VsVKQ+u0vJPCMaJYJtzb5Nvgq/OXjjWQ5mF8YZammx4EbaHG+HvR8IkWWe2DggtkbETRCgg1rZ+vzwHaGTDQbM321Ruc34iwxIIOgF4bKAI631u+vxiC+S7lLZWldGGenA37qdIzMD/MRayuJMMRzujkFUKW+DYItyFe2sFmpmPJcMuPI93hA5trY399v6riWyEhrqW5ESv+F2mTIdFla23sSTmZqjqV+pFFijFqPzO5gh64ATIEB17ZySg4/cKXk4al6BtT1AF+Te96ITBO3XYzjD21tCN02xNAKbgB2HNDw1kmSjRrvOKcckvmwPLJx96vd23brIMMkkiTJ0aAgix8tRc4dbGA=

Hello.

CoqHammer (https://github.com/lukaszcz/coqhammer) can also solve this
goal, and similar goals as long as they are not too complicated.

Best,
Lukasz

On Wed, 24 Jul 2019 at 17:40, 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.
>

[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