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)


example : ¬ ( P ∧ ¬ P ) := by
  change P ∧ ¬ P → False
  intro h
  conj_elim hp hnp from h
  change P → False at hnp
  apply hnp
  exact hp


example ( h : P → Q ) ( hnq : ¬ Q ) : ¬ P := by
  change P → False
  intro hp
  change Q → False at hnq
  apply hnq
  apply h
  exact hp

/- goal-oriented reasoning -/
example (h : P ) : P ∨ Q := by
  apply Or.intro_left
  exact h

/- hypothesis-oriented reasoning -/
example (h : P ) : P ∨ Q := by
  disj_intro_left hpq from h Q
  exact hpq

/- hypothesis-oriented reasoning -/
example ( h : P ∨ Q ) : Q ∨ P := by
  disj_elim hp hq from h
  disj_intro_right hqp from Q hp
  exact hqp
  disj_intro_left hqp from hq P
  exact hqp

/- a little bit more goal-oriented, using the cases tactic -/
example ( h : P ∨ Q ) : Q ∨ P := by
  cases h -- Since P ∨ Q is true, we can reason by cases:
  case inl hp => -- Suppose P is true.
    apply Or.intro_right -- By disjunction introduction, we can prove Q ∨ P by proving P,
    exact hp -- and we know that P is true.
  case inr hq => -- Suppose Q is true.
    apply Or.intro_left -- By disjunction introduction, we can prove Q ∨ P by proving Q,
    exact hq -- and we know that Q is true.


/- 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!


example ( 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 -/
example ( h : P → Q ) : ¬ P ∨ Q := by
  cases em P
  case inl hp =>
    apply Or.intro_right
    apply h
    exact hp
  case inr hnp =>
    apply Or.intro_left
    exact hnp

/- another proof, using em Q -/
example ( 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