Wie benutze ich Auto mit Wiederholung in benutzerdefinierten Taktiken?

Question

In meiner Coq-Entwicklung lerne ich, wie man neue Taktiken erstellt, die auf meine Problemdomäne zugeschnitten sind, a la Prof. Adam Chlipala.

Auf dieser Seite beschreibt er, wie man mächtige Taktiken erstellt, indem man repeat um eine match wickelt, die auf verschiedene interessante Bedingungen reagiert. Die repeat iteriert dann und ermöglicht eine weitreichende Inferenz.

Die Verwendung von repeat hat einen Vorbehalt (Hervorhebung von mir):

Die repeat, die wir hier verwenden eine taktische oder Taktik combinator genannt wird. Das Verhalten von repeat t besteht darin, dass eine Schleife durchlaufen wird, indem t läuft, t für alle generierten Subziele ausgeführt wird, tihre generierten Subziele ausgeführt wird, und so weiter. Wenn t an irgendeinem Punkt in diesem Suchbaum fehlschlägt, wird dieses spezielle Unterziel durch spätere Taktiken behandelt. Daher ist es wichtig, niemals repeat mit einer Taktik zu verwenden, die immer erfolgreich ist.

Jetzt habe ich bereits eine starke Taktik im Einsatz, auto. Es führt in ähnlicher Weise Ketten von Schritten zusammen, diesmal aus Hint-Datenbanken. Von auto ‚s Seite:

auto entweder vollständig löst das Ziel oder sonst überlässt es intakt. auto und trivial nie fehlschlagen.

Boo! Ich habe schon einige Mühe in Kuratieren auto ‚s Hinweis Datenbanken investiert, aber es scheint mir verboten werde von ihnen in Taktiken repeat mit (das heißt, interessante Taktik.)

Gibt es eine Variation von auto, die ausfallen können, oder ansonsten in loops richtig verwendet werden?

Zum Beispiel scheitert vielleicht diese Variante, wenn sie [das Ziel] intakt lässt.

EDIT: auto in Schleifen Einbindung ist nicht die „richtige“ Art und Weise, es trotzdem zu tun (siehe this), aber die eigentliche Frage nach einer fehlerhaften Version von Auto ist vielleicht noch interessant.

Answer 1

Wie von @AntonTrunov erwähnt, können Sie immer die Taktik progress verwenden, um die Taktik fehlschlagen zu lassen, wenn das Ziel nicht geändert wurde. Im Fall von auto, da es das Ziel lösen oder unverändert lassen soll, können Sie es auch in solve [ auto ] einbinden, was den gleichen Effekt hat, weil es fehlschlägt, wenn auto das Ziel nicht vollständig löst (here is the doc for solve).