如何处理Coq中只使用一次的引理?

Question

我声明了一个引理，只用于一个证明(代码中的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.

Answer 1

相反，您可以为它找到一个好名字(something_imp_something_else)，这通常是一个好迹象，表明该引理以后可以重用。

Answer 2

不，我觉得还可以。如果你想强调这只是证明的一个步骤，你可以把它降级为Remark。