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

Question

Я застрял на следующем. У меня есть вывод перехода pi-исчисления, который происходит в некотором контексте Γ, плюс доказательство того, что Γ ≡ Γ′. Я хотел бы привести вывод к переходу в Γ, используя 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 привести из Γ ⟿ в Γ' ⟿. Наивно, я хотел бы тогда также использовать subst изменить тип R из Proc (target a) в Proc (target (subst _⟿ q a) показывая, что индексы Proc равны. Однако по самой своей природе subst _⟿ q a имеет тип, отличный от a, поэтому я не уверен, как это сделать. Может быть, мне нужно снова использовать доказательство Γ ≡ Γ ′ или как-то "отменить" внутренний subst унифицировать типы.

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

Answer 1

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

Доказательство того, что 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

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