■

#coq
去年末、スマリヤンのコンビネータ論理を使ったパズル本を手に入れて、これcoqで出来るんかもかもと試してみた。

出来んかった・・・

本の回答だと、

   forall x : Bird,
   exists C : Bird, bird_respond C x = bird_respond A (bird_respond M x)

で xにCを代入出来るはずなんだが・・・

coqで出来ないのは、

1. 単に私の定義が悪い。
2. 私の証明の進めかたが悪い。
3. そもそもcoqで出来るくらい形式化されてねーよ。
4. 本の回答が循環論法で無効。

のいずれかですが、3と4は考えにくい。ような気もする。

最初、以下のように書いてた。

Theorem any_bird_loves_one :
(exists C : Bird , forall A B x : Bird, 
bird_respond C x = bird_respond A (bird_respond B x)) ->
(exists M : Bird, forall x : Bird, bird_respond M x = bird_respond x x) ->
 
forall A : Bird, exists B : Bird,B = bird_respond A B. 

これだと簡単に証明は終るんだけど、
「任意の鳥AとB(同じであっても異なっていてもよい)に対して、任意の鳥xをとれば、Cx = A(Bx)であるような鳥Cがいる。」
という条件とは違うような気がするし。

こんなふうに定義すればよいかもというのも、かなりテキトーであるので、定義からして間違ってる可能性は高いが、どんなふうに間違ってるのかも分からない。

本はこれだ。
数学パズル ものまね鳥をまねる POD版 ―愉快なパズルと結合子論理の夢の鳥物語
残り一冊でラッキーだった。