直観主義

直観主義

古典論理から排中律を除いた論理は、普通「直観主義論理」と呼ばれているので、ここの表題を上記のようにしました。それだけですので、直観主義論理に関する詳しい説明をここでする気は毛頭ありません。

Intui.v：排中律なしで成立する恒真式などを証明するテキストファイル。
Intui.vo：上記ファイルをコンパイルしたもの。

ここを最初に作ってから、随分時間がたちました。今から見ると、そんなやり方で証明しなくていいのに、と思うようなところも随分ありますが、全部直すとなるとまた時間がかかるので、ここはそのまま使いたいと思います。

表記について

(*...*)はコメント行である。つまり自由に説明などが記述できる。
「A <-> B」は「iff A B」の略記であり、「iff A B」は「(A -> B) /\ (B -> A)」で定義されている。
「~ A」は「Aの否定」のことですが、Coqでは「A -> False」の略記です。Falseは定項です。意味は「成立しない命題」と思っておけば大丈夫です。とりあえずはFalseの定義は気にしなくてもいいと思います。

論理式の読み方の補足

A -> Bなる論理式は、論理式Aを仮定すれば論理式Bが成立するという意味にとることができますが、では仮定を増やして、論理式A,B,Cを仮定すれば、論理式Dが成立するという意味に取れる論理式はどのような論理式でしょうか。ひとつは「かつ」の意味を持つ「/\」を使った(A /\ B /\ C) -> Dというのがあります。が、「->」のみを使ったA -> B -> C -> Dもその意味にとることができます。なぜなら、（A -> B -> C -> DはA -> (B -> (C -> D))の略記であることに注意して）

A -> B -> C -> D	A
B -> C -> D		B
C -> D			C
D

のように、A -> B -> C -> Dがあれば、A,B,CからDを導くことができるからです。

Intui.vの内容の解説

上の方にあるIntui.vをダウンロードして、CoqIdeに読み込ませて Navigation→Forwardで前に進んだり、Navigation→Backwardで戻ったりしながら解説を読んだ方がいいと思います。

------------------------------------------------------------------------
(*三段論法*)
Theorem Syllog : forall A B C:Prop, (A -> B) -> (B -> C) -> (A -> C).
Proof.
intros A B C H H0 H1.
apply H0.
apply H.
assumption.
Qed.
・Syllogの解説
この定理は

A -> B	B -> C
A -> C

を正当化します。
------------------------------------------------------------------------

(*三段論法同値*)
Theorem Syllogeq : forall A B C:Prop, (A <-> B) -> (B <-> C) -> (A <-> C).
Proof.
intros A B C AB BC.
elim AB; intros ABa ABb.
elim BC; intros BCb BCc.
split; apply Syllog with B; assumption.
Qed.
・Syllogeqの解説
記号「;」は複数の命令を一度に実行させるときの区切り記号として使います。
elim AB; intros ABa ABb.は、仮定のAB : A <-> Bを、ABa : A -> Bと ABb : B -> Aに分けています。
それはここでもやりました。
次にsplit; apply Syllog with B; assumption.ですが、ここで記号「;」を使わない場合、証明がどうなるか次に示します。

Proof.
intros A B C AB BC.
elim AB; intros ABa ABb.
elim BC; intros BCb BCc.
split.
apply Syllog with B.
assumption.
assumption.
apply Syllog with B.
assumption.
assumption.
Qed.

Proof.の後、3行は先程と同じです。次ですが、記号「;」を使ったときは
split; apply Syllog with B; assumption.
の1行しかなかったのが、記号「;」を使わない場合、split.命令からQed.の前までの7行にもなっています。実は記号「;」を使った場合、記号「;」直前の命令で生成されたsubgoalの全てに対して記号「;」直後の命令が適用されるのです。

では、apply Syllog with B.命令の説明に入りましょう。これはapply Syllog.命令にwith Bという補足をつけたものです。まず、apply Syllog with B.命令の適用直前のsubgoalを見てください。一番上のものは

　　　　　A -> C

になっていると思います。これはたしかにSyllog（ファイルの最初に証明されている定理）のhead typeになっています。ですから、apply Syllog.命令を適用できるはずですが、ちょっと注意があります。ここで説明の都合上、次なるSyllog0を考えます。

