消除只有一个有效案例的擦除参数

Question

我定义了无限流如下：

record Stream (A : Set) : Set where
    coinductive
    field head : A
    field tail : Stream A

和一个归纳类型，它表明流中的某些元素最终满足谓词：

data Eventually {A} (P : A -> Set) (xs : Stream A) : Set where
    here  : P (head xs) -> Eventually P xs
    there : Eventually P (tail xs) -> Eventually P xs

我想编写一个函数来跳过流的元素，直到流的头部满足谓词。为确保终止，我们必须知道元素最终满足谓词，否则我们可能会永远循环下去。因此，Eventually 的定义必须作为参数传递。此外，该函数在计算上不应依赖于 Eventually 谓词，因为它只是用来证明终止，所以我希望它是一个已删除的参数。

dropUntil : {A : Set} {P : A -> Set} (decide : ∀ x → Dec (P x)) → (xs : Stream A) → @0 Eventually P xs → Stream A
dropUntil decide xs ev with decide (head xs)
... | yes prf = xs
... | no contra = dropUntil decide (tail xs) ?

问题来了 - 我想填补定义中的漏洞。从作用域中的contra，我们知道流的头部不满足P，因此根据eventually的定义，流尾的某个元素必须满足P。如果 Eventually 在这种情况下没有被删除，我们可以简单地对谓词进行模式匹配，并证明 here 的情况是不可能的。通常在这些情况下，我会写一个擦除的辅助函数，行如下：

@0 eventuallyInv : ∀ {A} {P : A → Set} {xs : Stream A} → Eventually P xs → ¬ P (head xs) → Eventually P (tail xs)
eventuallyInv (here x) contra with contra x
... | ()
eventuallyInv (there ev) contra = ev

这种方法的问题在于 Eventually 证明是 dropUntil 中的结构递归参数，并且调用此辅助函数不会通过终止检查器，因为 Agda 不会“查看内部”函数定义。

我尝试的另一种方法是将上面删除的函数内联到 dropUntil 的定义中。不幸的是，我也没有采用这种方法 - 使用此处描述的 case ... of 的定义 https://agda.readthedocs.io/en/v2.5.2/language/with-abstraction.html 也没有通过终止检查程序。

我在 Coq 中编写了一个等效的程序，它被接受（使用 Prop 而不是擦除类型），所以我相信我的推理是正确的。 Coq 接受定义而 Agda 不接受的主要原因是 Coq 的终止检查器扩展了函数定义，因此“辅助擦除函数”方法成功了。

编辑：

这是我使用大小类型的尝试，但是它没有通过终止检查器，我不明白为什么。

record Stream (A : Set) : Set where
    coinductive
    field
        head : A
        tail : Stream A

open Stream


data Eventually {A} (P : A → Set) (xs : Stream A) : Size → Set where
    here : ∀ {i} → P (head xs) → Eventually P xs (↑ i)
    there : ∀ {i} → Eventually P (tail xs) i → Eventually P xs (↑ i)


@0 eventuallyInv : ∀ {A P i} {xs : Stream A} → Eventually P xs (↑ i) → ¬ P (head xs) → Eventually P (tail xs) i
eventuallyInv (here p) ¬p with ¬p p
... | ()
eventuallyInv (there ev) ¬p = ev


dropUntil : ∀ {A P i} → (∀ x → Dec (P x)) → (xs : Stream A) → @0 Eventually P xs (↑ i) → Stream A
dropUntil decide xs ev with decide (head xs)
... | yes p = xs
... | no ¬p = dropUntil decide (tail xs) (eventuallyInv ev ¬p)

Answer 1

在您的情况下，您可以使用较弱的 Eventually 概念，它与 dropUntil 实际需要知道的相匹配。它也是单个构造函数，因此即使被擦除也可以匹配它。

  data Eventually' {A} (P : A -> Set) (xs : Stream A) : Set where
    next : (¬ P (head xs) → Eventually' P (tail xs)) → Eventually' P xs

  eventuallyInv : ∀ {A} {P : A → Set} {xs : Stream A} → (ev : Eventually P xs) → Eventually' P xs
  eventuallyInv (here p) = next \ np → ⊥-elim (np p)
  eventuallyInv (there ev) = next \ np → eventuallyInv ev

  dropUntil' : {A : Set} {P : A -> Set} (decide : ∀ x → Dec (P x)) → (xs : Stream A) → @0 Eventually' P xs → Stream A
  dropUntil' decide xs (next ev) with decide (head xs)
  ... | yes prf = xs
  ... | no contra = dropUntil' decide (tail xs) (ev contra)

  dropUntil : {A : Set} {P : A -> Set} (decide : ∀ x → Dec (P x)) → (xs : Stream A) → @0 Eventually P xs → Stream A
  dropUntil decide xs ev = dropUntil' decide xs (eventuallyInv ev)

消除只有一个有效案例的擦除参数

Eliminating erased argument with only one valid case

agda

dependent-type

coinduction