下の方に説明があります。
次の定理を証明せよ。ただし、Coq.LogicおよびCoq.Setsに定義されている公理を用いても構わない。各定理について、それを証明するのに必要な公理はできるだけ弱いものに留めるのが望ましい。
なお、autoやtautoなどの自動証明タクティックを用いてもよい。
(* 必要な公理を入れる *)
Lemma ABC_iff_iff :
forall A B C : Prop, ((A <-> B) <-> C) <-> (A <-> (B <-> C)).
Proof.
(* ここに証明を書く *)
Qed.
(* 必要な公理を入れる *)
Goal
forall P Q R : Prop,
(IF P then Q else R) ->
exists b : bool,
(if b then Q else R).
Proof.
(* ここに証明を書く *)
Qed.
(* 必要な公理を入れる *)
Goal
forall P Q R : nat -> Prop,
(forall n, IF P n then Q n else R n) ->
exists f : nat -> bool,
(forall n, if f n then Q n else R n).
Proof.
(* ここに証明を書く *)
Qed.
ヒント
次の定理を証明せよ。ただし、Coq.LogicおよびCoq.Setsに定義されている公理を用いても構わない。各定理について、それを証明するのに必要な公理はできるだけ弱いものに留めるのが望ましい。
(* 必要な公理を入れる *)
Record isomorphism{A B : Type} (f : A -> B) : Prop := {
inverse : B -> A;
is_retraction b : f (inverse b) = b;
is_section a : inverse (f a) = a
}.
Notation isomorphic A B :=
(exists f, @isomorphism A B f).
Lemma neg_unique :
forall A,
{ isomorphic (A -> Empty_set) Empty_set } +
{ isomorphic (A -> Empty_set) unit }.
Proof.
(* ここに証明を書く *)
Qed.
ヒント
(* isomorphic の証明の仕方 *)
Record isomorphism{A B : Type} (f : A -> B) : Prop := {
inverse : B -> A;
is_retraction b : f (inverse b) = b;
is_section a : inverse (f a) = a
}.
Notation isomorphic A B :=
(exists f, @isomorphism A B f).
Lemma option_unit_isom : isomorphic (option unit) bool.
Proof.
(* A -> B の写像を指定する *)
exists (fun o => match o with Some _ => true | None => false end).
(* その逆写像 B -> A を指定する *)
exists (fun b : bool => if b then Some tt else None).
- intros [|]; reflexivity.
- intros [[]|]; reflexivity.
Qed.
次の定理を証明せよ。ただし、Coq.LogicおよびCoq.Setsに定義されている公理を用いても構わない。各定理について、それを証明するのに必要な公理はできるだけ弱いものに留めるのが望ましい。
Definition compose {A B C} (f : A -> B) (g : B -> C) :=
fun x => g (f x).
Parameter X Y : Type.
Parameter f : X -> Y.
Axiom epi : forall Z (g h : Y -> Z), compose f g = compose f h -> g = h.
(* 必要な公理を入れる *)
Lemma surj : forall y, exists x, f x = y.
Proof.
(* ここに証明を書く *)
Qed.
(* 必要な公理を入れる *)
Lemma split_epi : exists g, compose g f = id.
Proof.
(* ここに証明を書く *)
Qed.
ヒント
次の定理を証明せよ。ただし、Coq.LogicおよびCoq.Setsに定義されている公理を用いても構わない。各定理について、それを証明するのに必要な公理はできるだけ弱いものに留めるのが望ましい。
Require Import Coq.Relations.Relations.
Require Import Coq.Classes.SetoidClass.
Parameter A : Type.
Parameter SetoidA : Setoid A.
Existing Instance SetoidA.
(* 必要な公理を入れる *)
Definition Q : Type := (* 定義を書く *) .
Definition pi(a : A) : Q := (* 定義を書く *) .
Lemma pi_surj : forall x, exists a, pi a = x.
Proof.
(* ここに証明を書く *)
Qed.
Lemma pi_ker : forall a b, pi a = pi b <-> a == b.
Proof.
(* ここに証明を書く *)
Qed.
(* 必要な公理を入れる *)
Lemma representative_exists :
exists f : A -> A, forall a b, f a = f b <-> a == b.
Proof.
(* ここに証明を書く *)
Qed.
次の定理を証明せよ。ただし、Coq.LogicおよびCoq.Setsに定義されている公理を用いても構わない。
Definition Nat : Type :=
forall A : Type, (A -> A) -> (A -> A).
Definition NatMult(n m : Nat) : Nat :=
fun A f => n _ (m _ f).
Lemma NatMult_comm: forall n m, NatMult n m = NatMult m n.
Proof.
(* ここに証明を書く *)
Qed.
(* 上のかわりに、次の定理を証明してもよい *)
Lemma NatMult_not_comm: ~forall n m, NatMult n m = NatMult m n.
Proof.
(* ここに証明を書く *)
Qed.
Coqのベースとなる論理は pCIC という型理論です。
型理論自体は単なる形式的な体系であり、それにどういう意味を割り当てるかにはある程度の任意性があります。通常の Coq では、型に集合を対応させて考えます。例えば、 nat という型は自然数全体の集合のことを指していると考えます。(ただし、Prop型をもつ型には命題を対応させます。)
pCIC 自体が強力な推論体系であり、かなりの証明能力を有しますが、集合論モデル的には正しいのに pCIC だけでは証明できない命題がいくつかあります。それらについては、公理として仮定することになります。
Coq.Logicに用意されている公理についていくつか説明を書いたので、参考にしてください。
今回の問題は、これらの公理のどれが必要かを考える練習です。よくわからない場合は、片っ端から公理を仮定して証明に臨んでも構いません。余裕がある人は、できるだけ少ない(弱い)公理だけで証明できるか考えてみましょう。