[Agda] Sized types problem

[Andrea Vezzosi]

Hi Roly,

If you give the size argument explicitly it goes through:

  ⊖ (ν• (νᶜ_ {ι} E)) (νν-swap P) with swap ᵀ* E
   ... | swap*E rewrite swap-involutive P | swap∘push
     = _ , νᵇ (ν•_ {ι = ι} swap*E)


Cheers,
Andrea

On Mon, Aug 18, 2014 at 9:39 AM, Roly Perera
<roly.perera at dynamicaspects.org> wrote:
> Hi,
>
> I'm modelling pi calculus in Agda and having difficulty using sized types in
> order to have the function ⊖ below pass the termination-checker. I'm also
> getting an error message which looks a bit odd, so perhaps there's a clue to
> what I'm doing wrong in there.
>
> {-# OPTIONS --sized-types #-}
>
> module Temp where
>
>    open import Data.Product public hiding (swap)
>    open import Relation.Binary.PropositionalEquality
>    open import Size
>
>    -- Processes.
>    data Proc : Set where
>       ν_ : Proc → Proc
>
>    -- Actions.
>    data ⟿ᵇ : Set where
>       input : ⟿ᵇ
>       boundOut : ⟿ᵇ
>
>    data ⟿ᶜ : Set where
>       out : ⟿ᶜ
>
>    data ⟿ : Set where
>       _ᵇ : ⟿ᵇ → ⟿
>       _ᶜ : ⟿ᶜ → ⟿
>
>    -- Renamings. Leave undefined for now.
>    data Ren : Set where
>
>    postulate
>       push : Ren
>       swap : Ren
>       _ᴬ*_ : Ren → ⟿ᶜ →  ⟿ᶜ
>
>    -- Transitions.
>    data _—[_]→_ : {ι : Size} → Proc → (a : ⟿) → Proc → Set where
>       ν•_ : ∀ {ι P R} → _—[_]→_ {ι = ι} P (out ᶜ) R →
>             _—[_]→_ {ι = ↑ ι} (ν P) (boundOut ᵇ) R
>       νᵇ_ : ∀ {ι P R} {a : ⟿ᵇ} → _—[_]→_ {ι = ι} P (boundOut ᵇ) R →
>             _—[_]→_ {ι = ↑ ι} (ν P) (a ᵇ) (ν R)
>       νᶜ_ : ∀ {ι P R} → _—[_]→_ {ι = ι} P ((push ᴬ* out) ᶜ) R →
>             _—[_]→_ {ι = ↑ ι} (ν P) (out ᶜ) (ν R)
>
>    infixl 0 _—[_]→_
>
>    postulate
>       _ᴾ*_ : Ren → Proc → Proc
>       _ᵀ*_ : ∀ {ι} (ρ : Ren) {P R} {a : ⟿ᶜ} → _—[_]→_ {ι = ι} P (a ᶜ) R →
>              _—[_]→_ {ι = ι} (ρ ᴾ* P) ((ρ ᴬ* a) ᶜ) (ρ ᴾ* R)
>       swap-involutive : ∀ (P : Proc) → swap ᴾ* swap ᴾ* P ≡ P
>       swap∘push : swap ᴬ* push ᴬ* out ≡ out
>
>    infixr 8 _ᵀ*_ _ᴾ*_ _ᴬ*_
>
>    -- Structural congruence.
>    infix 4 _≅_
>    data _≅_ : Proc → Proc → Set where
>       νν-swap : ∀ P → ν (ν (swap ᴾ* P)) ≅ ν (ν P)
>
>    -- "Residual" of a transition E after a structural congruence φ.
>    ⊖ : ∀ {ι P P′} {a : ⟿} {R} (E : _—[_]→_ {ι = ι} P a R) (φ : P ≅ P′) →
>        Σ[ R ∈ Proc ] _—[_]→_ {ι = ι} P′ a R
>    ⊖ (ν•_ (νᶜ E)) (νν-swap P) with swap ᵀ* E
>    ... | swap*E rewrite swap-involutive P | swap∘push =
>       _ , {!!} -- νᵇ (ν• swap*E)
>    ⊖ E φ = {!!}
>
> (I can try to boil the code down further if that would help, but I wanted to
> maintain some of the structure of my setting.)
>
> In the first goal above, I'm matching on the situation where there are
> adjacent ν binders, and showing that if I transpose the binders (by applying
> the 'swap' renaming under the binders) then the associated steps in the
> derivation also tranpose. Intuitively this preserves the size of the
> transition derivation. And indeed, toggling hidden arguments reveals that
> the goal has type _—[_]→_ {↑ (↑ .ι)}, so I expect to be able to apply two
> constructors (νᵇ and ν• in this case) in return for two I eliminated (ν• and
> νᶜ).
>
> I can also see that E has type _—[_]→_ {.ι}. Since I've postulated that ᵀ*
> is size-preserving, the variable swap*E also has this type. Naively, I
> expect νᵇ (ν• swap*E) to therefore be size-consistent with the goal. However
> Agda complains that the constraints are inconsistent.
>
> Weirdly, if I use a "with" clause to introduce ν• swap*E into the context, I
> get the following error:
>
> .ι !=< P of type Size
> when checking that the expression E has type
> swap ᴾ* P —[ (push ᴬ* out) ᶜ ]→ .R
>
> This is baffling because the appearance of meta-variable P in the error
> message suggests that Agda is trying to match a size index against a
> variable of type Proc, does it not?
>
> Can anyone shed any light on what's going on here?
>
> many thanks,
> Roly
>
>
> Roly Perera
> LFCS, School of Informatics
> University of Edinburgh
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>