Избегайте повторения в 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

(Btw Любые другие комментарии по стилю или что-нибудь ценное).

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