coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] an equivalent to Isabelle's Sledgehammer

From: noam neer <noamneer AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] an equivalent to Isabelle's Sledgehammer
Date: Wed, 7 Jun 2017 16:42:07 +0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=noamneer AT gmail.com; spf=Pass smtp.mailfrom=noamneer AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f50.google.com
Ironport-phdr: 9a23:gLnLVB19yt6//bS0smDT+DRfVm0co7zxezQtwd8Zse0WKvad9pjvdHbS+e9qxAeQG96KtLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q89pDXYQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiCkJOT0k/m/JlsN9l7hUrA67qhFl34LYfIOYOfxjda3dZ9MaQm9BU95XVyxGGIy8apYED+wfMulGtYn2ulwDrR25BQa2AePvzCFHiWHs3aAh3OQhFBvJ3A0kH94UrHvUq9D1Ob4UXOuowqfIyjDDYOlX2Tf78IXHaA4hruuXXbJsa8be1U4vFwbDg16NqoLlJyuY2+YCvmSB8uZsS+Kih3Qkpg1vuDSixtsgh4/UjYwP0F/E7z92wIMtKN24VkF7ZdmkHYNVty6ANot2RtouQm9tuCom07EGt562cDQQxJQowB7fbPOHc4yW7R75SOmRJjJ4iGpkeLK5mRmy7VCtx+/zW8WuzVpGsCpInsPPu3wTzRDe6tSLRuN4/ki72DaP0w7T6vtDIUAxjafbLZkhzaQ1lpoVr0vMADX2lV75jK+TbEok++yo5/77bbXho5+QL5V0hR3mMqQyhsy/Bvw1PRQJX2iC4OizyLnj/VDiT7hRlf03kqzZsIjAKsgBp665BRVV0oc55BqlATemyodQoX5SJ1VcPRmDkoLBOlfUIfm+A+3srU6rlWJtwPnDdrvsD4+Fen7EmbLncLtnw0FZwQs3i9tY4sQHWfk6PPvvVxqp55TjBRgjPlnszg==

Hello everybody.

I'm pretty new to Coq but I have some experience with Isabelle.

Isabelle has a tool called Sledgehammer that is very convenient for proving simple claims of any kind. It is much easier to use than the simplifier, which requires deep knowledge of the lemma libraries.

my question is, does Coq have an analogue to Sledgehammer?

many thanx

Virus-free. www.avast.com

[Coq-Club] an equivalent to Isabelle's Sledgehammer, noam neer, 06/07/2017