　　　　　Syllog0 : forall D E F:Prop, (D -> E) -> (E -> F) -> (D -> F)

これは、Syllogの束縛変数を変えただけのものなので、これで考えても上記１．は head typeになります。つまり（Syllog0が存在するとして） apply Syllog0.命令を適用できるはずです。でも良く考えてください。apply Syllog0.命令を適用する場合、Coqとしては DとしてA、FとしてCを採用すればよいとわかっても、Eをどうすればいいかわかりません。こういう時も、Coqはエラーを返してよこします。そうならないように、EとしてBを採用するよう、指定してやればいいのですが、それには

　　　　　apply Syllog0 with (E := B).

とするのです。これをもとのSyllogで考えるならapply Syllog with (B := B).となりますが、これはapply Syllog with B.と省略できるのです。

ついでですので、withを使わない方法も紹介しましょう。実は、上記のapply Syllog with B.のかわりに、

　　　　　apply (Syllog A B).

としてもうまくいくのです。説明します。まず、Syllogの型を見ましょう。

　　　　　Syllog : forall A B C:Prop, (A -> B) -> (B -> C) -> (A -> C).
　　　　　Syllog : ΠA:Prop. ΠB:Prop. ΠC:Prop. (A -> B) -> (B -> C) -> (A -> C).

上記６．は、ｆｏｒａｌｌの部分をλ式の普通の書き方に戻したものです。さて、型を見ると、「型付きλ式の２．のイメージ」のところで説明したように、Syllogは第1，2，3引数として、Prop型のλ式をとることがわかります。ここで、A,B,D,E,FをProp型を持つλ式とすると、「型付きλ式の３．のイメージ」で説明したように、

　　　　　Syllog D E : forall C:Prop, (D -> E) -> (E -> C) -> (D -> C).
　　　　　Syllog D E F : (D -> E) -> (E -> F) -> (D -> F).
　　　　　Syllog A B : forall C:Prop, (A -> B) -> (B -> C) -> (A -> C).

などのようになります。上記の９．なら、head typeとして１．を持つので、 apply命令を適用できます。つまり、apply (Syllog A B).が実行できるわけです。この場合は、forall CのCとして、Cを採用すればよいという判断はCoqには容易にできます。（下記のAndABABの証明でも、このwithを使用しない方法がとられています。）
------------------------------------------------------------------------

(*2重否定の導入*)
Theorem InDN : forall A:Prop, A -> ~ ~ A.
Proof.
intros A H H0.
elim H0.
assumption.
Qed.
特に解説はありません。

------------------------------------------------------------------------
(*Andの除去　左を残す*)
Theorem Andell : forall A B:Prop, A /\ B -> A.
Proof.
intros A B H.
elim H; intros a b.
assumption.
Qed.
特に解説はありません。

------------------------------------------------------------------------
(*Andの除去　右を残す*)
Theorem Andelr : forall A B:Prop, A /\ B -> B.
Proof.
intros A B H.
elim H; intros a b.
assumption.
Qed.
特に解説はありません。以下、特に解説がないときは、いちいち断らないことにします。（境界線も面倒なので省略します。）

------------------------------------------------------------------------
(*上記2つの応用*)
(*Impから同値にさかのぼるABAB*)
Theorem AndABAB : forall A B:Prop, (A <-> B) -> (A -> B).
Proof.
intros A B.
unfold iff.
apply (Andell (A -> B) (B -> A)).
Qed.

・AndABABの解説
unfold iff.について。unfold iff.直前のsubgoalは、

　　　　　(A <-> B) -> A -> B

ですが、これではわかりにくいので、Unset Printing Notations.命令を実行した上で、上記の証明をやり直してみると、今度のunfold iff.直前のsubgoalは、（括弧を補うと）

　　　　　(iff A B) -> A -> B

となります。つまり、A <-> Bは、iff A Bの略記だったわけです。さて、このままでは証明をさかのぼることができないので、iffの定義に戻りたいと思います。その命令がunfold iff.なのです。実際、unfold iff.を実行した直後のsubgoalは、（今度はUnset Printing Notations.命令を実行せずに証明をやり直してみると）

　　　　　(A -> B) /\ (B -> A) -> A -> B

