NanoProof

NanoProof is a tiny dependently typed proof checker in one Haskell file.

It supports:

• a single universe, *
• Pi, Sigma, equality, empty, unit, bit, and fixpoint types
• lambdas, pairs, pattern eliminators, recursive values, and local lets
• {==} reflexivity proofs
• %proof; body equality rewriting
• first-class guarded reduction views used consistently by printing, rewriting, and equality

NanoProof intentionally has no termination checker. Recursive definitions and fixpoints are accepted as written, so users are responsible for keeping them terminating or productive.

Install

ghc -O2 nanoproof.hs -o nanoproof
cp nanoproof ~/.local/bin/nanoproof

Make sure ~/.local/bin is on PATH.

Usage

Check a file:

nanoproof demo/mul_comm.npf

If the file defines @main, NanoProof prints its normalized value after the file checks.

Demo

demo/mul_comm.npf contains a Peano natural-number development and proves:

@mul_comm
: ∀@Nat. λa. ∀@Nat. λb.
  {((@mul a) b) = ((@mul b) a) : @Nat}

The demo’s @main instantiates this theorem at 2 and 3.

Syntax

Comments:

// line comment

Definitions:

@name : type = term;

Core forms:

*                         type of types
@name                     top-level reference
!x = value; body          local let
$x. body                  guarded recursive value
μx. body                  fixpoint
∀A. F                     Pi over an explicit family
λx. body                  lambda
(f x)                     application
ΣA. F                     Sigma over an explicit family
#(a,b)                    pair
~f                        pair eliminator
⊥                         empty type
λ{}                       empty eliminator
⊤                         unit type
()                        unit value
λ() body                  unit eliminator
𝔹                         bit type
0 / 1                     bit values
λ{0: a; 1: b;}            bit eliminator
{a = b : T}               equality type
{==}                      reflexivity proof
%proof; body              rewrite with an equality proof
↓source ~> reduct          guarded reduction view

Function application is binary and prefix:

((@mul x) y)

Pi and Sigma codomains are ordinary families. Constant codomains are written by returning the constant from a lambda:

∀@Nat. λx. @Nat
Σ@Nat. λx. @Nat