Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] Non shortcut OR chaining of tactics

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Non shortcut OR chaining of tactics


Chronological Thread 
  • From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: RE: [Coq-Club] Non shortcut OR chaining of tactics
  • Date: Mon, 21 Nov 2016 18:04:32 +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 mga05.intel.com
  • Ironport-phdr: 9a23:O3lbGRRBo0x/d+ZZaajJFhmQctpsv+yvbD5Q0YIujvd0So/mwa6yYRaN2/xhgRfzUJnB7Loc0qyN4vumAzdLuM7b+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe71/IRG4oAnLqMUbj4RuJrstxhfXv3BFZ/lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/WfKgcJyka1bugqsqRxhzYDJfIGbOvlwfq3fctMbWWVOUd1cWDZdDo64dYYDE/YNMfheooLgp1UOtxy+BQy0Ce/h1zFIgWH53aIm0+Q7FgHGxBQsFM8JvnTVsNr1NL0dXv6xzKXG0D7OaPZW2Tbh54jIaB8uv/WMUahrccrW10YvGB/Fjk+XqYz9JD6V1+INs3SF4OpkT+6gl2knqwRorzWp28wihI7JhocPxVDF8yV02Ic1JdukSEFlZd6oCoZfuD+cOoBrQc0iW3lltDs+x7EYo5K2fCgHxI4nyhLBcfCKfIaF7gr+WOuQLzp0nnxodbylixqs/0WtzvfwWtS33VpXtiZJj9jBu3QX2xDN6sWKReFx8lm71TuN0w3e7PxPL1oumqrBMZEhx6Y9lpoNvkTHGS/7gED2jKCMeUk4+uWk8eXnYrP6ppCCM494kB3xMqMrmsCnAOQ4NBYBX3SD9Oih0LDv41f1TbVKg/EskqTVrorWKMsVq6KhBg9ayIcj6xKxDze819QYmGEKLFdEeB2bj4jmIU/BIPTiAfekhFSjjjhrx+zcPr3mGpXANXnDkLH9fblj705Q0hY8zdda555MELEOPOrzWlPttNzfFhI2Lwu0w//+BNph0oMeRHmAD7SCMKLStF+I/vggL/ONZI8Tojb9KuIq6+TgjX8jyhchevzj1pwOLXu8A/5OIkODYHOqjM1LWTMBuRN7R+j3gnWDVyRSbjC8RfRvyCs8DdfsNoDOSZy3h6TFlAK6FZ1fa2QMQgSJEHzofoiAHewLZS2OOMh5uj0CSbWlDYQm0Ef950fB17N7I7+MqWUjvpX52Y0t6g==

Dear Coq Users,

 

please ignore my previous mail – it is easy to write a tactic notation for this.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Soegtrop, Michael
Sent: Monday, November 21, 2016 6:57 PM
To: coq-club AT inria.fr
Subject: [Coq-Club] Non shortcut OR chaining of tactics

 

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

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




Archive powered by MHonArc 2.6.18.

Top of Page