Coq-在不丢失信息的情况下归纳功能 [英] Coq - Induction over functions without losing information

问题描述

在尝试对函数结果进行案例分析(返回归纳类型)时，我在Coq中遇到了一些麻烦.使用elim，induction，destroy等常用策略时，信息会丢失.

I'm having some troubles in Coq when trying to perform case analysis on the result of a function (which returns an inductive type). When using the usual tactics, like elim, induction, destroy, etc, the information gets lost.

我举个例子:

我们首先有一个像这样的功能:

We first have a function like so:

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

现在，想象一下我们正处于特定定理证明的这一步:

Now, imagine we are at this step in the proof of a specific theorem:

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

当我采用战术时，例如induction (f n)，会发生这种情况:

When I apply a tactic, like let's say, induction (f n), this happens:

Subgoal 1
n:nat
H: true = other_stuff
------
P true

Subgoal 2
n:nat
H: false = other_stuff
------
P false

但是，我想要的是这样的东西:

However, what I want is something like this instead:

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完全一样的东西，但是战术/证明较少

In the way it actually works, I lose information, specially I lose any information about f n. In the problems I work with, I need to use the information that f n = true or f n = false, to use with other hypothesis, etc. Is there a way to do the 2nd option? I tried using stuff like cut(f n = false \/ f n = true) but it becomes very tiresome, specially when I have several of these "special" inductions in a row. I want to know if there is something that basically works exactly like the cut above, but with fewer tactics/proofs

推荐答案

问题是您对构造的术语而不是单个变量执行induction.将信息保存在您的案例中已被证明是一个非常困难的问题.

The issue is that you perform induction on a constructed term, not a single variable. Keeping the information in your case has been proved to be a very difficult problem.

通常的解决方法是使用remember策略来抽象您构造的术语.我现在没有确切的语法，但是您应该尝试类似

The usual work-around is to abstract your constructed term using the remember tactic. I don't have the exact syntax in mind right now but you should try something like

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.

这篇关于Coq-在不丢失信息的情况下归纳功能的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！