前回に引き続き、練習してます。
今回はちょうど見つけたCoq-99 : Part 1の問題をやってみました。一応、答えを見ずに全部できましたが、所々詰まったりしました。ある意味、人間バックトラックです。
Lemma Coq_01 : forall A B C:Prop, (A->B->C) -> (A->B) -> A -> C. intros. apply H. apply H1. apply H0. apply H1. Qed. Lemma Coq_02 : forall A B C:Prop, A /\ (B /\ C) -> (A /\ B) /\ C. intros. destruct H. destruct H0. split. split. apply H. apply H0. apply H1. Qed. Lemma Coq_03 : forall A B C D:Prop, (A -> C) /\ (B -> D) /\ A /\ B -> C /\ D. intros. destruct H. destruct H0. destruct H1. split. apply H. apply H1. apply H0. apply H2. Qed. Lemma Coq_04 : forall A : Prop, ~(A /\ ~A). intro. intro. destruct H. apply H0. apply H. Qed. Lemma Coq_05 : forall A B C:Prop, A \/ (B \/ C) -> (A \/ B) \/ C. intros. destruct H. left. left. apply H. destruct H. left. right. apply H. right. apply H. Qed. Lemma Coq_06 : forall A, ~~~A -> ~A. intro. intro. intro. destruct H. intro. apply H. apply H0. Qed. Lemma Coq_07 : forall A B:Prop, (A->B)->~B->~A. intros. intro. apply H0. apply H. apply H1. Qed. Lemma Coq_08: forall A B:Prop, ((((A->B)->A)->A)->B)->B. intros. apply H. intro. apply H0. intro. apply H. intro. apply H1. Qed. Lemma Coq_09 : forall A:Prop, ~~(A\/~A). intro. intro. case H. right. intro. case H. left. apply H0. Qed.
感じはつかめてきたんですが、まだまだうまくタクティクを実行した後の状態が想像できてないときもあります。
でも、簡単な問題であれば自力でできるというのがわかってちょっと安心しました。
