エンジニアですよ!

頑張れ俺くん、巨匠と呼ばれるその日まで

Coq入門 - 3

Coq入門 - 2.1 - エンジニアですよ! に追記したが、Lemma le_n_0_eqが証明できた

あと補完が効くようになったらなぜか.を押すだけでC-c C-n相当の部分まで進むようになった。

False_indFalseの証明の仕方が少しわかった。

しかし、その後も証明ははかどらない。

ムリ

Coqの使い方とかtacticがどうこう、というより単に証明するだけの頭脳が私にないような気がしてきた

もしくは自然数の証明は難しいのではないのか?

そんなことはないか

ペアノの公理数学ガールで読んだことがあるというくらいの知識はあるんだがw

高校でも大学受験でも証明はすごい苦手だったなぁ

さて戻って、証明の続きをしてる。

全然証明進まないし、答え(標準ライブラリのコード)を見ても全然わからないんで飛ばす。

ArithとかImportしてるんで証明は進む。intuitionだけで進むw

intuitionだけで進まなくなったle_elim_relを証明してみようと思って取り組んでみる

さっぱりわからーん。

inductiondestructしか使えるものがないので全然進まない

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 napplyできなくて進まない。

証明ができない! こんなときにもgeneralizeしないと進まないことあるよ、みたいに書いてあるからやってみたけどそれでも進まん。

まぁとりあえずintrosするときには名前を付けると何が違うのかと、elimについて学ぼうと思う

Coq タクティクリファレンス: 帰納法と場合分け

ここがとても詳しいので、ここを読む。