“subst”，其中要等同的索引也使用 subst

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 将 a 从 Γ ⟿ 强制转换为 Γ' ⟿。天真地，我还想使用 subst 通过显示 Proc 索引相等来将 R 的类型从 Proc (target a) 更改为 Proc (target (subst _⟿ q a)。但是，就其本质而言，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 : Γ ⟿ 到Γ′ ⟿ 的变化。

据我所知，标准库没有提供任何替代的substs 来捕获这种交互。简单的解决方案是自己编写组合器：

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

正如您在 cmets 中所指出的，这可以进一步概括。但是，除非您希望进行大量此类证明，否则这种泛化并不是很有用，因为问题相当罕见，而且对于更简单的情况，异质相等通常可以解决问题。