Strict Proof Verification

It is straight-forward to write a mixed proof verifying some aspects of the proof and leaving the rest to plain English for the reader. For those so inclined, it is also possible to verify the entirety of the proof in LSTS. The first step for writing a strict proof is to declare the assumptions and the conclusion.

The Assumptions and Conclusion method of starting a proof fits conveniently into the form of a function definition. The arguments to the function become the assumptions. The return value of the function becomes the conclusion.

let some_proof <A:Integer,B:Odd,C:Prime> (
   assumption1: Property1<A,B>,
   assumption2: Property2<C> ):
   Conclusion<A,B,C> = {
   //Here we will derive the conclusion
   //starting from the assumptions
}

This code snippet can be read as

  1. for all quantified variables in the assumptions: A, B, C
  2. assume the given properties: Property1<A,B>, Property2<C>
  3. show that there exists a concluding result: Conclusion<A,B,C>

There is a strong relation between proofs and programs. This is a very direct relationship between proof objects and simple function declarations.

Proof Objects

In strict mode, LSTS will also produce a proof object. A proof object is a program that, when run, will attempt to reduce all logical statements made in the LSTS program. The proof object runs on a much simpler kernel of logical statements, so it may help expose some flaws that occur in higher-level logic. When run, the proof object will produce True, False, or diverge. Currently, for proof objects, we are targeting languages that closely resemble Lambda Calculus to make the translation easier.

// Creates a tree with `2^n` elements
(Gen 0) = (Leaf 1)
(Gen n) = (Node (Gen(- n 1)) (Gen(- n 1)))

// Adds all elements of a tree
(Sum (Leaf x))   = x
(Sum (Node a b)) = (+ (Sum a) (Sum b))

// Performs 2^n additions in parallel
(Main n) = (Sum (Gen n))
Copyright Andrew Johnson, 2023.