coq - 不需要在子项上使用“记住”的归纳策略的变体

Question

假设我有两个关系R1和R2。如果我需要通过对术语的归纳来解决问题R1 A (R2 B C)，我需要先做remember R2 B C，否则我会丢失第二个参数R1等于的信息R2 B C。是否有一种不需要我处理这个策略的感应变体？

标签： coqcoq-tactic

Answer 1

答案是不。

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