≡-Рассуждение и «с» узорами

Question

Я проверял некоторые свойства 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) 
-- ... 

Но, увы, это не сработало , После попытки в течение одного часа, я, наконец, сдался и доказал это таким образом:

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

Но typechecker не согласен со мной. Казалось бы, текущая цель остается 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 забывает информацию, полученную им из шаблона, если вы заранее не забронируете эту информацию для сохранения.

Более точно, когда Agda видит положение with expression, он заменяет все вхождения expression в текущем контексте и целях с новым переменной w, а затем дает этому переменный с обновленным контекстом и целями в с-п, забывая все о его происхождении.

В вашем случае, вы пишете filter p (map f (x ∷ xs)) внутри с-блок, поэтому он переходит в сферу после Agda выполнила перезапись, так Agda уже забыла о том, что p (f x) является true и не уменьшает срок.

Вы можете сохранить доказательство равенства, используя один из шаблонов «Inspect» из стандартной библиотеки, но я не уверен, как это может быть полезно в вашем случае.