[Agda] Associativity and Heterogeneous Equality

[Andreas Abel]

One semantics is extensional type theory.  But currently, with 
arbitrarily added rewrite rules, and no Knuth-Bendix completion, we do 
not get a nice equality relation...

On 11.06.2015 15:33, Alan Jeffrey wrote:
> 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
>>
>>
> _______________________________________________
> 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/