coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Autos that fail if goals are not solved

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Autos that fail if goals are not solved
Date: Fri, 29 Mar 2019 06:00:21 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:hxpnwBPiugfMkLqK1XYl6mtUPXoX/o7sNwtQ0KIMzox0I/n9rarrMEGX3/hxlliBBdydt6sczbqL+PC8EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCehbb9oLxi7rQrdu8oZjIB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRjnhjoaNz4i6GHYlNB/jL5VrhKmohxw2Y/UYIeIP/Z6ca7QedYWSGxcVchTSiNBGJuxYYsRAeQcIeZWoYrzp1UMohu/GQaiC+zgxyRUhn/vx6A2z/gtHR3G0QEmAtkAsG7UrNLwNKoKVe660rPIwivGb/JWxDzz5pLHcx46ofGLW7J7bM3cx00xGAPfkFqQrIzkMymb2OsXvWmb9O1gVeS0hmE9rQFxvyKjydkxhYnUnI4a0E3E+Dx/zY0oK9O4T0t7bsSlEJtWryyaOIp2Qt8iQ2F1oyk20LwGuZm9cSMXy5on3wbSZvObf4SS/x7vSOScLS1liH9reb+znQu+/Eakx+HkWcS51ExGojdGn9XQrHwA1R3e5tKZRvdh+kqtwTiP2B7Q5+1YJE05kKrWJp09zrMzk5cfrEbOEyDrlEjziKKWeEop9+mt5uj6fLnrop2ROolpgQ/kKKsugNawAeEgPwgOQWeb/eO82aX/8EL3XbtGkuA6nrDevp7VOMgXv6m5DBRL3Yo57Ba/Eium388fnXkaKlJKZQiLj5DzO1HJPPD3E+uwg0itkDdswfDKJLrhAojRLnjHl7fherV951RAxwo0yNBT/5NUCrcfL/LvQkL8u8DUAgUkPwCowevrEshx240fVG6VH6OUPqffvUeN5u01IumMYIEVuCz6K/gg//PgiWE2mUUDcqms3Zobcn62Ee5oIkWCZnrshMwMHn0MvgojVuDllkCNUSNJa3moQqIw/is7B56+DYffWoCth6SM0zu8Hp1Pf2xJFlSMEWrzeIifQPcNaCeSItd7nTAeVLihTZUh1RC0uwPgxbpnNLmcxipN/5nkzZ1+4/DZvRA07z19ScqHmSnZRGZt22gMWjUe3aZloEU7xE3VgoZihPkNN9FJ6vZYGiszKoXbyaQuKd3oVwfQOPuAV02hRP2vByx3Q94shdYTNRUuU+6+hwzOinL5S4QekKaGUcBlq/OO7z3KP894jk3++uwkhlgiTNFIMDT81Kd56k7eC5OPmljLzv/2J5RZ5zbE8SK49UTLpFtRCVQiWKPYG30Tew3fsIahvx6Qf/qVEb0idzB554uCJ69NNoK7pGh9HK6mHfmHJmW7liG3GAqCwa6KYMzyYWIB0S7BCU8C1QcO4XKBMgt4DSCk8TvT

Hi Jason,

would something like
auto ; fail
do what you want?

In HOL4 there is an (apparently) equivalent construct, according to
whose clearly defined semantics, the tactic "fail" is applied to all
subgoals (if any) resulting from the application of "auto"

Cheers,

Jeremy

On 03/29/2019 08:17 AM, Jason -Zhong Sheng- Hu wrote:
> Hi all,
>
> I am wondering if there is a way to implement variants of autos, which
> fail if goals are not solved?
>
> Note that it's not the same as `solve [auto]`, because in this case,
> when auto fails to solve the goals, it's not going to back track and
> just fail the tactics.
>
> This variant is going to be helpful when dealing with massive number of
> evars, where instantiation order normally matters, so this will make Coq
> attempts to fill in different options, instead of just try the first one
> and turns the goals unprovable.
>
> *Thanks,*
> *Jason Hu*
> *https://hustmphrrr.github.io/*
> ****

[Coq-Club] Autos that fail if goals are not solved, Jason -Zhong Sheng- Hu, 03/28/2019
- Re: [Coq-Club] Autos that fail if goals are not solved, Jeremy Dawson, 03/29/2019