如何处理Cubical Agda中的非终止错误

Question

我使用的是 M 型的通常共归纳定义，定义如下。

record M (S : Set) (Q : S → Set) : Set where
  coinductive
  constructor sup-M
  field
    shape : S
    pos : Q shape → M S Q
open M

我在

Pos

上定义了一个族

M

，它指定了目标类型（即目标类型使用

sup-M

并且对于任何

m : M

都不是通用的）。

data Pos : M S Q → Set where
    here : {s : S} {f : Q s → M S Q} → Pos (sup-M s f) 
    below : {s : S} {f : Q s → M S Q} → (q : Q s) → Pos (f q) → Pos (sup-M s f)

假设对于固定的

S : Set

、

Q : S → Set

、

X Y : Set

、

s : S

、

h : Q s → Y

、

g : Y → X

，我定义了下面的函数进入

M

。

β₁ : Y → M S Q
shape (β₁ y) = s
pos (β₁ y) = β₁ ∘ h

然后，如果我想定义一个函数

β₂ : (y : Y) → Pos (β₁ y) → X

，我无法对第二个参数进行模式匹配，因为它不是

Pos (sup-M s f)

的形式。我可以通过几种方式解决这个问题，其中之一是注意到在 Cubical Agda 中我们有

M

的（命题）eta 等式：

M-eta-eq : {S : Set} {Q : S → Set} (m : M S Q) → sup-M (shape m) (pos m) ≡ m
shape (M-eta-eq m i) = shape m
pos (M-eta-eq m i) = pos m

所以我可以定义一个允许模式匹配的辅助函数

β₂' : (y : Y) → Pos (sup-M s (β₁ ∘ h)) → X

，然后使用

β₂

这一事实根据

β₂'

定义

M-eta-eq (β₁ y) : sup-M s (β₁ ∘ h) ≡ β₁ y

。

β₂' : (y : Y) → Pos (sup-M s (β₁ ∘ h)) → X
β₂' y here = g y
β₂' y (below q p) = β₂' (h q) (subst Pos (sym (M-eta-eq (β₁ (h q)))) p)

β₂ : (y : Y) → Pos (β₁ y) → X
β₂ y p = β₂' y (subst Pos (sym (M-eta-eq (β₁ y))) p)

这样做的问题是它会引发非终止错误，大概是因为 Agda 无法判断

subst Pos (sym (M-eta-eq (β₁ (h q)))) p

在结构上小于

below q p

。所以我的问题是：

我可以向 Agda 证明

β₂'

已终止吗？也许有些东西利用了

subst-filler

？

附注我尝试过其他方法，例如使用

β₂

的消除器定义

Pos

，或者将

m ≡ sup-M s f

形式的等式添加到

Pos

的构造函数，然后使目标类型为

Pos m

类型。虽然我在这两种情况下都能成功定义

β₂

，但这两种方法都引入了许多

subst

和

transport

涉及

β₂

的等式证明，我稍后必须做这些。我想知道是否有更好的方法来定义

Pos

，特别是因为我知道 Cubical Agda 仍然没有完全支持归纳族。

非常感谢您的帮助！

Answer 1

避免绿色粘液：

  β₂ : (y : Y) → ∀ {y'} → y' ≡ β₁ y → Pos y' → X
  β₂ y eq here = g y
  β₂ y eq (below {s} {f} q p) = β₂ (h (subst Q (cong shape eq) q)) eq' p
    where
    eq' : f q ≡ β₁ (h (subst Q (λ i → shape (eq i)) q))
    eq' = (fromPathP⁻ (cong pos eq) ≡$ q) ∙ transportRefl _