Как вы доказываете в Coq, что (e: p = p) = eq_refl? - PullRequest
Новая
       4

Как вы доказываете в Coq, что (e: p = p) = eq_refl?

0 голосов
/ 13 марта 2020

Я пытаюсь доказать это: 

Lemma eq_eq: forall (U: Type) (p: U) (eqv: p = p), eq_refl = eqv.

Но, похоже, просто нет способа сделать это. Проблема в том, что тип p = p равен на одном и том же члене, а затем пытается найти соответствие его экземпляру. Если бы это было не так, достаточно легко доказать, что термин типа с одним конструктором равен этому конструктору. 

Lemma eq_tt: forall (U: Type) (x: unit), tt = x.
Proof
  fun (U: Type) (x: unit) =>
    match x as x'
      return tt = x'
      with tt => eq_refl
    end.

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

Lemma eq_eq: forall (U: Type) (p: U) (eqv: p = p), eq_refl = eqv.
Proof
  fun (U: Type) (p: U) (eqv: p = p) =>
    match eqv as e
      in _ = p'
      return eq_refl = e
      with eq_refl => eq_refl
    end.

Это терпит неудачу с Термин "e" имеет тип "p = p", в то время как ожидается, что он будет иметь тип "p = p" (не может объединить "p" "и "p").

Проблема в том, что здесь выражение return внутренне переводит в функцию предиката что-то вроде этого: 

fun (p': U) (e: p = p') =>
  eq_refl = e

, которая не может проверить тип, потому что мы имеем теперь потерял ограничение между двумя членами в равенстве e и eq_refl требует этого ограничения.

Есть ли способ обойти эту проблему? Я что-то упустил?

1 Ответ

1 голос
/ 13 марта 2020

Ваша предложенная лемма в точности соответствует утверждению уникальности идентификационных доказательств (UIP) . Впервые было доказано, что отрицание UIP согласуется в MLTT с моделью группоида Хофмана и Штрейхера (pdf link). В этой модели типы интерпретируются как группоиды, где тип идентичности x = y представляет собой набор морфизмов от x до y в группоиде. В этой модели может быть несколько различных e: x = y.

В последнее время теория гомотопического типа приняла эту точку зрения. Вместо простых группоидов типы интерпретируются как ∞-группоиды, с возможностью не только множественных равенств между x и y, но также, возможно, множественных идентичностей между идентичностями p q: x = y, et c.

Достаточно сказать, что ваша лемма не доказуема без дополнительной аксиомы, такой как UIP, упомянутой выше, или Аксиома K .

...