CAP, Coq и Евклид30.12.2024 21:15

ef622b3bf8ccc13974da549fb478f926.png

Продолжаем серию статей о CAP-теореме и языке Coq. В предыдущей части мы детально проанализировали определения CAP-теоремы, готовясь к её формализации на языке Coq, и нашли там серьёзную ошибку (теперь будет о чём поговорить при случае на system design interview).

В этой статье мы познакомимся с основами языка Coq и для практики формализуем небольшой фрагмент геометрической системы, близкой к евклидовой.

О пользе Coq

Что такое Coq? Процитирую википедию (выделение моё):

Coq (фр. coq — петух) — интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования (Gallina)[2] с зависимыми типами. Позволяет записывать математические теоремы и их доказательства, удобно модифицировать их, проверяет их на правильность. Пользователь интерактивно создаёт доказательство сверху вниз, начиная с цели (то есть от гипотезы, которую необходимо доказать). Coq может автоматически находить доказательства в некоторых ограниченных теориях с помощью так называемых тактик.

Зачем это может быть нужно? Если бы все математики использовали средства типа Coq, то при анализе доказательства теоремы Ферма можно было бы избежать вот такой ситуации:

Доказательство представляло собой гигантскую цепочку рассуждений, весьма хитроумно выстроенных из сотен математических вычислений, склеенных воедино логическими связями.
…
«Вопросы возникали вплоть до августа, — вспоминает Катц, — пока я не наткнулся на нечто, показавшееся еще одной небольшой проблемой. Где-то около 23 августа я отправил Эндрю запрос по электронной почте. Проблема оказалась несколько более сложной, поэтому ответ Эндрю прислал по факсу. Меня этот ответ не удовлетворил, поэтому я еще раз направил Эндрю запрос по электронной почте и получил еще один ответ по факсу, который меня также не удовлетворил».

Уайлс поначалу предполагал, что очередная ошибка столь же несерьезна, как и предыдущие…

Саймон СИНГХ, ВЕЛИКАЯ ТЕОРЕМА ФЕРМА

Напрашиваются очевидные аналогии с разработкой ПО:

Я четыре раза прочитал этот код, но так и не увидел ошибку. И решил, что это ложное срабатывание, которое надо править. Но прав анализатор, а я просто невнимательный человек.

habr: Любите статический анализ кода

Только вот «анализатор» Эндрю Уайлс и Ник Катц не использовали…

С abc-гипотезой дело обстояло ещё более драматично:

На математическом форуме MathOverflow математики со всего мира стали оспаривать и обсуждать заявление Мотидзуки. Вопрос, который быстро стал самым популярным на форуме, был прост: «Кто-нибудь может объяснить философию его работы и прокомментировать, почему она может пролить свет на abc-гипотезу?» — спросил Энди Путман, ассистент профессора в Университете Райса. Или, если перефразировать: «Я ничего не понял. Кто-нибудь понял?»

habr: Перевод «Парадокс доказательства», Caroline Chen

С другой стороны, если ограничиваться существующим инструментарием, то доказательство abc-гипотезы вообще бы не появилось. Как известно, «серебряной пули» нет, и Coq — не исключение. Как мы увидим, его применение для изложения CAP-теоремы тоже в известной степени иллюстрирует этот тезис.

Но обо всём по порядку.

В данной статье я кратко расскажу о принципах записи и отладки доказательств в Coq. Существует много статей и руководств по Coq, ключевые отличия «ещё одной» статьи такие:

  • Всё в одной статье.

  • Фокус на доказательствах, а не на теории типов Coq.

  • Будет использован онлайн-инструментарий Coq, ничего не надо устанавливать.

  • В качестве примера будет рассмотрен фрагмент геометрии Евклида.

Установка

Ставить ничего не надо. Всё будет работать в онлайн-инструментарии Coq: scratchpad (официально это здесь, но появились проблемы, возможно, тот самый «хабрэффект»).

Простейшие

Прежде чем взяться за геометра нашего Евклида, рассмотрим простейшие примеры.

intros, exact

Theorem example_intros_exact : forall P : Prop, P -> P.
Proof.
  intros P H. (* Introduce P and the assumption H : P *)
  exact H.    (* Directly use the assumption H to complete the proof *)
Qed.

Здесь мы определили теорему с названием example_intros_exact, название отражает названия используемых операторов тактик intros и exact. На человеческом языке эту теорему можно сформулировать так: «Для любого утверждения P, если верно P, то верно P». Докажем же сие☝️.

Копируем текст в scratchpad и нажимаем два раза зелёную кнопку «Down» (делаем два шага):

82823c462ae6b76aee9d3913f2ace06d.png

Справа, в окошке Goals, показывается текущая цель.

Следующий шаг — выполнить тактику intros. Тактика «разбирает» текущую цель на части и перемещает эти части в контекст. Что можно сказать, исходя из цели:

  • P — это высказывание (proposition).

  • P — истинно, так как мы исходим из «если верно P».

  • Нужно доказать, что P — истинно (принято говорить, что «P holds»).

