Coqチュートリアルと平行して始めて見た。 証明はできてるんだろうけど、自分で書いてて日本語に訳せないので全然分かってない。

coqex_1.v

Theorem tautology : forall P : Prop, P -> P.
Proof.
  intros P H.
  assumption.
Qed.

(* Error: Attempt to save an incomplete proof *)
(*
Theorem wrong : forall P : Prop, P.
Proof.
  intros P.
Qed.
*)

(* 課題1 *)
Theorem Modus_ponens : forall P Q : Prop, P -> (P -> Q) -> Q.
Proof.
  intros.
  apply (H0 H).
Qed.

(* 課題2 *)
Theorem Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P.
Proof.
  unfold not.
  intros.
  apply H.
  apply H.
  assumption.
Qed.

Theorem DeMorgan1 : forall P Q : Prop, ~P \/ ~Q -> ~(P /\ Q).
Proof.
  unfold not.
  intros.
  destruct H.
  destruct H0.
  apply (H H0).
  destruct H0.
  apply (H H1).
Qed.

Theorem DeMorgan2 : forall P Q : Prop, ~P /\ ~Q -> ~(P \/ Q).
Proof.
  unfold not.
  intros.
  destruct H.
  destruct H0.
  apply (H H0).
  apply (H1 H0).
Qed.

Theorem DeMorgan3 : forall P Q : Prop, ~(P \/ Q) -> ~P /\ ~Q.
Proof.
  unfold not.
  split.
  intro.
  apply H.
  apply (or_introl H0).
  intro.
  apply H.
  apply (or_intror H0).
Qed.

Theorem NotNot_LEM : forall P : Prop, ~ ~(P \/ ~P).
Proof.
  unfold not.
  intros.
  apply H.
  right.
  intro.
  apply (H (or_introl H0)).
Qed.