≡推論と 'with'パターン

Question

私はfilterとmapといういくつかのプロパティを証明していましたが、このプロパティを見つけ出すまではすべてがうまくいっていました：filter p (map f xs) ≡ map f (filter (p ∘ f) xs)。ここでは、関連のコードの一部です：私は≡-Reasoningモジュールを使用して書い証明を愛しているから

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 

は、今、私が試した最初のものでした：

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) 
-- ... 

しかし残念ながら、動作しませんでしたこと。一時間のためにしようとした後、私は最終的にあきらめ、この方法でそれを証明した：≡-Reasoningを介さが機能しなかった理由について

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 

それでも好奇心、私は非常に些細な何かを試してみました：

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)に一致するパターンであっても、filterはf x ∷ filter p (map f xs)に縮小されません。

≡-Reasoningでこの方法を使用する方法はありますか？

ありがとうございます！

Answer 1

withの悩みは、この情報が保存されることを事前にアレンジしていない限り、パターンマッチで学んだ情報を忘れるということです。

はより正確には、Agdaはwith expression句を見たとき、それは新鮮な変数wと、現在のコンテキスト、ゴールにexpressionのすべての出現箇所を置換した後、忘れる、と、句の中にあなたの更新状況や目標とその変数を与えますその起源についてのすべて。あなたのケースでは

は、あなたが内側にfilter p (map f (x ∷ xs))を書くと、ブロック、Agdaはすでにp (f x)がtrueで、用語を低下させないという事実を忘れているようAgdaは、書き換えを行った後に、それはスコープに入るようにします。

あなたは標準ライブラリから「点検」-patternsのいずれかを使用して、平等の証拠を保存することができますが、私はそれはあなたの場合に有用であることができるかどうかはわかりません。