哈斯克爾 - 用歸納法證明的暗示

我已經通過歸納證明哈斯克爾 - 用歸納法證明的暗示

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

但我不確定它是否正確，因爲我已經證明它們都是正確的，而不是如果左邊的部分是真的，第二部分是假的，那麼含義是假的（即==>的定義）。這是正確的嗎？如何繼續證明？我不清楚如何使用感應來證明暗示...

謝謝您提前！

來源

2015-12-07 Fossa

你在基本情況下做了什麼是正確的，因爲你的「含義」也是一個Haskell函數。因此，當您在基本情況下使用xs的空列表時，沒關係。 –

甚至不需要檢查'no f []'。我們知道，只要擴展定義，null（filter f []）= null [] = True'就是True。您可以立即開始證明您的歸納案例！ – hao

「如果第二部分是假的」。你剛剛證明第二部分其實是真的。因此，如果第二部分是假的，那麼任何事情都是真的。 –

下面是完整的證明。後來，當我有更多時間時，我會在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

其中完成證明。

來源

2015-12-07 17:09:59

這個證明是完美和清晰的！謝謝！ – Fossa

哈斯克爾 - 用歸納法證明的暗示

回答

相關問題