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

Question

在尝试对函数的结果(返回归纳类型)执行案例分析时，我在 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 基本相同的东西以上，但策略/证明较少

Answer 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 *.

希望能帮助到你，
五、