避免在 Coq 中重复

Question

我目前正在尝试在 Coq 中实现希尔伯特几何。证明时，证明的一部分经常重复多次；例如，这里我试图证明存在 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

（顺便说一句，任何其他 cmets 的风格或任何赞赏）。

Answer 1

首先，一些简单的建议，分别重构这三个案例。

在他们每个人的开始，目标是这样的：

...
--------------
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].
{ ...
  ...
}
{ ...
  ...
}
{ ...
  ...
}