Тактика intros P H. перемещает истинные утверждения в контекст, именуя их P и H, в качестве цели остаётся P.

ed9fcf4fa1254fd6309ba6afe3f9c93f.png

Теперь следующим оператором тактикой exact H. мы говорим Coq, что цель соответствует части, которая уже есть в контексте и называется H.

Coq проверяет, так ли это, и закрывает текущую цель. Всё, теорема доказана, Qed aka quod erat demonstrandum aka ЧТД.

assumption

Theorem example_assumption : forall P : Prop, P -> P.
Proof.
  intros P H. (* Introduce P and the assumption H : P *)
  assumption.
Qed.

assumption похоже на exact, но в отличие от exact, assumption сама ищет в контексте подходящее утверждение.

Feature

exact

assumption

Explicit term

Requires you to provide the term explicitly.

Automatically searches for a matching term.

Automation

Manual: You must know the term in advance.

Automatic: Coq finds the matching hypothesis.

Error behavior

Fails if the term doesn’t match the goal.

Fails if no matching hypothesis is found.

auto

В простых случаях Coq может и сам всё доказать при помощи тактики auto, и этот случай именно таков.

Theorem example_auto : forall P : Prop, P -> P.
Proof.
  auto.
Qed.

apply

Теперь можно взяться за что-то посложнее. Докажем, что если из P следует Q, и P — истинно, то и Q — истинно (это правило вывода Modus ponens).

Theorem example_modus_ponens : forall (P Q : Prop),
  (P -> Q) -> P -> Q.
Proof.
  intros P Q P_implies_Q P_holds.

  (* 
    PQ : ℙ 
    P_implies_Q : P → Q 
    P_holds : P 
    ------ 
    Q 
  *)  
  apply P_implies_Q in P_holds as Q_holds. (* New context Q_holds Q*)

  exact Q_holds.
Qed.

  • intros разбирает цель на части и перемещает их в контекст, именуя полезным для понимания образом. Напоминаю, что «P holds» означает, что P — истинно.

  • В комментарии показано, что происходит в контексте перед apply.

Теперь apply. Эта тактика в данном случае подставляет P_implies_Q (если P, то Q) в P_holds (там получается Q) и результат записывает в Q_holds.

Q_holds теперь совпадает с целью, и мы можем закрыть доказательство через exact Q_holds.

destruct, contradiction

В следующей теореме используется Principle of explosion: если у нас есть A и ~A, то мы можем доказать любое B.

Рассмотрим это не совсем тривиальное утверждение на примере, приняв за истину «Все лимоны жёлтые» и одновременно «Не все лимоны жёлтые».

  • Мы знаем, что «Не все лимоны жёлтые», поскольку это было принято как истина.

  • Мы знаем, что «Все лимоны жёлтые», поскольку это тоже было принято как истина.

  • Следовательно, составное утверждение «Все лимоны жёлтые или единороги существуют» также должно быть истинным, поскольку первая часть утверждения («Все лимоны жёлтые») уже была принята как истина, а использование «или» означает, что если хотя бы одна часть утверждения истинна, то и всё утверждение должно быть истинным.

  • Однако, поскольку мы также знаем, что «Не все лимоны жёлтые» (это было принято как истина), первая часть ложна, и, следовательно, вторая часть должна быть истинной, чтобы обеспечить истинность составного утверждения, то есть таки единороги существуют.

Theorem example_destruct_contradiction : 
  forall A B : Prop,
  (* If we have (A and not A), then we can prove any B *)
  (A /\ ~A) -> B.
