Gallina и CIC
Формальный язык, который используется в Coq для описания математических утверждений и доказательств называется курица (Gallina это “курица“ в переводе с испанского на русский). Этот язык основан на формализме (разновидности теории типов), который называется Исчисление Индуктивных Конструкций (Calculus of Inductive Constructions, сокращённо CIC).
Логические утверждения отождествляются с некоторыми типами, а их доказательства с термами соответствующих типов. Таким образом, чтобы доказать утверждение необходимо сконструировать (предъявить) терм нужного типа. Короче говоря: утверждения это типы, а программы это доказательства. Кстати, в обратную сторону это не всегда работает.
Каждое выражение в Gallina это терм CIC, а любой терм имеет тип (в некотором контексте).
Зависимые типы и функции
Рекомендую предварительно получить какое-то представление или освежить знания о зависимых типах. Достаточно потратить 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 это зависимая
ф-ция, в том случае, когда возвращаемый тип никак не зависит от
входного значения.
Вообще говоря, обычное функциональное пространство является тем частным случаем, когда область значений не зависит от входного параметра.
Типы, термы и вычисления
Простейшие термы это переменные и два сорта: \( 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.