Require Import Utf8.
Variable P Q R : Prop.

Notation in₁ := or_introl.
Notation in₂ := or_intror.
Notation π₁ := (fun p => match p with conj a b => a end).
Notation π₂ := (fun p => match p with conj a b => b end).
Notation " ⟨ a , b ⟩ " := (conj a b).
Notation "⊥e" := (False_ind _).

Lemma Q1 : P → ¬¬P.
exact (λ p n, n p).
Qed.

Lemma Q2 : P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R).
exact (λ x,
  match π₂ x with
  | in₁ q => in₁ ⟨π₁ x, q⟩
  | in₂ r => in₂ ⟨π₁ x, r⟩
  end).
Qed.

Lemma Q3 : (P → ¬Q) → ¬(P ∧ Q).
exact (λ n x, n (π₁ x) (π₂ x)).
Qed.

Lemma Q4 : (P → Q) → ¬Q → ¬P.
exact (λ f n p, n (f p)).
Qed.

Lemma Q5 : (P → Q) → (P → ¬Q) → ¬P.
exact (λ pq pnq p, (pnq p) (pq p)).
Qed.

Lemma Q6 : ((P ∨ Q) → R) → (P → R) ∧ (Q → R).
exact (λ f, ⟨λ p, f(in₁ p), λ p, f(in₂ p)⟩).
Qed.

Lemma Q7 : (P → R) ∨ (Q → R) → P ∧ Q → R.
exact (λ x pq,
  match x with
  | in₁ pr => pr (π₁ pq)
  | in₂ qr => qr (π₂ pq)
  end).
Qed.

Lemma Q8 : (P → ¬¬Q) → ¬¬(P → Q).
exact (λ pnnq npq,
  npq (λ p,
    ⊥e (pnnq p (λ q,
          npq (λ _, q))))).
Qed.

Axiom emp : P ∨ ¬P.

Lemma Q9 : (P ∧ Q → R) → (P → R) ∨ (Q → R).
exact (λ f ,
  match emp with
  | in₁ p => in₂ (λ q, f ⟨p, q⟩)
  | in₂ np => in₁ (λ p, ⊥e (np p))
  end).
Qed.

Lemma Q10 : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
split.
  exact (λ npq ,
    match emp with
    | in₁ p => in₂ (λ q, ⊥e (npq ⟨p, q⟩))
    | in₂ np => in₁ np
    end).
  exact (λ x pq,
    match x with
    | in₁ np => np (π₁ pq)
    | in₂ nq => nq (π₂ pq)
    end).
Qed.

Lemma Q11 : (P → P ∧ Q) ∨ (Q → P ∧ Q).
exact (match emp with
  | in₁ p => in₂ (λ q, ⟨p, q⟩)
  | in₂ np => in₁ (λ p, ⊥e (np p))
  end).
Qed.