Coq - 在不丢失信息的情况下对函数进行归纳答案

【问题标题】：Coq - Induction over functions without losing informationCoq - 在不丢失信息的情况下对函数进行归纳
【发布时间】：2013-12-31 12:18:42
【问题描述】：

在尝试对函数的结果（返回归纳类型）进行案例分析时，我在 Coq 中遇到了一些麻烦。当使用常用策略时，如elim、induction、destroy 等，信息会丢失。

我举个例子：

我们首先有一个这样的函数：

Definition f(n:nat): bool := (* definition *)

现在，假设我们正处于证明特定定理的这一步：

n: nat
H: f n = other_stuff
------
P (f n )

当我应用一种策略时，比如induction (f n)，就会发生这种情况：

Subgoal 1
n:nat
H: true = other_stuff
------
P true

Subgoal 2
n:nat
H: false = other_stuff
------
P false

但是，我想要的是这样的：

Subgoal 1
n:nat
H: true = other_stuff
H1: f n = true
------
P true

Subgoal 2
n:nat
H: false = other_stuff
H1: f n = false 
------
P false

实际上，我丢失了信息，特别是丢失了有关f n 的任何信息。在我处理的问题中，我需要使用f n = true 或f n = false 的信息，用于其他假设等。有没有办法做第二个选项？我尝试使用cut(f n = false \/ f n = true) 之类的东西，但它变得非常烦人，特别是当我连续有几个这样的“特殊”感应时。我想知道是否有一些基本上与上面的cut 完全一样的东西，但策略/证明更少

【问题讨论】：

标签： coq induction

【解决方案1】：

问题是您在构造术语上执行induction，而不是单个变量。事实证明，将信息保存在您的案例中是一个非常困难的问题。

通常的解决方法是使用remember 策略抽象您构造的术语。我现在没有确切的语法，但你应该尝试类似

remember (f n) as Fn. (* this introduces an equality HeqFn : Fn = f n *)
revert f n HeqFn. (* this is useful in many cases, but not mandatory *)
induction Fn; intros; subst in *.

希望对你有帮助，五、

【讨论】：

谢谢！它确实对我有用，但我必须这样做：remember (f n) as Fn.，然后是 induction Fn.，它对 Fn 进行了归纳（在这种情况下，true 有一个子目标，false 有一个子目标），但在HeqFn 保留了有关 (fn) 的信息，HeqFn : true = f n 或 HeqFn : false = f n。干杯! （编辑：revert f n HeqFn 对我来说不是必需的。不知道您是否应该将其保留在答案中）
很高兴知道，在我的经历中，我总是不得不使用revert。很高兴得到其他用户的反馈：D 谢谢！
我尝试了还原，但这只会将某些内容从“H |- G”更改为“|- H-> G”（即反转介绍）。不知道这在这种情况下如何真正有用：P
当您有一个比f n 复杂一点的术语时，它会变得很有用，例如与其他变量/参数。如果您需要非常强大的归纳假设，您可能需要恢复这些变量/参数（这也迫使您恢复等式）。我只是意识到这是我的情况，因此我总是恢复平等。
在这种情况下，我通常使用“case_eq”策略而不是“destruct”。