Agda: std-lib: List: 检查过滤后的列表是否为空

Question

我有一个函数filter':

filter' : {A : Set} → (A → Bool) → List A → List A
filter' p []               = l.[]
filter' p (x ∷ xs) with (p x)
...                | true  = x l.∷ filter' p xs
...                | false = filter' p xs

和函数DeleteNat:

DeleteNat : (List ℕ) → ℕ → (List ℕ)
DeleteNat nats id = filter' (λ n → not (n ≡ᵇ id)) nats

其中 _≡ᵇ_ 是：

open import Agda.Builtin.Nat public
  using () renaming (_==_ to _≡ᵇ_)

并想证明在应用 DeleteNat 之后，没有自然数等于 List 中的 id:

DeleteNatRemoveNatWithId :
  (nats : List ℕ) (id : ℕ) →
    filter' (λ n → n ≡ᵇ id) (DeleteNat nats id) ≡ l.[]
DeleteNatRemoveNatWithId []       id         = refl
DeleteNatRemoveNatWithId (x ∷ xs) id with x ≡ᵇ id
...                                  | true  = DeleteNatRemoveNatWithId xs id
...                                  | false = {!  !}

我不确定如何在 {! !} 继续。我有预感应该使用 cong.

来完成

使用C-c C-.我看到我需要满足这种类型：

(filter' (λ n → n ≡ᵇ id) (x List.∷ filter' (λ n → not (n ≡ᵇ id)) xs) | x ≡ᵇ id) ≡ List.[]

我想我需要一种方法以某种方式将 x List.∷ 放入第一个 filter'.

的第二个参数中

我能得到关于如何在此处前进的提示吗？我关于使用 cong 的假设是错误的吗？

Answer 1

filter' ... (x ∷ filter' ... xs) | x ≡ᵇ id)表示评价这个功能卡在了测试x ≡ᵇ id.

要减少它，您通常会使用 with x ≡ᵇ id。但你已经做到了！是的，但是您使用的 with 针对的是 inner filter 当时卡住了。一旦它脱离困境，它的计算足以发出 x ∷ _ 和使外部 filter 卡在第二个测试中（恰好相等到第一个）。

处理这个问题的惯用方法是通过 inspect idiom 这样一来，您不仅可以 with x ≡ᵇ id 的结果，但也证明了结果是由此计算得出的表达。一旦到达外部 filter 卡住的位置，您可以通过这个等式简单地 rewrite 然后你应该能够看到函数计算刚好可以调用归纳假设。

Agda: std-lib: List: 检查过滤后的列表是否为空

Agda: std-lib: List: check that a filtered list is empty

list

agda

agda-stdlib