伊莎貝爾：舉證責任 - 證明使用的反

對於這樣一個例子引理：這給使用時，下列快速檢查伊莎貝爾：舉證責任 - 證明使用的反

lemma someFuncLemma: "∀ (e::someType) . pre_someFunc 2 e"

：

Auto Quickcheck found a counterexample: 
    e = - 1

或使用雞蛋裏挑骨頭（這是不是真的，當這裏的要點）：

Nitpick found a counterexample: 

    Skolem constant: 
    e = - 1

那我該如何用這個反例來完成證明呢？

正如你所看到的，我對伊莎貝爾和採購訂單不是很熟悉。

謝謝你的幫助！

來源

2016-01-16 MooMooCoding

一個反例的存在通常表明你將不能夠證明自己的主張，也許除了

的反例是虛假的;
底層邏輯不一致。

來源

2016-01-17 07:56:18

或者存在挑剔/快速檢查的錯誤。來自nitpick/quickcheck的反例不會通過Isabelle內核，即僅僅因爲nitpick/quickcheck告訴你一些反例，你不會自動得到一個Isabelle定理，它確實是一個例子。如果你想要的話，你必須自己證明。（在大多數情況下，可以通過簡單的重寫來實現） –

我假設你想證明存在一些e這樣pre_someFunc 2 e是假的。你將不得不改變你的引理使用存在而不是FORALL，並與前綴您的謂語不：

lemma "∃e::someType. ¬(pre_someFunc 2 e)"

然後您就能夠使用rule exI[where x=...]的反例，其設置自由變量x在exI的東西。你可以看看exI的定義以及如何使用x，方法是在Isabelle JEdit中按住Ctrl。

一個簡單的例子：

lemma "∃n :: nat. ¬ odd n" 
apply (rule exI[where x=2]) 
apply simp 
done

來源

2016-05-14 14:21:07 Shou

伊莎貝爾：舉證責任 - 證明使用的反

回答

相關問題