Agda实现HoTT引理2.3.9时约束求解失败问题排查

问题背景 #

阅读HoTT（同伦类型论）教材编写Agda代码时，在实现引理2.3.9的过程中遇到类型检查阻塞，初始编写的Agda代码如下：

data _≡_ {X : Set} : X -> X -> Set where
  refl : {x : X} -> x ≡ x
infix 4 _≡_

-- Lemma 2.1.2
_·_ :  {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z
refl · refl = refl

-- Lemma 2.3.1
transp : {A : Set} {P : A -> Set} {x y : A} -> x ≡ y -> P x -> P y
transp refl f = f

lemma2'3'9 : {A : Set}{P : A -> Set}{x y z : A}{p : x ≡ y}{q : y ≡ z}{u : P x} -> 
             (transp q (transp p u)) ≡ (transp (p · q) u)
lemma2'3'9 {p = refl} {q = refl} = ?

使用Agda Emacs模式执行类型检查时，抛出如下错误信息：

?0 : transp refl (transp refl u) ≡ transp (refl · refl) u
_X_53 : Set  [ at /home/user/prog/agda/sample.agda:12,38-39 ]

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  P x =< _X_53 (blocked on _X_53)

备注：已在Coq中完成该引理的可正常运行的实现，确认引理可在依赖类型证明助手中验证通过，对应Coq代码如下：

Inductive eq {X:Type} (x: X) : X -> Type :=
  | refl : eq x x.
Notation "x = y" := (eq x y)
                       (at level 70, no associativity)
                     : type_scope.

Definition eqInd{A} (C: forall x y: A, x = y -> Type) (c: forall x: A, C x x (refl x)) (x y: A): forall p: x = y, C x y p :=
  fun xy: x = y => match xy with
            | refl _ => c x
            end.

Definition dot'{A}{x y: A}: x = y -> forall z: A, y = z -> x = z :=
  let D := fun x y: A => fun p: x = y => forall z: A, forall q: y = z, x = z in
  let d: forall x, D x x (refl x) := let E: forall x z: A, forall q: x = z, Type := fun x z: A => fun q: x = z => x = z in
                                let e := fun x => refl x
                                in  fun x z => fun q => eqInd E e x z q
  in fun p: x = y => eqInd D d x y p.

(* Lemma 2.1.2 *)
Definition dot{A}{x y z: A}: x = y -> y = z -> x = z :=
  fun p: x = y => dot' p z.

Definition id {A} := fun a: A => a.

(* Lemma 2.3.1 *)
Definition transp{A} {P: A -> Type} {x y: A}: x = y -> P x -> P y :=
  fun p =>
  let D := fun x y: A => fun p: x = y => P x -> P y in
  let d: forall x, D x x (refl x) := fun x => id
  in  eqInd D d x y p.

Lemma L_2_3_9{A}{P: A -> Type}{x y z: A}{p: x = y}{q: y = z}{u: P x}:
  transp q (transp p u) = transp (dot p q) u.
Proof.
  unfold transp, dot, dot'.
  rewrite <- q.
  rewrite <- p.
  reflexivity.
  Qed.

待解决疑问 #

• 报错信息中的_X_53是什么？为什么会生成P x <= _X_53的约束？
• 如何修复该错误，完成引理2.3.9的Agda实现？

问题解答 #

1. _X_53与约束生成原因 #

_X_53是Agda类型检查阶段生成的未定元（metavariable），代表暂时无法推导确定的未知类型，后缀数字是Agda内部分配的唯一编号。
这个报错约束的生成原因是依赖类型模式匹配时的信息不足：当对依赖类型的等式构造器refl做模式匹配时，Agda需要将等式两端的项做合一（unification），但原写法仅指定了隐式参数p和q为refl，跳过了y、z等和p、q类型直接相关的隐式参数绑定，导致Agda无法确定第二次调用transp时传入的类型族P的具体参数类型，于是生成未定元_X_53。P x =< _X_53的约束表示Agda需要验证P x类型的项可以适配这个未知类型，但因为缺少推导信息被阻塞，无法完成类型检查。

2. 错误修复与引理实现 #

修复的核心是在模式匹配时为Agda提供足够的参数绑定信息，让依赖类型可以正常完成合一：当p = refl时y与x相等，当q = refl时z与y（即x）相等，此时等式两边的项都会自动归约为u，直接用refl即可完成证明。
可通过类型检查的完整Agda实现如下：

data _≡_ {X : Set} : X -> X -> Set where
  refl : {x : X} -> x ≡ x
infix 4 _≡_

-- Lemma 2.1.2
_·_ :  {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z
refl · refl = refl

-- Lemma 2.3.1
transp : {A : Set} {P : A -> Set} {x y : A} -> x ≡ y -> P x -> P y
transp refl f = f

lemma2'3'9 : {A : Set}{P : A -> Set}{x y z : A}{p : x ≡ y}{q : y ≡ z}{u : P x} -> 
             (transp q (transp p u)) ≡ (transp (p · q) u)
lemma2'3'9 {x = x} {y = .x} {z = .x} {p = refl} {q = refl} = refl

其中.x是Agda的不可访问模式（dot pattern），表示该位置的参数由p=refl、q=refl的匹配结果强制确定为x，不需要额外匹配。
如果不想手动写dot pattern，也可以按隐式参数的定义顺序显式列出所有参数，让Agda自动完成合一，写法如下：

lemma2'3'9 {A = _} {P = _} {x = _} {y = _} {z = _} {p = refl} {q = refl} {u = _} = refl

内容的提问来源于stack exchange，提问作者Nuclear Catapult