仅用一个有效案例消除已删除的参数答案

【问题标题】：Eliminating erased argument with only one valid case仅用一个有效案例消除已删除的参数
【发布时间】：2020-07-28 10:12:24
【问题描述】：

我已经定义了无限流如下：

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，因此根据最终定义，流尾部的某些元素必须满足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)

【问题讨论】：

我很难理解为什么你的函数不应该在计算上依赖于证明，因为它包含了你编写函数所需的信息。
Eventually 证明指定 is 元素满足谓词，但不一定找到 第一个元素 - 而 dropUntil 应该停止在满足谓词的第一个元素处。因此，无论如何我都需要在每个元素上调用decide，因此检查Eventually 是多余的，因此可以删除。
关于流的Eventually 谓词的想法大致取自这篇论文：hal.inria.fr/inria-00070658/document，这可能比我更好地证明了它的使用。
我删除了我的答案，因为我似乎遗漏了您的要求。
澄清一下，流必须保持共导，如下所述：agda.readthedocs.io/en/v2.6.1/language/coinduction.html（最好采用“新式”共导）

标签： agda dependent-type coinduction

【解决方案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)

【讨论】：