Theorem Proving

Theorem Proving in a Makefile??

Tip

This demo is a variation on many others that are using inlined data and container-definitions and/or working with foreign languages. This is an instance of a custom containerized interpreter, and also demonstrates custom interpreter invocations.

Realistically most people are not sitting around and wondering whether they can prove Euclid¹ or Gödel² by using some wild matrioshka doll of a Makefile. But then again, people do get up to all kinds of weird things. 🤔

For the purposes of this demo, we'll use compose.mk to take the Lean4 prover for a test drive, and for starters just prove the law of the excluded middle.

It's fun, self-contained, and marginally practical! Partly because more academic tools like lean frequently do not have official containers =P, but mostly because this is part of a larger demo about notebooking.

Caveat

Note that this demo is big, and the lean/lake/mathlib toolchain here takes significant time to build, and the image on disk afterwards is ~10gb. If you're not interested in running the notebooking demo later then you may not want to run this one.

Lean Demo

The lean demo comes in 2 flavors. The first one is using compose.mk as a library, i.e. pure Makefile.

#!/usr/bin/env -S make -f
# Demonstrates an embedded container with a lean+mathlib container, 
# plus enough glue code for dispatch so that container usage is abstracted away.
# Included is a script and a theorem that we'll test with, but of course external files 
# are supported as well.
#
# Part of the `compose.mk` repo. This file runs as part of the test-suite.  
#
# USAGE: ./demos/lean.mk
# DOCS: http://robot-wranglers.github.io/compose.mk/demos/lean

include compose.mk

# Look, it's a minimal Dockerfile for running lean4 
# See also: https://leanprover-community.github.io/install/debian.html
define Dockerfile.Lean
FROM ${IMG_DEBIAN_BASE:-debian:bookworm-slim}
SHELL ["/bin/bash", "-x", "-c"]
RUN apt-get -qq update && apt-get install -qq -y git make curl sudo procps
RUN curl -sSf \
  https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
    > /usr/local/bin/elan-init.sh
RUN bash /usr/local/bin/elan-init.sh -y \
  --default-toolchain leanprover/lean4:v4.17.0
RUN cp /root/.elan/bin/lean /usr/local/bin 
RUN cp /root/.elan/bin/lake /usr/local/bin 
ENV PATH="$PATH:/root/.elan/bin/"
RUN lean --help
RUN lake new default
RUN cd default && \
  printf '[[require]]\nname = "mathlib"\nscope = "leanprover-community"' \
    >> lakefile.toml
RUN cd default && lake update && lake build
RUN elan --version; lean --version; leanc --version; lake --version; 
ENTRYPOINT ["lean"]
endef

# Look, it's hello-world in scriptwise lean-lang
# https://lean-lang.org/functional_programming_in_lean/hello-world/running-a-program.html
define my.script
def main : IO Unit := IO.println "Hello, world!"
endef

# Look, it's a theorem we might want to prove
# https://leanprover-community.github.io/logic_and_proof/classical_reasoning.html
# https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html
define my.theorem 
section
open Classical
example : A ∨ ¬ A := by
  apply byContradiction
  intro (h1 : ¬ (A ∨ ¬ A))
  have h2 : ¬ A := by
    intro (h3 : A)
    have h4 : A ∨ ¬ A := Or.inl h3
    show False
    exact h1 h4
  have h5 : A ∨ ¬ A := Or.inr h2
  show False
  exact h1 h5
end
endef

# Main entrypoint.  Ensures the container is ready, 
# then dispatches execution of both script and theorem
__main__: \
    Dockerfile.build/Lean \
    lean.run.script/my.script \
    lean.run.theorem/my.theorem

# Helpers that write embedded script/theorem to disk before use, 
# run them inside the container, and clean up afterwards.
lean.run.script/%:; lean_args="--run" ${make} lean.run.generic/${*}

lean.run.generic/% lean.run.theorem/%:
    ${io.mktemp} && ${make} mk.def.to.file/${*}/$${tmpf} \
    && img=Lean cmd="$${lean_args:-} $${tmpf}" \
        ${make} mk.docker

Lean Demo (CMK)

The 2nd version of the demo is mostly the same, but uses compose.mk as an interpreter, and is expressed in CMK-lang, which compiles to Makefile. This helps to clean up the syntax a bit and clarify intent.

#!/usr/bin/env -S ./compose.mk mk.interpret!
# CMK-lang translation of demos/lean.mk
#
# Part of the `compose.mk` repo. This file runs as part of the test-suite.  
#
# See also: http://robot-wranglers.github.io/compose.mk/demos/lean
#           http://robot-wranglers.github.io/compose.mk/demos/polyglots
#
# USAGE: ./demos/cmk/lean.cmk

# Look, a minimal Dockerfile for running lean4 
# See also: https://leanprover-community.github.io/install/debian.html
⫻ Dockerfile.Lean
FROM ${IMG_DEBIAN_BASE:-debian:bookworm-slim}
SHELL ["/bin/bash", "-x", "-c"]
RUN apt-get -qq update && apt-get install -qq -y git make curl sudo procps
RUN curl -sSf \
  https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
  > /usr/local/bin/elan-init.sh
RUN bash /usr/local/bin/elan-init.sh -y \
  --default-toolchain leanprover/lean4:v4.17.0
RUN cp /root/.elan/bin/lean /usr/local/bin 
RUN cp /root/.elan/bin/lake /usr/local/bin 
ENV PATH="$PATH:/root/.elan/bin/"
RUN lean --help
RUN lake new default
RUN cd default \
  && printf '[[require]]\nname = "mathlib"\nscope = "leanprover-community"' >> lakefile.toml
RUN cd default && lake update && lake build
RUN elan --version; lean --version; leanc --version; lake --version; 
ENTRYPOINT ["lean"]
⫻

# Look, it's hello-world in scriptwise lean-lang
# https://lean-lang.org/functional_programming_in_lean/hello-world/running-a-program.html
⟦ my.script
def main : IO Unit := IO.println "Hello, world!"
⟧ with lean.run.script as target

# Look, it's a theorem we might want to prove
# https://leanprover-community.github.io/logic_and_proof/classical_reasoning.html
# https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html
⟦ my.theorem 
section
open Classical
example : A ∨ ¬ A := by
  apply byContradiction
  intro (h1 : ¬ (A ∨ ¬ A))
  have h2 : ¬ A := by
    intro (h3 : A)
    have h4 : A ∨ ¬ A := Or.inl h3
    show False
    exact h1 h4
  have h5 : A ∨ ¬ A := Or.inr h2
  show False
  exact h1 h5
end
⟧ with lean.run.theorem as target

# Main entrypoint.  Ensures the container is ready, 
# then dispatches execution of both script and theorem
__main__: Lean.build my.theorem.run my.script.run

# Top-level helpers. 
# These write embedded script/theorem to disk before use, 
# run them inside the container, and clean up afterwards.
lean.run.script/%:; lean_args="--run" ${make} lean.run.generic/${*}

lean.run.generic/% lean.run.theorem/%:
    img=Lean cmd="$${lean_args:-} ${*}" ${make} mk.docker

Theorem Proving in a Makefile??

Lean Demo

Lean Demo (CMK)

References