Gallina и CIC Link to heading

Формальный язык, который используется в Coq для описания математических утверждений и доказательств называется курица (Gallina это “курица“ в переводе с испанского на русский). Этот язык основан на формализме (разновидности теории типов), который называется Исчисление Индуктивных Конструкций (Calculus of Inductive Constructions, сокращённо CIC).

Логические утверждения отождествляются с некоторыми типами, а их доказательства с термами соответствующих типов. Таким образом, чтобы доказать утверждение необходимо сконструировать (предъявить) терм нужного типа. Короче говоря: утверждения это типы, а программы это доказательства. Кстати, в обратную сторону это не всегда работает.

Каждое выражение в Gallina это терм CIC, а любой терм имеет тип (в некотором контексте).

Зависимые типы и функции Link to heading

Рекомендую предварительно получить какое-то представление или освежить знания о зависимых типах. Достаточно потратить 5 минут на чтение русской вики

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

Если \( x \) – переменная, а \( T \) и \( U \) – термы, тогда \( \forall x : T, U \) тоже терм. В то же время это тип, который представляет собой семейство типов \( U \), индексированных элементами типа \( T \).

  • Когда \( x \) встречается в терме \( U \) (как свободная переменная) мы говорим, что \( \forall x : T, U \) – зависимый тип
  • Если \( x \) не используется в \( U \), то мы получим обычную ф-цию типа \( T \rightarrow U \)

Нет никакой разницы между \( A \rightarrow B \) и \( \forall x : A, B \) (кроме нотации).

В Coq нотация вида "A -> B" := forall _ : A, B это зависимая ф-ция, в том случае, когда возвращаемый тип никак не зависит от входного значения.

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

Типы, термы и вычисления Link to heading

Простейшие термы это переменные и два сорта: \( Prop \) и \( Type_{i} \) для \( i \in \mathbb{N} \).

Как известно, утверждения типизации вроде \( \Gamma \vdash t : T \) связывают некоторый контекст \( \Gamma \) (гамма) и два терма \( t \) и \( T \). Контекст \( \Gamma \) это такое место, где хранятся все известные нам факты и предположения в тот момент, когда нам встречается терм, который мы видим справа от \( \vdash \). Контекст может быть пустым или содержать типизированные переменные и определения:

  • Типизированная переменная – пара из имени и типа: Variable n : nat
  • Типизированное определение – тройка из имени, терма и типа: Definition a : T := t

Утверждения типизации в пустом контексте выражают аксиомы:

  • \( \vdash Prop : Type_{1} \)
  • \( \vdash Type : Type_{i+1} \)

Т.е. сорта \( Prop \) и \( Type \) это одновременно и типы и типы типов.

Тип это терм, который может быть типизирован сортом в некотором контексте:

  • \( \Gamma \vdash T : Prop \)
  • \( \Gamma \vdash T : Type \)

Контексты позволяют нам конструировать более сложные типы, например:

\( \Gamma \vdash T : Type \wedge \Gamma,x : T \vdash U : Type \Longrightarrow \Gamma \vdash \forall x : T, U : Type \)

полученный тип \( \Gamma \vdash \forall x : T, U : Type \) это тип функций \( T \rightarrow U \), которые описываются следующим правилом: \( \Gamma \vdash \forall x : T, U : Type \wedge \Gamma,x : T \vdash t : U \Longrightarrow \Gamma \vdash fun \space x \Rightarrow t : \forall x : T, U \)

Применение можно типизировать так: \( \Gamma \vdash u : \forall x : T, U \wedge \Gamma \vdash t : T \Longrightarrow \Gamma \vdash u \space t : U [t/x] \)

где \( U [t/x] \) это тип, полученный путём замены переменной \( x \) на терм \( t \) в \( U \).

Рассмотрим тавтолгию \( A \rightarrow A \). Здесь символ импликации \( \rightarrow \) можно понимать как логическую импликацию (“если…, то…”), но этот же символ мы используем и для функций.

Терм fun x : A => x это единичная функция для термов типа \( A \) и программа типа \( A \rightarrow A \).

Если понимать тип \( A \) как утверждение, а термы этого типа как доказательства (свидетельства) этого утверждения, то вышеупомянутая функция это единичиная функция над доказательствами \( A \).

Вообще, доказательства импликаций можно рассматривать как функции, трансформирующие доказательства предпосылок в доказательства заключений.

Рассмотрим правила ввода для импликации и универсальной квантификации. Следующая запись означает: для того, чтобы доказать \( A \rightarrow B \) нам нужно доказать \( B \), при условии, что \( A \) уже доказано.

\( {\dfrac{{A \atop \vdots} \atop B}{A \rightarrow B}} \rightarrow I \)

Аналогично и здесь: чтобы доказать \( \forall x, B \) мы должны доказать \( B \) для некоторой переменной \( x \).

\( {\dfrac{B}{\forall x, B}}{\space \forall_{I} \space (x \space \textsf{fresh})} \)

Аннотируем эти правила типизации термами, имеющими соответствующие типы:

\( {\dfrac{{x \space : \space A \atop \vdots} \atop {b \space : \space B}}{(fun \space x : A \Rightarrow b) : A \rightarrow B}} \rightarrow I \)

\( \dfrac{b : B}{(fun \space x : A \Rightarrow b) : \forall x, B} \space \forall_{I} \)

Заметим, что терм (абстракция) \( fun … \Rightarrow … \) служит доказательством для обоих правил. И в том и в другом случае терм \( b \) является доказательством \( B \). Единственная разница в том, что \( x \) может быть свободной переменной в \( B \) только во втором правиле.

Сделаем тоже самое для соответствующий правил элиминации\удаления. Имеем следующие правила:

\( \dfrac{A \rightarrow B \qquad A}{B} \rightarrow E \)

\( \dfrac{\forall x, B}{B[t/x]} \space \forall_E \space (t \space \textsf{is a term})\)

Как видно из аннотированных правил ниже, в случае элиминации доказательством становится применение функции.

\( \dfrac{f : A \rightarrow B \qquad t : A}{(f \space t) : B} \rightarrow E \)

\( \dfrac{f : \forall x : A, B \qquad t : A}{(f \space t) : B[t/x]} \space \forall_E \)

Для более глубокого погружения можно почитать вышеупомянутую книгу и Introduction to the Calculus of Inductive Constructions.