Если я не ошибаюсь, в статье Аводея нотация Φ(a) означает замену некоторой неявной свободной переменной в Φ на выражение a.
В своем ответе я буду использовать следующие более явные обозначения (что соответствует Φ(a) в статье):
Φ[z ⟼ a]
Это означает, что в выражении Φ свободная переменная z будет заменена на выражение a.
Пример:
(x = z)[z ⟼ a]
результат в
(x = a)
Теперь я предполагаю, что вы уже знакомы с обычным изложением теории типов с помощью правил вывода, как в Приложении A.2 HoTT Book .
Теория типов использует два понятия равенства.
Типы идентификации : Обычно пишется с использованием символа = в правилах вывода. Чтобы заключить утверждение типа a = b, нам нужно предоставить проверочный термин для него. Например, давайте посмотрим на правило введения для типов идентификации:
a : A
---------------- (=)-INTRO
refl a : a = a
Здесь refl a выступает в качестве проверочного термина или доказательства, которое оправдывает наше утверждение о том, что a = a имеет место (а именно refl a представляет собой тривиальное доказательство или доказательство рефлексивности). Таким образом, утверждение типа p : a = b выражает, что a и b могут быть идентифицированы по доказательствам p.
Определительное равенство : Обычно пишется с использованием символа ≡ в правилах вывода. Утверждение a ≡ b означает, что a и b являются взаимозаменяемыми, заменяемыми в любом месте или эквивалентными. Это равенство охватывает такие понятия, как «по определению», «вычислением», «упрощением». Этот вид равенства не несет с собой доказательственного термина, т. Е. Не является типизирующим утверждением. Это тот тип равенства, который Coq использует неявно, когда вы используете тактику simpl и compute. Например, давайте посмотрим на правило рефлексивности для ≡:
a : A
--------- (≡)-REFLE
a ≡ a
Обратите внимание, что слева от a ≡ a нет проверочного термина (сравните с правилом (=)-INTRO выше). В этом случае система доказательств рассматривает a ≡ a как факт, то, что имеет место без необходимости явно указывать свое обоснование, поскольку единственное использование ≡ в системе доказательств будет для переписывания выражений.
То, что ≡ используется только для упрощения выражений, можно найти в других правилах вывода, например, в правиле сохранения типов для ≡:
a : A A ≡ B
------------------ (≡)-TYPE-PRESERV
a : B
Другими словами, если вы начинаете с термина a типа A и знаете, что типы A и B являются взаимозаменяемыми, то термин a также имеет тип B. Обратите внимание, что (и это будет важно позже!) Термин или доказательство для B не изменились, это все тот же термин, что и для A.
Теперь мы можем перейти к вопросу.
Что отличает Теорию экстенсиональных типов (ETT) от Теории интенсиональных типов, таких как HoTT или CoC, так это то, как они обрабатывают типы идентичности и равенство определений.
ETT делает типы идентичности и определения равенства взаимозаменяемыми, добавляя следующее правило вывода:
p : a = b
----------- (=)-EXT
a ≡ b
Другими словами, свидетельство p для идентичности становится неактуальным, и мы рассматриваем a и b как взаимозаменяемые в системе доказательств (благодаря таким правилам, как (≡)-TYPE-PRESERV и другим аналогичным правилам).
Исходя из гипотез p : a = b и a : A, в ЕТТ мы можем сделать что-то вроде следующего:
a : A p : a = b
--------- (≡)-REFLE ----------- (=)-EXT
a ≡ a a ≡ b
------------------------------------- (=)-CONG (*1)
(a = a) ≡ (a = b)
Где (=)-CONG - это правило конгруэнтности (т. Е. Определенно эквивалентные термины производят определенно эквивалентные типы идентичности), и я называю этот вывод (*1).
Используя (*1), мы можем получить:
a : A
----------------- (=)-INTRO -------------------- (*1)
refl a : a = a (a = a) ≡ (a = b)
-------------------------------------------------- (≡)-TYPE-PRESERV
refl a : a = b
Где в (*1) мы вставляем деривацию, которую мы сделали выше.
Другими словами, если мы игнорируем гипотезы a : A и промежуточные шаги, это как если бы мы сделали следующий вывод:
p : a = b refl a : a = a
-------------------------------------
refl a : a = b
Поскольку ETT рассматривает a и b как взаимозаменяемые (благодаря гипотезе p : a = b и (=)-EXT rule), доказательство refl a для a = a также можно рассматривать как доказательство для a = b. Таким образом, нетрудно видеть, что в ETT наличие доказательства идентичности, подобного a = b, достаточно для замены некоторых или всех вхождений a на b в ЛЮБОМ утверждении, включающем a.
Теперь, что происходит в теории типов напряженности (ITT)?
В ITT правило (=)-EXT не предполагается. Поэтому мы не можем выполнить вывод (*1), который мы сделали выше, и, в частности, следующий вывод недействителен:
p : a = b refl a : a = a
-------------------------------------
refl a : a = b
Это пример, когда у нас есть тождество p : a = b, но из утверждения (refl a : a = z)[z ⟼ a] мы не можем завершить утверждение (refl a : a = z)[z ⟼ b]. Это пример того, на что ссылается статья Аводея, я думаю.
Почему это неверный вывод? Потому что refl a : a = b заставляет a и b быть определенно равными (то есть единственный способ ввести refl a в деривацию - через правило (=)-INTRO), но это не обязательно верно из гипотезы p : a = b. Например, в HoTT тип интервала I (раздел 6.3 в Книге HoTT ) содержит два члена 0 : I и 1 : I, они не являются по определению равными, но у нас есть доказательство seg : 0 = 1.
Тот факт, что могут существовать другие доказательства идентичности, которые не являются тривиальными или рефлексивными, это то, что дает Теории Преднамеренного Типа ее богатство. Это то, что позволяет HoTT иметь однолистность и более высокие индуктивные типы, например.
Итак, что мы можем сделать из гипотез p : a = b и refl a : a = a в ITT?
В вашем вопросе теорема, которую вы доказали в Coq, называется «транспортной» функцией в HoTT (раздел 2.3 в HoTT Book ). Используя свою теорему (удаляя неявные параметры), вы сможете выполнить следующий вывод:
p : a = b refl a : a = a
------------------------------------------
subs p (λx => a = x) (refl a) : a = b
Другими словами, мы можем сделать вывод, что a = b, но наш проверочный термин для этого изменился! В ETT мы просто провели замену (потому что a и b были взаимозаменяемыми), что позволило нам использовать одно и то же доказательство в заключении (а именно refl a). Но в ITT мы не можем трактовать a и b как эквивалентно эквивалентные из-за богатства типов идентичности. И чтобы отразить это намерение, нам нужно объединить доказательства гипотез, чтобы построить наши новые доказательства в заключении.
Итак, из (refl a : a = z)[z ⟼ a] мы не можем заключить (refl a : a = z)[z ⟼ b], но мы можем заключить subs p (λx => a = x) (refl a) : a = b, что не является результатом простой замены гипотезы, как в ETT.