2007/11/10

Transitivity

scm 老師把 MSS 寫到剩兩個 lemma(實在太強了!),讓我們練習證明。我證了一下讓 program check,很高興就廣播出去,然後很快就後悔了 XD。因為第一個 lemma 的證明我用窮舉法,但因為 less-than 有 transitivity 而漏掉兩個不可能發生的 cases。這樣程式就有瑕疵,因為形式上那個 lemma 只是 partially correct(可是 Agda 對此從不抱怨)。真的要做應該還是得證明整數的 transitivity,可是很麻煩 XD。

--
凡事三思而後行 XD。


整個狀況想一想實在很詭異 XD。


現在 scm 老師把整個結果發佈在他的 blog 上啦!

Labels: