4

尝试对函数的结果（返回归纳类型）执行案例分析时，我在 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上述完全一样的东西，但策略/证据较少

4

1 回答 1

4

问题是您执行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 *.

希望对你有帮助，V。

于 2013-12-13T08:55:31.123 回答