[Agda] Equalities between elements of different sizes

[Oleg Grenrus]

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