となります。これは上記定理Andell : forall A B:Prop, A /\ B -> A.のhead typeのinstanceになっていることがすぐにわかると思います。また、apply Andell.だけではCoqに「わかりません」という意味のエラーを返されてしまいますので、上記の証明のようにします。その説明はここにあります。

------------------------------------------------------------------------
(*Impから同値にさかのぼるABBA*)
Theorem AndABBA : forall A B:Prop, (A <-> B) -> (B -> A).
Proof.
intros A B.
apply (Andelr (A -> B) (B -> A)).
Qed.

(*andの交換則右*)
Theorem Andcomr : forall A B:Prop, A /\ B -> B /\ A.
Proof.
intros A B H.
elim H.
intros a b.
split; assumption.
Qed.

(*andの交換則*)
Theorem Andcom : forall A B:Prop, A /\ B <-> B /\ A.
Proof.
intros A B.
split.
apply Andcomr.
apply Andcomr.
Qed.

(*andの結合則左右*)
Theorem Andasl : forall A B C:Prop, (A /\ B) /\ C -> A /\ (B /\ C).
Proof.
intros A B C H.
elim H.
intros ab c.
elim ab.
intros a b.
split.
assumption.
split; assumption.
Qed.

(*andの結合則右左*)
Theorem Andasr : forall A B C:Prop, A /\ (B /\ C) -> (A /\ B) /\ C.
Proof.
intros A B C H.
elim H.
intros a bc.
elim bc.
intros b c.
split.
split; assumption.
assumption.
Qed.

(*andの結合則同値*)
Theorem Andas : forall A B C:Prop, (A /\ B) /\ C <-> A /\ (B /\ C).
Proof.
intros A B C.
split.
apply Andasl.
apply Andasr.
Qed.

(*orの交換則右*)
Theorem Orcomr : forall A B:Prop, A \/ B -> B \/ A.
Proof.
intros A B H.
elim H.
intro a.
right.
assumption.
intro b.
left.
assumption.
Qed.

[a:A]

[b:B]
A \/ Bと
A->B \/ Aと
B->B \/ Aから
B \/ Aを結論しています。

A \/ B B \/ A B \/ A a,b

B \/ A

(*orの交換則*)
Theorem Orcom : forall A B:Prop, A \/ B <-> B \/ A.
Proof.
intros A B.
split.
apply Orcomr.
apply Orcomr.
Qed.

(*orの結合則左右*)
Theorem Orasl : forall A B C:Prop, (A \/ B) \/ C -> A \/ (B \/ C).
Proof.
intros A B C H.
elim H.
intros Hab.
elim Hab.
intro a.
left.
assumption.
intro b.
right.
left.
assumption.
intro c.
right.
right.
assumption.
Qed.

(*orの結合則右左*)
Theorem Orasr : forall A B C:Prop, A \/ (B \/ C) -> (A \/ B) \/ C.
Proof.
intros A B C H.
elim H.
intro a.
left.
left.
assumption.
intro H0.
elim H0.
intro b.
left; right.
assumption.
intro c.
right.
assumption.
Qed.

(*orの結合則同値*)
Theorem Oras : forall A B C:Prop, (A \/ B) \/ C <-> A \/ (B \/ C).
Proof.
intros A B C.
split.
apply Orasl.
apply Orasr.
Qed.

(*andの分配則*)
Theorem Anddist : forall A B C:Prop, A /\ ( B \/ C) -> (A /\ B) \/ (A /\ C).
Proof.
intros A B C H.
elim H.
intros a bc.
elim bc.
intro b.
left.
split; assumption.
intro c.
right.
split; assumption.
Qed.

(*andでくくる*)
Theorem Anddisc : forall A B C:Prop, (A /\ B) \/ (A /\ C) -> A /\ ( B \/ C).
Proof.
intros A B C H.
elim H.
intro ab.
elim ab.
intros a b.
split.
assumption.
left.
assumption.
intro H0.
elim H0.
intros a c.
split.
assumption.
right.
assumption.
Qed.

(*andの分配則同値*)
Theorem Anddiste : forall A B C:Prop, A /\ ( B \/ C) <-> (A /\ B) \/ (A /\ C).
Proof.
intros A B C.
split.
apply Anddist.
apply Anddisc.
Qed.

(*andでくくる同値*)
Theorem Anddisce : forall A B C:Prop, (A /\ B) \/ (A /\ C) <-> A /\ ( B \/ C).
Proof.
intros A B C.
split.
apply Anddisc.
apply Anddist.
Qed.

(*orの分配則*)
Theorem Ordist : forall A B C:Prop, A \/ ( B /\ C) -> (A \/ B) /\ (A \/ C).
Proof.
intros A B C H.
elim H.
intro a.
split; left; assumption.
intro bc.
elim bc; intros b c.
split; right; assumption.
Qed.

(*orでくくる*)
Theorem Ordisc : forall A B C:Prop, (A \/ B) /\ (A \/ C) -> A \/ ( B /\ C).
Proof.
intros A B C H.
elim H.
intros ab ac.
elim ab.
intro a.
left.
assumption.
intro b.
elim ac.
intro a.
left.
assumption.
intro c.
right.
split; assumption.
Qed.

(*orの分配則*)
Theorem Ordiste : forall A B C:Prop, A \/ ( B /\ C) <-> (A \/ B) /\ (A \/ C).
Proof.
intros A B C.
split.
apply Ordist.
apply Ordisc.
Qed.

(*orでくくる*)
Theorem Ordisce : forall A B C:Prop, (A \/ B) /\ (A \/ C) <-> A \/ ( B /\ C).
Proof.
intros A B C.
split.
apply Ordisc.
apply Ordist.
Qed.

(*ド・モルガンorの否定*)
Theorem Dm_nor : forall A B:Prop, ~ (A \/ B) -> ~ A /\ ~ B.
Proof.
intros A B H.
split.
intros a.
elim H.
left; assumption.
intros b.
elim H.
right; assumption.
Qed.

(*ド・モルガン否定のand*)
Theorem Dm_nandn : forall A B:Prop, ~ A /\ ~ B -> ~ (A \/ B).
Proof.
intros A B H H0.
elim H.
intros na nb.
elim H0; assumption.
Qed.

(*ド・モルガンandの否定同値*)
Theorem Dm_nore : forall A B:Prop, ~ (A \/ B) <-> ~ A /\ ~ B.
Proof.
intros A B.
split.
apply Dm_nor.
apply Dm_nandn.
Qed.

(*ド・モルガン否定のand同値*)
Theorem Dm_nandne : forall A B:Prop, ~ A /\ ~ B <-> ~ (A \/ B).
Proof.
intros A B.
split.
apply Dm_nandn.
apply Dm_nor.
Qed.

(*ド・モルガン否定のor*)
Theorem Dm_norn : forall A B:Prop, ~ A \/ ~ B -> ~ (A /\ B).
Proof.
intros A B H H0.
elim H0; intros a b.
elim H.
intro na.
elim na; assumption.
intro nb.
elim nb; assumption.
Qed.

(*ならばに変形*)
Theorem Impno : forall A B:Prop, (~ A \/ B) -> (A -> B).
Proof.
intros A B H a.
elim H.
intro na.
elim na.
assumption.
intro b; assumption.
Qed.

(*対偶否定の導入*)
Theorem Contp : forall A B:Prop, (A -> B) -> (~ B -> ~A).
Proof.
intros A B H nb a.
elim nb.
apply H.
assumption.
Qed.

------------------------------------------------------------------------
(*ド・モルガン存在の否定*)
Theorem Dm_nex : forall A:Set -> Prop,
(~ exists x:Set, A x) -> forall x:Set, ~ A x.
Proof.
intros A H x ax.
elim H.
exists x.
assumption.
Qed.
・上記exists x.について。
命令exists x.を実行するときに、仮定の中にxなるλ式（上記証明中ではx : Set）があることに注意してください。それがないと、exists x.はエラーになります。
------------------------------------------------------------------------
(*ド・モルガン否定の全称*)
Theorem Dm_alln : forall A:Set -> Prop,
(forall x:Set, ~ A x) -> (~ exists x:Set, A x).
Proof.
intros A H H0.
elim H0.
intro x.
apply H.
Qed.

(*ド・モルガン存在の否定同値*)
Theorem Dm_nexe : forall A:Set -> Prop,
(~ exists x:Set, A x) <-> forall x:Set, ~ A x.
Proof.
intro A.
split.
apply Dm_nex.
apply Dm_alln.
Qed.

