[Agda] How can I prove associativity of vectors?

[Andreas Abel]

Thanks, Conor!

With a different argument ordering for vc you can do with resp2, which 
is hcong' only with an explicit first argument to f rather than an 
implicit one.

But resp2 seems to be just cong₂ from the standard library. 
(Relation.Binary.HeterogeneousEquality)

So there seems to be no urgency to add i-cong.  Maybe a cong_3 would be 
useful sometimes...

...

resp2 : {A : Set}{B : A -> Set}{C : (a : A)(b : B a) -> Set}
  (f : (a : A)(b : B a) ->  C a b) ->
  {a a' : A} -> a == a' ->
  {b : B a}{b' : B a'} -> b == b' ->
  f a b == f a' b'
resp2 f refl refl = refl

-- Swapped argument order for vector cons.

vc : {X : Set}(x : X)(n : Nat) -> Vec X n -> Vec X (su n)
vc x n 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


On 18.12.2014 00:52, Conor McBride wrote:
> 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'
> --------------------------------------------------------------
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/