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

/- a hypothesis oriented proof -/
example (hp : P) (hpq : P → Q) : Q := by
  impl_elim hq from hp hpq
  exact hq

/- a goal oriented proof -/
example (hp : P) (hpq : P → Q) : Q := by
  apply hpq
  exact hp

/- a hypothesis oriented proof -/
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

/- a goal oriented proof -/
example (hpq : P → Q) (hqr : Q → R) : P → R := by
  intro hp
  apply hqr
  apply hpq
  exact hp

/- a hypothesis oriented proof -/
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

/- a goal oriented proof -/
example ( h : P ∧ Q → R ) : ( P → Q → R ) := by
  intro hp
  intro hq
  apply h
  apply And.intro
  exact hp
  exact hq




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

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


/- a hypothesis oriented proof -/
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 goal oriented proof -/
example (h : P ∨ Q) : Q ∨ P := by
  apply Or.elim h
  intro hp
  apply Or.intro_right
  exact hp
  intro hq
  apply Or.intro_left
  exact hq


/- a hypothesis oriented proof -/
example (h : P ∨ (Q ∨ R)) : (P ∨ Q) ∨ R := by
  disj_elim hp hqr from h
  disj_intro_left hpq from hp Q
  disj_intro_left hpqr from hpq R
  exact hpqr
  disj_elim hq hr from hqr
  disj_intro_right hpq from P hq
  disj_intro_left hpqr from hpq R
  exact hpqr
  disj_intro_right hpqr from (P∨Q) hr
  exact hpqr


/- a goal oriented proof -/
example (h : P ∨ (Q ∨ R)) : (P ∨ Q) ∨ R := by
  sorry