# proofery

> **⚠️ WORK IN PROGRESS - PROTOTYPE ⚠️**
>
> **This project is currently a prototype and proof verification is not yet rigorous.**
> 
> The verification logic is still under development and should not be relied upon for critical mathematical work. Use at your own risk for experimental purposes only.

A mathematical proof verifier.

## Overview

proofery is both a **command-line tool** and a **JavaScript/TypeScript library** that verifies mathematical proofs written in the `.prf` format. It parses proof content, checks the logical validity of theorem proofs, and reports any errors with helpful line numbers.

Use it as a CLI tool to verify `.prf` files, or import it as a library to integrate proof verification into your web applications or Node.js projects.

## Features

- **Full proof verification** - Supports all proof step types including:
  - `unpack-and`, `cases`, `witness`, `exact`
  - `calculate` with equational reasoning
  - `consider`, `forall-apply`, `deconstruct-exists`
  - `we-have`, `focus-or`, `define`, `assert`, `assert-goal`
- **Axiom and theorem management** - Collect and verify theorems based on axioms
- **Clear error messages** - Reports errors with line numbers
- **Verbose mode** - Optional detailed output during verification

## Installation

```bash
npm install proofery
```

Or use directly with npx (no installation required):

```bash
npx proofery example.prf
```

### Development Installation (from source)

If you want to contribute or modify the code:

```bash
git clone <repository-url>
cd proofery
npm install
npm run build
```

## Usage

### As a Command-Line Tool

#### Using npx (recommended)

```bash
# Basic usage
npx proofery example.prf

# With verbose output
npx proofery --verbose example.prf
```

#### Using global installation

```bash
# Install globally
npm install -g proofery

# Then use directly
proofery example.prf
proofery --verbose example.prf
```

**Command-line options:**
- `--verbose`, `-v` - Enable verbose output showing verification progress
- `--help`, `-h` - Display help message

### As a Library

First, install the package:

```bash
npm install proofery
```

#### In Node.js or TypeScript

```typescript
import { parseContent, verifyFile } from 'proofery';

const prfContent = `
axiom my_axiom
    suppose a : Nat
    conclude eq(a, a)

theorem reflexivity
    suppose x : Nat
    conclude eq(x, x)
    proof
        calculate x
            = x by-lhs my_axiom x
`;

try {
    const blocks = parseContent(prfContent);
    verifyFile(blocks, false);
    console.log('✓ Proof verified successfully!');
} catch (error) {
    console.error('Verification failed:', error.message);
}
```

#### Parsing from files in Node.js

```typescript
import { parseFileSync } from 'proofery/nodeParser';
import { verifyFile } from 'proofery';

const blocks = parseFileSync('example.prf');
verifyFile(blocks, true); // true for verbose output
```

#### In the Browser

You'll need to use a bundler like webpack, vite, or esbuild to use proofery in the browser:

```javascript
// Using a bundler (webpack, vite, etc.)
import { parseContent, verifyFile } from 'proofery';

function verifyProof() {
    const content = document.getElementById('proof-input').value;
    const resultDiv = document.getElementById('result');
    
    try {
        const blocks = parseContent(content);
        verifyFile(blocks, false);
        resultDiv.textContent = '✓ Proof verified successfully!';
        resultDiv.style.color = 'green';
    } catch (error) {
        resultDiv.textContent = '✗ Error: ' + error.message;
        resultDiv.style.color = 'red';
    }
}
```

For a complete browser example, see `examples/demo.html` in the repository.

#### Available Exports

```typescript
// Main functions
import { parseContent, verifyFile } from 'proofery';

// Node.js specific (file parsing)
import { parseFileSync } from 'proofery/nodeParser';

// Types
import { Block, Expression, Context } from 'proofery';

// Error classes
import { VerificationError, ParseError } from 'proofery';
```

## File Format

Proof files use the `.prf` extension and consist of:

- **Axioms** - Statements assumed to be true
- **Theorems** - Statements that must be proven

Each theorem includes:
- `suppose` blocks - Hypotheses and variable declarations
- `conclude` block - The goal to prove
- `proof` block - The proof steps

Example:

```
axiom associativity_of_addition
    suppose a : Nat
    suppose b : Nat
    suppose c : Nat
    conclude eq(add(add(a, b), c), add(a, add(b, c)))

theorem test1
    suppose a : Prop
    suppose b : Prop
    suppose h1 : a
    suppose h2 : b
    conclude and(a, b)
    proof
        unpack-and
            goal a
                proof
                    exact h1
            goal b
                proof
                    exact h2
```

For complete language reference, see the original `LANGUAGE_REFERENCE.md`.

## Development

Want to contribute? Clone the repository and install dependencies:

```bash
git clone <repository-url>
cd proofery
npm install
npm run build
```

### Project Structure

```
proofery/
├── src/
│   ├── index.ts              # Library entry point (exports)
│   ├── cli.ts                # CLI entry point
│   ├── nodeParser.ts         # Node.js file parser
│   ├── parser.ts             # .prf content parser
│   ├── verifier.ts           # Main proof verifier
│   ├── expression.ts         # Expression tree representation
│   ├── block.ts              # Block structure
│   ├── context.ts            # Context tracking
│   ├── simplifier.ts         # Expression simplification
│   ├── calculateVerifier.ts  # Calculate step verifier
│   └── errors.ts             # Custom error classes
├── examples/
│   └── example.prf           # Example proof file
├── package.json
├── tsconfig.json
└── README.md
```

### Building

```bash
npm run build
```

This compiles TypeScript to JavaScript in the `dist/` directory.

### Testing

Test the CLI:

```bash
npm run build
npx proofery --verbose examples/example.prf
```

Test the library API:

```bash
npm run build
node --input-type=module -e "
import { parseContent, verifyFile } from './dist/index.js';
import { readFileSync } from 'fs';
const content = readFileSync('examples/example.prf', 'utf-8');
const blocks = parseContent(content);
verifyFile(blocks, true);
console.log('\n✓ Library API test passed!');
"
```

## Differences from Python Version

This TypeScript implementation is a faithful port of the Python version with the following technical differences:

- Uses TypeScript's type system for enhanced type safety
- Uses `Map` instead of Python dictionaries for axiom/theorem storage
- Console output uses Node.js conventions
- File I/O uses Node.js `fs` module

The verification logic and proof language remain identical to the Python version.

## License

MIT

## Links

- [npm package](https://www.npmjs.com/package/proofery)
- [GitHub repository](https://github.com/magland/proofery)