(*ド・モルガン否定の全称同値*)
Theorem Dm_allne : forall A:Set -> Prop,
(forall x:Set, ~ A x) <-> (~ exists x:Set, A x).
Proof.
intro A.
split.
apply Dm_alln.
apply Dm_nex.
Qed.

(*ド・モルガン否定の存在*)
Theorem Dm_exn : forall A:Set -> Prop,
(exists x:Set, ~ A x) -> (~ forall x:Set, A x).
Proof.
intros A H H0.
elim H.
intros x H1.
elim H1.
apply H0.
Qed.

(*orの分配則述語*)
Theorem OrdistP : forall (A:Prop)(B:Set -> Prop),
A \/ (forall x:Set, B x) -> forall x:Set, (A \/ (B x)).
Proof.
intros A B H x.
elim H.
intro a.
left; assumption.
intro H0.
right.
apply H0.
Qed.

(*andの分配則述語*)
Theorem AnddistP : forall (A:Prop)(B:Set -> Prop),
A /\ (exists x:Set, B x) -> exists x:Set, (A /\ (B x)).
Proof.
intros A B H.
elim H.
intros a exB.
elim exB.
intros x Bx.
exists x.
split; assumption.
Qed.

(*andでくくる述語*)
Theorem AnddiscP : forall (A:Prop)(B:Set -> Prop),
(exists x:Set, (A /\ (B x))) -> A /\ (exists x:Set, B x).
Proof.
intros A B H.
elim H.
intros x ABx.
elim ABx.
intros a bx.
split.
assumption.
exists x.
assumption.
Qed.

(*andの分配則述語同値*)
Theorem AnddistPe : forall (A:Prop)(B:Set -> Prop),
A /\ (exists x:Set, B x) <-> exists x:Set, (A /\ (B x)).
Proof.
intros A B.
split.
apply AnddistP.
apply AnddiscP.
Qed.

(*andでくくる述語同値*)
Theorem AnddiscPe : forall (A:Prop)(B:Set -> Prop),
(exists x:Set, (A /\ (B x))) <-> A /\ (exists x:Set, B x).
Proof.
intros A B.
split.
apply AnddiscP.
apply AnddistP.
Qed.

------------------------------------------------------------------------
(*andを全称へ*)
Theorem Alland : forall (A B:Set -> Prop),
(forall x:Set, ((A x) /\ (B x))) ->
(forall x:Set, A x) /\ (forall x:Set, B x).
Proof.
intros A B H.
split.
intro x.
cut ((A x) /\ (B x)).
intro AB.
elim AB.
intros ax bx.
assumption.
apply H.
intro x.
cut ((A x) /\ (B x)).
intro AB.
elim AB.
intros ax bx.
assumption.
apply H.
Qed.
・cut命令の具体例が上記にあります。
------------------------------------------------------------------------
(*全称をandの外へ*)
Theorem AllandAll : forall (A B:Set -> Prop),
(forall x:Set, A x) /\ (forall x:Set, B x) ->
(forall x:Set, ((A x) /\ (B x))).
Proof.
intros A B H x.
elim H.
intros aA aB.
split.
apply aA.
apply aB.
Qed.

(*andを全称へ同値*)
Theorem Allande : forall (A B:Set -> Prop),
(forall x:Set, ((A x) /\ (B x))) <->
(forall x:Set, A x) /\ (forall x:Set, B x).
Proof.
intros A B.
split.
apply Alland.
apply AllandAll.
Qed.

(*全称をandの外へ同値*)
Theorem AllandAlle : forall (A B:Set -> Prop),
(forall x:Set, A x) /\ (forall x:Set, B x) <->
(forall x:Set, ((A x) /\ (B x))).
Proof.
intros A B.
split.
apply AllandAll.
apply Alland.
Qed.

(*orを存在へ*)
Theorem Exor : forall (A B:Set -> Prop),
(exists x:Set, ((A x) \/ (B x))) ->
(exists x:Set, A x) \/ (exists x:Set, B x).
Proof.
intros A B H.
elim H.
intros x AB.
elim AB.
intro ax.
left.
exists x.
assumption.
intro bx.
right.
exists x.
assumption.
Qed.

