定理証明支援 Coqで遊ぶぞ

1. はじめに
2. ここを読む人
3. ダウンロードとインストール
4. Coqで証明
   
   1. まずはいじってみる
   2. ちょっと証明を
   3. 型のないλ式
   4. 型付きλ式
   5. 型付きλ式から証明を読み取ってみる
   6. CoqIdeを使ってみる
   7. いくつかのtacticについて
5. 証明の実際
6. 論理
   
   1. Intui.v 排中律なしで成立する恒真式など
7. 形式的集合論
   
   1. Nota.v 記号の定義など
   2. a0Seteq.v 集合の相等
   3. a1Axset.v 集合論の公理
   4. a2Seteq2.v
   5. a3Emp01.v 空集合
   6. a4Pair01.v 対集合
8. とりあえず、解説なしで。もともと、排中律を証明するつもりで始めたわけではないので、排中律の証明には必要のない定理もたくさん記述されています。 また、他のファイルから証明をもらったりしているので、自分で見ても明らかに遠回りになっているところがあります。
   7. a5Sum01.v
   8. a6Pow01.v
   9. a7Rep01.v
   10. a8Relf01.v
   11. a8Relf02.v
   12. a8Relf03.v
   13. a9Func01.v
   14. a9Func02.v
   15. a9Func03.v
   16. a9Func04.v
   17. a9Func05.v
   18. a+0ac201.vここで、排中律が証明されています。選択公理から証明する定理と、基礎の公理から証明する定理の2種類あります。
9. a+0acsh.v（所々証明図）排中律の証明だけを、1つのファイルにまとめました。このファイル以外のファイルは参照せずに証明が終わります。但し、集合論の公理としては
   • Set_eq　集合が等しいことを定義する公理。
   • PrEmp　空集合の存在公理。但し、空集合記号を使用。
   • SPairf　対集合の存在公理。但し、対集合を表す2変数関数記号を使用。
   • SComf　分出集合の存在公理。但し、分出集合を表す2変数関数記号を使用。
   • ACf　選択公理。但し、選択関数を用いた表現の公理。
   • SReg　基礎の公理。
   を用いました。集合論の公理として、関数記号を用いた表現のものを採用すると、証明までの道筋が短くなったので、1つのファイルにまとめる気になりました。意外だったのは、Intui.vを参照していないことです。Coqに慣れると、そのような定理は証明する必要がなくなるみたいです。
10. ほにゃらら

工事中

TOP