≡-Reasoning và 'with' patterns

Question

Tôi đã chứng minh một số thuộc tính của filter và map, mọi thứ diễn ra khá tốt cho đến khi tôi tình cờ gặp tài sản này: filter p (map f xs) ≡ map f (filter (p ∘ f) xs). Dưới đây là một phần của mã có liên quan:

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 

Bây giờ, vì tôi yêu văn bản chứng minh việc sử dụng mô-đun ≡-Reasoning, điều đầu tiên tôi đã cố gắng là:

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

Nhưng than ôi, điều đó không làm việc . Sau khi thử trong một giờ, cuối cùng tôi đã từ bỏ và chứng minh nó theo cách này:

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 

Tuy nhiên tò mò về lý do tại sao trải qua ≡-Reasoning đã không làm việc, tôi đã cố gắng một cái gì đó rất tầm thường:

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

Nhưng typechecker không đồng ý với tôi. Dường như mục tiêu hiện tại vẫn là filter p (f x ∷ map f xs) | p (f x) và mặc dù tôi đã khớp với mẫu trên p (f x), filter sẽ không giảm xuống f x ∷ filter p (map f xs).

Có cách nào để thực hiện công việc này với ≡-Reasoning không?

Cảm ơn!

Answer 1

Sự cố với with -như là Agda quên thông tin mà nó đã học được từ kết hợp mẫu trừ khi bạn sắp xếp trước để thông tin này được giữ nguyên.

Chính xác hơn, khi Agda thấy mệnh đề with expression, nó thay thế tất cả các lần xuất hiện của expression trong ngữ cảnh và mục tiêu hiện tại bằng biến mới w và sau đó cung cấp cho bạn biến đó với ngữ cảnh và mục tiêu được cập nhật mọi thứ về nguồn gốc của nó.

Trong trường hợp của bạn, bạn viết filter p (map f (x ∷ xs)) bên trong khối, do đó, nó đi vào phạm vi sau khi Agda đã thực hiện viết lại, vì vậy Agda đã quên thực tế là p (f x) là true và không giảm thời hạn.

Bạn có thể lưu giữ bằng chứng bình đẳng bằng cách sử dụng một trong các mẫu "Kiểm tra" từ thư viện chuẩn, nhưng tôi không chắc cách nó có thể hữu ích trong trường hợp của bạn.