coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Non shortcut OR chaining of tactics

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Non shortcut OR chaining of tactics
Date: Mon, 21 Nov 2016 17:57:06 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga06.intel.com
Ironport-phdr: 9a23:z/W7ahP/osKwaWe4E5Ul6mtUPXoX/o7sNwtQ0KIMzox0Ivn9rarrMEGX3/hxlliBBdydsKMfzbCN+Pm4AyQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9GiTe5b75+Ngu6oAveusULnYduNLs6xwfUrHdPZ+lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRneVgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gyoBKjU38nzYitZogaxbvhyvugB/zYDXboGUKPVxcbjQcskGSWdFRMtdSzBNDp26YoASD+QBJ+FYr4zlqlcAsBW+AhejBOzzyj9SgX/2xbU22PkmHwHHwAMgH8gBv2rQrNn7KawfVuW1zKjUwjXDdfxZxzP95JLTchAmv/6MUq5wcdDWyUk3DA7Fj1OQqZD7MDORzOgCr2+b7+95WO+plmUppQZxoj21ycctjInEnoMVylbY9SpnxIY5P8C3R1B9bNW5E5VQrzmXO5Z4T84tWW1kpSg3x7IctZKmciUHyY4ryhDCZ/CfboSF4xzuWPyfLDp2nn5pZryyihKo/US9yeDwS9G43EtLoydBiNXAqHAA2hPJ5sSZUPdw/EOs1DCS3A7J8O5EO1o7la/DJp4h3LEwkp0TvFzGHi/5gkr6kK6bel8l+uiu9+TofLHmqoWAOI9zjwHyKqUumsqhDuQkKgUCQmaW9Oum2LH+80D0T69GguA4n6TYqpzXK9kXqra8AwBP04Yj7xi/Dy2h0NQdhXQHKVNFdw6Hj4fzJV7OJOr0Dey4g1uynzdr2+rGPrr5ApjWL3jDlqvhcqh560JG1AUzytVf64pOCr4dOPLzRlPxtNvAAxAlNAy02v/rB8l51oMDQm2CGbSZMaPXsV+Q/O0jOeiMZIkPuDb8Mfcp/fDujWVq0WMaKOOi2oJSY3SlFNxnJV+YaDzimJ1JRWwNp081SPHgoFyESz9aIXioCfES/DY+XcidCorMWpqqmPjJ+SawHpRbYioOXlWNGnfheoHCQPABZz6IJddJkzoYWLznQIgkg0L9/DTmwqZqe7KHshYTsojugYB4

Dear Coq Users,

is there an operator which chains tactics such that all tactics which don’t fail are executed one after another and the chain succeeds if at least one tactic in the chain succeeded? The tactics don’t create new goals or change the goal, the just create new hypothesis. This would be similar to the || operator, except that it doesn’t stop after the first successful tactic.

My application is extensible forwarding using the tactic notation / Ltac ::= trick Jonathan suggested. This works with ||, but it adds a quadratic (with number of tactics chained) overhead when repeated until failure.

Thanks & Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Non shortcut OR chaining of tactics, Soegtrop, Michael, 11/21/2016
- RE: [Coq-Club] Non shortcut OR chaining of tactics, Soegtrop, Michael, 11/21/2016