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証明が の構造的に再帰的な引数で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 に答える