coqt2

gistfile1.txt

Definition prop0 : forall (A : Prop), A -> A.
Proof.
intros.
apply H.
Qed.

Goal forall (P Q : Prop), (forall P : Prop, (P -> Q) -> Q) -> ((P -> Q) -> P) -> P.
Proof.
intro.
intro.
intro.
intro.
apply H0.
intro.
apply (H (P -> Q)).
apply (H P).
Qed.

Goal forall (P Q R : Prop), (P -> Q) -> (Q -> R) -> P -> R.
intros.
apply H0.
apply H.
apply H1.
Qed.

(* リスト定義
Inductive list (A : Type) : Type :=
  | nil : list A
  | cons : A -> list A -> list A.
*)

Goal forall P : Prop, P -> ~~P.
intros.
intro.
apply H0.
apply H.
Qed.

Goal forall (P Q : Prop), P \/ Q -> Q \/ P.
intros.
case H.
apply or_intror.
apply or_introl.
Qed.

Goal forall (P Q : Prop), P /\ Q -> Q /\ P.
intros.
destruct H.
apply conj.
apply H0.
apply H.
Qed.

Goal forall (P : Prop), ~(P /\ ~P).
intros.
intro.
destruct H.
apply H0.
apply H.
Qed.

Goal forall (P Q : Prop), ~P \/ ~Q -> ~(P /\ Q).
intros.
intro.
destruct H.
destruct H0.
apply H.
apply H0.
destruct H0.
apply H.
apply H1.
Qed.

Goal forall (P : Prop), (forall (P : Prop), ~~P -> P) -> P \/~P.
intros.
apply H.
unfold not.
intros.
apply H0.
right.
intro.
apply H0.
left.
apply H1.