在案例拆分期间遇到统一问题

Question

假设我们有以下代码：

open import Data.Fin
open import Data.Nat

data SType : ℕ → Set where

variable
  ℓ : ℕ
  ι : Fin ℓ
  τ τ' : SType ℓ

infixl 5 _,_
data Ctx : ℕ → Set where
  ⊘   : Ctx zero
  _,_ : Ctx ℓ → SType ℓ → Ctx (suc ℓ)

variable Γ : Ctx ℓ

postulate weaken : SType ℓ → SType (suc ℓ)

infix 4 _∈_at_
data _∈_at_ : SType ℓ → Ctx ℓ → Fin ℓ → Set where
  ∈-zero : weaken τ ∈ Γ , τ at zero
  ∈-suc  : τ ∈ Γ at ι
         → weaken τ ∈ Γ , τ' at suc ι

它模拟了类型系统的范围广泛的表示的一小部分（并且我保持 weaken postulated 和 SType 没有任何构造函数简洁）。

现在假设我们要编写一个基本上是 ∈-suc 构造函数的“逆函数”的函数：

∈-chop : weaken τ ∈ Γ , τ' at suc ι
       → τ ∈ Γ at ι
∈-chop ∈ = {! !}

现在，如果我们尝试在 ∈ 上进行拆分，Agda 将得到所有的怀疑和犹豫：

I'm not sure if there should be a case for the constructor ∈-suc,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  {suc τ.ℓ₁} ≟ {suc τ.ℓ₂}
  weaken τ₁ ≟ weaken τ₂
  Γ₁ , τ'' ≟ Γ₂ , τ'''
  suc ι₁ ≟ suc ι₂
when checking that the expression ? has type τ ∈ Γ at ι

为什么不确定，解决这个问题的最佳方法是什么？

Answer 1

您的定义似乎暗示，在 ∈-chop 中没有 τ 的可能值，如下所示：

∈-chop : ∀ {Γ τ ι} → weaken τ ∈ Γ , τ' at suc ι → τ ∈ Γ at ι
∈-chop {τ = ()}

这不会直接回答您的问题，但它可能不是最终可以解决您问题的缩进行为。

Answer 2

你的问题是绿色史莱姆。

Quoting 贾斯帕·科克斯：

The error message "cannot generalize over the indices" is thrown by Agda when it encounters a unification problem of the form c us =?= c vs where c is a constructor of an indexed datatype, but the indices in the type of this equation are something other than distinct variables (i.e. they should be fully general). If they are not, Agda tries to apply a technique called higher-dimensional unification (see our CPP 2017 paper) to bring them in a fully general form. However, this unfortunately doesn't always succeed, for example in your code it gets stuck on the + function in the index of con.

One way to fix your problem would be to get rid of the 'green slime' in the type of con: it's better to use only variables and constructors in the indices of your datatypes, and use explicit proofs of equality for the heavier work.

您可以通过使 weaken 成为 SType 的构造函数来检查确实是这种情况，然后您可以根据需要通过模式匹配来定义 ∈-chop。

在 ∈-suc 上匹配相当于求解

weaken τ ∈ Γ , τ' at suc ι =?= weaken _τ ∈ _Γ , _τ' at suc _ι

其中 LHS 是您在类型签名中提供的类型，RHS 是 ∈-suc 的推断类型，其中每个隐式变量都变成了元数据。现在统一，比方说，suc ι 和 suc _ι 没问题，因为构造函数是内射的，但函数通常不是（见的第一部分），所以当 weaken是无法将 weaken τ 与 weaken _τ.

统一的函数

您可以使用显式相等来解决此问题：

open import Relation.Binary.PropositionalEquality
 
infix 4 _∈_at_
data _∈_at_ : SType ℓ → Ctx ℓ → Fin ℓ → Set where
  ∈-zero : τ' ≡ weaken τ → τ' ∈ Γ , τ at zero
  ∈-suc  : τ' ≡ weaken τ
         → τ ∈ Γ at ι
         → τ' ∈ Γ , τ at suc ι

这允许您在 ∈-chop 中进行模式匹配，即使 weaken 是一个函数。

在案例拆分期间遇到统一问题

Stuck on unification problems during case splitting

agda