MoreLogic.v 練習問題。all_forallbようやっと、Coqで仕様を記述し、証明する。という本来の目的のモノが出てくる。問題は、「仕様とは何か？」ということが分かってないことだが。とりあえず、allを以下のように書く。これはこれで間違ってはいない・・・と…

Rel.v 反射推移閉包とかこれ何かの役に立つんじゃろか。関係をラップするとか。clos_refl_transとかrefl_step_closureとかまったく意図とか分かってないけど、だいたいこんな感じだろうというレバガチャで証明は出来た。何の役に立つとか、読み進めたら出て…