" subst“，其中要等号的索引也使用subst

Question

我被困在下面。我导出了在某些上下文Γ中发生的π演算转换，以及一个证明Γ≡Γ‘的证明。我希望使用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不同的类型，所以我不确定如何做到这一点。也许我需要再次使用Γ≡Γ的证明，或者以某种方式“撤消”内部Γ≡Γ来统一类型。

我想做的是合理的吗？如果是这样的话，在异质性的情况下，我如何强迫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

正如您在评论中所指出的，这可以进一步推广。但是，除非您期望做很多这类的证明，否则这种推广并不是很有用，因为这个问题很少见，对于更简单的情况，异构等式通常是起作用的。