subst, где приравниваемые индексы также используют subst

Я застрял на следующем. У меня есть вывод перехода исчисления пи, который имеет место в некотором контексте Γ, а также доказательство того, что Γ ≡ Γ′. Я хотел бы принудить вывод к переходу в Γ', используя subst. Детали настройки в основном неважны, как обычно.

module Temp where
   open import Data.Nat as Nat using (_+_) renaming (ℕ to Cxt)
   open import Function
   open import Relation.Binary.PropositionalEquality

   data _⟿ (Γ : Cxt) : Set where
      bound : Γ ⟿
      nonBound : Γ ⟿

   target : ∀ {Γ} → Γ ⟿ → Cxt
   target {Γ} bound = Γ + 1
   target {Γ} nonBound = Γ

   data Proc (Γ : Cxt) : Set where
   data _—[_]→_ {Γ} : Proc Γ → (a : Γ ⟿) → Proc (target a) → Set where

   -- Use a proof that Γ ≡ Γ′ to coerce a transition in Γ to one in Γ'.
   coerce : ∀ {Γ Γ′} {P : Proc Γ} {a R} → P —[ a ]→ R → (q : Γ ≡ Γ′) →
               subst Proc q P —[ subst _⟿ q a ]→ subst (Proc ∘ target) {!!} R
   coerce E refl = {!!}

Достаточно легко указать как источник P перехода, так и действие a, которое отображается как метка перехода. Проблема заключается в цели R перехода, тип которой зависит от a. В принудительном переходе я использую subst, чтобы перевести a из Γ ⟿ в Γ' ⟿. Наивно, я хотел бы также использовать subst, чтобы изменить тип R с Proc (target a) на Proc (target (subst _⟿ q a), показав, что индексы Proc равны. Однако по своей природе subst _⟿ q a имеет тип, отличный от a, поэтому я не знаю, как это сделать. Может быть, мне нужно снова использовать доказательство Γ ≡ Γ′ или каким-то образом «отменить» внутреннее subst, чтобы унифицировать типы.

Разумно ли то, что я пытаюсь сделать? Если да, то как принудить R с учетом неоднородности?


equality agda subst
person Roly    schedule 21.08.2014    source источник
comment
Работает ли это?   -  person Vitus    schedule 21.08.2014
comment
Да, это так. Спасибо. (Я заметил, что subst' не нужно принимать P в качестве параметра.)   -  person Roly    schedule 21.08.2014
comment
Хм, кажется, это было намного банальнее, чем я думал (как это часто бывает). Не стесняйтесь натолкнуть это на ответ. Насколько общим может быть subst'? Очевидно, вы можете параметризовать Proc. Или в стандартной библиотеке уже что-то есть?   -  person Roly    schedule 21.08.2014
comment
Я пробовал это с неоднородным равенством. Но кажется, что у обоих subst есть проблема с изменением типа a с Γ ⟿ на Γ′ ⟿. В библиотеке может быть что-то, но мне ничего не известно. Я напишу ответ позже.   -  person Vitus    schedule 21.08.2014
comment
Вот немного более общая версия subst'...   -  person Roly    schedule 21.08.2014

Ответы (1)


arrow_upward
2
arrow_downward

Как правило, когда вы хотите сравнить две вещи разных типов (которые могут стать равными при подходящем сокращении), вам следует использовать разнородное равенство.

Доказательство того, что subst на самом деле не меняет значение, не может быть сделано с помощью обычного (пропозиционального) равенства, потому что a и subst P q a имеют разные типы. Однако, как только вы узнаете, что q = refl, вы можете сократить эти выражения настолько, чтобы теперь их типы совпадали. Это можно выразить с помощью неоднородного равенства:

data _≅_ {ℓ} {A : Set ℓ} (x : A) : {B : Set ℓ} → B → Set ℓ where
   refl : x ≅ x

Это позволяет даже выразить тот факт, что a ≅ subst P q a. Когда вы затем сопоставляете шаблон на q, цель сводится к простому a ≅ a, что затем можно доказать с помощью рефлексивности:

≡-subst-removable : ∀ {a p} {A : Set a}
                    (P : A → Set p) {x y} (eq : x ≡ y) z →
                    P.subst P eq z ≅ z
≡-subst-removable P refl z = refl

Итак, первый порыв — заменить последние subst на разнородные subst (из Relation.Binary.HeterogeneousEquality) и использовать доказательство ≡-subst-removable. Это почти работает; проблема в том, что этот subst не может зафиксировать изменение с a : Γ ⟿ на Γ′ ⟿.

Насколько мне известно, стандартная библиотека не предоставляет никаких альтернативных subst, фиксирующих это взаимодействие. Простое решение — написать комбинатор самостоятельно:

subst′ : ∀ {Γ Γ′} {a} (q : Γ ≡ Γ′) (R : Proc (target a)) →
         Proc (target (subst _⟿ q a))
subst′ refl R = R

Как вы отметили в комментариях, это может быть дополнительно обобщено. Однако, если вы не собираетесь делать много доказательств такого рода, это обобщение не очень полезно, поскольку проблема возникает довольно редко, а в более простых случаях обычно работает неоднородное равенство.

person Vitus    schedule 21.08.2014
comment
Отлично, спасибо за подробный ответ. Я заметил ≡-subst-removable в библиотеке, так что я посмотрю на его использование в будущем. - person Roly; 22.08.2014