Agda递归证明问题：索引操作一致性证明遇类型错误

问题背景 #

我在Agda中定义了递归数据类型Positive，用于为Tree类型建立索引。目标是证明：当对索引q执行set操作时，不会影响对另一索引p的get操作结果（要求i ≢ j）。

代码与遇到的错误 #

1. gso证明函数的递归错误 #

编写的证明函数框架：

gso : {A : Set} -> ∀ (i j : Positive) (t : Tree A) (v : A) → ((i ≡ j) → ⊥) → get i (set j v t) ≡ get i t
gso (xI p) (xI p) t v = ? 
gso (xO p) (xO p) t v = ?
gso p q t v = ? -- 此分支可正常工作

尝试拆分Tree分支递归调用时：

gso (xI p) (xI q) (Nodes (node001 t)) v neq = gso p q (Nodes t) v neq

出现类型错误：

p != (xI p) of type Positive
when checking that the expression neq has type p ≡ q → ⊥

2. 辅助证明函数的递归错误 #

尝试编写证明xI构造子保持相等性的辅助函数：

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; _≢_)
open Eq.≡-Reasoning

data Positive : Set where 
    xH : Positive
    xI : Positive -> Positive
    xO : Positive -> Positive

proof : ∀ (p q : Positive) → (p ≡ q) → ((xI p) ≡ (xI q))
proof xH xH = λ _ → refl
proof (xI p) xH = λ ()
proof (xO p) xH = λ ()  
proof xH (xI q) = λ ()
proof (xI p) (xI q) = proof p q -- 此处出现错误   
proof (xO p) (xI q) = λ ()
proof xH (xO q) = λ () 
proof (xI p) (xO q) = λ ()
proof (xO p) (xO q) = ?

递归步骤出现类型不匹配错误。

错误原因与解决方法 #

1. 核心问题：构造子的单射性需要显式证明 #

Agda不会默认认为数据类型的构造子是单射的（即xI p ≡ xI q能推导出p ≡ q），必须显式证明这一点，才能在递归调用中转换不等性证明的类型。

步骤1：证明xI和xO的单射性

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; _≢_)
open Eq.≡-Reasoning
open import Data.Empty using (⊥; ⊥-elim)

data Positive : Set where 
    xH : Positive
    xI : Positive -> Positive
    xO : Positive -> Positive

xI-inj : ∀ {p q : Positive} → xI p ≡ xI q → p ≡ q
xI-inj refl = refl

xO-inj : ∀ {p q : Positive} → xO p ≡ xO q → p ≡ q
xO-inj refl = refl

步骤2：修正gso函数的递归调用

在递归分支中，用cong函数将p ≡ q映射为xI p ≡ xI q，从而把原有的neq（类型xI p ≡ xI q → ⊥）转换为递归所需的p ≡ q → ⊥：

-- 假设Tree和get/set的定义如下（根据上下文补全）
data Tree (A : Set) : Set where
  Leaf : A -> Tree A
  Nodes : Tree A -> Tree A -- 示例构造子，根据实际定义调整

get : Positive -> Tree A -> A
get xH (Leaf v) = v
get (xI p) (Nodes t) = get p t
-- 其他get分支省略

set : Positive -> A -> Tree A -> Tree A
set xH v (Leaf _) = Leaf v
set (xI p) v (Nodes t) = Nodes (set p v t)
-- 其他set分支省略

gso : {A : Set} -> ∀ (i j : Positive) (t : Tree A) (v : A) → i ≢ j → get i (set j v t) ≡ get i t
-- 处理i和j构造子相同的情况：直接用⊥-elim消去矛盾
gso (xI p) (xI p) t v neq = ⊥-elim (neq refl)
gso (xO p) (xO p) t v neq = ⊥-elim (neq refl)
-- 递归处理xI分支
gso (xI p) (xI q) (Nodes t) v neq = 
  gso p q t v (λ eq → neq (cong xI eq))
-- 处理i和j构造子不同的情况（示例）
gso (xI p) xH t v neq = refl -- 根据实际get/set逻辑调整
gso xH (xI q) t v neq = refl
-- 其他分支同理补充

2. 辅助函数的修正 #

你写的proof函数其实就是库函数cong xI，不需要手动实现。如果一定要自己写，正确的写法是利用模式匹配处理相等性：

proof : ∀ (p q : Positive) → p ≡ q → xI p ≡ xI q
proof p .p refl = refl

之前的递归错误是因为proof p q的类型是p ≡ q → xI p ≡ xI q，但当前分支需要的是xI p ≡ xI q → xI (xI p) ≡ xI (xI q)，类型不匹配，直接用模式匹配处理refl即可。

关键总结 #

• Agda要求显式证明数据构造子的单射性，不能依赖默认推导
• 递归调用时，需要通过cong或单射性引理转换不等性证明的类型，确保参数类型匹配
• 对于矛盾分支（如i ≡ j但参数要求i ≢ j），用⊥-elim直接消去即可

内容的提问来源于stack exchange，提问作者Max Podpera