[Agda] Equalities between elements of different sizes

[Guillaume Allais]

Hi Guillaume,

There is ongoing work [1] to make these work well via the notion of
shape irrelevance.

I have faced a similar issue when working on generic-syntax [2] and
the solution I have used until we get [1] is to:
* define a size-heterogeneous notion of equality
* prove it is equivalent to propositional equality when both sides
  use size infinity.

Hope this helps,
Cheers,
--
gallais

[1] See Section 2 for a similar problem with sized natural numbers:
https://hal.archives-ouvertes.fr/hal-01596179/document

[2] https://gallais.github.io/generic-syntax/Generic.Identity.html#504

On 27/10/18 00:47, Guillaume Brunerie wrote:
> Thanks! It does fix my problem.
> Is that the recommended way to define data types using sized types? I
> didn’t know about this up arrow, all other examples of sized types
> that I have seen so far use Size< as in my first message.
> 
> Best,
> Guillaume
> Den fre 26 okt. 2018 kl 21:40 skrev Oleg Grenrus <oleg.grenrus at iki.fi>:
>>
>> Hi Guillaume,
>>
>> If you define your list differently:
>>
>> open import Agda.Builtin.Size
>> open import Agda.Builtin.Equality
>>
>> postulate
>>   A : Set
>>
>> data List : (i : Size) → Set where
>>   []  : {i : Size} → List (↑ i)
>>   _∷_ : {i : Size} → A → List i → List (↑ i)
>>
>> _++_ : List ω → List ω → List ω
>> [] ++ l = l
>> (a ∷ l) ++ l' = a ∷ (l ++ l')
>>
>> cong : {i : Size} {x : A} {l l' : List i} → l ≡ l' → x ∷ l ≡ x ∷ l'
>> cong refl = refl
>>
>> test : (l : List ω) → l ++ [] ≡ l
>> test [] = refl
>> test (x ∷ l) = cong (test l)
>>
>> Agda 2.5.3 accepts the program.
>>
>> - Oleg
>>
>> On 26.10.2018 14.13, Guillaume Brunerie wrote:
>>> Hi all,
>>>
>>> I am trying to use sized types to do some definitions and proofs and I
>>> have an issue (full code below).
>>>
>>> I define lists using sized types, and concatenation of lists (which
>>> has List ∞ for both domains and the codomain, as there is no addition
>>> of sizes). Then I want to prove that l ++ [] is equal to l by
>>> structural induction. But the obvious proof doesn’t typecheck, because
>>> for the induction case, the right-hand side l is in List j whereas the
>>> left-hand-side l ++ [] is in List ∞, but they are supposed to be in
>>> the same type.
>>> If I remove all sized types, then the proof goes through, but in my
>>> actual code I need to use sized types somewhere while also needing to
>>> prove something like l ++ [] = l somewhere else.
>>>
>>> Is there a workaround to that?
>>>
>>> Best,
>>> Guillaume
>>>
>>>
>>> open import Agda.Builtin.Size
>>> open import Agda.Builtin.Equality
>>>
>>> postulate
>>>   A : Set
>>>
>>> data List (i : Size) : Set where
>>>   [] : List i
>>>   _∷_ : {j : Size< i} → A → List j → List i
>>>
>>> _++_ : List ∞ → List ∞ → List ∞
>>> [] ++ l = l
>>> (a ∷ l) ++ l' = a ∷ (l ++ l')
>>>
>>> cong : {i : Size} {x : A} {l l' : List i} → l ≡ l' → x ∷ l ≡ x ∷ l'
>>> cong refl = refl
>>>
>>> test : (l : List ∞) → l ++ [] ≡ l
>>> test [] = refl
>>> test (x ∷ l) = cong (test l)
>>> _______________________________________________
>>> 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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181031/627dfeae/attachment.sig>