[Agda] Re: How can I prove associativity of vectors?

[Andreas Abel]

Hi Kenichi,

recently, I also wondered why cong for heterogeneous equality was 
homogeneous.  That makes little sense.  I needed a heterogeneous 
congruence.  The current cong is no better than

   module Relation.Binary.HeterogeneousEquality where

   ...

   cong : ∀ {a b} {A : Set a} {B : A → Set b} {x y}
          (f : (x : A) → B x) → x ≡ y → f x ≅ f y
   cong f P.refl = refl

which takes you from homogeneous to heterogeneous equality.

The hcong' you suggest would be a nice addition to the standard library. 
  Feel free to create a pull request to

   https://github.com/agda/agda-stdlib

Cheers,
Andreas

On 17.12.2014 05:02, Kenichi Asai wrote:
> Thank you for the messages!  I could now implement it in two ways.
>
>>   * Use Data.Vec.Equality rather than PropositionalEquality.
>
> Attached Append.agda.
>
>>   * Use Relation.Binary.HeterogeneousEquality rather than
>>     PropositionalEquality.
>
> Attached Append2.agda.  But I had to use hcong' as shown in the
> following stackoverflow article:
>
> http://stackoverflow.com/questions/24139810/stuck-on-proof-with-heterogeneous-equality
>
> Rather than using hcong', I wanted to say:
>
> assoc : ∀ {l m n} → (l1 : Vec ℕ l) → (l2 : Vec ℕ m) → (l3 : Vec ℕ n) →
>          (l1 ++ l2) ++ l3 ≅ l1 ++ (l2 ++ l3)
> assoc [] l2 l3 = refl
> assoc (x ∷ l1) l2 l3 = cong (λ l → x ∷ l) (assoc l1 l2 l3)
>
> but it did not work, because cong appears to assume that two sides of
> ≅ has the same type.  Why is it so?  I think it is more natural that
> cong etc. in HeterogeneousEquality module are defined for heterogeneous
> types.
>
> The above stackoverflow article implies that there are general
> versions hcong, hsubst, etc.  Are they going to be included in the
> standard library?
>
>>   * Use Relation.Binary.PropositionalEquality.Core.subst and
>>     Data.Nat.Properties.Simple.+-assoc to make the types match.
>>
>> The last option gets ugly but allows you to keep using
>> PropositionalEquality.
>
> I dare not try this one.  I think HeterogeneousEquality is the way to
> go.
>
>> May be, this can be used instead?
>
> I did not use toList because I wanted to keep the length of vectors.
>
> Sincerely,


-- 
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/