Coq

短いRel_J.vを読んだ。
証明自体はそう難しいものは無いけれど、ほとんどサールの中国人の部屋状態。規則に従って何かを生成しているが、それが何を意味するのかほとんど分かっておりませぬ。

まとめ

• 関係Rが反射的とは、Xの任意の要素 xについて R x xが成立することです。
• 関係Rが推移的(transitive)であるとは、R a bかつR b cならば常にR a c となることです。
• 関係Rが対称的(symmetric)であるとは、R a bならばR b aとなることです。
• 関係Rが反対称的(antisymmetric)であるとは、R a bかつR b aならば a = b となることです。
• 関係が同値関係(equivalence)であるとは、その関係が、 反射的、対称的、かつ推移的であることです。
• 関係が半順序(partial order)であるとは、その関係が、 反射的、反対称的、かつ推移的であることです。
  • Coq 標準ライブラリでは、半順序のことを単に"順序(order)"と呼びます。
• 前順序(preorder)とは、半順序の条件から反対称性を除いたものです。

• 関係Rの反射推移閉包とは、Rを含み反射性と推移性の両者を満たす最小の関係のことです。

Inductive refl_step_closure {X:Type} (R: relation X)
                            : X -> X -> Prop :=
  | rsc_refl : forall (x : X),
                 refl_step_closure R x x
  | rsc_step : forall (x y z : X),
                    R x y ->
                    refl_step_closure R y z ->
                    refl_step_closure R x z.

あと、SfLib_J.vも。ところどころAdmittedになってるのでもっかい証明しなおすことで復習になった。
そこで、n <= m のような命題に対してnの帰納法を適用するときに、nとmは対称でないので

intros n.
induction n.
Case "n = 0".
  induction m...

とすることと

intros n m.
generalize dependent n.
induction m.
Case "m = 0".
  induction n...

とすることに違いが出るということに気がつきました。少しは理解が進んでると考えていいのだろうか…
あとSfLibに自然数に関する定理がほとんどないということは、これから算数的な話はあんまり出てこないんだろうね・・・

---

13週が過ぎようとしている。前半の山は越えたか。