「ソフトウェア科学基礎」より問題集

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