[Agda] Associativity and Heterogeneous Equality

[Alan Jeffrey]

I wonder what it would take to give this a semantics, preferably by 
translating down to a core language, in the same way that 
pattern-matching can. My back-of-envelope thinking is that a use of 
rewriting:

   Gamma |- E : T(M)
   ----------------- [ REWRITE P : M == N ]
   Gamma |- E : T(N)

is elaborated to:

   Gamma |- E : T(M)
   -------------------------------
   Gamma |- transport T P E : T(N)

but this is a bit dubious, as there may be more than one choice of 
elaboration, and it is not obvious that there's enough rewrite rules to 
make the choice irrelevant.

A.

On 06/11/2015 12:13 AM, Andreas Abel wrote:
> 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
>
>