[Agda] Equalities between elements of different sizes

[Guillaume Brunerie]

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