Coq 使用引理本身进行证明

Question

我正在解决下面的 Coq 问题，我很好奇如何再次重复使用引理本身（作为假设）来进行证明。

Inductive lparen : T -> Prop :=
| leps : lparen eps
| lseq : forall (lp: T) (lp': T), lparen lp /\ lparen lp' -> lparen (LPs +++ lp +++ RPs +++ lp').

(* +++ operator concats between parenthesess *)

Lemma lparen_concat : forall l l':T, lparen l -> lparen l' -> lparen (l +++ l').
Proof.
  intros l l' IHl IHl'.
  induction IHl as [|lp lp' [IHHl IHHl']].
  - simpl.
    assumption.
  - rewrite par_assoc.
    apply lseq.
    split.
    + assumption.
    +
Qed.

剩下的目标是跟随

lparen (lp' +++ l')

，这可以通过再次应用

lparen_concat

本身来证明。

l', lp, lp' : T
IHHl : lparen lp
IHHl' : lparen lp'
IHl' : lparen l'
-----------------------
lparen (lp' +++ l')

Answer 1

请注意，在你的证明中，当你做

induction IHl as [|lp lp' [IHHl IHHl']]

时，

IHHl

和

IHHl'

是不是归纳假设。原因是您以不规范的方式编写了归纳谓词，因此 Coq 推断归纳方案的默认方法失败了。

相反，尝试像这样定义归纳谓词：

Inductive lparen : T -> Prop :=
| leps : lparen eps
| lseq : forall (lp: T) (lp': T), lparen lp -> lparen lp' -> lparen (LPs +++ lp +++ RPs +++ lp').

区别在于我们给出了两个前提条件

lparen lp

和

lparen lp'

，而不是一个连词。在 Coq 中，这更加自然（因为

->

是一个原语）。

那么，归纳方案实际上包含了归纳假设，这使得证明得以通过：

Lemma lparen_concat : forall l l':T, lparen l -> lparen l' -> lparen (l +++ l').
Proof.
  intros l l' Hl Hl'.
  induction Hl as [|lp lp' Hlp IHlp  Hlp' IHlp']].
  - simpl.
    assumption.
  - rewrite par_assoc.
    apply lseq.
    split.
    + assumption.
    + apply IHlp'.
Qed.

请注意，

Hlp

对应于您的

IHHl

，尽管它不是归纳假设，但它的名称令人困惑的是

IH

。同样，第一行中的

intro

d 不是归纳假设，因此按照惯例未命名为

IH

。