coq-hurry P10 練習問題

10ページの練習問題2問をやってみる
1問目　Exercise on sorting
 Define a function that takes a list as input and returns true when it has less than 2 elements or when the first element is smaller than or equal to the second one. Then define a function that takes a list as input and returns true exactly when this list is sorted.
 入力としてリストをとる関数を定義し、戻り値はリストの要素が２未満か最初の要素が２番目の要素以下のときTrueとなる関数を定義せよ。それからリストが完全にソート済みならTrueとなる関数を定義せよ。

最初、なかなかうまくいかない。
Fixpoint check_fs2 l := match l with nil => true | a::nil => true | a1::a2::tl => if leb a1 a2 then check_fs2 (a2::tl) else false end.
このように一つの関数でできそうな気がしたが、なぜかエラーとなる。まだ、coqの使い方が
よくわかっていない。

こういうときは、少し時間を置くことにしている。しばらくして、再挑戦したらできた。
問題で説明しているように、２つの関数でやってみた。最初の関数は、２つの要素の比較だけ行い、再帰はさせないようにした。もうひとつの関数で再帰を使ったらうまくいった。
もう少しスマートな方法がありそうだが、、、、。

Fixpoint check_fs l := match l with nil => true | a::nil => true | a1::a2::tl => if leb a1 a2 then true else false end.
Fixpoint check_sort l := match l with nil => true | a::tl => if check_fs (a::tl) then check_sort tl else false end.
これで、なんとかうまくいった。

２問目　Exercise on counting
 Knowing that the Coq system provides a function beq_nat to compare two natural numbers,
define a function count_list that takes a natural number and a list and returns the nubmer of times the natural number occurs in the list.

これについては
Fixpoint count_list n l s:= match l with nil => s | a::tl => if beq_nat n a then count_list n tl s+1 else count_list n tl s end.
としてみた。ただ、３つめの引数はムダなので、できればなくしたい。
その方法がよくわからない。

ネットで検索するとすでに、解答されている方がいた。
Fixpoint count_list2 n l:= match l with nil => 0 | a::tl => if beq_nat n a then 1+count_list2 n tl else count_list2 n tl  end.
これでいいようだ。
　nil=>0のところを、nil=>sにしようとこだわりすぎたようだ。自身の戻り値に１をたすならば、戻り値に１が累積されていくということに気づかなかった。自分が考えた引数に１をたしていくやり方だと、最後の関数で表示せざるをえないので、nil=>sとなり、スマートな方法とはいえない。