Pureでどうやって証明する？ 自明に思えるが、やり方が分からない。 typedecl A axiomatization f:: "A ⇒ A" lemma uniq: "x == y ==> f x == f y"

IsabelleやCoqだけを責めることは出来ないな。論理学の用語や概念が曖昧だったんだよな。ものごとをハッキリさせるはずの学問が曖昧な記述で済ませていた。だから、ソフトウェア実装でも曖昧な概念と用語法が引き継がれ、混乱がより悪化した、という事情だろ…

propositin, fact, goal と並べて書いてあるのを見て、ひょっとして、と思った。 propositionとは、真偽の判定を伴わない単なるexpression、つまり論理式のこと factとは、propositionに |- のマークが付いたもの。つまり、判断主張文。 goalとは、propositi…

証明支援系って、ほんとにマダマダ - 檜山正幸のキマイラ飼育記 メモ編 現状がこれでは、先が長くて気が遠くなる。 証明オブジェクトは人間が見ても意味不明（Coq）か、見えない（Isabelle）。 リーズニングの記録としての証明スクリプト（＝タクティクの列…

isar-refのp.46に書いてある話。コンテキストとは、処理系が持っている定理＆ルールのデータベースのことだとする。このコンテキストが見えないことがわかりにくさの大きな原因だ。さらに、コンテキストは入れ子になる。Isarでは、コンテキストを可視化する…

おまえは何を考えているんだ？ 教えてくれ！ - 檜山正幸のキマイラ飼育記 メモ編 apply(assumption) でゴールが解けてしまうことが多いが、具体的な仮定（コンテキストが持っている定理）がどれかワカランことがある。autoだけでなくて、なんかの根拠をつか…