import cats._
import cats.instances._

sealed trait Proof[P]
case class QED[P]() extends Proof[P]

implicit val proofFunctor: Functor[Proof] = new Functor[Proof] {
  def map[A, B](fa: Proof[A])(f: A => B): Proof[B] = QED[B]()
}

implicit val proofApplicative: Applicative[Proof] = new Applicative[Proof] {
  def ap[A, B](ff: Proof[A => B])(fa: Proof[A]): Proof[B] = QED[B]()
  def pure[A](a: A): Proof[A] = QED[A]()
}

implicit val proofMonad: Monad[Proof] = new Monad[Proof] {
  def flatMap[A, B](fa: Proof[A])(f: A => Proof[B]): Proof[B] = QED[B]()
  def pure[A](a: A): Proof[A] = QED[A]()
  def tailRecM[A, B](a: A)(f: A => Proof[Either[A, B]]): Proof[B] = QED[B]()
}

case class :::[A, P](value: A)

sealed trait TRUE
sealed trait FALSE
sealed trait &&&[P, Q]
sealed trait |||[P, Q]
sealed trait -->[P, Q]
sealed trait Not[P]
sealed trait ===[P, Q]

def axiom[P]: Proof[P] = QED[P]()

def and_intro[P, Q](p: P)(q: Q): Proof[P &&& Q] = axiom
def and_elimL[P, Q](p_and_q: P &&& Q): Proof[P] = axiom
def and_elimR[P, Q](p_and_q: P &&& Q): Proof[Q] = axiom
def or_introL[P, Q](p: P): Proof[P ||| Q] = axiom
def or_introR[P, Q](q: Q): Proof[P ||| Q] = axiom
def impl_intro[P, Q](p_proves_q: P => Proof[Q]): Proof[P --> Q] = axiom
def impl_elim[P, Q](p_implies_q: P --> Q)(p: P): Proof[Q] = axiom
def not_intro[P](p_proves_false: P => Proof[FALSE]): Proof[Not[P]] = axiom
def contradicts[P](p: P)(not_p: Not[P]): Proof[FALSE] = axiom
def absurd[P](proof_of_false: FALSE): Proof[P] = axiom
def refl[P]: Proof[P === P] = axiom

type Theorem[P, Q] = (P --> Q) --> (Not[Q] --> Not[P])

def proof1[P, Q]: Proof[Theorem[P, Q]] = {
  impl_intro { p_implies_q => 
    impl_intro { not_q =>
      not_intro { p => 
        implicitly[Monad[Proof]].flatMap(impl_elim(p_implies_q)(p)) { q =>
          contradicts(q)(not_q)
        }
      }
    }
  }
}

println(proof1) // = QED()