对具有产品类型参数的谓词进行归纳

Question

如果我有这样的谓词：

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.
  (* :( *)

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

引理仍然可以用 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.

这解决了所有问题。然而，就我的目的而言，我发现以前的 ("tupled") 方法更优雅一些。有没有办法保持谓词不变，并且仍然能够进行可管理的归纳证明？问题到底来自哪里？

Answer 1

问题是归纳法只适用于变量，不适用于构造项。这就是为什么你应该首先证明类似

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

now induction 1. 证明了你的引理。

如果您不希望中间引理有名称，您的解决方案是正确的：您需要帮助 Coq remember 来概括您的目标，然后您将能够证明一下。

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

Answer 2

通常在这些情况下，可以对 sub-terms 之一进行归纳。

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

Lemma bar_refl : forall n n' m m',  bar (n, m) (n', m') -> n = n'.
Proof. induction n; intros; inversion H; auto. Qed.

Answer 3

另一种方式...

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.

Answer 4

... all assumptions about variables disappear... Why is this happening? If I replace induction with inversion, then it behaves as expected.

此博客 post 中完美描述了发生这种情况的原因： Dependent Case Analysis in Coq without Axioms 詹姆斯·威尔科克斯。让我引用与此案例最相关的部分：

When Coq performs a case analysis, it first abstracts over all indices. You may have seen this manifest as a loss of information when using destruct on predicates (try destructing even 3 for example: it just deletes the hypothesis!), or when doing induction on a predicate with concrete indices (try proving forall n, even (2*n+1) -> False by induction on the hypothesis (not the nat) -- you'll be stuck!). Coq essentially forgets the concrete values of the indices. When trying to induct on such a hypothesis, one solution is to replace each concrete index with a new variable together with a constraint that forces the variable to be equal to the correct concrete value. destruct does something similar: when given a term of some inductive type with concrete index values, it first replaces the concrete values with new variables. It doesn't add the equality constraints (but inversion does). The error here is about abstracting out the indices. You can't just go replacing concrete values with arbitrary variables and hope that things still type check. It's just a heuristic.

举一个具体的例子，当使用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'

为了获得几乎准确的证明状态，我们应该使用 clear H. 命令从上下文中删除 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 类型的组件与目标之间的联系——我们明确命名了 p 和 p' 对因为我们告诉 Coq 将我们的目标视为 fst p = fst p'，所以它将用 (a,b) 替换目标中的 p 和 p'。我们的证明状态现在看起来像这样：

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 将它们全部替换为适当的变量，这将防止信息丢失。

对具有产品类型参数的谓词进行归纳

Induction on predicates with product type arguments

coq

induction

coq-tactic