13

と のいくつかのプロパティを証明していましたが、このプロパティに出くわすfilterまでmap、すべてがうまくいきました: filter p (map f xs) ≡ map f (filter (p ∘ f) xs)。関連するコードの一部を次に示します。

open import Relation.Binary.PropositionalEquality
open import Data.Bool
open import Data.List hiding (filter)

import Level

filter : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
filter _ [] = []
filter p (x ∷ xs) with p x
... | true  = x ∷ filter p xs
... | false = filter p xs

≡-Reasoningさて、モジュールを使って証明を書くのが大好きなので、最初に試したことは次のとおりです。

open ≡-Reasoning
open import Function

filter-map : ∀ {a b} {A : Set a} {B : Set b}
             (xs : List A) (f : A → B) (p : B → Bool) →
             filter p (map f xs) ≡ map f (filter (p ∘ f) xs)
filter-map []       _ _ = refl
filter-map (x ∷ xs) f p with p (f x)
... | true = begin
  filter p (map f (x ∷ xs))
    ≡⟨ refl ⟩
  f x ∷ filter p (map f xs)
--  ...

しかし、残念ながら、それはうまくいきませんでした。1時間試した後、最終的にあきらめて、次のように証明しました。

filter-map (x ∷ xs) f p with p (f x)
... | true  = cong (λ a → f x ∷ a) (filter-map xs f p)
... | false = filter-map xs f p

≡-Reasoningなぜ通り抜けることがうまくいかなかったのかまだ興味があるので、私は非常に些細なことを試しました：

filter-map-def : ∀ {a b} {A : Set a} {B : Set b}
                 (x : A) xs (f : A → B) (p : B → Bool) → T (p (f x)) →
                 filter p (map f (x ∷ xs)) ≡ f x ∷ filter p (map f xs)
filter-map-def x xs f p _  with p (f x)
filter-map-def x xs f p () | false
filter-map-def x xs f p _  | true = -- not writing refl on purpose
  begin
    filter p (map f (x ∷ xs))
  ≡⟨ refl ⟩
    f x ∷ filter p (map f xs)
  ∎

しかし、タイプチェッカーは私に同意しません。現在の目標は残っているように見えます.でfilter p (f x ∷ map f xs) | p (f x)パターンマッチしたとしても.p (f x)filterf x ∷ filter p (map f xs)

これを機能させる方法はあり≡-Reasoningますか？

ありがとう！

4

1 に答える 1

6

with-clausesの問題点は、Agda がパターン マッチから学習した情報を忘れてしまうことです。この情報が保持されるように事前に手配しない限り、この情報は保持されません。

より正確には、Agda が句を検出すると、現在のコンテキストとゴールでのwith expressionすべての発生を新しい変数に置き換え、更新されたコンテキストとゴールを使用してその変数を with 句に渡し、その起源に関するすべてを忘れます。expressionw

あなたの場合、filter p (map f (x ∷ xs))with-block 内に書き込むため、Agda が書き換えを実行した後にスコープに入るため、Agda はその事実をすでに忘れておりp (f x)、true用語を削減していません。

標準ライブラリの「検査」パターンの 1 つを使用することで、同等性の証明を保持できますが、それがどのように役立つかはわかりません。

于 2012-04-30T15:17:55.987 に答える