I've to prove by induction that
no f xs ==> null (filter f xs)
Where :
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
So, I've supposed that the followings are my assumption and my claim:
Assumption: no f xs ==> null (filter f xs)
Claim: no f (x:xs) ==> null (filter f (x:xs))
And I started to try to prove the base case (the empty list):
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
But I'm not sure it is correct, because I've proved that they are both True and not that if the left part is True and the second part is False, then the implication is False (that is the definition of ==>). Is this correct? How can I go on with the proof? I don't clearly get how can I use induction to prove an implication...
Thank you in advance!
Here's the complete proof. Later, when I have a bit more of time, I'll prove this on Agda or Idris and post the code here.
Proof by induction over xs.
Case 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
Case xs = y : ys. Suppose that no f ys == null (filter f ys). Consider the following cases:
Case f y == True:
no f (y : ys) ==> null (filter f (y : ys))
== {- no - f y == True -}
False ==> null (filter f (y : ys))
==
True
Case 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
Which finishes the proof.