当尝试对函数的结果（返回归纳类型）执行案例分析时，我在 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 or f n = false，与其他假设一起使用等。
有办法做第二个选项吗？
我尝试使用类似的东西cut(f n = false \/ f n = true)但这变得非常烦人，特别是当我连续进行几次这样的“特殊”归纳时。我想知道是否有一些东西基本上与cut如上所述，但策略/证据较少
问题是你执行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 *.
希望能帮助到你，
五、
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