(*存在をorの外へ*)
Theorem ExorEx : forall (A B:Set -> Prop),
(exists x:Set, A x) \/ (exists x:Set, B x) ->
(exists x:Set, ((A x) \/ (B x))).
Proof.
intros A B H.
elim H.
intro EA.
elim EA.
intros x ax.
exists x.
left.
assumption.
intro EB.
elim EB.
intros x bx.
exists x.
right.
assumption.
Qed.

(*orを存在へ同値*)
Theorem Exore : forall (A B:Set -> Prop),
(exists x:Set, ((A x) \/ (B x))) <->
(exists x:Set, A x) \/ (exists x:Set, B x).
Proof.
intros A B.
split.
apply Exor.
apply ExorEx.
Qed.

(*存在をorの外へ同値*)
Theorem ExorExe : forall (A B:Set -> Prop),
(exists x:Set, A x) \/ (exists x:Set, B x) <->
(exists x:Set, ((A x) \/ (B x))).
Proof.
intros A B.
split.
apply ExorEx.
apply Exor.
Qed.

(*同値対称性*)
Theorem PeqSym : forall A B:Prop, (A <-> B) -> (B <-> A).
Proof.
intros A B.
apply (Andcomr (A -> B) (B -> A)).
Qed.

(*同値反射性*)
Theorem Peqref : forall A:Prop, A <-> A.
Proof.
intro A.
split; intro a; assumption.
Qed.

(*同値and*)
Theorem Peqand : forall A B C D:Prop,
(A <-> C) -> (B <-> D) -> ((A /\ B) <-> (C /\ D)).
Proof.
intros A B C D H H0.
elim H; intros AC CA; clear H.
elim H0; intros BD DB; clear H0.
split.
intro ab.
elim ab; intros a b; clear ab.
split.
apply AC; assumption.
apply BD; assumption.
intro cd.
elim cd; intros c d; clear cd.
split.
apply CA; assumption.
apply DB; assumption.
Qed.

(*同値or*)
Theorem Peqor : forall A B C D:Prop,
(A <-> C) -> (B <-> D) -> ((A \/ B) <-> (C \/ D)).
Proof.
intros A B C D H H0.
elim H; intros AC CA; clear H.
elim H0; intros BD DB; clear H0.
split.
intro ab.
elim ab.
intro a.
left.
apply AC; assumption.
intro b.
right.
apply BD; assumption.
intro cd.
elim cd.
intro c.
left.
apply CA; assumption.
intro d.
right.
apply DB; assumption.
Qed.

(*同値not*)
Theorem Peqnot : forall A B:Prop, (A <-> B) -> (~ A <-> ~ B).
Proof.
intros A B H.
elim H; intros ab ba; clear H.
split; apply Contp; assumption.
Qed.

(*同値imply*)
Theorem Peqimp : forall A B C D:Prop,
(A <-> C) -> (B <-> D) -> ((A -> B) <-> (C -> D)).
Proof.
intros A B C D H H0.
elim H; intros AC CA; clear H.
elim H0; intros BD DB; clear H0.
split.
intros AB c.
apply BD; apply AB; apply CA; assumption.
intros CD a.
apply DB; apply CD; apply AC; assumption.
Qed.

(*同値<->*)
Theorem Peqeq : forall A B C D:Prop,
(A <-> C) -> (B <-> D) -> ((A <-> B) <-> (C <-> D)).
Proof.
intros A B C D Ha Hb.
unfold iff at 2.
unfold iff at 2.
apply Peqand.
apply Peqimp; assumption.
apply Peqimp; assumption.
Qed.

unfold命令にもatが使えるようですね。
------------------------------------------------------------------------

(*同値all*)
Theorem Peqall : forall A B:Set -> Prop,
(forall x:Set, A x <-> B x) ->
((forall x:Set, A x) <-> (forall x:Set, B x)).
Proof.
intros A B H.
split.
intros FA x.
cut (A x).
cut (A x <-> B x).
intro H0; elim H0; intros AB BA; assumption.
apply H.
apply FA.
intros FB x.
cut (B x).
cut (A x <-> B x).
intro H0; elim H0; intros AB BA; assumption.
apply H.
apply FB.
Qed.

