在Coq中使用“断言”创建的展开术语
可以找到所讨论的证明在这里。在当前状态下，我想在假设eqveq中展开eqvid eqvneg ，以简化投影并获得矛盾的平等性两个不同的功能。但是，这两个术语使用servert策略合成为子观念，并且当前环境似乎没有对术语值的记忆。我知道我可以手动写两个术语，但这在我看来会很麻烦。是否有一种更优雅的方法来恢复解决子目标时产生的定义？
The proof in question can be found here. At the current state, I would like to unfold eqvid and eqvneg in hypothesis eqveq, in order to simplify the projection and obtain a contradictory equality between two different functions. However, these two terms were synthesized as subgoals using the assert tactic, and it seems that the current environment bears no memory of the values of the terms. I know that I could write the two terms manually, but that would be quite cumbersome in my opinion. Is there a more elegant way to recover the definitions generated in solving the subgoals?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
incant：
姿势/set是透明的，而sustert不是。_成为一个新的存在变量（或更标准的条件中的统一变量）。正常的姿势会失败，因为它无法解决变量，但是epose跳过了支票。存在变量通常不会直接受到策略的攻击（它们是通过统一解决的），因此它们会自动搁置，但是unshelve采用了由其控制的策略所制造的所有EVAR，并将其转化为目标。用此替换断言（如果需要的话，可以进行自定义符号）并
完成证明。
请注意，如果您这样做，则证明状态将迅速不可读。避免这种方法的技巧是拥有
和使用
。然后，直到您揭示该假设，假设不会显示凌乱的术语。
Incant:
pose/setare transparent whileassertis not. The_becomes a new existential variable (or unification variable in more standard parlance). A normalposewould fail because it can't solve for the variable, buteposeskips the check. Existential variables aren't usually attacked by tactics directly (they are solved for by unification), so they are automatically shelved, butunshelvetakes all the evars made by the tactic it controls and turns them into goals.Replace the asserts with this (you could make a custom notation if you wanted) and
finishes your proof.
Note that the proof state gets rapidly unreadable if you do this. A trick to avoid that is to have
And use
instead. Then the hypotheses will not show the messy term until you reveal it.