不需要在子词上使用`remember`的归纳策略的变体

问题描述 投票:0回答:1

假设我有两个关系R1R2。如果我需要通过对R1 A (R2 B C)进行归纳来解决问题,则需要先执行remember R2 B C,否则我将丢失R1的第二个参数等于R2 B C的信息。是否有一种不需要我应对这种策略的归纳法变体?

coq coq-tactic
1个回答
0
投票

答案为否。>

归纳的工作方式,它用出现在归纳谓词构造函数中相同位置的值替换每个参数的每个实例。为了简化操作,remember策略用一个变量替换复合表达式(R2 B C)。如果您的目标中出现(R2 B C),您有时可以避免这种情况,但这很少见。

© www.soinside.com 2019 - 2024. All rights reserved.