[Agda] Equalities between elements of different sizes

[Guillaume Brunerie]

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)

[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

Post by Guillaume Brunerie
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
https://lists.chalmers.se/mailman/listinfo/agda

[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

Post by Oleg Grenrus
Hi Guillaume,
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

Post by Guillaume Brunerie
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
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[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

Post by 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

Post by Oleg Grenrus
Hi Guillaume,
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

Post by Guillaume Brunerie
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
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda