[Agda] Associativity and Heterogeneous Equality

[Andreas Abel]

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/
-------------- next part --------------
module HAssociativity where

open import Relation.Binary.PropositionalEquality

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)