<p>This goes through if you change <code>_≈_</code> and <code>·-distribˡ</code> to take arguments in <code>Lang ∞ A</code> instead of <code>Lang i A</code>, as Abel does in <a href="https://www2.tcs.ifi.lmu.de/%7Eabel/cmcs16/html/Lang.html#5886" rel="nofollow noreferrer">his proof</a> of the same fact:</p>
<pre><code>{-# OPTIONS --guardedness --sized-types #-}

module Languages where

open import Relation.Binary.PropositionalEquality
open import Agda.Builtin.Size
open import Data.Bool
open import Data.Bool.Properties

record Lang (i : Size) (A : Set) : Set where
  coinductive
  field
    ν : Bool
    δ : ∀{j : Size&lt; i} → A → Lang j A

open Lang

infix 4 _≈_
record _≈_ {i : Size} {A : Set} (L M : Lang ∞ A) : Set where
  coinductive
  field
    ν-≈ : ν L ≡ ν M
    δ-≈ : ∀ {j : Size&lt; i} (a : A) → _≈_ {j} (δ L a) (δ M a)

open _≈_

-- union
infixr 6 _∪_
_∪_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
ν (L ∪ M) = ν L ∨ ν M
δ (L ∪ M) a = δ L a ∪ δ M a

-- concatenation
infixr 7 _·_
_·_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
ν (L · M) = ν L ∧ ν M
δ (L · M) x = if ν L then δ L x · M ∪ δ M x else δ L x · M

·-distribˡ : ∀ {i A} (L M N : Lang ∞ A) → _≈_ {i} (L · (M ∪ N)) (L · M ∪ L · N)
ν-≈ (·-distribˡ L M N) = ∧-distribˡ-∨ (ν L) (ν M) (ν N)
δ-≈ (·-distribˡ L M N) a with ν L
... | true = {!!}
... | false = ·-distribˡ (δ L a) M N
<span class="math-container">```</span>
</code></pre>

CC BY-SA 4.0
2024-11-30T15:43:47.850Z
that answers it, thank you!
Lorenzo
CC BY-SA 4.0
2024-11-29T15:57:37.673Z
2024-11-29T15:57:37.673Z
Naïm Favier
<p>I was having a look at how to use <a href="https://agda.readthedocs.io/en/v2.7.0.1/language/sized-types.html" rel="nofollow noreferrer">sized types</a> in order to define finite languages in a coinductive way.
I immediately got stuck going one step further
when trying to prove that concatenation distributes over union.</p>
<p>Here is the M(n)WE:</p>
<pre><code>{-# OPTIONS --guardedness --sized-types #-}

module Languages where

open import Relation.Binary.PropositionalEquality
open import Agda.Builtin.Size
open import Data.Bool
open import Data.Bool.Properties

record Lang (i : Size) (A : Set) : Set where
  coinductive
  field
    ν : Bool
    δ : ∀{j : Size&lt; i} → A → Lang j A

open Lang

infix 4 _≈_
record _≈_ {i : Size} {A : Set} (L M : Lang i A) : Set where
  coinductive
  field
    ν-≈ : ν L ≡ ν M
    δ-≈ : ∀ {j : Size&lt; i} (a : A) → δ L {j} a ≈ δ M {j} a

open _≈_

-- union
infixr 6 _∪_
_∪_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
ν (L ∪ M) = ν L ∨ ν M
δ (L ∪ M) a = δ L a ∪ δ M a

-- concatenation
infixr 7 _·_
_·_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
ν (L · M) = ν L ∧ ν M
δ (L · M) x = if ν L then δ L x · M ∪ δ M x else δ L x · M

·-distribˡ : ∀ {i A} (L M N : Lang i A) → L · (M ∪ N) ≈ L · M ∪ L · N
ν-≈ (·-distribˡ L M N) = ∧-distribˡ-∨ (ν L) (ν M) (ν N)
δ-≈ (·-distribˡ L M N) a with ν L
... | true = {!!}
... | false = {! ·-distribˡ (δ L a) M N !} -- : δ L a · (M ∪ N) ≈ δ L a · M ∪ δ L a · N

-- j != i of type Size
-- when checking that the expression ·-distribˡ (δ L a) M N has type
-- (if false then δ L a · (M ∪ N) ∪ δ M a ∪ δ N a else
--  δ L a · (M ∪ N))
-- ≈
-- (if false then δ L a · M ∪ δ M a else δ L a · M) ∪
-- (if false then δ L a · N ∪ δ N a else δ L a · N)
</code></pre>
<p>The problem is at the very end, where</p>
<blockquote>
<p><code>·-distribˡ (δ L a) M N</code></p>
</blockquote>
<p>gives the desired type</p>
<blockquote>
<p><code>δ L a · (M ∪ N) ≈ δ L a · M ∪ δ L a · N</code>,</p>
</blockquote>
<p>however sizes do not match:</p>
<ul>
<li><p>The size of <code>M ∪ N</code> should be <code>i</code>,
since <code>M</code>, <code>N</code> have size <code>i</code> and this is preserved by union.</p>
</li>
<li><p>The size of <code>M ∪ N</code> should be <code>j</code>,
since <code>δ L a</code> has size <code>j</code> and concatenation expects both arguments to be of the same size.</p>
</li>
</ul>
<p>Since <code>i</code> and <code>j</code> are different, this is impossible.
Does any Agda expert have any idea whether this can be overcome
or it is an inherent limitation of sized types? Thank you!</p>

CC BY-SA 4.0
2024-11-29T14:02:21.260Z
Interestingly, [Abel 2017](https://www.cse.chalmers.se/~abela/jlamp17.pdf) features that exact proof (for languages of size ∞, but this doesn't seem to make a difference) and he doesn't seem to run into a problem. I wonder if something changed in Agda. Morally, you should be able to prove that `_∪_ {j} M N` and `_∪_ {i} M N` are equal, at least up to `_≈_`. Being explicit about the subtyping embedding `inc : Lang i A → Lang j A`, this says that `inc M ∪ inc N ≈ inc (M ∪ N)`; in other words `_∪_` is natural/parametric in the sizes. It might be worth asking this question on proofassistants.SE
Naïm Favier
CC BY-SA 4.0
2024-12-04T17:32:31.747Z
Two things. (1) you might find more Agda-specific help on the Proof Assistants Stack Exchange, and (2) unfortunately, sized types are inconsistent in Agda (see https://blog.ielliott.io/sized-types-and-coinduction-in-safe-agda), so beware if you're using them
Joey Eremondi
<type-theory><dependent-type><typed-lambda-calculus><agda>
proof problem with Agda's sized types
Lorenzo
# proof problem with Agda's sized types

(Asked by: username_0 on 2024-11-29)

I was having a look at how to use sized types in order to define finite languages in a coinductive way.
I immediately got stuck going one step further
when trying to prove that concatenation distributes over union.
Here is the M(n)WE:
{-# OPTIONS --guardedness --sized-types #-}

module Languages where

open import Relation.Binary.PropositionalEquality
open import Agda.Builtin.Size
open import Data.Bool
open import Data.Bool.Properties

record Lang (i : Size) (A : Set) : Set where
  coinductive
  field
    ν : Bool
    δ : ∀{j : Size< i} → A → Lang j A

open Lang

infix 4 _≈_
record _≈_ {i : Size} {A : Set} (L M : Lang i A) : Set where
  coinductive
  field
    ν-≈ : ν L ≡ ν M
    δ-≈ : ∀ {j : Size< i} (a : A) → δ L {j} a ≈ δ M {j} a

open _≈_

-- union
infixr 6 _∪_
_∪_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
ν (L ∪ M) = ν L ∨ ν M
δ (L ∪ M) a = δ L a ∪ δ M a

-- concatenation
infixr 7 _·_
_·_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
ν (L · M) = ν L ∧ ν M
δ (L · M) x = if ν L then δ L x · M ∪ δ M x else δ L x · M

·-distribˡ : ∀ {i A} (L M N : Lang i A) → L · (M ∪ N) ≈ L · M ∪ L · N
ν-≈ (·-distribˡ L M N) = ∧-distribˡ-∨ (ν L) (ν M) (ν N)
δ-≈ (·-distribˡ L M N) a with ν L
... | true = {!!}
... | false = {! ·-distribˡ (δ L a) M N !} -- : δ L a · (M ∪ N) ≈ δ L a · M ∪ δ L a · N

-- j != i of type Size
-- when checking that the expression ·-distribˡ (δ L a) M N has type
-- (if false then δ L a · (M ∪ N) ∪ δ M a ∪ δ N a else
--  δ L a · (M ∪ N))
-- ≈
-- (if false then δ L a · M ∪ δ M a else δ L a · M) ∪
-- (if false then δ L a · N ∪ δ N a else δ L a · N)

The problem is at the very end, where

·-distribˡ (δ L a) M N

gives the desired type

δ L a · (M ∪ N) ≈ δ L a · M ∪ δ L a · N,

however sizes do not match:

The size of M ∪ N should be i,
since M, N have size i and this is preserved by union.

The size of M ∪ N should be j,
since δ L a has size j and concatenation expects both arguments to be of the same size.


Since i and j are different, this is impossible.
Does any Agda expert have any idea whether this can be overcome
or it is an inherent limitation of sized types? Thank you!

**Tags:** type-theory, dependent-type, typed-lambda-calculus, agda

> **Comments:**
> **username_1**: Interestingly, [Abel 2017](https://www.cse.chalmers.se/~abela/jlamp17.pdf) features that exact proof (for languages of size ∞, but this doesn't seem to make a difference) and he doesn't seem to run into a problem. I wonder if something changed in Agda. Morally, you should be able to prove that `_∪_ {j} M N` and `_∪_ {i} M N` are equal, at least up to `_≈_`. Being explicit about the subtyping embedding `inc : Lang i A → Lang j A`, this says that `inc M ∪ inc N ≈ inc (M ∪ N)`; in other words `_∪_` is natural/parametric in the sizes. It might be worth asking this question on proofassistants.SE  
> **username_2**: Two things. (1) you might find more Agda-specific help on the Proof Assistants Stack Exchange, and (2) unfortunately, sized types are inconsistent in Agda (see https://blog.ielliott.io/sized-types-and-coinduction-in-safe-agda), so beware if you're using them  

---

## 1 answers

### Answer by username_1 on 2024-11-29. Score: 4 | Accepted answer

This goes through if you change _≈_ and ·-distribˡ to take arguments in Lang ∞ A instead of Lang i A, as Abel does in his proof of the same fact:
{-# OPTIONS --guardedness --sized-types #-}

module Languages where

open import Relation.Binary.PropositionalEquality
open import Agda.Builtin.Size
open import Data.Bool
open import Data.Bool.Properties

record Lang (i : Size) (A : Set) : Set where
  coinductive
  field
    ν : Bool
    δ : ∀{j : Size< i} → A → Lang j A

open Lang

infix 4 _≈_
record _≈_ {i : Size} {A : Set} (L M : Lang ∞ A) : Set where
  coinductive
  field
    ν-≈ : ν L ≡ ν M
    δ-≈ : ∀ {j : Size< i} (a : A) → _≈_ {j} (δ L a) (δ M a)

open _≈_

-- union
infixr 6 _∪_
_∪_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
ν (L ∪ M) = ν L ∨ ν M
δ (L ∪ M) a = δ L a ∪ δ M a

-- concatenation
infixr 7 _·_
_·_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
ν (L · M) = ν L ∧ ν M
δ (L · M) x = if ν L then δ L x · M ∪ δ M x else δ L x · M

·-distribˡ : ∀ {i A} (L M N : Lang ∞ A) → _≈_ {i} (L · (M ∪ N)) (L · M ∪ L · N)
ν-≈ (·-distribˡ L M N) = ∧-distribˡ-∨ (ν L) (ν M) (ν N)
δ-≈ (·-distribˡ L M N) a with ν L
... | true = {!!}
... | false = ·-distribˡ (δ L a) M N
```

> **Comments:**
> **username_0**: that answers it, thank you!  

---

