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 

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

Заранее спасибо!

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 

случай 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

Который заканчивает доказательство.