macro "conj_elim" hp:ident hq:ident "from" h:ident : tactic =>
  `(tactic|(apply And.elim _ $h; intro $hp $hq))

macro "conj_intro" h:ident "from" hp:ident hq:ident : tactic =>
  `(tactic|(have $h : _∧_ := And.intro $hp $hq))

macro "disj_elim" hp:ident hq:ident "from" h:term:arg : tactic =>
  `(tactic|(refine Or.elim $h (fun $hp => ?_) (fun $hq => ?_)))

macro "disj_intro_left" h:ident "from" hp:ident q:term:arg : tactic =>
  `(tactic|(have $h : _∨($q) := Or.inl $hp))

macro "disj_intro_right" h:ident "from" p:term:arg hq:ident : tactic =>
  `(tactic|(have $h : ($p)∨_ := Or.inr $hq))

macro "impl_elim" hq:ident "from" hp:ident hpq:ident : tactic =>
  `(tactic|(have $hq := $hpq $hp))

namespace And
theorem elim' {P Q : Prop} {R : Sort} (h : P ∧ Q) (f : P → Q → R) : R := by
  sorry
end And


variable (P Q R S : Prop)

/- a proof by cases -/
example ( hpr : P → R ) ( hqr : Q → R ) : P ∨ Q → R := by
  sorry

/- ex falso -/
example : False → P := by
  sorry


theorem Thm1 ( h : ¬ P ∨ Q ) : P → Q := by
  sorry


open Classical
example : ( P ∨ ¬ P ) := by
  sorry

/- a proof using em P -/
theorem Thm2 ( h : P → Q ) : ¬ P ∨ Q := by
  cases em P -- P is either true or false, so we argue by cases.
  sorry

/- another proof, using em Q -/
theorem Thm3 ( h : P → Q ) : ¬ P ∨ Q := by
  cases em Q -- Q is either true or false, so we argue by cases.
  sorry

example : (P → Q) ↔ (¬ P ∨ Q) := by
  sorry

example ( h : ¬ (P ∨ Q) ) : ¬ P ∧ ¬ Q := by
  sorry

example ( h : ¬ P ∧ ¬ Q ) : ¬ (P ∨ Q) := by
  sorry


theorem Thm4 : ¬ ( P ∨ Q ) ↔ (¬ P ∧ ¬ Q) := by
  sorry


open Classical
theorem Thm5 : ¬ ( P ∧  Q ) ↔ (¬ P ∨  ¬ Q) := by
  sorry