Доказательство в Coq, что равенство рефлексивности

Question

Книга HOTT пишет на странице 51:
... мы можем доказать по индукции пути на р: х = у, что

$(x, y, p) =_{ \sum_{(x,y:A)} (x=y)} (x, x, refl x)$ . 

Может кто-то показать мне, как доказательство это в COQ?

Примечания:

• Извините, что я не знаю, как сделать латексный код здесь.
• Это не домашнее задание.

Answer 1

На самом деле, это является можно доказать этот результат в Coq:

Notation "y ; z" := (existT _ y z) (at level 80, right associativity). 

Definition hott51 T x y e : 
    (x; y; e) = (x; x; eq_refl) :> {x : T & {y : T & x = y} } := 
    match e with 
    | eq_refl => eq_refl 
    end. 

Здесь я использовал точку с запятой кортеж обозначения для выражения зависимых пар; в Coq, {x : T & T x} - это сигма тип \sum_{x : T} T x. Существует также немного проще для чтения варианта, где мы не упоминаем y:

Definition hott51' T x e : (x; e) = (x; eq_refl) :> {y : T & x = y} := 
    match e with 
    | eq_refl => eq_refl 
    end. 

Если вы не привыкли писать термины доказательства вручную, этот код может выглядеть немного таинственный, но это делая то, что говорит книга HoTT: продолжение по индукции пути. Здесь есть один решающий бит информации, который представляет собой аннотации типа , необходимые для индукции пути. Coq способен вывести их, но мы можем попросить его рассказать нам, что они явно, напечатав этот термин. Для hott51', мы получаем следующее (после некоторого переписывания):

hott51' = 
fun (T : Type) (x : T) (e : x = x) => 
match e as e' in _ = y' return (y'; e') = (x; eq_refl) with 
| eq_refl => eq_refl 
end 
    : forall (T : Type) (x : T) (e : x = x), 
     (x; e) = (x; eq_refl) 

Важная деталь есть, что в типе возвращаемого match, как x и e обобщаются y' и e'. Единственная причина, по которой это возможно - это потому, что мы обернули x в паре. Подумайте, что произойдет, если мы пытались доказать UIP:

Fail Definition uip T (x : T) (e : x = x) : e = eq_refl := 
    match e as e' in _ = y' return e' = eq_refl with 
    | eq_refl => eq_refl 
    end. 

Здесь Coq жалуется, говоря:

The command has indeed failed with message: 
In environment 
T : Type 
x : T 
e : x = x 
y' : T 
e' : x = y' 
The term "eq_refl" has type "x = x" while it is expected to have type 
"x = y'" (cannot unify "x" and "y'"). 

Что это сообщение об ошибке говорит, что, в типе возвращаемого match, тем e' имеет тип x = y', где y' обобщен. Это означает, что равенство e' = eq_refl плохо напечатано, поскольку правая сторона должна иметь тип x = x или y' = y'.

Answer 2

Простой ответ: вы не можете. Все доказательства x = y в Coq не являются экземплярами eq_refl x. Вы должны будете признать уникальность удостоверения личности, чтобы иметь такой результат. Это очень хорошая аксиома, но это все еще аксиома в Исчислении индуктивных конструкций.