避免在 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

（顺便说一句，任何其他关于风格的评论或任何赞赏）。

Answer 1

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

在每个开始时，目标看起来像这样：

...
--------------
AB <> BC

后面对(AB = BC)的案例分析有些多余。第一种情况 (AB = BC) 很有趣，你需要证明矛盾，第二种情况 (AB <> BC) 很简单。一种较短的方法是 intro AB_e_BC，它只要求您证明第一种情况。这是有效的，因为 AB <> BC 实际上意味着 AB = BC -> False.

其他步骤大多是简单的命题推理，可以通过 tauto 强制执行，除了一些重写和 specialize 的关键使用。重写仅使用变量 AB 和 BC 之间的等式，在这种情况下，您可以使用 subst shorthand 重写，其中一侧是变量。所以这个片段：

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

避免在 Coq 中重复

Avoid repetition in Coq

dry

coq