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

Я написал определение группы В Идрисе: 

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 = (мимо 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.

2 2
proof formal-verification

2 ответа:

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

Например, легко видеть, что neutralL нарушает принцип несвязности (разных) конструкторов данных, т. е. Constr1 <data> != Constr2 <data>. 
starAndUnitAreDisjoint : (*) a (Unit x) = a -> Void
starAndUnitAreDisjoint Refl impossible

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

contradiction : Void
contradiction = starAndUnitAreDisjoint $ neutralL Z (Unit Z)
[5]}Finita la commedia! То, что вы на самом деле хотите, - это record или класс типов, см., например, contrib/Control/Algebra.idr и contrib / Interfaces / Verified.idr . Кроме того, версии Agda синтаксически довольно близки к Idris (agda-stdlib/src/Algebra.agda и, вероятно, абстрактная алгебра в учебнике Agda - Возможно, вы захотите взглянуть на них.
3

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

%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, которые представляют собой обязательства доказательства.

2