2

我必须通过归纳证明

no f xs ==> null (filter f xs)

在哪里 ：

filter p []    = []
filter p (x:xs) 
  | p x        = x : filter p xs
  | otherwise  = filter p xs

null [] = True; null _ = False 

no p [] = True
no p (x:xs)
  | p x = False
  | otherwise = no p xs

Logic implication:
True ==> False = False
_    ==> _     = True

所以，我认为以下是我的假设和我的主张：

Assumption: no f xs ==> null (filter f xs)
Claim: no f (x:xs) ==> null (filter f (x:xs))

我开始尝试证明基本情况（空列表）：

no f [] ==> null (filter f [])
== {- Filter.1, filter p [] = [] -}
no f [] ==> null ([])
== {- No.1,  no p [] = True-}
True ==> null ([])
== {- Null.1, null [] = True -}
True ==> True

但是我不确定它是否正确，因为我已经证明它们都是 True 而不是如果左边部分是 True 而第二部分是 False，那么暗示是 False （即 ==> 的定义）。这个对吗？我怎样才能继续证明？我不清楚如何使用归纳来证明含义...

先感谢您！

4

1 回答 1

1

这是完整的证明。稍后，当我有更多时间时，我将在 Agda 或 Idris 上证明这一点，并在此处发布代码。

归纳证明xs。

案例xs = []：

no f [] ==> null (filter f [])
== {- Filter.1, filter p [] = [] -}
no f [] ==> null ([])
== {- No.1,  no p [] = True-}
True ==> null ([])
== {- Null.1, null [] = True -}
True ==> True

案例xs = y : ys。假设no f ys == null (filter f ys). 考虑以下情况：

案例f y == True：

no f (y : ys) ==> null (filter f (y : ys))
== {- no - f y == True -}
False ==> null (filter f (y : ys))
== 
True

案例f y == False：

no f (y : ys) ==> null (filter f (y : ys))
=={- By definition of filter and no -}
no f ys ==> null (filter f ys)
== {By I.H.}
True

这完成了证明。

于 2015-12-07T17:09:59.267 回答