Proof.
  intros A B H.
  (* First, let's break down the conjunction *)
  (* 
    A, B : ℙ 
    H : A ∧ ~ A 
    ------
    B  
  *)
  destruct H as [H1 H2].
  (* H1 is A, H2 is ~A *)
  (* Apply H2 to H1 to get a contradiction *)
  contradiction H1.
Qed.

  • destruct разбивает часть контекста H : A ∧ ~ A на две части: H1 : A, H2 : ~A.

  • contradiction H1 указывает Coq, что у нас есть где-то противоречие с H1, Coq находит это противоречие (используя H2) и закрывает доказательство, так как противоречие означает, что любая цель доказана.

split

Theorem example_split : 
  forall A B : Prop,
  (* If we have A and B, we can get B and A *)
  (A /\ B) -> (B /\ A).
Proof.
  intros A B H.
  (*
    AB : ℙ 
    H : A ∧ B 
    ------
    B ∧ A
  *)
  (* split creates two subgoals: we need to prove B and A separately *)
  split.
  - (* First subgoal: prove B *)
    destruct H as [HA HB].
    exact HB.
  - (* Second subgoal: prove A *)
    destruct H as [HA HB].
    exact HA.
Qed.

  • split разбивает цель B ∧ A на две подцели: B и A.

  • - начинает новую подцель, которую нужно доказать.

  • - используется дважды, так как у нас две подцели.

Ну всё, тренерские инструкции вам даны, пора приступать к Евклиду.

Евклид

Исходный текст см. здесь: github: euclid.v. Возможно, после копирования его в scratchpad придётся нажать кнопку Reset worker, см. выше скриншот.

Начало определения EuclidianGeometry: 

Class EuclidianGeometry (Point : Type) := {

  (* Core relations that define geometric relationships *)

  is_collinear : Point -> Point -> Point -> Prop;     (* Three points lie on a line *)
  is_between : Point -> Point -> Point -> Prop;       (* Second point lies between first and third *)
  ...

На языке Go этому примерно соответствует следующий код: 

type EuclidianGeometryStruct[Point any] struct {

    is_collinear  func(A, B, C Point) bool
    is_between    func(A, B, C Point) bool
    ...

То есть мы определяем как бы «generic»-тип EuclidianGeometry, для которого конкретный тип должен будет содержать методы для проверки коллинеарности (точки лежат на одной прямой) и того, что одна точка лежит между двумя другими.

После этого мы определяем четыре аксиомы: 

  (* Axiom: If points A,B,C are collinear, then C,B,A are also collinear *)
  collinear_symmetric : forall A B C : Point,
    is_collinear A B C -> is_collinear C B A;
    
  (* Axiom: If points A,B,C are collinear, then A,C,B are also collinear *)
  collinear_swap_23 : forall A B C : Point,
    is_collinear A B C -> is_collinear A C B;

  (* Axiom: No point can be between itself and another point *)
  between_irreflexive12 : forall P Q : Point, 
    ~ is_between P P Q;

  (* Axiom: If B is between A and C, then B is between C and A *)
  between_symmetric : forall A B C : Point, 
    is_between A B C -> is_between C B A

  • collinear_symmetric: если точки A, B, C коллинеарны (лежат на одной прямой), то и C, B, A коллинеарны.

  • collinear_swap_23: если точки A, B, C коллинеарны, то и A, C, B коллинеарны.

  • between_irreflexive12: точка не может быть между собой и другой точкой.

  • between_symmetric: если B между A и C, то B также между C и A.

Затем доказываются четыре теоремы:

  • collinear_rotate: если A, B, C коллинеарны, то C, A, B коллинеарны.

  • collinear_swap12: если A, B, C коллинеарны, то B, A, C коллинеарны.

  • between_irreflexive23: точка не может быть между другой точкой и собой.

  • between_points_distinct: если Q между P и R, то Q отличается от P и R.

Из нового тут то, что between_irreflexive23 для примера принимается без доказательств, используя тактику admit. Это означает, что мы признаём, что это утверждение верно, но не будем его доказывать.

(* Theorem: A point cannot be between a point and itself *)
Theorem between_irreflexive23 :
  forall P Q : Point, ~ is_between P Q Q.
Proof.
(*  
  intros P Q H1.
  apply between_symmetric in H1.
  apply between_irreflexive12 in H1.
  contradiction.
*)  
  admit.
Admitted.

На следующем этапе создаётся экземпляр EuclidianGeometry для nat (т.е. в качестве «точки» используются натуральные числа): 

(* Instance of EuclidianGeometry using nat as Point *)
#[local] Instance EuclidianGeometryN : EuclidianGeometry(nat) := {

  (* All points are collinear *)
  is_collinear := fun A B C => True;
  
  (* Betweeness is defined based on ordering *)
  is_between := fun A B C => (A < B < C) \/ (C < B < A);  

  (* Axioms *)

  collinear_symmetric := nat_collinear_symmetric;
  collinear_swap_23 := nat_collinear_swap_23;
  
  between_irreflexive12 := nat_between_irreflexive12;
  between_symmetric := nat_between_symmetric;
}.

  • is_collinear: все «точки» коллинеарны.

  • is_between: расположение одной «точки» между двумя другими определяется их сравнением.

  • в качестве collinear_symmetric используется nat_collinear_symmetric.

  • в качестве collinear_swap_23 используется nat_collinear_swap_23.

  • в качестве between_irreflexive12 используется nat_between_irreflexive12, при этом необходимо доказать, что nat_between_irreflexive12 удовлетворяет контракту between_irreflexive12.

  • в качестве between_symmetric используется nat_between_symmetric, и доказывается, что nat_between_symmetric удовлетворяет контракту between_symmetric.

Заключение

Мы рассмотрели основные тактики Coq (intros, exact, assumption, auto, apply, destruct, contradiction, split) на простых примерах и увидели, как они помогают пошагово строить доказательства.

Затем применили эти идеи в рамках упрощённой геометрической теории Евклида: определили коллинеарность и «лежание между точками» в стиле Coq, сформулировали аксиомы и даже создали конкретную реализацию на натуральных числах.

В следующей части займёмся изложением CAP на языке Coq.

Habrahabr.ru прочитано 2570 раз