Require Export Utf8 IndefiniteDescription ClassicalEpsilon
        ssreflect ssrbool ssrfun.

(* Modus ponens:
   https://en.wikipedia.org/wiki/Modus_ponens *)

Theorem modus_ponens : ∀ p q : Prop, p → (p → q) → q.
Proof.
  intros.
  apply H0 in H.
  exact.
Qed.

(* Modus tollens:
   https://en.wikipedia.org/wiki/Modus_tollens *)

Theorem modus_tollens : ∀ p q : Prop, (p → q) → ¬ q → ¬ p.
Proof.
  intros.
  pose proof (classic p).
  destruct H1.
  apply H in H1.
  contradiction.
  exact.
Qed.

(* Hypothetical syllogism:
   https://en.wikipedia.org/wiki/Hypothetical_syllogism *)

Theorem hypothetical_syllogism : ∀ p q r : Prop, (p → q) → (q → r) → (p → r).
Proof.
Admitted.

(* Disjunctive syllogism:
   https://en.wikipedia.org/wiki/Disjunctive_syllogism *)

Theorem disjunctive_syllogism : ∀ p q : Prop, (p ∨ q) → ¬ p → q.
Proof.
  intros.
  destruct H.
  contradiction.
  exact.
Qed.

(* Constructive dilemma:
   https://en.wikipedia.org/wiki/Constructive_dilemma *)

Theorem constructive_dilemma :
  ∀ p q r s : Prop, (p → q) → (r → s) → (p ∨ r) → q ∨ s.
Proof.
  intros.
  destruct H1.
  apply H in H1.
  left.
  exact.
  apply H0 in H1.
  right.
  exact.
Qed.

(* Destructive dilemma:
   https://en.wikipedia.org/wiki/Destructive_dilemma *)

Theorem destructive_dilemma :
  ∀ p q r s : Prop, (p → q) → (r → s) → (¬ q ∨ ¬ s) → ¬ p ∨ ¬ r.
Proof.
Admitted.

(* Conjunction elimination:
   https://en.wikipedia.org/wiki/Conjunction_elimination *)

Theorem conjunction_elimination_left : ∀ p q : Prop, p ∧ q → p.
Proof.
  intros.
  destruct H.
  exact.
Qed.

Theorem conjunction_elimination_right : ∀ p q : Prop, p ∧ q → q.
Proof.
Admitted.

(* Disjunction introduction:
   https://en.wikipedia.org/wiki/Disjunction_introduction *)

Theorem disjunction_introduction_left : ∀ p q : Prop, p → p ∨ q.
Proof.
Admitted.

Theorem disjunction_introduction_right : ∀ p q : Prop, q → p ∨ q.
Proof.
Admitted.

Theorem NNPP : ∀ p, ¬ ¬ p → p.
Proof.
Admitted.

(* Exercises. For each N = 1,2,3,4,5, prove either QNa or QNb,
   but not both. *)

Theorem Q1a : ∀ p q : Prop, (p → q) → (q → p).
Proof.
Admitted.

Theorem Q1b : ¬ (∀ p q : Prop, (p → q) → (q → p)).
Proof.
Admitted.

Theorem Q2a : ∀ p q : Prop, (¬ p → ¬ q) → (q → p).
Proof.
Admitted.

Theorem Q2b : ¬ (∀ p q : Prop, (¬ p → ¬ q) → (q → p)).
Proof.
Admitted.

Theorem Q3a : ∀ p q : Prop, (¬ p → ¬ q) → (p → q).
Proof.
Admitted.

Theorem Q3b : ¬ (∀ p q : Prop, (¬ p → ¬ q) → (p → q)).
Proof.
Admitted.

Theorem Q4a : ∀ p q : Prop, ¬ (¬ p ∧ ¬ q) → p ∨ q.
Proof.
Admitted.

Theorem Q4b : ¬ (∀ p q : Prop, ¬ (¬ p ∧ ¬ q) → p ∨ q).
Proof.
Admitted.

Theorem Q5a : ∀ p q : Prop, (p → q) → (¬ p ∨ ¬ q).
Proof.
Admitted.

Theorem Q5b : ¬ (∀ p q : Prop, (p → q) → (¬ p ∨ ¬ q)).
Proof.
Admitted.

(* De Morgan's laws:
   https://en.wikipedia.org/wiki/De_Morgan%27s_laws#Extension_to_predicate_and_modal_logic *)

Theorem Q6 : ∀ A (P : A → Prop), (∀ x, P x) ↔ ¬ (∃ x, ¬ P x).
Proof.
  intros.
  split.
  unfold not.
  intros.
  destruct H0.
  contradiction H0.
  apply H.
  intros.
  pose proof (classic (P x)).
  destruct H0.
  exact.
  contradiction H.
  exists x.
  exact H0.
Qed.

Theorem Q7 : ∀ A (P : A → Prop), (∃ x, P x) ↔ ¬ (∀ x, ¬ P x).
Proof.
Admitted.