Coq - 不丢失信息的函数归纳

Question

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

我来举个例子：

我们首先有一个函数：

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

现在，想象我们正在证明一个特定定理的步骤中：

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

当我使用一种策略，比如说，归纳（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完全相同，但使用更少的策略/证明的方法。

- gonzaw

Answer 1

问题是你对构造的术语进行归纳，而不是单个变量。保留你的案例信息已被证明是一个非常困难的问题。

通常的解决方法是使用“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.

- Vinz

---

谢谢！对我有用，但我必须这样做：remember (f n) as Fn. 然后跟着执行 induction Fn. 这样就能对 Fn 进行归纳（在这种情况下，一个子目标为 true，另一个为 false），但在 HeqFn 中仍保留了关于 (f n) 的信息，即 HeqFn : true = f n 或 HeqFn : false = f n。干杯！（编辑：对我来说，revert f n HeqFn 是不必要的。不知道你是否应该在答案中保留它） - gonzaw

很高兴知道，我在以前的经验中总是不得不使用“revert”。能够得到其他用户的反馈真是太好了:D谢谢！ - Vinz

我尝试了回退，但那只是将"H |- G"变成了"| - H-> G"（即介绍的反向）。不知道在这种情况下它真的有多大用处 :P - gonzaw

当你有一个比 f n 更复杂的术语时，例如带有其他变量/参数时，它就非常有用。如果你需要归纳假设真正强大，你可能需要恢复这些变量/参数（这也迫使你恢复相等关系）。我意识到这正是我的情况，这就是为什么我总是恢复相等关系。 - Vinz

我在这种情况下通常使用“case_eq”策略，而不是“destruct”。 - krokodil