如何解决Agda: std-lib: List: 检查过滤列表是否为空
我有一个函数 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
的假设是错误的吗?
解决方法
filter' ... (x ∷ filter' ... xs) | x ≡ᵇ id)
表示对
此函数卡在测试 x ≡ᵇ id
上。
要减少它,您通常会使用 with x ≡ᵇ id
。但你已经
做到了!是的,但是您使用的 with
针对的是 inner filter
当时卡住了。一旦它解开,它的计算足以发出 x ∷ _
和
使外部 filter
卡在第二个测试中(恰好等于
到第一个)。
解决这个问题的惯用方法是通过 inspect
idiom
这将使您能够在一个 with
中不仅获得
x ≡ᵇ id
的结果,但也证明了结果是从这个计算出来的
表达。一旦到达外部 filter
卡住的点,您
可以通过这个方程简单地rewrite
,然后你应该能够看到
该函数计算刚好可以调用
归纳假设。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。