tmiyaさんが出している問題に触発されました。
http://study-func-prog.blogspot.com/2010/07/coq-coq-99-part-1.html
数をこなせば自然と出来るようになるのではないか。
Section FoundationOfSoftwareScience. Lemma e_1_23 : forall A B C : Prop, (A -> B) -> ((B -> C) -> (A -> C)). Proof. intros. apply H0. apply H. exact H1. Qed. Lemma ex_1_17_1 : forall A B C : Prop, (A -> (B -> C)) -> (B -> (A -> C)). Proof. intros. simple apply H. assumption. assumption. Qed. Lemma ex_1_17_2 : forall A B C : Prop, A -> ((A -> B) -> B). Proof. intros. apply H0. assumption. Qed. Lemma ex_1_17_3 : forall A B C : Prop, (A -> B) -> ((A -> (B -> C)) -> (A -> C)). Proof. intros. simple apply H0. assumption. apply H. assumption. Qed. Lemma e_1_24 : forall A B : Prop, (A /\ B) -> (B /\ A). Proof. intros. elim H. intros. clear H. split. assumption. assumption. Qed. Lemma e_1_25 : forall A B : Prop, A -> (B -> A). Proof. intros. assumption. Qed. Lemma ex_1_18_1 : forall A B C : Prop, (A /\ (B /\ C)) -> (A /\ B) /\ C. Proof. intros. elim H. intros. elim H1. intros. split. split. assumption. assumption. assumption. Qed. Lemma ex_1_18_2 : forall A B C : Prop, ((A /\ B) -> C) -> (A -> (B -> C)). Proof. intros. simple apply H. split. assumption. assumption. Qed. Lemma e_1_26 : forall A B C : Prop, A \/ (B \/ C) -> (A \/ B) \/ C. Proof. intros. elim H. intro. clear H. left. left. assumption. intro. elim H0. intro. left. right. assumption. intro. right. assumption. Qed. Lemma ex1_19_1 : forall A B C : Prop, A /\ (B \/ C) <-> (A /\ B) \/ (A /\ C). Proof. intros. split. intros. elim H. intros. elim H1. intros. left. split. assumption. assumption. intros. right. split. assumption. assumption. intros. elim H. intros. elim H0. intros. split. assumption. left;assumption. intros; elim H0. intros. split. assumption. right. assumption. Qed. Lemma ex_1_19_2 : forall A B C : Prop, ((A \/ B) -> C) <-> (A -> C) /\ (B -> C). Lemma ex_1_19_3 : forall A B C D : Prop, (A -> C) /\ (B -> D) -> ((A \/ B) -> (C \/ D)). Lemma e_1_27_a : forall A : Prop, ~ A <-> (A -> False). Lemma e_1_27_b : forall A : Prop, A -> ~~A. Lemma e_1_28 : forall A B :Prop, (A -> B) -> (~B -> ~A). Lemma ex_1_20_1 : forall A : Prop, ~~~A <-> ~A. Lemma ex_1_20_2 : forall A B : Prop, (~B -> ~A) <-> (A -> ~~B). Lemma ex_1_20_3 : forall A B : Prop, (~A \/ ~B) -> ~(A /\ B). Lemma e_1_29 : forall A B : Prop, (A \/ B) /\ ~B -> A. End FoundationOfSoftwareScience