Haskell

Question

我要用归纳法证明

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（即==>) 的定义。这个对吗？我怎样才能继续证明？我不清楚如何使用归纳法来证明蕴涵...

提前致谢！

Answer 1

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

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

证明到此结束。

Haskell - 使用归纳法证明蕴涵

Haskell - Use induction to prove an implication

theorem-proving

implication

induction