CODEWITHSUNDEEP
haskelltheorem-provinginductionimplication
Fossa
Fossa

Reputation: 159

Haskell - Use induction to prove an implication

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!

Upvotes: 2

Views: 669

Answers (1)

Rodrigo Ribeiro
Rodrigo Ribeiro

Reputation: 3218

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.

Upvotes: 1

Related Questions