用产品类型参数对谓词进行归纳 [英] Induction on predicates with product type arguments

问题描述

如果我有这样的谓词:

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.

这解决了所有问题.但是，出于我的目的，我发现以前的(纠缠")方法更为优雅.有没有一种方法可以使谓词保持原样，并且仍然能够进行可管理的归纳证明?问题甚至从何而来?

解决方案

问题是归纳只能使用变量，不能使用构造的术语.这就是为什么您应该首先证明类似

的原因

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

这是now induction 1.证明您的引理的简单证明.

如果您不希望中间引理有一个名称，那么您的解决方案是正确的:您需要使用remember帮助Coq概括您的目标，然后您就可以证明它./p>

我不记得这个限制的确切来源，但是我想起了一些无法确定的统一问题.

If I have a predicate like this:

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

then I can trivially use induction to prove some dummy lemmas:

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

However, for a predicate with product type arguments:

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

a similar proof for nearly identical lemma gets stuck because all assumptions about variables disappear:

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

Why is this happening? If I replace induction with inversion, then it behaves as expected.

The lemma is still provable with induction but requires some workarounds:

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.

Unfortunately, this way proofs gets completely cluttered and are impossible to follow for more complicated predicates.

One obvious solution would be to declare bar like this:

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

This solves all the problems. Yet, for my purposes, I find the previous ("tupled") approach somewhat more elegant. Is there a way to keep the predicate as it is and still be able to do manageable inductive proofs? Where does the problem even come from?

解决方案

The issue is that induction can only works with variables, not constructed terms. This is why you should first prove something like

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

which is trivially proved by now induction 1. to prove your lemma.

If you don't want the intermediate lemma to have a name, your solution is the correct one: you need to help Coq with remember to generalize your goal, and then you'll be able to prove it.

I don't remember exactly where this restriction comes from, but I recall something about making some unification problem undecidable.

这篇关于用产品类型参数对谓词进行归纳的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！