Re-Rozumowanie i wzory "z"

Question

Udowodniłem pewne właściwości filter i map, wszystko poszło całkiem nieźle, dopóki nie natknąłem się na tę właściwość: filter p (map f xs) ≡ map f (filter (p ∘ f) xs). Oto część kodu, który jest istotny:

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 

teraz, bo kocham pisanie dowodów za pomocą modułu ≡-Reasoning, pierwszą rzeczą próbowałem było:

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

Ale niestety, że nie działa . Po wypróbowaniu przez jedną godzinę, ale w końcu poddał się i okazało się to w ten sposób:

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 

Nadal ciekawi dlaczego przeżywa ≡-Reasoning nie działa, próbowałem coś bardzo trywialny:

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

Ale typechecker nie zgadza się ze mną. Wydaje się, że obecny cel pozostaje filter p (f x ∷ map f xs) | p (f x) i mimo że pasuję do wzoru p (f x), filter po prostu nie zmniejszy się do f x ∷ filter p (map f xs).

Czy istnieje sposób, aby to zadziałało z ≡-Reasoning?

Dzięki!

Answer 1

Kłopot z with - przyczynami jest to, że Agda zapomina informacji, których nauczyła się na podstawie dopasowania do wzorca, chyba że wcześniej umówiono się na zachowanie tych informacji.

Dokładniej, gdy Agda widzi with expression klauzuli, to zastępuje wszystkie wystąpień expression w bieżącym kontekście i celu ze świeżym zmiennej w a następnie daje taką zmienną ze zaktualizowanym kontekst i cel do z-klauzuli, zapominając wszystko o jego pochodzeniu.

W twoim przypadku, piszesz filter p (map f (x ∷ xs)) wewnątrz z bloku, więc idzie do zakresu po Agda występował przepisanie, więc Agda już zapomniany fakt p (f x) jest true i nie zmniejsza termin.

Możesz zachować dowód równości za pomocą jednej z rycin "Sprawdź" ze standardowej biblioteki, ale nie jestem pewien, w jaki sposób może być przydatny w twoim przypadku.