(*同値exists*)
Theorem Peqex : forall A B:Set -> Prop,
(forall x:Set, A x <-> B x) ->
((exists x:Set, A x) <-> (exists x:Set, B x)).
Proof.
intros A B H.
split.
intros (x,Ax).
exists x.
cut (A x).
cut (A x <-> B x).
intro H0; elim H0; intros AB BA; assumption.
apply H.
assumption.
intros (x,Bx).
exists x.
cut (B x).
cut (A x <-> B x).
intro H0; elim H0; intros AB BA; assumption.
apply H.
assumption.
Qed.

(*同値exists!*)
Theorem Pequex : forall A B:Set -> Prop,
(forall x:Set, A x <-> B x) ->
((exists! x:Set, A x) <-> (exists! x:Set, B x)).
Proof.
intros A B H.
apply (Peqex (unique (fun x:Set => A x)) (unique (fun x:Set => B x))).
intro x.
unfold unique.
apply Peqand.
apply H.
apply Peqall.
intro y.
apply Peqimp.
apply H.
apply Peqref.
Qed.

(*orとnot*)
Theorem Ornot : forall A B:Prop, (A \/ B) -> ~A -> B.
Proof.
intros A B Ho Hn.
elim Ho.
intro a.
elim Hn.
assumption.
intro b.
assumption.
Qed.

(*2種類の唯一存在の同値性uniqueness->！*)
Theorem UniexseqtoI : forall (A:Type) (P:A->Prop),
((exists x, P x) /\ uniqueness P) -> (exists! x, P x).
Proof.
intros A P.
intros ((x,Hx),Huni).
exists x.
(*次はred.でもOKだった。*)
unfold unique.
split.
assumption.
intros y Py.
apply Huni.
assumption.
assumption.
Qed.

(*2種類の唯一存在の同値性！->uniqueness*)
Theorem Uniexseqtoness : forall (A:Type) (P:A->Prop),
(exists! x, P x) -> ((exists x, P x) /\ uniqueness P).
Proof.
intros A P.
intros (x,(Hx,Huni)).
split.
exists x.
assumption.
(*次はred.でもOKだった。*)
unfold uniqueness.
intros z y Hz Hy.
transitivity x.
symmetry.
apply Huni.
assumption.
apply Huni.
assumption.
Qed.

(*2種類の唯一存在の同値性*)
Theorem Uniexseq : forall (A:Type) (P:A->Prop),
((exists x, P x) /\ uniqueness P) <-> (exists! x, P x).
Proof.
intros A P.
split.
apply UniexseqtoI.
apply Uniexseqtoness.
Qed.

(*forallと等号->forall*)
Theorem Eqallr : forall (A:Set -> Prop) (y:Set),
A y -> forall x:Set, (x = y -> A x).
Proof.
intros A y Hay x He.
rewrite He.
assumption.
Qed.

(*forallと等号<-forall*)
Theorem Eqalll : forall (A:Set -> Prop) (y:Set),
(forall x:Set, (x = y -> A x)) -> A y.
Proof.
intros A y Hf.
apply Hf.
reflexivity.
Qed.

(*forallと等号*)
Theorem Eqall : forall (A:Set -> Prop) (y:Set),
A y <-> forall x:Set, (x = y -> A x).
Proof.
intros A y.
split.
apply Eqallr.
apply Eqalll.
Qed.

(*existsと等号->exists*)
Theorem Eqexr : forall (A:Set -> Prop) (y:Set),
A y -> exists x:Set, (x = y /\ A x).
Proof.
intros A y Hay.
exists y.
split.
reflexivity.
assumption.
Qed.

(*existsと等号<-exists*)
Theorem Eqexl : forall (A:Set -> Prop) (y:Set),
(exists x:Set, (x = y /\ A x)) -> A y.
Proof.
intros A y (x,Ha).
elim Ha; intros Ha1 Ha2.
rewrite <- Ha1.
assumption.
Qed.

(*forallと等号*)
Theorem Eqex : forall (A:Set -> Prop) (y:Set),
A y <-> exists x:Set, (x = y /\ A x).
Proof.
intros A y.
split.
apply Eqexr.
apply Eqexl.
Qed.

もどる

	[a:A]	[b:B]		A \/ Bと A->B \/ Aと B->B \/ Aから B \/ Aを結論しています。
A \/ B	B \/ A	B \/ A	a,b
B \/ A			a,b