如何在Coq证明中复用引理lparen_concat完成自证？

我正在解决以下Coq问题，想了解如何在证明中再次复用引理本身作为假设。

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

(* +++ 为括号间的连接运算符 *)

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')

解决方法 #

在Coq的归纳证明中，直接递归调用引理本身即可，只要递归参数满足良基性（这里lp'是原始l的子结构，符合归纳终止要求）。

在剩余目标的位置执行以下步骤：

1. 调用引理本身：apply lparen_concat.
2. 此时会生成两个子目标，分别用上下文里的假设证明：
   • 第一个子目标lparen lp'用IHHl'证明：apply IHHl'.
   • 第二个子目标lparen l'用IHl'证明：apply IHl'.

补全后的完整证明如下：

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.
    + apply lparen_concat.
      * apply IHHl'.
      * apply IHl'.
Qed.

内容的提问来源于stack exchange，提问作者Liu