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 :=
  And.elim f h
end And


variable (P Q R S : Prop)

/- a proof by cases -/
example ( hpr : P → R ) ( hqr : Q → R ) : P ∨ Q → R := by
  intro h -- We want to prove P ∨ Q → R, so we begin by assuming P ∨ Q.  We need to show R.
  cases h -- Now we argue by cases (disjunction elimination) on P ∨ Q. 
  case inl hp => -- First we assume P and prove R. 
    apply hpr -- Since we know P → R, it will be sufficient to prove P. 
    exact hp -- But P is one of our assumptions, so we're done with this case!
  case inr hq => -- In the second case, we assume Q and prove R. 
    apply hqr -- Since we know Q → R, it will be enough to prove Q.
    exact hq -- And Q is one of our assumptions, so we are done!

/- ex falso -/
example : False → P := by
  intro h -- h is a proof of False
  cases h -- For each proof of False, we need to give a proof of P.
          -- But there are no proofs of False, so there's nothing we need to do!


theorem Thm1 ( h : ¬ P ∨ Q ) : P → Q := by
  intro hp
  cases h
  case inl hnp =>
    exfalso
    apply hnp
    exact hp
  case inr hq =>
    exact hq


open Classical
example : ( P ∨ ¬ P ) := by
  exact em P

/- a proof using em P -/
theorem Thm2 ( h : P → Q ) : ¬ P ∨ Q := by
  cases em P -- We know that P is either true or false, so we argue by cases.
  case inl hp => -- First assume that P is true and prove ¬ P ∨ Q.
    apply Or.intro_right -- We need to show ¬ P ∨ Q.  We will do it by proving Q, using disjunction introduction.
    apply h -- We know P → Q, so it will be enough to prove P.
    exact hp -- And P was one of our assumptions, so we are done with this case.
  case inr hnp => -- Now we assume P is false and prove ¬ P ∨ Q.
    apply Or.intro_left -- This time we will use the other disjunction introduction rule, so now we need to show ¬ P.
    exact hnp -- And that is exactly what we assumed in this case, so we are done!

/- another proof, using em Q -/
theorem Thm3 ( h : P → Q ) : ¬ P ∨ Q := by
  cases em Q
  case inl hq =>
    apply Or.intro_right
    exact hq
  case inr hnq =>
    apply Or.intro_left
    change P → False
    intro hp
    change Q → False at hnq
    apply hnq
    apply h
    exact hp

example : (P → Q) ↔ (¬ P ∨ Q) := by
  apply Iff.intro
  · show (P → Q) → (¬ P ∨ Q)
    intro h
    apply Thm2
    exact h
  · show (¬ P ∨ Q) → (P → Q)
    intro h
    apply Thm1
    exact h

example ( h : ¬ (P ∨ Q) ) : ¬ P ∧ ¬ Q := by
  apply And.intro
  intro hp
  apply h
  apply Or.intro_left
  exact hp
  intro hq
  apply h
  apply Or.intro_right
  exact hq

example ( h : ¬ P ∧ ¬ Q ) : ¬ (P ∨ Q) := by
  intro hpq
  conj_elim hnp hnq from h
  cases hpq
  case inl hp =>
    apply hnp
    exact hp
  case inr hq =>
    apply hnq
    exact hq


theorem Thm4 : ¬ ( P ∨ Q ) ↔ (¬ P ∧ ¬ Q) := by
  apply Iff.intro
  · intro h
    apply And.intro
    · intro hp
      apply h
      apply Or.intro_left
      exact hp
    · intro hq
      apply h
      apply Or.intro_right
      exact hq
  · intro h
    intro hpq
    conj_elim hnp hnq from h
    cases hpq
    case inl hp =>
      apply hnp
      exact hp
    case inr hq =>
      apply hnq
      exact hq


open Classical
theorem Thm5 : ¬ ( P ∧  Q ) ↔ (¬ P ∨  ¬ Q) := by
  apply Iff.intro
  · intro h
    cases em P
    case mp.inl hp =>
      apply Or.intro_right
      intro hq
      apply h
      apply And.intro
      exact hp
      exact hq
    case mp.inr hnp =>
      apply Or.intro_left
      exact hnp
  · intro h
    intro hpq
    cases h
    case mpr.inl hnp =>
      apply hnp
      conj_elim hp hq from hpq
      exact hp
    case mpr.inr hnq =>
      apply hnq
      conj_elim hp hq from hpq
      exact hq