Agda中能否借助Vec.insertAt单射引理实现→′⊢模式匹配？

问题背景 #

在实现类型推导的cut函数时，尝试对Γ,τ⊢k⦂κ进行模式匹配，代码如下：

infix 4.5 _⊢_⦂_
data _⊢_⦂_ : ∀ {n} → Vec Type n → Term n → Type → Set where
  →′⊢ : ∀ {i} →
    Γ ⊢ φ ⦂ σ → τ ∷ Γ ⊢ k ⦂ κ →
    Vec.insertAt Γ i (σ →′ τ) ⊢ # i · incrIf-≥ i φ ⨟ incrIf-≥ (Fin.suc i) k ⦂ κ
  -- 其他构造子省略

cut : ∀ {i} → Γ ⊢ φ ⦂ τ → Vec.insertAt Γ i τ ⊢ k ⦂ κ → ∃[ k′ ] Γ ⊢ k′ ⦂ κ
cut Γ⊢φ⦂τ Γ,τ⊢k⦂κ = ?

Agda无法匹配→′⊢构造子，卡在求解等式：

Vec.insertAt Γ₁ i₁ (σ →′ τ₁) ≟ Vec.insertAt Γ₂ i₂ τ₂

核心疑问：能否通过证明Vec.insertAt是单射的引理，实现→′⊢构造子的反转？已知可以重构_⊢_⦂_构造子避免依赖非平凡函数，但希望保留现有结构。

注：Vec.insertAt并非全局单射，例如Vec.insertAt [y] 0 x ≡ Vec.insertAt [x] 1 y，本问题属于典型的“green slime”示例。

解答 #

1. 全局单射引理不存在，无法直接解决问题 #

首先明确：Vec.insertAt没有全局单射性，用户提到的反例已经证明——同一个向量结果可以由不同的原向量、插入位置和插入元素生成。因此不存在能覆盖所有情况的Vec.insertAt单射引理，自然无法用它来让Agda自动完成模式匹配的等式求解。

2. 局部单射引理也无法辅助自动模式匹配 #

即使在你的场景中，插入的元素类型（σ→′τ和普通τ）有区分度，可以构造局部的单射引理（比如当插入的元素类型属于不同的子类型时，Vec.insertAt的输入唯一），也无法让Agda的模式匹配自动利用这个引理。

原因在于：Agda的模式匹配是在定义阶段进行语法层面的等式统一，而不是在运行时调用用户提供的语义引理。当匹配→′⊢构造子时，Agda需要直接将Vec.insertAt Γ i τ与Vec.insertAt Γ₁ i₁ (σ→′τ₁)的语法结构统一，但这两个表达式的结构因Vec.insertAt的歧义性无法直接对齐，用户提供的引理无法介入这个统一过程。

3. 保留现有构造子的可行（但繁琐）方案 #

如果一定要保留当前的_⊢_⦂_构造子，只能手动对Γ,τ⊢k⦂κ进行case分析，在每个分支中手动调用局部引理来证明等式成立：

• 先对Γ,τ⊢k⦂κ的构造子做穷举
• 对每个构造子（比如→′⊢），手动证明当前的Vec.insertAt Γ i τ与构造子中的Vec.insertAt Γ₁ i₁ (σ→′τ₁)是同一个上下文，从而提取出对应的φ和k
• 最后基于提取出的项构造k′并证明其类型

这种方式本质上是把模式匹配的工作手动转化为证明代码，会产生大量重复、繁琐的“green slime”代码，维护成本极高。

4. 更优方案：重构构造子 #

最简洁的解决方式是重构_⊢_⦂_的构造子，避免将Vec.insertAt的结果作为上下文参数，而是显式保留插入的位置和原上下文信息。例如：

-- 定义显式的上下文插入类型（替代Vec.insertAt的结果）
data CtxInsert : ∀ {n} → Vec Type n → Fin (suc n) → Type → Vec Type (suc n) where
  ctx-insert : ∀ {Γ i τ} → CtxInsert Γ i τ → Vec.insertAt Γ i τ

-- 修改→′⊢构造子
→′⊢ : ∀ {i} →
  Γ ⊢ φ ⦂ σ → τ ∷ Γ ⊢ k ⦂ κ →
  (ctx : CtxInsert Γ i (σ →′ τ)) →
  CtxInsert Γ i (σ →′ τ) ⊢ # i · incrIf-≥ i φ ⨟ incrIf-≥ (Fin.suc i) k ⦂ κ

这样模式匹配时可以直接获取i、Γ等显式参数，无需求解Vec.insertAt的等式，从根源上避免了歧义问题。

内容的提问来源于stack exchange，提问作者William Ryman