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)) 

И я начал пытаться доказать, базовый вариант (пустой список):

Но я не уверен, что это правильно, потому что я доказал, что они оба являются Истинными, а не то, что если левая часть является Истиной, а вторая - False, то импликация False (то есть определение ==>). Это правильно? Как я могу продолжить доказательство? Я не понимаю, как я могу использовать индукцию для доказательства импликации ...

Спасибо заранее!

Answer 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 

Case 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 

что завершает доказательство.