Я хочу определить функцию сохранения размера при выводе отношения перехода для исчисления числа Пи. Я не могу убедить Агду в том, что он действительно сохраняет размер. Я также получаю сообщение об ошибке, которое кажется бессмысленным, так что, возможно, в этом есть подсказка.
Я максимально сжал код, сохранив при этом аромат настройки. Вот преамбула.
{-# OPTIONS --sized-types #-}
module SizedTypes 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.
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 φ = {!!}
Грубо говоря, я сравниваю ситуацию, когда есть соседние ν связующие, и показываю, что если я транспонирую связующие (применяя переименование «своп» под связующими), то связанные шаги в деривации также перемещаются. Интуитивно это сохраняет размер перехода.
Переключение скрытых аргументов (в Emacs) показывает, что цель в проблемном предложении имеет тип _—[_]→_ {↑ (↑ .ι)}
, поэтому я ожидаю, что смогу применить два конструктора (в данном случае νᵇ и ν •). Я также вижу, что E имеет тип _—[_]→_ {.ι}
, как и swap*E
, и поэтому я (наивно) ожидаю, что νᵇ (ν• swap*E)
будет соответствовать цели по размеру. Однако Agda жалуется, что ограничения непоследовательны.
Как ни странно, если я использую предложение with
, чтобы ввести ν• swap*E
в контекст, я получаю следующую ошибку:
.ι !=< P of type Size
when checking that the expression E has type
swap ᴾ* P —[ (push ᴬ* out) ᶜ ]→ .R
Это сбивает с толку, потому что выбор метапеременной P предполагает, что Agda пытается сопоставить индекс размера с переменной типа Proc.
Что я здесь делаю не так?