Переписывание простого доказательства теоремы

Я написал определение group в Idris:

data Group: Type -> Type where
    Unit: (x: t) -> Group t
    (*): Group t -> Group t -> Group t
    Inv: Group t -> Group t
postulate
    assoc: (a : Group t) -> (b : Group t) -> (c : Group t) -> ((a*b)*c = a*(b*c))
postulate
    neutralL: (x: t) -> (a : Group t) -> a * Unit x = a
postulate
    neutralR: (x: t) -> (a : Group t) -> Unit x * a = a
postulate
    invUnitL: (x: t) -> (a : Group t) -> a * (Inv a) = Unit x
postulate
    invUnitR: (x: t) -> (a : Group t) -> (Inv a) * a = Unit x

Затем я доказал пару простых утверждений:

cong : (a : Group t) -> (b : Group t) -> (c: Group t) -> a = b -> a*c = b*c
cong a b c post = rewrite post in Refl

neutralL1: (x: t) -> (a : Group t) -> a = a * Unit x
neutralL1 x a = rewrite neutralL x a in Refl

neutralR1: (x: t) -> (a : Group t) -> a = Unit x * a
neutralR1 x a = rewrite neutralR x a in Refl

Однако у меня проблема с доказательством того, что существует только один единичный элемент:

singleUnit : (x: t) -> (y: t) -> (Unit x = Unit y)

Я пробовал различные выражения, используя общую идею, что Unit x = (by neutralL1 y (Unit x)) = Unit x * Unit y = (by neutralR x (Unit y)) = Unit y, но безуспешно:

singleUnit x y = rewrite neutralL1 y (Unit x) in neutralR x (Unit y)
singleUnit x y = rewrite neutralL1 y (Unit x) in rewrite neutralR x (Unit y) in Refl
singleUnit x y = rewrite neutralR x (Unit y) in neutralL1 y (Unit x)
singleUnit x y = rewrite neutralR x (Unit y) in rewrite neutralL1 y (Unit x) in Refl

Как я могу это доказать? У меня такое ощущение, что проблема здесь связана с подстановкой сложных выражений, типа Unit x * Unit y.


dependent-type theorem-proving idris proof formal-verification
person stop-cran    schedule 05.07.2017    source источник

Ответы (2)


arrow_upward
3
arrow_downward

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

Например. легко увидеть, что neutralL нарушает принцип непересекаемости (разных) конструкторов данных, т.е. Constr1 <data> != Constr2 <data>.

starAndUnitAreDisjoint : (*) a (Unit x) = a -> Void
starAndUnitAreDisjoint Refl impossible

Теперь мы можем доказать ложь:

contradiction : Void
contradiction = starAndUnitAreDisjoint $ neutralL Z (Unit Z)

Финита ля комедия!

На самом деле вам нужен record или класс типов, см., например. contrib/Control/Algebra. idr и contrib/Interfaces/Verified.idr. Кроме того, версии Agda синтаксически довольно близки к Idris (agda- stdlib/src/Algebra.agda и, возможно, Абстрактная алгебра в учебном пособии Agda) -- вы можете взглянуть на них.

person Anton Trunov    schedule 05.07.2017

arrow_upward
2
arrow_downward

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

%default total

interface Group t where
  Unit: t
  (*): t -> t -> t
  Inv: t -> t

  assoc: (a : t) -> (b : t) -> (c : t) -> ((a*b)*c = a*(b*c))
  neutralL: (x: t) -> (a : t) -> a * Unit = a
  neutralR: (x: t) -> (a : t) -> Unit * a = a
  invUnitL: (x: t) -> (a : t) -> a * (Inv a) = Unit
  invUnitR: (x: t) -> (a : t) -> (Inv a) * a = Unit

cong : Group t => (a : t) -> (b : t) -> (c: t) -> a = b -> a*c = b*c
cong a b c post = rewrite post in Refl

neutralL1: Group t => (x: t) -> (a : t) -> a = a * Unit
neutralL1 x a = rewrite neutralL x a in Refl

neutralR1: Group t => (x: t) -> (a : t) -> a = Unit * a
neutralR1 x a = rewrite neutralR x a in Refl

is_left_unit : Group t => (x : t) -> Type
is_left_unit x = (y : t) -> x * y = y

only_one_left_unit : Group t => (x : t) -> is_left_unit x -> x = Unit
only_one_left_unit x is_left_unit_x = 
  let x_times_unit_is_unit = is_left_unit_x Unit in
  let x_times_unit_is_x = neutralL Unit x in
    trans (sym x_times_unit_is_x) x_times_unit_is_unit

is_right_unit : Group t => (x : t) -> Type
is_right_unit x = (y : t) -> y * x = y

only_one_right_unit : Group t => (x : t) -> is_right_unit x -> x = Unit
only_one_right_unit x is_right_unit_x = 
  let unit_times_x_is_unit = is_right_unit_x Unit in
  let unit_times_x_is_x = neutralR Unit x in
    trans (sym unit_times_x_is_x) unit_times_x_is_unit

Вы заметите, что тип t на самом деле является типом группы, а Unit — это значение, а не функция с одним параметром. Я определил отдельные функции is_left_unit и is_right_unit, представляющие понятия быть левым или правым юнитом соответственно.

Чтобы убедиться, что все это имеет смысл, мы хотели бы определить некоторую реальную конкретную группу, предоставляющую реализации для Unit, * и Inv, а также дополнительные реализации для assoc, neutralL, neutralR, invUnitL и invUnitR, которые представляют собой обязательства доказательства.

person Philip Dorrell    schedule 06.07.2017