Coq

Coq演習をやってみて、やはりあんまり自分が理解してない。ということが分かった。
とくに、

• 命題とブール値の違い

命題とブール値は、一見とてもよく似ているように見えます。しかしこの二つは根本的に違うものです！

・ブール値は、「計算の世界における値」です。 bool 型の式は全て、（自由変数を持っていない限り）
必ず true か false のどちらかに簡約することができます。
・命題は「論理の世界における型」です。
これらは「証明可能（この型の式を書くことができる）」か、「証明不能（そのような式は存在しない）」か
のいずれかです。従って「命題が true である」というような言い方は意味を持ちません。

我々は時折、命題に対してそれが "true" か "false" というようなことを言ってしまいがちですが、
厳格に言えばこれは間違っています。命題は「証明可能かそうでないか」のどちらかです。

Software Foundationより

• =とか、<が 関係を表す命題であること
• exists x : A, ... という命題の証明の仕方。
• そもそもinversionて何するもんなんだろう
• 命題に対して帰納法を適用するって？

などなど