[Agda] Associativity and Heterogeneous Equality

[Marco Vassena]

Thank you all for the useful tips about how to handle this issue.

> you can add rewrite rules to the *definitional* equality, making more types equal.

Often, like in this case, we know exactly which rule/lemma should be used to make type equal.
Currently signatures can contain arbitrary terms, including function applications and let bindings.

Wouldn't it be possible to include the with clause (or a similar case construct) in signatures?
Pattern matching on the equality proof, would bring in scope the piece of information needed
to make the two types equal.

I could write:

assoc-+++ : ∀ {xs ys zs} (a : HList xs) (b : HList ys) (c : HList zs) 
			case assoc-++ xs ys zs of
		     		refl -> a +++ b +++ c ≡ (a +++ b) +++ c
assoc-+++ [] b c = refl
assoc-+++ {_ ∷ xs} {ys} {zs} (x ∷ a) b c = cong (_∷_ x) (assoc-+++ {xs} {ys} {zs} a b c)

All the best,
Marco

On 10/giu/2015, at 23.21, Andreas Abel wrote:

> This is more a feature /preview/ than a mature feature, but in Agda 2.4.2.3 you can add rewrite rules to the *definitional* equality, making more types equal.
> 
> The following type-checks:
> 
> open import Relation.Binary.PropositionalEquality
> 
> -- Rewrite rules for a definition currently must be in the same module
> -- as the definition, so we roll our own _++_.
> 
> infixr 5 _∷_ _++_
> 
> data List {a} (A : Set a) : Set a where
>  [] : List A
>  _∷_ : (x : A) (xs : List A) → List A
> 
> _++_ : ∀{a} {A : Set a} (xs ys : List A) → List A
> [] ++ ys = ys
> (x ∷ xs) ++ ys = x ∷ (xs ++ ys)
> 
> assoc-++ : ∀ (a b c : List Set) -> (a ++ b) ++ c ≡ a ++ b ++ c
> assoc-++ [] b c = refl
> assoc-++ (x ∷ a) b c = cong (_∷_ x) (assoc-++ a b c)
> 
> {-# BUILTIN REWRITE _≡_ #-}
> {-# REWRITE assoc-++ #-}
> 
> postulate View : List Set -> Set -> Set
> 
> data HList : List Set -> Set₁ where
>  [] : HList []
>  _∷_ : ∀ {xs x} -> x -> (ts : HList xs) -> HList (x ∷ xs)
> 
> _+++_ : ∀ {xs ys} -> HList xs -> HList ys -> HList (xs ++ ys)
> [] +++ bs = bs
> (a ∷ as) +++ bs = a ∷ (as +++ bs)
> 
> infixr 5 _+++_
> 
> assoc-+++ : ∀ {xs ys zs} (a : HList xs) (b : HList ys) (c : HList zs) -> a +++ b +++ c ≡ (a +++ b) +++ c
> assoc-+++ [] b c = refl
> assoc-+++ {_ ∷ xs} {ys} {zs} (x ∷ a) b c = cong (_∷_ x) (assoc-+++ {xs} {ys} {zs} a b c)
> 
> 
> On 07.06.2015 16:33, Marco Vassena wrote:
>> Given an heterogeneous list data-type:
>> 
>> data HList : List Set -> Set₁ where
>>   [] : HList []
>>   _∷_ : ∀ {xs x} -> x -> (ts : HList xs) -> HList (x ∷ xs)
>> 
>> I have defined the append function:
>> _+++_ : ∀ {xs ys} -> HList xs -> HList ys -> HList (xs ++ ys)
>> [] +++ bs = bs
>> (t ∷ as) +++ bs = t ∷ (as +++ bs)
>> 
>> Now I want to prove that _+++_ is associative: a +++ b +++ c = (a +++ b) +++ c.
>> 
>> I could not state this lemma using propositional equality, because _+++_
>> appends the list of types using _++_ :
>> a +++ b +++ c :: HList (xs ++ ys ++ zs)
>> (a +++ b) +++ c :: HList ((xs ++ ys) ++ zs)
>> 
>> the two indexes are not considered equal, leading to different types, preventing the use of propositional equality.
>> In order to solve this I should use associativity of _++_ in the signature itself, but I could not find any
>> way to do that.
>> 
>> I tried then to use heterogeneous equality.
>> 
>> assoc-+++ : ∀ {xs ys zs} (a : HList xs) (b : HList ys) (c : HList zs) -> a +++ b +++ c ≅ (a +++ b) +++ c
>> assoc-+++ [] b c = refl
>> assoc-+++ {_ ∷ xs} {ys} {zs} (x ∷ a) b c = H.cong (_∷_ x) (assoc-+++ a b c)  -- (xs +++ ys) != xs (needs associativity)
>> 
>> The term (assoc-+++ a b c) is ill-typed because of the associativity of _++_ .
>> At this point I have tried to use firstly associativity of _++_, but this failed with an error about the generated with function being ill-typed.
>> 
>> Is there a way to prove associativity of _+++_ ?
>> 
>> I have attached a file with this problem.
>> 
>> All the best,
>> Marco
>> 
>> 
>> 
>> 
>> 
>> 
>> 
>> _______________________________________________
>> 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/
> <HAssociativity.agda>