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:ident : 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))

variable ( P Q R S : Prop )

/- We prove that P and Q implies Q and P -/
example ( h : P ∧ Q ) : Q ∧ P := by
  conj_elim hp hq from h -- conjunction elimination gives P and Q from P ∧ Q
  conj_intro hqp from hq hp -- conjunction introduction gives Q ∧ P from Q and P
  exact hqp

/- The same thing can be proved by a combination of simplifying
goals and increasing knowledge. -/
example ( h : P ∧ Q ) : Q ∧ P := by
  conj_elim hp hq from h -- conjunction elimination, same as before
  apply And.intro -- simplify the goal by conjunction introduction
  exact hq -- we have Q already!
  exact hp -- we have P already!

/- We can do the whole proof by goal simplification...  But it's
not necessarily easier to read or think about. -/
example ( h : P ∧ Q ) : Q ∧ P := by
  apply And.intro -- we have to prove Q and P individually
  apply And.elim _ h -- the blank leaves a hole to fill in below
/- if h is P ∧ Q and the goal is X, this turns a goal from X
   into P → Q → X -/
  intro _ hq
  exact hq
  apply And.elim _ h
  intro hp _
  exact hp

example ( h : P∧Q∧R ) : (P∧Q)∧R := by
  conj_elim hp hqr from h
  conj_elim hq hr from hqr
  apply And.intro
  apply And.intro
  exact hp
  exact hq
  exact hr

example ( hpq : P → Q ) ( hqr : Q → R ) : P → R := by
  intro hp
  impl_elim hq from hp hpq
  impl_elim hr from hq hqr
  exact hr

example ( hpq : P → Q ) ( hqr : Q → R ) : P → R := by
  intro hp
  apply hqr
  apply hpq
  exact hp

example ( hpq : P → Q ) ( hqr : Q → R ) ( hrs : R → S ) : P → S := by
  intro hp
  apply hrs
  apply hqr
  apply hpq
  exact hp

example ( h : P∧Q → R ) : P → Q → R := by
  intro hp
  intro hq
  conj_intro hpq from hp hq
  impl_elim hr from hpq h
  exact hr