≡-Reasoning和“with”模式

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

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-clauses的问题是，它会忘记从模式匹配中学习到的信息，除非您事先安排保留这些信息。

更准确地说，当Agda看到with expression子句时，它会用一个新的变量w替换当前上下文和目标中所有出现的expression，然后将该变量与更新后的上下文和目标一起提供给with -子句，忘记所有关于其起源的信息。

在您的例子中，您在with-块中编写filter p (map f (x ∷ xs))，因此它在Agda执行重写之后进入作用域，因此Agda已经忘记了p (f x)是true并且不会减少术语的事实。

您可以通过使用标准库中的一个“检查”-patterns来保存相等的证明，但我不确定它在您的情况下如何有用。