coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Autos that fail if goals are not solved
Date: Thu, 28 Mar 2019 21:17:04 +0000
Accept-language: en-CA, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM05-DM3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:j0ZOChCfwEB7i6wkp13oUyQJP3N1i/DPJgcQr6AfoPdwSPX5pMbcNUDSrc9gkEXOFd2Cra4d06yG7+u5BTNIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfK9+IA+1oAjeucUanIRvJ6QswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwIMCM38HzMisxokq1UvA6hqRJ4w47Reo6VNfx+db7Zcd4VQWdNW8BcXDFDDIyhdYsCF+oPM/hFoYnhqVUArgexCga3Cez11jNEmmX70bEm3+g8FwzNwQwuH8gJsHTRtNj7ML0dUfuyzKnO0D7PdvBZ2Tf66IjOfRAqvOyCXbJufsrXxkkjDh7OgFeNqYf4OD6V2PkCs2ia7up7S+6jl3Mrpx1qrzivwccslozJiZgUylDA7yl23IE1JdihRUN9fNWqHpxQtySAOIt3RMMvW25ouCcmyr0GpJ60ZzIGyJUgxxPZdveJcJCI7wrsWeqNOzt1gGxpdKiiixu960StzuPxWtG60FlUrSdJjtzBu3UD1xHT6sWIVv5w8Vq91TqS1w3e7+VJLVwpmqfYLpMt3709mocdvEnFAyT4gl/5jLWMeUUh4uWo6/roYrHhppKEL4F5lgbwPrgul8CmD+o2NQYDU3Gc+eunyrLv50r5QKhWjvItlanZrZbaKtkBqq6hGQ9V1Zoj5AijADe60dQYmn8HIEhCeBKak4jpP1bOIPf7Dfuln1uslzJry+jHPr3nHJrNMmDOnbj9cbpn70NQ1hA/wc1Q6p5ODrwMLur/Wkrru9zZCh85PRa0w+HiCNhl2IMRRGKPA66CMK/MrVOE+/4jLvKMZI8SpDb9LuIq5//qjXMjhVAdeqyp0YMNaH+kBvRmP1mZYX30j9gdFmcKpxMyQ/DuiF2fSjFefG2yXqI55jEjEo2qF4bDRoa3gLyAxii3BJNWZnoVQmyLRD3jcJzBUPMRYgqTJNVgm3oKT/LpH4QmzFSlsBLw47thNOvdvCMC48HNzt9wss/ajhY0vXlGD8Ob3Cm2T2xykSZAZyJ+iK5zoV5mkA/aiYB4hOBdHN1XofhOV1FpZtbn0+VmBoWqCUr6ddCTRQP6E4z3UwF0dco4xpo1W2g4Htyjih7Z2C/zWO0VkKCODZ0wtKnb2iqofpov+zP9zKAkymIebI5XL2T/3fx/8BTWDo/N1U6ekvTyLPlO7Gv27G6GiFG2kgRYXQp3DfqXe1k6PhaTgfGio0TIQvmpFKgtNRZHxYiaMKxWZ9b1jFJAAvD+JNDZZGH3kGC1V0+F

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