Idris - réécriture dans le théorème simple, la preuve

Question

j'ai écrit une définition de 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 

Je prouvé quelques propositions simples:

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 

Cependant, j'ai un problème avec proving qu'il n'y a qu'un seul élément d'unité:

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

J'ai essayé diverses expressions en utilisant un général idée, que Unit x = (par neutralL1 y (Unit x)) = Unit x * Unit y = (par neutralR x (Unit y)) = Unit y, mais sans succès:

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 

Comment puis-je prouver? J'ai le sentiment, que le problème ici est lié à la substitution d'expressions complexes, comme Unit x * Unit y.

Answer 1

Malheureusement, cette définition d'un groupe ne fonctionnera pas. En général, vous devez être très soigneusement introduit de nouveaux axiomes (postulats).

E.g. il est facile de voir que neutralL viole le principe de disjonction des constructeurs de données (différents), c'est-à-dire Constr1 <data> != Constr2 <data>.

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

Maintenant, nous pouvons prouver faux:

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

Finita la Commedia!

Ce que vous voulez réellement est un record ou une classe de type, voir par ex. contrib/Control/Algebra.idr et contrib/Interfaces/Verified.idr. De plus, les versions d'Agda sont syntaxiquement très proches d'Idris (agda-stdlib/src/Algebra.agda et probablement le tutoriel Abstract Algebra in Agda) - vous pourriez vouloir les voir.

Answer 2

Votre définition de groupe est structurée d'une manière qui aurait du sens si c'était une interface. Je l'ai réécrite comme suit, en gardant vos variables d'origine et les noms des fonctions, autant que possible:

%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 

Vous remarquerez que le type t est en fait le type de groupe, et Unit est une valeur plutôt qu'une fonction avec un paramètre. J'ai défini des fonctions séparées is_left_unit et is_right_unit représentant les notions d'être une unité gauche ou droite respectivement.

Pour être sûr tout cela est logique que nous voulons définir un certain groupe concret réel, fournissant les mises en œuvre pour Unit, * et Inv, et en outre fournir des implémentations pour assoc, neutralL, neutralR, invUnitL et invUnitR qui représentent les obligations de preuve.