4

这是自然数均匀性的归纳和计算定义。

Inductive ev : nat -> Prop :=
  | ev_0 : ev O
  | ev_SS : forall n:nat, ev n -> ev (S (S n)).

Definition even (n:nat) : Prop := 
  evenb n = true.

以及一个暗示另一个的证明。

Theorem ev__even : forall n,
  ev n -> even n.
intros n E.
induction E as [ | n' E' ]. 
reflexivity. apply IHE'. Qed.

起初我并没有多想这个证据，但仔细一看，我发现了一些令人不安的事情。问题是在这reflexivity一步之后，我希望看到上下文

1 subgoal
n' : nat
E : ev (S (S n'))
E' : ev n'
IHE' : ev n' -> even n'
====================================================================== (1/1)
even (S (S n'))

但我实际上得到的是

1 subgoal
n' : nat
E' : ev n'
IHE' : even n'
====================================================================== (1/1)
even (S (S n'))

尽管这个定理仍然可以证明，但看到假设神秘地消失是令人不安的。我想知道如何获得我最初期望的上下文。从网络搜索中，我了解到这是对 Coq 中构造术语进行归纳的一般问题。关于 SO 的一种建议解决方案建议使用remember保留假设的策略。但是当我在这个证明中尝试这样做时，

Theorem ev__even : forall n,
  ev n -> even n.
intros n E.
remember E.
induction E as [ | n' E' ].

induction我在步骤中收到以下错误消息。

Error: Abstracting over the term "n" leads to a term
"fun n : nat => forall e : ev n, e = E -> even n" which is ill-typed.

我不太明白。我认为问题在于它E有一个自由变量，但在那种情况下我会被卡住，因为没有E引入n. （generalize dependent n会用它来概括E）

有没有办法获得最初预期的上下文？

4

2 回答 2

3

为了有用，归纳策略试图概括所有依赖于你正在做归纳的事物的变量，以及依赖于其类型索引的事物。在您的情况下，这意味着n对新生成的证明e : ev n和等式进行泛化e = E。然而，它并没有对E自身进行概括，因为为命题自动生成的归纳原则忽略了证明论证。不幸的是，这意味着泛化将是错误类型的，并且您的直觉是正确的：因为E没有使用 进行泛化n，所以它的类型会提到一个不同的数字，这将使等式成为错误e = E类型。

于 2014-06-29T11:32:17.913 回答
2

我不明白这个induction战术在这里做什么。每当我不明白一个策略在做什么时，我都会尝试自己编写证明项。如果你手动调用归纳原理，你可以保持原假设：

Theorem ev__even : forall n, ev n -> even n.
  intros n E.
  refine (ev_ind even _ _ n E).
  - reflexivity.
  - intros n' E' IH.
    apply IH.
Qed.

这是归纳的第二种情况下的上下文：

  n : nat
  E : ev n
  n' : nat
  E' : ev n'
  IH : even n'
  ============================
   even (S (S n'))

假设

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O        => true
  | S O      => false
  | S (S n') => evenb n'
  end.
于 2014-06-28T16:35:27.813 回答