Coq中仅使用一次的引理如何处理？是否存在问题？

问题 #

我声明了一个仅在Theorem SoS_equiv_SoS2的证明中使用的引理SoS2_imp_Pos，请问这种做法是否存在问题？除了定义引理的方式外，还有什么其他处理方案？我考虑过使用assert forall s t u, SoS2 u s t -> PoS s u，但不确定这是否是更优选择。

附原代码：

Lemma SoS2_imp_Pos: forall s t u, SoS2 u s t -> PoS s u.
Proof.
  intros s t u H; apply NNPP; intros NPoSsu.
  pose proof (slot_strong_supp u s NPoSsu) as (v & PoSvs & NOoSvu).
  apply pos_implies_overlap in PoSvs.
  destruct H with (v:=v).
  destruct H1.
  left; apply oos_comm; assumption.
  apply NOoSvu.
  exists x; apply and_comm; assumption.
Qed.

Theorem SoS_equiv_SoS2: forall u s t, SoS u s t <-> SoS2 u s t.
Proof.
  intros u s t.
  split.
  - intros (PoSsu & PoStu & H) v.
    split.
    + intros (w & PoSwu & PoSwv).
      pose proof (H w PoSwu) as [H1|H1];
      [left|right];
      apply part_overlap_implies_whole_overlap with (t:=w);
      assumption.
    + intros [|];
      apply oos_comm in H0;
      apply oos_comm;
      [apply part_overlap_implies_whole_overlap with (t:=s)|
       apply part_overlap_implies_whole_overlap with (t:=t)];
      assumption.
  - intros H.
    repeat split.
    + apply SoS2_imp_Pos with (t:=t); assumption.
    + apply SoS2_imp_Pos with (t:=s).
      unfold SoS2 in *.
      setoid_rewrite (or_comm (OoS s _)) in H.
      assumption.
    + intros v PoSvu.
      apply H.
      apply oos_comm.
      apply pos_implies_overlap.
      assumption.
Qed.

解答 #

单独声明引理的做法是否有问题？ #

这种做法本身没有逻辑问题，但存在两个小弊端：

• 会污染全局命名空间：如果项目规模变大，这类仅局部使用的引理名字可能和其他地方的定义冲突；
• 可读性稍差：其他阅读代码的人可能会疑惑这个引理是否在其他地方被使用，需要额外确认。

不过它也有优点：引理可以单独编译、测试，调试时能单独验证这部分逻辑的正确性，适合证明较长、逻辑独立的辅助命题。

替代处理方案 #

1. 使用assert（你考虑的方案）

这是处理局部辅助命题的常用方式，把引理嵌入到定理的证明内部，不会污染全局命名空间。

修改后的代码示例：

Theorem SoS_equiv_SoS2: forall u s t, SoS u s t <-> SoS2 u s t.
Proof.
  intros u s t.
  (* 声明局部辅助引理 *)
  assert (SoS2_imp_Pos: forall s' t' u', SoS2 u' s' t' -> PoS s' u').
  {
    intros s' t' u' H; apply NNPP; intros NPoSsu.
    pose proof (slot_strong_supp u' s' NPoSsu) as (v & PoSvs & NOoSvu).
    apply pos_implies_overlap in PoSvs.
    destruct H with (v:=v).
    destruct H1.
    left; apply oos_comm; assumption.
    apply NOoSvu.
    exists x; apply and_comm; assumption.
  }
  split.
  - intros (PoSsu & PoStu & H) v.
    split.
    + intros (w & PoSwu & PoSwv).
      pose proof (H w PoSwu) as [H1|H1];
      [left|right];
      apply part_overlap_implies_whole_overlap with (t:=w);
      assumption.
    + intros [|];
      apply oos_comm in H0;
      apply oos_comm;
      [apply part_overlap_implies_whole_overlap with (t:=s)|
       apply part_overlap_implies_whole_overlap with (t:=t)];
      assumption.
  - intros H.
    repeat split.
    + apply SoS2_imp_Pos with (t:=t); assumption.
    + apply SoS2_imp_Pos with (t:=s).
      unfold SoS2 in *.
      setoid_rewrite (or_comm (OoS s _)) in H.
      assumption.
    + intros v PoSvu.
      apply H.
      apply oos_comm.
      apply pos_implies_overlap.
      assumption.
Qed.

这种方案的优势是代码紧凑，局部性强，适合证明较短的辅助命题；缺点是如果辅助引理的证明很长，会让定理的整体证明显得臃肿，可读性下降。

2. 使用Section包裹局部引理

如果辅助引理的证明较长，又不想污染全局命名空间，可以用Section把引理和定理包裹起来。Section结束后，内部定义的引理就会被隐藏，不会影响全局命名空间。

修改后的代码示例：

Section SoS_Equivalence.

Lemma SoS2_imp_Pos: forall s t u, SoS2 u s t -> PoS s u.
Proof.
  intros s t u H; apply NNPP; intros NPoSsu.
  pose proof (slot_strong_supp u s NPoSsu) as (v & PoSvs & NOoSvu).
  apply pos_implies_overlap in PoSvs.
  destruct H with (v:=v).
  destruct H1.
  left; apply oos_comm; assumption.
  apply NOoSvu.
  exists x; apply and_comm; assumption.
Qed.

Theorem SoS_equiv_SoS2: forall u s t, SoS u s t <-> SoS2 u s t.
Proof.
  intros u s t.
  split.
  - intros (PoSsu & PoStu & H) v.
    split.
    + intros (w & PoSwu & PoSwv).
      pose proof (H w PoSwu) as [H1|H1];
      [left|right];
      apply part_overlap_implies_whole_overlap with (t:=w);
      assumption.
    + intros [|];
      apply oos_comm in H0;
      apply oos_comm;
      [apply part_overlap_implies_whole_overlap with (t:=s)|
       apply part_overlap_implies_whole_overlap with (t:=t)];
      assumption.
  - intros H.
    repeat split.
    + apply SoS2_imp_Pos with (t:=t); assumption.
    + apply SoS2_imp_Pos with (t:=s).
      unfold SoS2 in *.
      setoid_rewrite (or_comm (OoS s _)) in H.
      assumption.
    + intros v PoSvu.
      apply H.
      apply oos_comm.
      apply pos_implies_overlap.
      assumption.
Qed.

End SoS_Equivalence.

这种方案兼顾了单独证明引理的清晰性和局部性，适合辅助引理逻辑独立、证明较长的场景。

方案选择建议 #

• 如果辅助引理的证明很短（几行），用assert更紧凑；
• 如果辅助引理的证明较长，用Section包裹的单独引理更易维护和调试；
• 全局声明引理只适合那些需要在多个定理中复用的辅助命题。

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