13

我正在证明 和 的一些性质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？

谢谢！

4

1 回答 1

6

-clauses的问题with在于 Agda 会忘记它从模式匹配中学到的信息，除非您事先安排好保留这些信息。

更准确地说，当 Agda 看到一个with expression子句时，它会将expression当前上下文和目标中w所有出现的

在您的情况下，您filter p (map f (x ∷ xs))在 with-block 内写入，因此在 Agda 执行重写后它进入范围，因此 Agda 已经忘记了这个事实p (f x)并且true不会减少该术语。

您可以使用标准库中的“检查”模式之一来保留相等性证明，但我不确定它在您的情况下如何有用。

于 2012-04-30T15:17:55.987 回答