Coq入門 - 2.1 - エンジニアですよ！ に追記したが、Lemma le_n_0_eqが証明できた
あと補完が効くようになったらなぜか.を押すだけでC-c C-n相当の部分まで進むようになった。
False_indやFalseの証明の仕方が少しわかった。
しかし、その後も証明ははかどらない。
ムリ
Coqの使い方とかtacticがどうこう、というより単に証明するだけの頭脳が私にないような気がしてきた
もしくは自然数の証明は難しいのではないのか？
そんなことはないか
ペアノの公理は数学ガールで読んだことがあるというくらいの知識はあるんだがｗ
高校でも大学受験でも証明はすごい苦手だったなぁ
さて戻って、証明の続きをしてる。
全然証明進まないし、答え（標準ライブラリのコード）を見ても全然わからないんで飛ばす。
ArithとかImportしてるんで証明は進む。intuitionだけで進むｗ
intuitionだけで進まなくなったle_elim_relを証明してみようと思って取り組んでみる
さっぱりわからーん。
inductionとdestructしか使えるものがないので全然進まない
2日ほど悩んでライブラリを読んでみると、なんだろうね
auto with arithとかやってるので自動で証明できるくらい些細な事なんだろうな。
わからんけどね。
でもelimっていうのもあるので、使ってみたら証明できた。
autoを使っていないところ以外はまるっきりライブラリ通り。
introsで名前を渡すところとか、できる気がしない・・・
introsで名前を特に渡さずにやると、進まなくなる。
具体的には、この部分。
Lemma le_elim_rel : forall P:nat -> nat -> Prop, (forall p, P 0 p) -> (forall p (q:nat), p <= q -> P p q -> P (S p) (S q)) -> forall n m, n <= m -> P n m. intros P H0 HS. induction n; trivial. intros m Le. elim Le. apply HS. intuition. |
2 subgoals, subgoal 1 (ID 97) P : nat -> nat -> Prop H0 : forall p : nat, P 0 p HS : forall p q : nat, p <= q -> P p q -> P (S p) (S q) n : nat IHn : forall m : nat, n <= m -> P n m m : nat Le : S n <= m ============================ P n n |
ここで、名前を付けずに進めていると、 IHn : forall m : nat, n <= m -> P n mこの部分がforall m : natが付いてないものになってしまい、P n nにapplyできなくて進まない。
証明ができない！ こんなときにもgeneralizeしないと進まないことあるよ、みたいに書いてあるからやってみたけどそれでも進まん。
まぁとりあえずintrosするときには名前を付けると何が違うのかと、elimについて学ぼうと思う
ここがとても詳しいので、ここを読む。
