我目前正在尝试在Coq中实现Hilbert的几何。在证明时，证明的一部分经常被重复多次；例如，在这里我试图证明存在3条彼此不同的线。
Proposition prop3_2 : (exists l m n: Line, (l<>m/m<>n/n<>l)).
Proof.
destruct I3 as [A [B [C [[AneB [BneC CneA]] nAlgn]]]].
destruct ((I1 A B) AneB) as [AB [incAB unAB]].
destruct ((I1 B C) BneC) as [BC [incBC unBC]].
destruct ((I1 C A) CneA) as [CA [incCA unCA]].
refine (ex_intro _ AB _).
refine (ex_intro _ BC _).
refine (ex_intro _ CA _).
split.
(* Proving AB <> BC through contradiction *)
case (classic (AB = BC)).
intros AB_e_BC.
rewrite AB_e_BC in incAB.
pose (conj incBC (proj2 incAB)) as incABC.
specialize (nAlgn BC).
tauto.
trivial.
split.
(* Proving BC <> CA through contradiction *)
case (classic (BC = CA)).
intros BC_e_CA.
rewrite BC_e_CA in incBC.
pose (conj incCA (proj2 incBC)) as incABC.
specialize (nAlgn CA).
tauto.
trivial.
(* Proving CA <> AB through contradiction *)
case (classic (CA = AB)).
intros CA_e_AB.
rewrite CA_e_AB in incCA.
pose (conj incAB (proj2 incCA)) as incABC.
specialize (nAlgn AB).
tauto.
trivial.
Qed.
如果在这些情况下有一个类似宏的东西，那就太好了。我想在中途创建一个子证明：
Lemma prop3_2_a: (forall (A B C:Point) (AB BC:Line)
(incAB:(Inc B AB / Inc A AB)) (incBC:(Inc C BC / Inc B BC))
(nAlgn : forall l : Line, ~ (Inc A l / Inc B l / Inc C l)),
AB <> BC).
Proof.
...
但这很麻烦，我必须创建三个不同版本的nAlgn，以不同的顺序排列，这是可以管理的，但很烦人。
代码可在此处找到：https://github.com/GiacomoMaletto/Hilbert/blob/master/hilbert.v
(顺便说一句，任何其他关于风格的评论或其他任何值得赞赏的东西(。
首先，给出一些简单的建议，分别重构这三种情况。
在每一个开始的时候，目标看起来是这样的：
...
--------------
AB <> BC
随后对(AB = BC)的案例分析有些多余。第一种情况(AB = BC)是有趣的，需要证明一个矛盾，而第二种情况(AB <> BC)是琐碎的。一个较短的方法是intro AB_e_BC，它只要求您证明第一个案例。这是因为AB <> BC实际上意味着AB = BC -> False。
其他步骤大多是直接的命题推理，可以通过tauto进行，除了一些重写和specialize的关键使用。重写只使用变量AB和BC之间的等式，在这种情况下，您可以使用subst简写法，在一侧为变量的情况下使用所有等式进行重写。所以这个片段：
(* Proving AB <> BC through contradiction *)
case (classic (AB = BC)).
intros AB_e_BC.
rewrite AB_e_BC in incAB.
pose (conj incBC (proj2 incAB)) as incABC.
specialize (nAlgn BC).
tauto.
trivial.
成为
intro; specialize (nAlgnABC BC); subst; tauto.
现在你还是不想写三次。现在唯一变化的部分是变量BC。幸运的是，你可以在intro之前从进球中读出这一点。
--------------
AB <> BC
^----- there's BC (and in the other two cases, CA and AB)
实际上，选择AB或BC是可以的，因为intro假设它们相等。你可以使用match goal with根据进球的位置来参数化你的战术。
match goal with
| [ |- _ <> ?l ] => intro; specialize (nAlgnABC l); subst; tauto
end.
(* The syntax is:
match goal with
| [ |- ??? ] => tactics
end.
where ??? is an expression with wildcards (_) and existential
variables (?l), that can be referred to inside the body "tactics"
(without the question mark) *)
接下来，在拆分前向上移动：
-------------------------------------------
AB <> BC / BC <> CA / CA <> AB
你可以制定策略，一次得到三个子目标：split; [| split].(意思是分裂一次，在第二个子目标中再次分裂(。
最后，您希望将上面的match策略应用于每个子目标，这是另一个分号：
split; [| split];
match goal with
| [ |- _ <> ?l ] => intro; specialize (nAlgnABC l); subst; tauto
end.
我还建议使用项目符号和大括号来构建你的证明，这样当你的定义发生变化时，你就可以避免因为策略应用于错误的子目标而进入令人困惑的证明状态。以下是三种情况证明的一些可能布局：
split.
- ...
...
- split.
+ ...
...
+ ...
...
split; [| split].
- ...
...
- ...
...
- ...
...
split; [| split].
{ ...
...
}
{ ...
...
}
{ ...
...
}