Haskell - используйте индукцию, чтобы доказать импликацию

Я должен доказать по индукции, что

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

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

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


haskell theorem-proving implication induction
person Fossa    schedule 07.12.2015    source источник
comment
То, что вы сделали в базовом случае, правильно, поскольку ваше значение также является функцией Haskell. Итак, когда вы используете пустой список для xs в базовом случае, это нормально.   -  person Rodrigo Ribeiro    schedule 07.12.2015
comment
Нет необходимости даже проверять no f []. Мы знаем, просто расширяя определения, что null (filter f []) = null [] = True истинно. Вы можете сразу приступить к доказательству индуктивного случая!   -  person hao    schedule 07.12.2015
comment
Если вторая часть - ложь. Вы только что доказали, что вторая часть действительно верна. Следовательно, если вторая часть - Ложь, тогда все вообще Истинно.   -  person n. 1.8e9-where's-my-share m.    schedule 07.12.2015
comment
Достижение True ==> True является правильным доказательством no f [] ==> null (filter f []), потому что некоторое утверждение считается доказанным, если оно эквивалентно True, а True ==> True тривиально True.   -  person user2407038    schedule 07.12.2015

Ответы (1)


arrow_upward
1
arrow_downward

Вот полное доказательство. Позже, когда у меня будет немного больше времени, я докажу это на 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

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

person Rodrigo Ribeiro    schedule 07.12.2015