coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Solve or chain a tactic application

From: Gregory Malecha <gmalecha AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Solve or chain a tactic application
Date: Tue, 15 Oct 2019 22:56:34 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gmalecha AT gmail.com; spf=Pass smtp.mailfrom=gmalecha AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f44.google.com
Ironport-phdr: 9a23:+MNsuRVM0eNYYwM3bq9nE9zYGXbV8LGtZVwlr6E/grcLSJyIuqrYbBaDt8tkgFKBZ4jH8fUM07OQ7/m7HzNcqsja+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi4oAnLtMQbjoRuJ6c/xxDUvnZGZuNayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0jioMKiU0+3/LhMNukK1boQqhpx1hzI7SfIGVL+d1cqfEcd8HWWZNQsNdWipGDY2hcosPFPIBMvhEoInhqVUOqh6+ChOtBOPp1zREgnD70Kk/3+knDArI3hEvH8gWvXvbrNv7OqQcX/2rwqbU1jjMde9a1C3n5YTUbhwso/eBVq9wf8rLzkkvEhvIgFSKqYP7MDOV0f4NsmiG5ORnT+2vj3AopB1xoje128whjYbJhocPxVDA6yp23IY1KsejRU50ZN6rCppQtyWAO4RqRcMiRnhltSAnwbMIvp67eTIFyJUhxxPHZPyHcpSI4hL+VOmKOzt4hXVldbSijBix6Uit0vPwWtWw3VpQrSdIksPAum4T2xDO8MSKRfRw80G80jiVzQ/T8PtLIUUsmKrbNZEhxrkwm4IWsUvZHy/2nFz6jaGMdkk54+So5evqb7r8qp+TMI90jQ7+MqAwlcClHes4NQ0OU3Ca+eS6yrLj4VX0TKtWgvAyiKXUs5DXKd4FqqKnHgNZyIku5hmnAzejytsYnH0HLFxfeBKAiojkI17OIPXiAve7nVujjDdryOrdM73uB5XCNHnDkLP7cblh7E5czRI/zcpD6JJMFrEBPPXzV1ftu9zfFx81KhC7w+L6CNpmzY4eQmKOAqqBMKzIq1OI5+QvI/ONZIAPojr9JeIltLbSiioSnkZVVq2019NDY3ehW/9iPk+xYHz2g95HH31c7SQkS+m/p0ePXjlJdj6XVqYx7TEyQNapCI7HS4utiZSO2S66GttdYWUQWQPEKmvha4jRA6REUymVOMI012FdDOnze8oazRir8TTC5f9iJ+vQ9DcfsMu6htdw7uzX0xo18G4tVpjP4yS2V2hx21gwaXouxqkm+B5yz16C1e5zhPkKTYUOtcMMaR8zMNvn98I/C932XVicLNKASVLjXc//RD9tEpQ+xNgBZ0s7ENKn3EjO

Hello --

I'm working with a generic lemma (I don't know what its structure is). I would like to apply it and, if it completely solves the goal, then it should completely solve the goal, and otherwise, I would like to require all but the last premise be solved by a tactic tac.

The ltac tactic that I have right now is:

Ltac do_it H :=

simple eapply H; [> tauto .. | ].

And this accomplishes the later very well, but it doesn't accomplish the former. In particular, the following fails.

Goal True.
simple eapply I; [> tauto .. | ].

I assume that I could do something like:

first [ solve [ simple eapply l ]

| simple eapply l; [> tauto .. | ] ]

but I'd like to avoid applying the lemma multiple times. Is there any way to code this behavior?

Thanks in advance.

gregory malecha

gmalecha.github.io

[Coq-Club] Solve or chain a tactic application, Gregory Malecha, 10/16/2019