VictorTaelin/nanoproof

Contribute to VictorTaelin/nanoproof development by creating an account on GitHub.

24 stars · 1 forks · 0 watchers

README

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

source

VictorTaelin/nanoproof: Contribute to VictorTaelin/nanoproof development by creating an account on GitHub.

VictorTaelin/nanoproof

README

Comments (0)