coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Implementation of Coq's automation tactics

From: Xuanrui Qi <xqi01 AT cs.tufts.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Implementation of Coq's automation tactics
Date: Thu, 07 Mar 2019 19:13:32 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=xqi01 AT cs.tufts.edu; spf=None smtp.mailfrom=xqi01 AT cs.tufts.edu; spf=None smtp.helo=postmaster AT vm-delivery1.eecs.tufts.edu
Ironport-phdr: 9a23:sN61WBSeLRV8m9LkWSyDDLPGzdpsv+yvbD5Q0YIujvd0So/mwa69YxyN2/xhgRfzUJnB7Loc0qyK6vimATVIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfK9+IA+qoQnMq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4KB3RRLmiioKOSc1/H3Yh8dtiK5WoA6tqxl5zoXJYo+aKeB+c7vec90HRWRPQMhfWDBPDYyzYIUCFPYBMORCooXhu1cDtxmzCA+xD+3v0D9IgXr20LU73OQ8Cw7G2hYgH88PsH/Jt9v1NboZXOe6zanRzDXPc+5a1Czh54jTaBwhveyMXbxsccrK00UgCR7KjkiJpIHjIjib2OMNs22B4OphU+Kik2EmqxxrrTip3Mcsl4jJhpsUylze6Sp5x4M1KNulQ0B4ed6pCIZcui+GO4dsQ84vTHtktDg0x7Ect5O2fjAGxIo7yxPbcfCKcpKE7x3tWeqLPDt1hXBodbSijBio60eg0PfzVsys3VZKsCVFlt7Mu2gT1xzW88SIV+Vy/kOg2TaRyQ/T8OFFLV0umaXFNZEu3qUwmoAPsUTeEC/2hF72gLWIeUo55+ik8+XnYrP4qZ+AL4J4lw/zPrg0lsG+Duk0KBYCUmaB9emy1rDv5Uj5T69Ljv0ynKnZqpfaJcEDq6+2Gg9V05ov5wukAji6y9QUh2UHLE9LeBKblIjlIU/BL+3lDfunmVSjjC9rx+zaPr3mGpjCMn/DkK74cblh705c1RE8wMtE55NUD7EBOOj8VlXwtNzeFB85Mha7z/zpCNVnhcsiXjeEBbbcO6fPu3eJ4PguKq+Cftw7ojH4fsg47vj0kH5xoF5VKbmw3MNOQHujWOh7LVmCJ3fgn4FSQi8xogMiQbmy2xW5WjlJaiPvB/tttAF+M5qvCML4fq7ohbWA2CmhGZgPOjJNERaQDHn0bMOJV+peMHvOcP8kqSQNUP2ac6FkzQun7VOowKEhMvfa5jZeuJ7+hoAsur/j0Coq/DkxNPyzlmGAS2YuzzEWQno60aR+v0Fn2w7F3KVzmLpECNJP/LVEXhpobZM=

Hello Coq-Clubbers,

I am wondering how Coq's automation tactics (auto, tauto, intuition
which is just tauto fail, etc.) are implemented. Are they implemented
in Ltac or in OCaml (or perhaps some in Ltac and some in OCaml)? Could
someone point me to their implementations, if possible?

Thanks!

Best,
Ray

--
Xuanrui (Ray) Qi

xqi01 AT cs.tufts.edu
me AT xuanruiqi.com
https://www.xuanruiqi.com

[Coq-Club] Implementation of Coq's automation tactics, Xuanrui Qi, 03/08/2019
- Re: [Coq-Club] Implementation of Coq's automation tactics, Joomy Korkut, 03/08/2019
  - Re: [Coq-Club] Implementation of Coq's automation tactics, Gaëtan Gilbert, 03/08/2019
- [Coq-Club] Coq Ocaml version, Laurent Thery, 03/14/2019
  - Re: [Coq-Club] Coq Ocaml version, CYRIL SIX, 03/14/2019
  - Re: [Coq-Club] Coq Ocaml version, Emilio Jesús Gallego Arias, 03/14/2019
    - Re: [Coq-Club] Coq Ocaml version, Xuanrui Qi, 03/14/2019
      - Re: [Coq-Club] Coq Ocaml version, Laurent Thery, 03/15/2019
        
        Re: [Coq-Club] Coq Ocaml version, Théo Zimmermann, 03/15/2019
        
        Re: [Coq-Club] Coq Ocaml version, Gaëtan Gilbert, 03/15/2019
        
        Re: [Coq-Club] Coq Ocaml version, Ian, 03/15/2019