2

我定义了无限流如下：

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证明是结构递归参数 in 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)
4

1 回答 1

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)
于 2020-08-04T08:10:56.907 回答