自己鳥

鳥xは自分自身が好きであれば、すなわちxのxへの応答がxであれば、自己中心的と呼ばれる。
記号的には、xx = x である。

結合条件とものまね鳥がいる条件のもとで、少なくとも一羽の鳥は自己中心的であることを示せ。coqで。

とりあえず。

Theorem there_is_egocentric_bird :
exists E : Bird, E = bird_respond E E.
assert(H: forall A : Bird, exists B : Bird, B = bird_respond A B).
apply any_bird_is_fond_of_least_one_bird.
destruct there_is_mockingbird as [M].
assert(HM: exists B: Bird, B = bird_respond M B).
apply H.
destruct HM as [B].
assert(HMB: bird_respond B B = bird_respond M B).
apply H0. 
exists B.  rewrite HMB. apply H1.
Qed.

何故

Axiom bird_composition :
forall A B : Bird, 
exists C : Bird,
forall x : Bird,
bird_respond C x = bird_respond A (bird_respond B x).

Axiom there_is_mockingbird :
exists M, forall x, bird_respond x x = bird_respond M x.


Theorem there_is_egocentric_bird2 :
bird_composition -> there_is_mockingbird ->
exists E : Bird, E = bird_respond E E.

と書くことが出来ないのか？

• >の左側には、Prop or Setでないと駄目とか言われる。

Definition bird_compsition : Prop :=
forall A B : Bird, 
exists C : Bird,
forall x : Bird,
bird_respond C x = bird_respond A (bird_respond B x).

であればいいのかな？未確認であるが。
今確認した。いけそーだな。
しかしその場合は、いちいちunfold しなきゃならんのか。めんどいな。