Например, когда я на агде доказывал, что реверс списка - это пермутация, то у меня было два типа:
data insert_into_==_ {A : Set} (x : A) : List A -> List A -> Set where
iihead : (xs : List A) -> insert x into xs == (x :: xs)
iimid : (xs : List A) -> (hs : List A) -> (h : A) -> insert x into xs == hs -> insert x into (h :: xs) == (h :: hs)
и
data Permutation {A : Set} : List A -> List A -> Set where
pnil : Permutation nil nil
p:: : forall {xs zs ys} -> (x : A) -> (y : A) -> insert y into zs == ys -> x == y -> Permutation xs zs -> Permutation (x :: xs) ys
Кажется, в Permutation можно и обойтись без x == y, а вот insert x into xs == ys всё-таки требует зависимого типа от x:A, чтобы insert 0 into xs == ys и insert 1 into xs == ys были отличимы на уровне компилирования - т.е. придётся моделировать и типы элементов списка, не только Nat.
Хотя, может, на самом деле можно как-то и обойтись.
no subject
Date: 2015-06-16 06:40 pm (UTC)Например, когда я на агде доказывал, что реверс списка - это пермутация, то у меня было два типа:
data insert_into_==_ {A : Set} (x : A) : List A -> List A -> Set where iihead : (xs : List A) -> insert x into xs == (x :: xs) iimid : (xs : List A) -> (hs : List A) -> (h : A) -> insert x into xs == hs -> insert x into (h :: xs) == (h :: hs)и
data Permutation {A : Set} : List A -> List A -> Set where pnil : Permutation nil nil p:: : forall {xs zs ys} -> (x : A) -> (y : A) -> insert y into zs == ys -> x == y -> Permutation xs zs -> Permutation (x :: xs) ysКажется, в Permutation можно и обойтись без x == y, а вот insert x into xs == ys всё-таки требует зависимого типа от x:A, чтобы insert 0 into xs == ys и insert 1 into xs == ys были отличимы на уровне компилирования - т.е. придётся моделировать и типы элементов списка, не только Nat.
Хотя, может, на самом деле можно как-то и обойтись.