[Agda] Associativity and Heterogeneous Equality

[Andreas Abel]

Seems like you want definitional equality modulo some definitional 
equalities.  Weirich et al have worked on this.  They have definitional 
equality based on congruence closure, but had to give up on automatic 
beta- and computational equality.

Vilhelm Sjöberg and Stephanie Weirich. Programming up to Congruence. In 
POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of 
Programming Languages, pages 369-382, Mumbai, India, January 2015.

On 12.06.2015 09:20, Marco Vassena wrote:
> 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>
>

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