2

如果我有这样的谓词：

Inductive foo : nat -> nat -> Prop :=
  | Foo : forall n, foo n n.

然后我可以简单地使用归纳法来证明一些虚拟引理：

Lemma foo_refl : forall n n',
  foo n n' -> n = n'.
Proof.
  intros.
  induction H.
  reflexivity.
Qed.

但是，对于具有产品类型参数的谓词：

Inductive bar : (nat * nat) -> (nat * nat) -> Prop :=
  | Bar : forall n m, bar (n, m) (n, m).

几乎相同引理的类似证明被卡住了，因为所有关于变量的假设都消失了：

Lemma bar_refl : forall n n' m m',
  bar (n, m) (n', m') -> n = n'.
Proof.
  intros.
  induction H.
  (* :( *)

为什么会这样？如果我用 替换induction，inversion那么它的行为符合预期。

引理仍然可以证明，induction但需要一些解决方法：

Lemma bar_refl : forall n n' m m',
  bar (n, m) (n', m') -> n = n'.
Proof.
  intros.
  remember (n, m) as nm.
  remember (n', m') as n'm'.
  induction H.
  inversion Heqnm. inversion Heqn'm'. repeat subst.
  reflexivity.
Qed.

不幸的是，这种方式的证明变得非常混乱，并且对于更复杂的谓词是不可能遵循的。

一个明显的解决方案是这样声明bar：

Inductive bar' : nat -> nat -> nat -> nat -> Prop :=
  | Bar' : forall n m, bar' n m n m.

这解决了所有问题。然而，就我的目的而言，我发现以前的（“元组”）方法更加优雅。有没有办法保持谓词不变并且仍然能够进行可管理的归纳证明？问题甚至来自哪里？

4

4 回答 4

2

问题是归纳只能处理变量，而不是构造项。这就是为什么你应该首先证明类似的东西

Lemma bar_refl : forall p q, bar p q -> fst p = fst q.

通过now induction 1.证明你的引理可以简单地证明这一点。

如果您不希望中间引理有名字，那么您的解决方案是正确的：您需要帮助 Coqremember概括您的目标，然后您将能够证明它。

我不记得这个限制的确切来源，但我记得一些关于使一些统一问题无法确定的事情。

于 2016-01-19T16:28:13.467 回答
1

...所有关于变量的假设都消失了...为什么会这样？如果我用 替换induction，inversion那么它的行为符合预期。

发生这种情况的原因在这篇博客文章中得到了完美的描述： James Wilcox在没有 Axioms 的情况下使用 Coq 进行的依赖案例分析。让我引用这个案例最相关的部分：

当 Coq 执行案例分析时，它首先对所有索引进行抽象。在使用谓词时，您可能已经看到这表现为信息丢失destruct（例如尝试破坏even 3：它只是删除了假设！），或者在对具有具体索引的谓词进行归纳时（尝试forall n, even (2*n+1) -> False通过对假设的归纳来证明（而不是nat）——你会被卡住的！）。Coq 基本上忘记了索引的具体值。当试图对这样的假设进行归纳时，一种解决方案是用一个新变量以及一个强制变量等于正确的具体值的约束来替换每个具体索引。destruct做类似的事情：当给定一个具有具体索引值的归纳类型的术语时，它首先用新变量替换具体值。它不会添加等式约束（但inversion会添加）。这里的错误是关于抽象出索引。您不能只是用任意变量替换具体值并希望仍然进行类型检查。这只是一个启发式。

举一个具体的例子，当使用destruct H.一个时，模式匹配基本上是这样的：

Lemma bar_refl : forall n n' m m',
  bar (n, m) (n', m') -> n = n'.
Proof.
  intros n n' m m' H.
  refine (match H with
          | Bar a b => _
          end).

具有以下证明状态：

n, n', m, m' : nat
H : bar (n, m) (n', m')
a, b : nat
============================
n = n'

为了得到几乎准确的证明状态，我们应该H从上下文中删除，使用clear H.命令：refine (...); clear H.。这种相当原始的模式匹配不允许我们证明我们的目标。Coq 抽象出来(n, m)并(n',m')用一些对 和 替换它们p，p'例如p = (a, b)和p' = (a, b)。不幸的是，我们的目标是有形式n = n'的，它既没有(n,m)也没有(n',m')——这就是为什么 Coq 没有用a = a.

但是有一种方法可以告诉 Coq 这样做。我不知道如何使用策略来做到这一点，所以我将展示一个证明项。它看起来有点类似于@Vinz 的解决方案，但请注意我没有更改引理的陈述：

  Undo.  (* to undo the previous pattern-matching *)
  refine (match H in (bar p p') return fst p = fst p' with
          | Bar a b => _
          end).

这次我们为 Coq 添加了更多注释来理解H's 类型的组件和目标之间的联系——我们明确地命名了pandp'对，因为我们告诉 Coq 对待我们的目标，因为fst p = fst p'它将替换目标中的p和。我们的证明状态现在看起来像这样：p'(a,b)

n, n', m, m' : nat
H : bar (n, m) (n', m')
a, b : nat
============================
fst (a, b) = fst (a, b)

简单reflexivity就可以完成证明。

我认为现在应该清楚为什么destruct在以下引理中可以正常工作（不要看下面的答案，先尝试弄清楚）：

Lemma bar_refl_all : forall n n' m m',
  bar (n, m) (n', m') -> (n, m) = (n', m').
Proof.
  intros. destruct H. reflexivity.
Qed.

答案：因为目标包含假设类型中存在的相同对，所以 Coq 将它们全部替换为适当的变量，这样可以防止信息丢失。

于 2016-11-24T13:56:20.977 回答
1

通常在这种情况下，人们可以对其中一个子项进行归纳。

n在您的情况下，您的引理可以通过归纳证明

Lemma bar_refl : forall n n' m m',  bar (n, m) (n', m') -> n = n'.
Proof. induction n; intros; inversion H; auto. Qed.
于 2016-01-20T07:34:07.027 回答
0

另一种方式 ...

Lemma bar_refl n n' m m' : bar (n, m) (n', m') -> n = n'.
Proof.
  change (n = n') with (fst (n,m) = fst (n',m')).
  generalize (n,m) (n',m').
  intros ? ? [ ]; reflexivity.
Qed.
于 2016-11-24T10:33:26.713 回答