[Agda] Associativity and Heterogeneous Equality

[Andreas Abel]

On 11.06.2015 04:08, Alan Jeffrey wrote:
> Oooh, I can convert a propositional equality to a definitional equality.
> Cool.
>
> Can I use this to build non-terminating programs?

Yes, you can.  And you can easily make Agda loop.  E.g., don't try to 
rewrite with communtativity

   forall x y -> x + y == y + x

as this game never ends.

> Is the semantics of REWRITE "you'd better know what you're doing", or
> "programs whose typechecking terminates are sound"?

The former.  You are extending Type Theory with additional equalities, 
so they better make sense.

Cheers,
Andreas

> On 06/10/2015 04:21 PM, 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
>>>
>>
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
> _______________________________________________
> 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/