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

当我尝试对函数的结果（返回归纳类型）执行实例分析时，我在Coq中遇到了一些麻烦。当使用通常的战术，如elim,induction,destroy等，信息会丢失。Coq - 在不丢失信息的情况下对函数进行归纳

我会把一个例子：

我们首先像这样的功能：

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一样，但是用较少的策略/证明

来源

2013-12-12 gonzaw

问题是，您对构造的术语执行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 *.

希望它能帮助，五

来源

2013-12-13 08:55:31 Vinz

谢谢！它确实对我有效，但我必须这样做：“记住（Fn）为Fn.”，接着是“归纳Fn”。然后，它通过Fn进行归纳（在这种情况下，一个子目标为“真”对于'false'），但是在HeqFn中保存了（fn）的信息，无论是“HeqFn：true = fn”还是“HeqFn：false = fn”。干杯! （编辑：'回复fn HeqFn'对我来说没有必要，不知道是否应该保留在答案中） – gonzaw

很高兴知道，我总是不得不在我的经历中使用'revert'。从其他用户得到反馈是很好的：D谢谢！ – Vinz

我试过还原，但是只是将某些东西从“H | - G”改变为“| - H-> G”（即介绍反转）。不知道在这种情况下这很有用：P – gonzaw

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

回答

相关问题