"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将a从Γ * *强制到Γ * *。天真地，我还想用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

正如你在评论中所指出的，这可以进一步推广。然而，除非你想做很多这样的证明，否则这种推广不是很有用，因为问题相当罕见，对于更简单的情况，异质相等通常会起作用。