content: = Automated Theorem Proving =
  
  ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
  <p>
  <button id='swap'>swap</button>
  <button id='implies'>implies</button>
  <button id='demorgan'>De Morgan</button>
  <button id='lem'>De Morgan LEM</button>
  <button id='nnlem'>&not;&not;LEM</button>
  <button id='vorobev'>Vorobev</button>
  <button id='uncurry'>uncurry</button>
  <button id='jonk'>jonk</button>
  </p>
  <p><textarea id='in' rows='1' style='box-sizing:border-box;width:100%;'></textarea></p>
  <p><button id='go'>Prove</button></p>
  <p id='mathy'></p>
  <p><textarea id='out' rows='4' style='box-sizing:border-box;width:100%;'></textarea></p>
  ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
  
  Prove that for any propositions P and Q:
  
  [latexmath]
  +++++++++++
  (\neg P \vee Q) \rightarrow (P \rightarrow Q)
  +++++++++++
  
  Easy, right? Just enumerate all possibilities \(P = 0, 1\) and \(Q = 0, 1\),
  and check we always get \(1\). From this, we can mechanically derive a logical
  proof in a link:hilbert.html[Hilbert system]; see Emil Post, _Introduction to a
  general theory of elementary propositions_.
  
  ------------------------------------------------------------------------
  easy = all (== 1) [max (1 - p) q --> (p --> q) | p <- [0, 1], q <- [0, 1]]
  
  0 --> 0 = 1
  0 --> 1 = 1
  1 --> 0 = 0
  1 --> 1 = 1
  ------------------------------------------------------------------------
  
  Perhaps the toughest part is remembering the truth table for
  \((\rightarrow)\). It's odd that \(0 \rightarrow 1\) holds, that is, "false
  implies true". But it's odder still that we say "implies" for this symbol.
  Should we be saying things like: "a hydrogen atom contains two protons implies
  Beethoven wrote nine symphonies"?
  
  It sounds illogical because in everyday use, the word "implies" implies
  causation. How can a proposition imply an unrelated proposition? Yet banishing
  the word "implies" is out of the question, because logic ought to be able to
  deal with causality.
  
  We patch this discrepancy by replacing 0 and 1 with mathematical objects
  called _proofs_. We represent a proof with an abstract syntax tree (that turns
  out be a good old lambda term). Then a proof of \(P \rightarrow Q\) is a
  syntax tree representing a function that maps a proof of \(P\) to a proof of
  \(Q\). The word "implies" has regained its dignity: we can only say "\(P\)
  implies \(Q\)" if we show how evidence of \(P\) leads to evidence of \(Q\).
  
  Instead of truth tables, we build proofs (syntax trees) from other proofs. A
  proof of the conjunction \(P \wedge Q\) is a syntax tree representing the pair
  `(p, q)` where `p` is a proof of \(P\) and `q` is a proof of \(Q\). A proof of
  the disjunction \(P \vee Q\) is either the syntax tree `Left p` where `p` is a
  proof of \(P\) or `Right q` where `q` is a proof of \(Q\).
  
  As for negation, we define a proposition \(\bot\) and stipulate that a proof
  of \(\bot\) immediately yields a proof of any arbitrary proposition;
  https://en.wikipedia.org/wiki/Principle_of_explosion[the principle of
  explosion; ex falso quodlibet]. We define \(\neg P\) to be \(P \rightarrow
  \bot\).
  
  Apart from fixing "implies", our logic is also _intuitionistic_, which just
  means https://web.math.princeton.edu/~nelson/papers/rome.pdf[we've added
  accuracy to classical logic]. Roughly speaking, all the theorems are the same
  except that rather than prove \(\exists x P(x)\), we sometimes prove \(\neg
  \forall x \neg P(x)\), and similarly, rather than prove \(A \vee B\) we
  sometimes prove \(\neg(\neg A \wedge \neg B)\).
  
  Classical logic equates these formulas, while intuitionistic logic keeps them
  apart to gain one extra bit of information. This bit signals whether the proof
  is _constructive_.
  
  For example, in intuitionistic logic, the law of the excluded middle (LEM)
  when written as \(A \vee \neg A\) has no proof, but the classically equivalent
  \(\neg (A \wedge \neg A)\) does. A proof of the former would be a decision
  procedure, that is, it would describe an algorithm to construct a proof of
  \(A\) or a proof of \(\neg A\) from any given \(A\); a tall order. The latter
  merely states it is impossible to have both a proof of \(A\) and a proof of
  \(\neg A\).
  
  It's fun to split philosophical hairs, but we really went to all this trouble
  for practical reasons. If we can automatically generate a constructive proof
  of a given proposition, then we can automatically generate the source code of
  a function of a given type, a fact known as the Curry-Howard correspondence.
  
  == Too much too early ==
  
  We restrict ourselves to propositional logic; no predicates nor quantifiers.
  We know classical logic has a sound and complete decision procedure under
  these conditions based on truth tables. Can we adapt it for intuitionistic
  logic?
  
  Alas, our simple strategy is wildly inappropriate. Recall we tried two
  different values for each atomic proposition. Unfortunately, there are
  infinitely many abstract syntax trees, and even if we could magically try each
  one, what good would it do? Suppose we wish to prove \(P \rightarrow P\). Our
  goal is to find a function that takes a proof of \(P\) and returns a proof of
  \(P\). The identity function clearly does the job, but how would enumerating
  all possible proofs of \(P\) lead to it?
  
  We could try to enumerate all syntax trees, link:../lambda/hm.html[infer the
  type of each tree] as we go, and see if it happens to be the proposition we're
  trying to prove. However, besides being grossly inefficient, this procedure
  fails to terminate when no proof exists.
  
  Chapter 4 of https://www.cs.cmu.edu/~fp/courses/atp/handouts/atp.pdf[Frank
  Pfenning's notes] describes a strategy to find proofs in first-order logic
  based on _sequents_. We take the parts relevant to propositional logic.
  
  A sequent consists of:
  
    * a list of _antecedent_ propositions \(A_1, ..., A_n\) a _succedent_
    * proposition \(B\)
  
  and is written:
  
  [latexmath]
  +++++++++++
  A_1, ..., A_n \Rightarrow B
  +++++++++++
  
  This sequent means: "given proofs of the antecedent propositions
  \(A_1, ..., A_n\), we can produce a proof of \(B\)".
  
  Given a proposition \(B\) to prove, we start with a sequent meaning we can
  prove \(B\) with no assumptions:
  
  [latexmath]
  +++++++++++
  \Rightarrow B
  +++++++++++
  
  Then we apply one of the rules described below to transform it into one or
  more sequents that logically lead to this sequent.
  
  We recursively apply rules on these new sequents until we reach a self-evident
  sequent. There are two kinds of such sequents. Either we have an _initial
  sequent_:
  
  [latexmath]
  +++++++++++
  ..., P, ... \Rightarrow P
  +++++++++++
  
  which means we can produce a proof of \(P\) if given a proof of \(P\) (and
  possibly other proofs), or we have a sequent with \(\bot\) as an antecedent:
  
  [latexmath]
  +++++++++++
  ..., \bot, ... \Rightarrow P
  +++++++++++
  
  which is an incarnation of ex falso quodlibet.
  
  A rule preserving completeness is _invertible_; such a rule never changes a
  viable sequent into sequents that eventually get stuck. Otherwise the rule is
  _non-invertible_.
  
  The rules lead to the following algorithm. We partition the antecedent
  propositions into two lists: the _passive_ list and the _active_ list. Every
  antecedent proposition starts off in the active list. Then:
  
    1. Apply as many invertible rules as possible to the succedent.
    Pfenning calls these cases _right asynchronous_.
  
    2. Until the active list is empty, apply as many invertible rules as possible
    to the head of the list, then move the head to the passive list.
    Pfenning calls these cases _left asynchronous_.
  
    3. The active list is empty and we must choose a non-invertible rule.
    We branch on each such rule. We can apply standard strategies such as
    breadth-first search, depth-first search, or iterative deepening. Pfenning
    calls these cases _synchronous_.
  
  We've swept a potential problem under the rug. How can we avoid going around in
  circles as we apply these rules? It turns out, with one exception, all the
  rules are one-way. They each replace a sequent with simpler sequents.
  
  The problematic exception crops up in the last step. If we branch on an
  implication \(P \rightarrow Q\) in the passive list, then a new antecedent is
  added while no existing ones are removed, which means we may later choose to
  branch on the same implication again.
  
  If a proposition has a proof, then a breadth-first search will eventually find
  it, but in general, this algorithm might never terminate on a proposition with
  no proof.
  
  For now, we sacrifice completeness to address this, and remove an implication
  antecedent when exploring it. This guarantees termination, but prevents us
  from finding proofs of certain theorems such as \(\neg \neg (A \vee \neg A)\).
  We fix this later.
  
  Let's walk through a proof of our first example.
  
  [latexmath]
  +++++++++++
  \Rightarrow ((P \rightarrow\bot) \vee Q) \rightarrow (P \rightarrow Q)
  +++++++++++
  
  The succedent is an implication, so the corresponding rule yields:
  
  [latexmath]
  +++++++++++
  (P\rightarrow\bot) \vee Q \Rightarrow P \rightarrow Q
  +++++++++++
  
  The succedent is an implication again, so we get:
  
  [latexmath]
  +++++++++++
  (P\rightarrow\bot) \vee Q, P \Rightarrow Q
  +++++++++++
  
  The antecedent disjunction leads to the two sequents:
  
  [latexmath]
  +++++++++++
  P \rightarrow \bot , P \Rightarrow Q
  +++++++++++
  [latexmath]
  +++++++++++
  Q, P \Rightarrow Q
  +++++++++++
  
  The second sequent is an initial sequent, while the only way to progress from
  the first sequent is to apply a non-invertible rule to the antecedent
  implication, yielding two sequents:
  
  [latexmath]
  +++++++++++
  \bot , P \Rightarrow Q
  +++++++++++
  [latexmath]
  +++++++++++
  P \Rightarrow P
  +++++++++++
  
  The first sequent has a \(\bot\) antecedent, while the second is initial.
  We have successfully found a proof.
  
  Below, the `incompleteOracle` function determines if a proof exists via a
  depth-first search. Hopefully our code alone is enough to explain the rules.
  For example, the first rule states if the sequent has the form:
  
  [latexmath]
  +++++++++++
  A_1, ..., A_n \Rightarrow P \wedge Q
  +++++++++++
  
  then we recurse on:
  
  [latexmath]
  +++++++++++
  A_1, ..., A_n \Rightarrow P
  +++++++++++
  
  and:
  
  [latexmath]
  +++++++++++
  A_1, ..., A_n \Rightarrow Q
  +++++++++++
  
  A logician might summarize this as:
  
  [latexmath]
  +++++++++++
  \frac{\Gamma \Rightarrow P \quad \Gamma \Rightarrow Q} { \Gamma \Rightarrow P \wedge Q }
  +++++++++++
  
  where \(\Gamma\) is a list of antecedent propositions. Roughly speaking, this
  notation says that to prove the thing below the horizontal line, we can prove
  the things above the line.
  
  Since we classify the antecedents as passive or active, we ought to be more
  pedantic and split \(\Gamma\) into two lists; see Pfenning for details.
  
  ++++++++++
  <script>
  function hideshow(s) {
    var x = document.getElementById(s);
    if (x.style.display === "none") {
      x.style.display = "block";
    } else {
      x.style.display = "none";
    }
  }
  </script>
  <p><a onclick='hideshow("boilerplate");'>&#9654; Toggle boilerplate</a></p>
  <div id='boilerplate' style='display:none'>
  ++++++++++
  
  \begin{code}
  module Main where
  import Base
  import Charser
  import System
  foreign export ccall "main" main
  {- GHC edition:
  import Control.Applicative ((<**>))
  import Control.Arrow
  import Data.List
  import Data.Function ((&))
  import Text.Megaparsec hiding (match)
  import Text.Megaparsec.Char
  type Charser = Parsec () String
  -}
  \end{code}
  
  ++++++++++
  </div>
  ++++++++++
  
  \begin{code}
  data Prop = Var String
    | Prop :& Prop
    | Prop :| Prop
    | Prop :-> Prop
    | Falso deriving (Show, Eq)
  
  incompleteOracle :: Prop -> Bool
  incompleteOracle = rAsyn [] [] where
    rAsyn pas act rhs = case rhs of
      a :& b -> rAsyn pas act a && rAsyn pas act b
      a :-> b -> rAsyn pas (a:act) b
      _ -> lAsyn pas act rhs
  
    lAsyn pas (x:xs) rhs = case x of
      Falso -> True
      a :& b -> lAsyn pas (a:b:xs) rhs
      a :| b -> lAsyn pas (a:xs) rhs && lAsyn pas (b:xs) rhs
      _ -> lAsyn (x:pas) xs rhs
  
    lAsyn pas [] rhs = elem rhs pas || any implyCases pas || orCases
      where
      orCases = case rhs of
        a :| b -> rAsyn pas [] a || rAsyn pas [] b
        _ -> False
      implyCases p = case p of
        a :-> b -> lAsyn pas' [b] rhs && rAsyn pas' [] a
          where pas' = filter (/= p) pas
        _ -> False
  \end{code}
  
  We write a parser for propositions so we can easily test our code.
  We use Haskell notation:
  
    * The conjunction of `p` and `q` is written `(p, q)`.
    * The disjunction of `p` and `q` is written `Either p q`.
    * Implication is written `(->)` and associates right.
    * The proposition \(\bot\) is written `Void` (from the `Data.Void` package).
  
  \begin{code}
  propo :: Charser Prop
  propo = space *> aps <* eof where
    aps = foldr1 (:->) <$> sepBy1 arg (spstr "->")
    arg = Var <$> sp ((:) <$> lowerChar <*> many alphaNumChar)
      <|> between (spch '(') (spch ')') prodOrProp
      <|> const Falso <$> spstr "Void"
      <|> spstr "Either" *> ((:|) <$> arg <*> arg)
    prodOrProp = (&) <$> aps <*> (spch ',' *> (flip (:&) <$> aps) <|> pure id)
    sp :: Charser a -> Charser a
    sp = (<* space)
    spch = sp . char
    spstr = sp . string
  \end{code}
  
  Evaluating the following confirms we can find a proof of our first example:
  
  ------------------------------------------------------------------------
  incompleteOracle <$> parse propo "" "Either (p -> Void) q -> p -> q"
  ------------------------------------------------------------------------
  
  == Proof by construction ==
  
  Our program has discovered a truly remarkable proof of our theorem, but the
  Boolean return value is too small to contain it.
  
  We remedy this by building lambda terms instead of just indicating whether it's
  possible to do so. This requires assigning names to various propositions when
  we first encounter them; we pass around an integer to help generate unique
  names.
  
  We associate each proposition in the active and passive lists with a lambda
  term representing its proof.
  
  We take this opportunity to properly fix our problematic implication rule:
  
  [latexmath]
  +++++++++++
  \frac
    {A \rightarrow B,\Gamma\Rightarrow A \quad B,\Gamma\Rightarrow G }
    {A \rightarrow B,\Gamma\Rightarrow G}
  +++++++++++
  
  It turns out our prover is sound and complete if we replace it with these 4
  rules:
  
  [latexmath]
  +++++++++++
  \frac
    {B,A,\Gamma\Rightarrow G \quad \text{atomic }A }
    {A \rightarrow B,A,\Gamma\Rightarrow G}
  +++++++++++
  
  [latexmath]
  +++++++++++
  \frac
    {A\rightarrow (B\rightarrow C),\Gamma\Rightarrow G}
    {(A\wedge B)\rightarrow C,\Gamma\Rightarrow G}
  +++++++++++
  
  [latexmath]
  +++++++++++
  \frac
    {A\rightarrow C, B\rightarrow C,\Gamma\Rightarrow G}
    {(A\vee B)\rightarrow C,\Gamma\Rightarrow G}
  +++++++++++
  
  [latexmath]
  +++++++++++
  \frac
    {B\rightarrow C,\Gamma\Rightarrow A\rightarrow B \quad C,\Gamma\Rightarrow G}
    {(A\rightarrow B)\rightarrow C,\Gamma\Rightarrow G}
  +++++++++++
  
  The `prove` function below performs a depth-first search to find programs of a
  given type.
  
  \begin{code}
  data Proof = V String | Lam String Proof | Proof :@ Proof
  
  prove :: Prop -> [Proof]
  prove prop = snd <$> rAsyn 0 [] [] prop where
    rAsyn n pas act prop = case prop of
      a :-> b -> do
        let s = 'a':show n
        second (Lam s) <$> rAsyn (n + 1) pas ((V s, a):act) b
      a :& b -> do
        (n1, f) <- rAsyn n pas act a
        (n2, s) <- rAsyn n1 pas act b
        pure (n2, V "," :@ f :@ s)
      _ -> lAsyn n pas act prop
  \end{code}
  
  The first 3 new implication rules are invertible.
  The first of them triggers on two antecedents; if the current active antecedent
  matches one of the patterns, then we search for suitable companions matching
  the other pattern in the passive list. If there are any, we proceed with the
  first matching pair we find.
  
  We also drop antecedents of the form \(X \rightarrow X\), as these are
  superfluous.
  
  \begin{code}
    lAsyn n pas (pp@(prf, prop):ps) rhs = case prop of
      a :-> b | a == b -> lAsyn n pas ps rhs
      a@(Var _) :-> b | Just (prfA, _) <- find (\(_, a') -> a' == a) pas ->
        lAsyn n pas ((prf :@ prfA, b):ps) rhs
      a@(Var _) -> lAsyn n (pp:pas') (take 1 act' <> ps) rhs
        where
        (pas', act') = foldl partitionMatch ([], []) pas
        partitionMatch (ps, as) x
          | (prfImp, a'@(Var _) :-> b) <- x, a == a' = (ps, (prfImp :@ prf, b):as)
          | otherwise = (x:ps, as)
      (a :& b) :-> c -> lAsyn n pas
        ((V "curry" :@ prf, a :-> (b :-> c)):ps) rhs
      (a :| b) :-> c -> lAsyn n pas
        ((V "." :@ prf :@ V "Left", a :-> c)
        :(V "." :@ prf :@ V "Right", b :-> c):ps) rhs
  \end{code}
  
  The other invertible rules are straightforward:
  
  \begin{code}
      Falso  -> pure (n, V "absurd" :@ prf)
      a :& b -> lAsyn n pas ((V "fst" :@ prf, a):(V "snd" :@ prf, b):ps) rhs
      a :| b -> do
        let l = 'a':show n
        (n1, lp) <- lAsyn (n + 1) pas ((V l, a):ps) rhs
        let r = 'a':show n1
        (n2, rp) <- lAsyn (n1 + 1) pas ((V r, b):ps) rhs
        pure (n2, V "either" :@ Lam l lp :@ Lam r rp :@ prf)
      _ -> lAsyn n (pp:pas) ps rhs
  \end{code}
  
  It remains to describe the non-invertible rules:
  
  \begin{code}
    lAsyn n pas [] rhs = lguesses <> rguesses where
      lguesses = pas >>= \l -> lSyn n (filter (\p -> snd p /= snd l) pas) l rhs
      rguesses = case rhs of
        _ :| _ -> rSyn n pas rhs
        _ -> []
    rSyn n pas rhs = case rhs of
      a :| b -> as <> bs where
        as = second (V "Left" :@) <$> rSyn n pas a
        bs = second (V "Right" :@) <$> rSyn n pas b
      _ -> rAsyn n pas [] rhs
  \end{code}
  
  We've saved the the non-invertible implication rule for last. It relies on the
  theorem:
  
  [latexmath]
  +++++++++++
  \begin{align}
  ((A \rightarrow B) \rightarrow C) \rightarrow (A \rightarrow B) \\
  \iff (B \rightarrow C) \rightarrow (A \rightarrow B)
  \end{align}
  +++++++++++
  
  I had trouble finding the program corresponding to this rule, so I first coded
  our incomplete search from above:
  
  ------------------------------------------------------------------------
      a :-> b -> do
        let v = 'a':show n
        (n1, fArg) <- lAsyn (n + 1) pas [(prf :@ V v, b)] rhs
        (n2, arg) <- rSyn n1 pas a
        pure (n2, sub v arg fArg)
  ------------------------------------------------------------------------
  
  I ran it on one direction of the theorem:
  
  ------------------------------------------------------------------------
  prove <$> parse propo ""
    "((b -> c) -> (a -> b)) -> ((a -> b) -> c) -> (a -> b))"
  ------------------------------------------------------------------------
  
  which found:
  
  ------------------------------------------------------------------------
  Right [\a0 -> \a1 -> \a2 -> ((a0 \a5 -> (a1 \a7 -> a5)) a2)]
  ------------------------------------------------------------------------
  
  This lambda term is equivalent to:
  
  ------------------------------------------------------------------------
  \a0 -> \a1 -> a0 (a1 . const)
  ------------------------------------------------------------------------
  
  which teaches us how to generate the code for our fiddly implication rule:
  
  \begin{code}
    lSyn n pas (prf, l) rhs = if l == rhs then pure (n, prf) else case l of
      (a :-> b) :-> c -> do
        let v = 'a':show n
        (n1, fArg) <- lAsyn (n + 1) pas [(prf :@ V v, c)] rhs
        let w = 'a':show n1
        (n2, premiss1) <- rAsyn (n1 + 1) pas [(V w, b :-> c)] (a :-> b)
        let arg = sub w (V "." :@ prf :@ V "const") premiss1
        pure (n2, sub v arg fArg)
      _ -> []
  
  sub v arg f = case f of
    V s | v == s -> arg
    Lam s t -> Lam s $ rec t
    x :@ y -> rec x :@ rec y
    _ -> f
    where rec = sub v arg
  \end{code}
  
  We prettyprint the proofs so they look like Haskell programs.
  
  \begin{code}
  instance Show Proof where
    show prf = case prf of
      V s             -> s
      V "." :@ x :@ y -> "(" <> show x <> " . " <> show y <> ")"
      V "," :@ x :@ y -> "(" <> show x <> ", " <> show y <> ")"
      x@(Lam _ _) :@ y -> "((" <> show x <> ")" <> show y <> ")"
      x :@ y          -> "(" <> show x <> " " <> show y <> ")"
      Lam s t         -> "\\" <> s <> " -> " <> show t
  \end{code}
  
  Then:
  
  ------------------------------------------------------------------------
  prove <$> parse propo "" "Either (p -> Void) q -> p -> q"
  ------------------------------------------------------------------------
  
  gives the proof:
  
  ------------------------------------------------------------------------
  \a0 -> \a1 -> (((either \a2 -> (absurd (a2 a1))) \a3 -> a3) a0)
  ------------------------------------------------------------------------
  
  ++++++++++
  <p><a onclick='hideshow("ui");'>&#9654; Toggle UI code</a></p>
  <div id='ui' style='display:none'>
  ++++++++++
  
  \begin{code}
  showLogic :: Prop -> String
  showLogic p = case p of
    a :-> Falso -> "&not;" <> showLogic a
    a :-> b -> "(" <> showLogic a <> "&rarr;" <> showLogic b <> ")"
    a :& b -> "(" <> showLogic a <> "&and;" <> showLogic b <> ")"
    a :| b -> "(" <> showLogic a <> "&or;" <> showLogic b <> ")"
    Falso -> "&perp;"
    Var s -> s
  
  main = do
    s <- getContents
    case parse propo "" s of
      Left e -> putStr ":" >> putStr "parse error" >> putStr s
      Right p -> do
        putStr (showLogic p)
        putStr ":"
        putStr $ case prove p of
          [] -> "no proof found"
          prfs -> unlines $ show <$> prfs
  \end{code}
  ++++++++++
  </div>
  ++++++++++
  
  == Q.E.D. ==
  
  See Dyckhoff, _Contraction-Free Sequent Calculi for Intuitionistic Logic_,
  for why we replace the non-terminating rule with 4 rules. Dyckhoff attributes
  the underlying method to Vorobev, and mentions it's been rediscovered a few
  times.
  
  http://comcom.csail.mit.edu/comcom/#Synquid[Synquid uses refinement types] to
  automatically write programs that sort, or transform a Boolean formula to
  negation normal form (NNF). See also the other amazing provers on that website,
  as well as https://www.youtube.com/watch?v=HnOix9TFy1A[Nadia Polikarpova]'s talk.
  
  https://www.youtube.com/watch?reload=9&v=mOtKD7ml0NU[Idris 2 uses dependent
  types and linear types] to discover a function for performing matrix
  transposition.
  
  https://reasonablypolymorphic.com/blog/typeholes/[Sandy Maguire uses GHC's type
  holes to think less when programming]. But on his `jonk` example, the computer
  can in fact take over completely. We type in:
  
  ------------------------------------------------------------------------
  (a -> b) -> ((a -> i) -> i) -> ((b -> i) -> i)
  ------------------------------------------------------------------------
  
  and our prover finds:
  
  ------------------------------------------------------------------------
  \a0 -> \a1 -> \a2 -> (a1 \a5 -> (a2 (a0 a5)))
  ------------------------------------------------------------------------
  
  http://hackage.haskell.org/package/djinn[The Djinn tool] is similar to what we
  built, though has considerably more features.
  
  https://arxiv.org/abs/1805.07518[Michael Shulman describes an intimate
  connection between linear logic and constructive mathematics].
  
  ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
  <script>
  function setup(name, t) {
    function act() {
      document.getElementById("in").value = t;
      document.getElementById("out").value = "";
      document.getElementById("mathy").innerHTML = "";
    }
    document.getElementById(name).addEventListener("click", act);
    if (name == "implies") act();
  }
  setup("swap", "(a, b) -> (b, a)");
  setup("demorgan", "(a -> Void, b -> Void) -> Either a b -> Void");
  setup("implies", "Either (p -> Void) q -> p -> q");
  setup("lem", "(p, p -> Void) -> Void");
  setup("nnlem", "(Either p (p -> Void) -> Void) -> Void");
  setup("uncurry", "(a -> b -> c) -> (a, b) -> c");
  setup("vorobev", "(((a -> b) -> c) -> (a -> b)) -> ((b -> c) -> (a -> b))");
  setup("jonk", "(a -> b) -> ((a -> i) -> i) -> ((b -> i) -> i)");
  
  const ctx = {};
  function run() {
    ctx.inp = (new TextEncoder()).encode(document.getElementById("in").value);
    ctx.out = [], ctx.cursor = 0;
    ctx.instance.exports.main();
    const out = (new TextDecoder()).decode(Uint8Array.from(ctx.out)).split(':');
    document.getElementById("mathy").innerHTML = out[0];
    document.getElementById("out").value = out[1];
  }
  async function loadWasm() {
    try {
      ctx.instance = (await WebAssembly.instantiateStreaming(fetch('atp.wasm'), {env:
        { putchar: c  => ctx.out.push(c)
        , eof    : () => ctx.cursor == ctx.inp.length
        , getchar: () => ctx.inp[ctx.cursor++]
        }})).instance;
  
      document.getElementById("in").addEventListener("keydown", (event) => { if (event.key == "Enter") { run(); event.preventDefault(); }});
      document.getElementById("go").addEventListener("click", (event) => run());
    } catch(err) {
      console.log(err);
    }
  }
  loadWasm();
  </script>
  ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
  