Скачать или смотреть How to Effectively Apply LTac to Subexpressions in Coq Goals

Discover how to apply LTac tactics to simplify specific subexpressions of a Coq goal, overcoming common errors with practical solutions.
---
This video is based on the question https://stackoverflow.com/q/68134187/ asked by the user 'push33n' ( https://stackoverflow.com/u/9910692/ ) and on the answer https://stackoverflow.com/a/68155666/ provided by the user 'pjm' ( https://stackoverflow.com/u/7508402/ ) at 'Stack Overflow' website. Thanks to these great users and Stackexchange community for their contributions.

Visit these links for original content and any more details, such as alternate solutions, latest updates/developments on topic, comments, revision history etc. For example, the original title of the Question was: apply ltac to subexpression of a goal

Also, Content (except music) licensed under CC BY-SA https://meta.stackexchange.com/help/l...
The original Question post is licensed under the 'CC BY-SA 4.0' ( https://creativecommons.org/licenses/... ) license, and the original Answer post is licensed under the 'CC BY-SA 4.0' ( https://creativecommons.org/licenses/... ) license.

If anything seems off to you, please feel free to write me at vlogize [AT] gmail [DOT] com.
---
Mastering LTac: Simplifying Coq Goals with Subexpressions

When working with Coq, a powerful proof assistant, you may encounter situations where you want to simplify a complex goal by only addressing a specific subexpression. This can be particularly tricky, especially when dealing with inductive definitions like relations in your goals. In this guide, we’ll explore a practical solution for a common challenge: how to apply LTac tactics to just a subexpression of a goal.

Understanding the Problem

Imagine you have an inductive relation defined in Coq as follows:

[[See Video to Reveal this Text or Code Snippet]]

You also have a custom LTac tactic that simplifies expressions:

[[See Video to Reveal this Text or Code Snippet]]

Now, let’s say you want to write another tactic, simplify_fst, which specifically targets the first term of a divisible goal. Here is what you might be tempted to write:

[[See Video to Reveal this Text or Code Snippet]]

However, if you try to apply this tactic in a lemma like this:

[[See Video to Reveal this Text or Code Snippet]]

You would likely encounter an error similar to this:

[[See Video to Reveal this Text or Code Snippet]]

This occurs because LTac cannot directly apply tactics to expressions like (n + m) without first extracting the variable in a usable form.

The Solution

In order to overcome this limitation, you can use the remember tactic to introduce a fresh name for the term you wish to simplify. This is how you can re-write the simplify_fst tactic to achieve your goal successfully.

Steps to Implement the Solution

Here’s the improved definition of the simplify_fst tactic:

[[See Video to Reveal this Text or Code Snippet]]

Let’s break down what this does:

Fresh Variables: let x := fresh "x" declares a new variable x that does not conflict with any existing variables.

Remember: The remember N as x eqn:Hx line introduces x as a new name for N, storing its original identity in Hx.

Auto-rewrite: The autorewrite tactic is then applied to Hx to simplify your goal based on the rewrite rules you’ve defined.

Substitution: Finally, subst x replaces occurrences of x in your goal with their corresponding values.

Resulting Usage

Now, when you apply the simplify_fst tactic in your lemma, it will work seamlessly:

[[See Video to Reveal this Text or Code Snippet]]

By using the remember tactic in conjunction with fresh variables, you can effectively isolate and simplify specific parts of your goals without running into variable coercion errors.

Conclusion

Implementing LTac tactics in Coq can be challenging, especially when it comes to manipulating subexpressions of complex goals. By leveraging the remember tactic to freshly bind the terms you want to simplify, you can navigate around the common pitfalls and enhance your proof strategies.

Hopefully, this guide provides clarity and practical steps for applying LTac effectively in your Coq proofs. Happy proving!