Coq入門 - 2

coq

こういうのをやることにした。

ただCoqの標準ライブラリからLemmaとTheoremを取り出してきただけ。

こんな初歩的なものなら簡単に証明できるだろ＼(^o^)／

と思っていたら、いきなりできない・・・ｗ

Lemma le_n_0_eq n : n <= 0 -> 0 = n.

こんな当たり前そうなものすら証明できない。

つらい・・・

こうなるじゃろ？

  Lemma le_n_0_eq n : n <= 0 -> 0 = n.
  intros.
  symmetry.
 
1 subgoals, subgoal 1 (ID 7)
  
  n : nat
  H : n <= 0
  ============================
   n = 0

で、induction nで行けると思うじゃろ？

こうなるじゃろ？

Lemma le_n_0_eq n : n <= 0 -> 0 = n.
  intros.
  symmetry.

  induction n.
  reflexivity.
 
1 subgoals, subgoal 1 (ID 18)
  
  n : nat
  H : S n <= 0
  IHn : n <= 0 -> n = 0
  ============================
   S n = 0
 
S n = 0

なんておかしい！こりゃ矛盾じゃ(´ω｀)

簡単じゃの(´ω｀)

・・・

・・・

・・・

・・・

で、できない(；´Д｀)

わからぬ・・・(；´Д｀)

基本がわからぬ・・・・(；´Д｀)

apply False_indしてみたところで、示せぬ・・・

ぐぬぬ・・・

とりあえずinductionしてみるけど、示し方が分からない。。。。

Lemma le_n_0_eq n : n <= 0 -> 0 = n.
  intros.
  symmetry.

  induction n.
  reflexivity.

  apply False_ind.
  induction n.

2 subgoals, subgoal 1 (ID 28)
  
  H : 1 <= 0
  IHn : 0 <= 0 -> 0 = 0
  ============================
   False

subgoal 2 (ID 34) is:
 False

分からない・・・

粘ったけど分からない・・・・

うぅ。。

仕方なくCoq本体見てみるも、証明が鮮やかだったり色んな他の補題や定理を使って証明しているのであまり練習にならない。。

むむむ・・・・

出直す・・・