[Agda] How can I prove associativity of vectors?
Conor McBride
conor at strictlypositive.org
Wed Dec 17 23:52:23 CET 2014
Hi
A little bird told me I should pay attention for a change. Here’s what I cooked up.
Given that intensional equality is always a disappointment, it is too much to expect
the values on either side of a propositional equation to have intensionally equal
types. The method for working with heterogeneous equality is always to work with
whole telescopes and make sure that whenever the types stretch apart (like the
vector types below), you always have an equation which tells you why they are
provably equal.
I could probably be more systematic about building the “resp” family, but it’s late and
I’m tired.
All the best
Conor
--------------------------------------------------------------
module VVV where
data Nat : Set where
ze : Nat
su : Nat -> Nat
_+_ : Nat -> Nat -> Nat
ze + y = y
su x + y = su (x + y)
data Vec (X : Set) : Nat -> Set where
[] : Vec X ze
_,_ : {n : Nat} -> X -> Vec X n -> Vec X (su n)
data _==_ {A : Set}(a : A) : {B : Set} -> B -> Set where
refl : a == a
_++_ : {X : Set}{m n : Nat} -> Vec X m -> Vec X n -> Vec X (m + n)
[] ++ ys = ys
(x , xs) ++ ys = x , (xs ++ ys)
record _*_ (S T : Set) : Set where
constructor _,_
field
fst : S
snd : T
open _*_ public
resp1 : {A : Set}{B : A -> Set}
(f : (a : A) -> B a)
{a a' : A} -> a == a' ->
f a == f a'
resp1 f refl = refl
resp3 : {A : Set}{B : A -> Set}{C : (a : A)(b : B a) -> Set}{D : (a : A)(b : B a)(c : C a b) -> Set}
(f : (a : A)(b : B a)(c : C a b) -> D a b c) ->
{a a' : A} -> a == a' ->
{b : B a}{b' : B a'} -> b == b' ->
{c : C a b}{c' : C a' b'} -> c == c' ->
f a b c == f a' b' c'
resp3 f refl refl refl = refl
vc : {X : Set}(n : Nat)(x : X) -> Vec X n -> Vec X (su n)
vc n x xs = x , xs
vass : {X : Set}{l m n : Nat}(xs : Vec X l)(ys : Vec X m)(zs : Vec X n) ->
(((l + m) + n) == (l + (m + n))) *
(((xs ++ ys) ++ zs) == (xs ++ (ys ++ zs)))
vass [] ys zs = refl , refl
vass (x , xs) ys zs with vass xs ys zs
... | q , q' = (resp1 su q) , resp3 vc q refl q'
--------------------------------------------------------------
More information about the Agda
mailing list