Haskell - Use induction to prove an implication

Question

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!

What you've done on the base case is correct, since your "implication" is also a Haskell function. So, when you use the empty list for xs in the base case, that's ok. — Rodrigo Ribeiro
It's unnecessary to even examine no f []. We know, just by expanding the definitions, that null (filter f []) = null [] = True is True. You can proceed immediately to proving your inductive case! — hao
"If the second part is False". You've just proved that the second part is in fact True. Therefore if the second part is False, then anything at all is True. — n. 1.8e9-where's-my-share m.
Arriving at True ==> True is a correct proof of no f [] ==> null (filter f []) because some statement is said to be proved if it is equivalent to True and True ==> True is trivially True. — user2407038

Rodrigo Ribeiro Rodrigo Ribeiro · Accepted Answer · 2015-12-07T17:09:59

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.

Haskell - Use induction to prove an implication

1 Answers