Sign in
concept-collection / proofery
initial
Jeremy Magland <jmagland@flatironinstitute.org> committed commit 8eaa3f7e2e86 Browse files
19 changed files+2491−0
.gitignoreadded+42−0View file
@@ -0,0 +1,42 @@
1+# Dependencies
2+node_modules/
3+npm-debug.log*
4+yarn-debug.log*
5+yarn-error.log*
6+
7+# Build output
8+dist/
9+build/
10+*.tsbuildinfo
11+
12+# Testing
13+coverage/
14+*.lcov
15+.nyc_output/
16+
17+# IDE / Editor
18+.vscode/
19+.idea/
20+*.swp
21+*.swo
22+*~
23+.DS_Store
24+
25+# Environment variables
26+.env
27+.env.local
28+.env.*.local
29+
30+# Logs
31+logs/
32+*.log
33+
34+# OS
35+.DS_Store
36+Thumbs.db
37+
38+# Temporary files
39+*.tmp
40+.cache/
41+temp/
42+tmp/
LICENSEadded+21−0View file
@@ -0,0 +1,21 @@
1+MIT License
2+
3+Copyright (c) 2026
4+
5+Permission is hereby granted, free of charge, to any person obtaining a copy
6+of this software and associated documentation files (the "Software"), to deal
7+in the Software without restriction, including without limitation the rights
8+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
9+copies of the Software, and to permit persons to whom the Software is
10+furnished to do so, subject to the following conditions:
11+
12+The above copyright notice and this permission notice shall be included in all
13+copies or substantial portions of the Software.
14+
15+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
20+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
21+SOFTWARE.
README.mdadded+289−0View file
@@ -0,0 +1,289 @@
1+# proofery
2+
3+> **⚠️ WORK IN PROGRESS - PROTOTYPE ⚠️**
4+>
5+> **This project is currently a prototype and proof verification is not yet rigorous.**
6+>
7+> 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.
8+
9+A mathematical proof verifier.
10+
11+## Overview
12+
13+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.
14+
15+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.
16+
17+## Features
18+
19+- **Full proof verification** - Supports all proof step types including:
20+ - `unpack-and`, `cases`, `witness`, `exact`
21+ - `calculate` with equational reasoning
22+ - `consider`, `forall-apply`, `deconstruct-exists`
23+ - `we-have`, `focus-or`, `define`, `assert`, `assert-goal`
24+- **Axiom and theorem management** - Collect and verify theorems based on axioms
25+- **Clear error messages** - Reports errors with line numbers
26+- **Verbose mode** - Optional detailed output during verification
27+
28+## Installation
29+
30+```bash
31+npm install proofery
32+```
33+
34+Or use directly with npx (no installation required):
35+
36+```bash
37+npx proofery example.prf
38+```
39+
40+### Development Installation (from source)
41+
42+If you want to contribute or modify the code:
43+
44+```bash
45+git clone <repository-url>
46+cd proofery
47+npm install
48+npm run build
49+```
50+
51+## Usage
52+
53+### As a Command-Line Tool
54+
55+#### Using npx (recommended)
56+
57+```bash
58+# Basic usage
59+npx proofery example.prf
60+
61+# With verbose output
62+npx proofery --verbose example.prf
63+```
64+
65+#### Using global installation
66+
67+```bash
68+# Install globally
69+npm install -g proofery
70+
71+# Then use directly
72+proofery example.prf
73+proofery --verbose example.prf
74+```
75+
76+**Command-line options:**
77+- `--verbose`, `-v` - Enable verbose output showing verification progress
78+- `--help`, `-h` - Display help message
79+
80+### As a Library
81+
82+First, install the package:
83+
84+```bash
85+npm install proofery
86+```
87+
88+#### In Node.js or TypeScript
89+
90+```typescript
91+import { parseContent, verifyFile } from 'proofery';
92+
93+const prfContent = `
94+axiom my_axiom
95+ suppose a : Nat
96+ conclude eq(a, a)
97+
98+theorem reflexivity
99+ suppose x : Nat
100+ conclude eq(x, x)
101+ proof
102+ calculate x
103+ = x by-lhs my_axiom x
104+`;
105+
106+try {
107+ const blocks = parseContent(prfContent);
108+ verifyFile(blocks, false);
109+ console.log('✓ Proof verified successfully!');
110+} catch (error) {
111+ console.error('Verification failed:', error.message);
112+}
113+```
114+
115+#### Parsing from files in Node.js
116+
117+```typescript
118+import { parseFileSync } from 'proofery/nodeParser';
119+import { verifyFile } from 'proofery';
120+
121+const blocks = parseFileSync('example.prf');
122+verifyFile(blocks, true); // true for verbose output
123+```
124+
125+#### In the Browser
126+
127+You'll need to use a bundler like webpack, vite, or esbuild to use proofery in the browser:
128+
129+```javascript
130+// Using a bundler (webpack, vite, etc.)
131+import { parseContent, verifyFile } from 'proofery';
132+
133+function verifyProof() {
134+ const content = document.getElementById('proof-input').value;
135+ const resultDiv = document.getElementById('result');
136+
137+ try {
138+ const blocks = parseContent(content);
139+ verifyFile(blocks, false);
140+ resultDiv.textContent = '✓ Proof verified successfully!';
141+ resultDiv.style.color = 'green';
142+ } catch (error) {
143+ resultDiv.textContent = '✗ Error: ' + error.message;
144+ resultDiv.style.color = 'red';
145+ }
146+}
147+```
148+
149+For a complete browser example, see `examples/demo.html` in the repository.
150+
151+#### Available Exports
152+
153+```typescript
154+// Main functions
155+import { parseContent, verifyFile } from 'proofery';
156+
157+// Node.js specific (file parsing)
158+import { parseFileSync } from 'proofery/nodeParser';
159+
160+// Types
161+import { Block, Expression, Context } from 'proofery';
162+
163+// Error classes
164+import { VerificationError, ParseError } from 'proofery';
165+```
166+
167+## File Format
168+
169+Proof files use the `.prf` extension and consist of:
170+
171+- **Axioms** - Statements assumed to be true
172+- **Theorems** - Statements that must be proven
173+
174+Each theorem includes:
175+- `suppose` blocks - Hypotheses and variable declarations
176+- `conclude` block - The goal to prove
177+- `proof` block - The proof steps
178+
179+Example:
180+
181+```
182+axiom associativity_of_addition
183+ suppose a : Nat
184+ suppose b : Nat
185+ suppose c : Nat
186+ conclude eq(add(add(a, b), c), add(a, add(b, c)))
187+
188+theorem test1
189+ suppose a : Prop
190+ suppose b : Prop
191+ suppose h1 : a
192+ suppose h2 : b
193+ conclude and(a, b)
194+ proof
195+ unpack-and
196+ goal a
197+ proof
198+ exact h1
199+ goal b
200+ proof
201+ exact h2
202+```
203+
204+For complete language reference, see the original `LANGUAGE_REFERENCE.md`.
205+
206+## Development
207+
208+Want to contribute? Clone the repository and install dependencies:
209+
210+```bash
211+git clone <repository-url>
212+cd proofery
213+npm install
214+npm run build
215+```
216+
217+### Project Structure
218+
219+```
220+proofery/
221+├── src/
222+│ ├── index.ts # Library entry point (exports)
223+│ ├── cli.ts # CLI entry point
224+│ ├── nodeParser.ts # Node.js file parser
225+│ ├── parser.ts # .prf content parser
226+│ ├── verifier.ts # Main proof verifier
227+│ ├── expression.ts # Expression tree representation
228+│ ├── block.ts # Block structure
229+│ ├── context.ts # Context tracking
230+│ ├── simplifier.ts # Expression simplification
231+│ ├── calculateVerifier.ts # Calculate step verifier
232+│ └── errors.ts # Custom error classes
233+├── examples/
234+│ └── example.prf # Example proof file
235+├── package.json
236+├── tsconfig.json
237+└── README.md
238+```
239+
240+### Building
241+
242+```bash
243+npm run build
244+```
245+
246+This compiles TypeScript to JavaScript in the `dist/` directory.
247+
248+### Testing
249+
250+Test the CLI:
251+
252+```bash
253+npm run build
254+npx proofery --verbose examples/example.prf
255+```
256+
257+Test the library API:
258+
259+```bash
260+npm run build
261+node --input-type=module -e "
262+import { parseContent, verifyFile } from './dist/index.js';
263+import { readFileSync } from 'fs';
264+const content = readFileSync('examples/example.prf', 'utf-8');
265+const blocks = parseContent(content);
266+verifyFile(blocks, true);
267+console.log('\n✓ Library API test passed!');
268+"
269+```
270+
271+## Differences from Python Version
272+
273+This TypeScript implementation is a faithful port of the Python version with the following technical differences:
274+
275+- Uses TypeScript's type system for enhanced type safety
276+- Uses `Map` instead of Python dictionaries for axiom/theorem storage
277+- Console output uses Node.js conventions
278+- File I/O uses Node.js `fs` module
279+
280+The verification logic and proof language remain identical to the Python version.
281+
282+## License
283+
284+MIT
285+
286+## Links
287+
288+- [npm package](https://www.npmjs.com/package/proofery)
289+- [GitHub repository](https://github.com/magland/proofery)
examples/demo.htmladded+150−0View file
@@ -0,0 +1,150 @@
1+<!DOCTYPE html>
2+<html lang="en">
3+<head>
4+ <meta charset="UTF-8">
5+ <meta name="viewport" content="width=device-width, initial-scale=1.0">
6+ <title>Proofery Demo - Browser Example</title>
7+ <style>
8+ body {
9+ font-family: 'Segoe UI', Tahoma, Geneva, Verdana, sans-serif;
10+ max-width: 900px;
11+ margin: 40px auto;
12+ padding: 20px;
13+ background-color: #f5f5f5;
14+ }
15+ h1 {
16+ color: #333;
17+ }
18+ .container {
19+ background: white;
20+ padding: 30px;
21+ border-radius: 8px;
22+ box-shadow: 0 2px 10px rgba(0,0,0,0.1);
23+ }
24+ textarea {
25+ width: 100%;
26+ height: 300px;
27+ font-family: 'Courier New', monospace;
28+ font-size: 14px;
29+ padding: 10px;
30+ border: 2px solid #ddd;
31+ border-radius: 4px;
32+ box-sizing: border-box;
33+ resize: vertical;
34+ }
35+ textarea:focus {
36+ outline: none;
37+ border-color: #4CAF50;
38+ }
39+ button {
40+ background-color: #4CAF50;
41+ color: white;
42+ padding: 12px 30px;
43+ font-size: 16px;
44+ border: none;
45+ border-radius: 4px;
46+ cursor: pointer;
47+ margin-top: 15px;
48+ }
49+ button:hover {
50+ background-color: #45a049;
51+ }
52+ button:active {
53+ transform: translateY(1px);
54+ }
55+ #result {
56+ margin-top: 20px;
57+ padding: 15px;
58+ border-radius: 4px;
59+ font-family: 'Courier New', monospace;
60+ white-space: pre-wrap;
61+ min-height: 50px;
62+ }
63+ .success {
64+ background-color: #d4edda;
65+ color: #155724;
66+ border: 1px solid #c3e6cb;
67+ }
68+ .error {
69+ background-color: #f8d7da;
70+ color: #721c24;
71+ border: 1px solid #f5c6cb;
72+ }
73+ .instructions {
74+ background-color: #fff3cd;
75+ padding: 15px;
76+ border-radius: 4px;
77+ margin-bottom: 20px;
78+ border: 1px solid #ffeaa7;
79+ }
80+ .instructions p {
81+ margin: 5px 0;
82+ }
83+ </style>
84+</head>
85+<body>
86+ <div class="container">
87+ <h1>🔍 Proofery - Browser Demo</h1>
88+
89+ <div class="instructions">
90+ <strong>Instructions:</strong>
91+ <p>1. Build the project: <code>npm run build</code></p>
92+ <p>2. Serve this file with a local HTTP server (can't use file:// due to ES modules)</p>
93+ <p>3. Edit the proof below and click "Verify Proof"</p>
94+ </div>
95+
96+ <h2>Enter your proof:</h2>
97+ <textarea id="proof-input">axiom test_axiom
98+ suppose a : Nat
99+ conclude eq(a, a)
100+
101+theorem simple_test
102+ suppose x : Nat
103+ suppose y : Nat
104+ suppose h : and(eq(x, x), eq(y, y))
105+ conclude and(eq(x, x), eq(y, y))
106+ proof
107+ exact h</textarea>
108+
109+ <button onclick="verifyProof()">Verify Proof</button>
110+
111+ <div id="result"></div>
112+ </div>
113+
114+ <script type="module">
115+ // Import the library - adjust path based on your server setup
116+ import { parseContent, verifyFile, VerificationError, ParseError } from '../dist/index.js';
117+
118+ window.verifyProof = function() {
119+ const content = document.getElementById('proof-input').value;
120+ const resultDiv = document.getElementById('result');
121+
122+ // Clear previous result
123+ resultDiv.className = '';
124+ resultDiv.textContent = 'Verifying...';
125+
126+ try {
127+ const blocks = parseContent(content);
128+ verifyFile(blocks, false);
129+
130+ resultDiv.className = 'success';
131+ resultDiv.textContent = '✓ Proof verified successfully!';
132+ } catch (error) {
133+ resultDiv.className = 'error';
134+ if (error instanceof VerificationError) {
135+ resultDiv.textContent = '✗ Verification Error:\n\n' + error.message;
136+ } else if (error instanceof ParseError) {
137+ resultDiv.textContent = '✗ Parse Error:\n\n' + error.message;
138+ } else {
139+ resultDiv.textContent = '✗ Unexpected Error:\n\n' + error.message;
140+ }
141+ }
142+ };
143+
144+ // Verify on load
145+ window.addEventListener('load', () => {
146+ console.log('Proofery demo loaded. Library imported successfully!');
147+ });
148+ </script>
149+</body>
150+</html>
examples/example.prfadded+178−0View file
@@ -0,0 +1,178 @@
1+axiom associativity_of_multiplication
2+ suppose a : Nat
3+ suppose b : Nat
4+ suppose c : Nat
5+ conclude eq(mult(mult(a, b), c), mult(a, mult(b, c)))
6+
7+axiom idempotence_of_one
8+ suppose a : Nat
9+ conclude eq(mult(1, a), a)
10+
11+axiom distributive_property_of_multiplication_over_addition
12+ suppose a : Nat
13+ suppose b : Nat
14+ suppose c : Nat
15+ conclude eq(mult(add(a, b), c), add(mult(a, c), mult(b, c)))
16+
17+axiom associativity_of_addition
18+ suppose a : Nat
19+ suppose b : Nat
20+ suppose c : Nat
21+ conclude eq(add(add(a, b), c), add(a, add(b, c)))
22+
23+axiom arithmetic1
24+ conclude eq(add(1, 1), 2)
25+
26+# If a and b are propositions, and a and b are both true,
27+# then a and b is true.
28+theorem test1
29+ suppose a : Prop
30+ suppose b : Prop
31+ suppose h1 : a
32+ suppose h2 : b
33+ conclude and(a, b)
34+ proof
35+ unpack-and
36+ goal a
37+ proof
38+ exact h1
39+ goal b
40+ proof
41+ exact h2
42+
43+# If a and b are propositions, and a and b are both true,
44+# then a and b and a is true.
45+theorem test2
46+ suppose a : Prop
47+ suppose b : Prop
48+ suppose h1 : a
49+ suppose h2 : b
50+ conclude and(a, and(b, a))
51+ proof
52+ unpack-and
53+ goal a
54+ proof
55+ exact h1
56+ goal and(b, a)
57+ proof
58+ unpack-and
59+ goal b
60+ proof
61+ exact h2
62+ goal a
63+ proof
64+ exact h1
65+
66+# If a and (b or c) are true,
67+# then (a and b) or (a and c) is true.
68+theorem test3
69+ suppose a : Prop
70+ suppose b : Prop
71+ suppose c : Prop
72+ suppose h : and(a, or(b, c))
73+ conclude or(and(a, b), and(a, c))
74+ proof
75+ we-have or_b_c : or(b, c)
76+ proof
77+ exact right(h)
78+ cases or_b_c
79+ case h_b : b
80+ proof
81+ assert-goal or(and(a, b), and(a, c))
82+ focus-or left
83+ assert-goal and(a, b)
84+ unpack-and
85+ goal a
86+ proof
87+ exact left(h)
88+ goal b
89+ proof
90+ exact h_b
91+ case h_c : c
92+ proof
93+ assert-goal or(and(a, b), and(a, c))
94+ focus-or right
95+ assert-goal and(a, c)
96+ unpack-and
97+ goal a
98+ proof
99+ exact left(h)
100+ goal c
101+ proof
102+ exact h_c
103+
104+# If there exists a natural number n such that P n is true,
105+# then there exists a natural number a such that P a is true.
106+theorem existence
107+ suppose P : func(Nat, Prop)
108+ suppose n : Nat
109+ suppose h : apply(P, n)
110+ conclude exists(a : Nat, apply(P, a))
111+ proof
112+ witness n
113+ assert-goal apply(P, n)
114+ exact h
115+
116+# If n is an even natural number,
117+# then n + 2 is also an even natural number.
118+theorem abc
119+ suppose n : Nat
120+ suppose h : exists(m : Nat, eq(n, mult(m, 2)))
121+ conclude exists(q : Nat, eq(add(n, 2), mult(q, 2)))
122+ proof
123+ deconstruct-exists h m h_m
124+ assert h_m : eq(n, mult(m, 2))
125+ define d_q : eq(q, add(m, 1))
126+ witness q
127+ assert-goal eq(add(n, 2), mult(q, 2))
128+ calculate add(n, 2)
129+ = add(mult(m, 2), 2) by-lhs h_m
130+ = add(mult(m, 2), mult(1, 2)) by-rhs idempotence_of_one 2
131+ = mult(add(m, 1), 2) by-rhs distributive_property_of_multiplication_over_addition m 1 2
132+ = mult(q, 2) by-rhs d_q
133+
134+# If for every natural number n there exists a natural number m such that m = n + 1,
135+# then for every natural number t there exists a natural number u such that u = t + 2.
136+theorem forall2
137+ suppose h : forall(n : Nat, exists(s : Nat, eq(s, add(n, 1))))
138+ conclude forall(t : Nat, exists(u : Nat, eq(u, add(t, 2))))
139+ proof
140+ consider t
141+ assert-goal exists(u : Nat, eq(u, add(t, 2)))
142+ forall-apply h t h2
143+ assert h2 : exists(s : Nat, eq(s, add(t, 1)))
144+ deconstruct-exists h2 m h_m
145+ assert h_m : eq(m, add(t, 1))
146+ forall-apply h m h3
147+ assert h3 : exists(s : Nat, eq(s, add(m, 1)))
148+ deconstruct-exists h3 u h_u
149+ assert h_u: eq(u, add(m, 1))
150+ witness u
151+ assert-goal eq(u, add(t, 2))
152+ calculate u
153+ = add(m, 1) by-lhs h_u
154+ = add(add(t, 1), 1) by-lhs h_m
155+ = add(t, add(1, 1)) by-lhs associativity_of_addition t 1 1
156+ = add(t, 2) by-lhs arithmetic1
157+
158+# If m divides n and n divides p, then m divides p.
159+theorem divides_transitive
160+ suppose m : Nat
161+ suppose n : Nat
162+ suppose p : Nat
163+ suppose h1 : exists(k1 : Nat, eq(n, mult(m, k1)))
164+ suppose h2 : exists(k2 : Nat, eq(p, mult(n, k2)))
165+ conclude exists(k3 : Nat, eq(p, mult(m, k3)))
166+ proof
167+ deconstruct-exists h1 k1 h_n
168+ assert h_n : eq(n, mult(m, k1))
169+ deconstruct-exists h2 k2 h_p
170+ assert h_p : eq(p, mult(n, k2))
171+ define d_k3 : eq(k3, mult(k1, k2))
172+ witness k3
173+ assert-goal eq(p, mult(m, k3))
174+ calculate p
175+ = mult(n, k2) by-lhs h_p
176+ = mult(mult(m, k1), k2) by-lhs h_n
177+ = mult(m, mult(k1, k2)) by-lhs associativity_of_multiplication m k1 k2
178+ = mult(m, k3) by-rhs d_k3
package-lock.jsonadded+54−0View file
@@ -0,0 +1,54 @@
1+{
2+ "name": "proofery",
3+ "version": "0.1.0",
4+ "lockfileVersion": 3,
5+ "requires": true,
6+ "packages": {
7+ "": {
8+ "name": "proofery",
9+ "version": "0.1.0",
10+ "license": "MIT",
11+ "bin": {
12+ "proofery": "dist/cli.js"
13+ },
14+ "devDependencies": {
15+ "@types/node": "^20.0.0",
16+ "typescript": "^5.3.0"
17+ },
18+ "engines": {
19+ "node": ">=18.0.0"
20+ }
21+ },
22+ "node_modules/@types/node": {
23+ "version": "20.19.27",
24+ "resolved": "https://registry.npmjs.org/@types/node/-/node-20.19.27.tgz",
25+ "integrity": "sha512-N2clP5pJhB2YnZJ3PIHFk5RkygRX5WO/5f0WC08tp0wd+sv0rsJk3MqWn3CbNmT2J505a5336jaQj4ph1AdMug==",
26+ "dev": true,
27+ "license": "MIT",
28+ "dependencies": {
29+ "undici-types": "~6.21.0"
30+ }
31+ },
32+ "node_modules/typescript": {
33+ "version": "5.9.3",
34+ "resolved": "https://registry.npmjs.org/typescript/-/typescript-5.9.3.tgz",
35+ "integrity": "sha512-jl1vZzPDinLr9eUt3J/t7V6FgNEw9QjvBPdysz9KfQDD41fQrC2Y4vKQdiaUpFT4bXlb1RHhLpp8wtm6M5TgSw==",
36+ "dev": true,
37+ "license": "Apache-2.0",
38+ "bin": {
39+ "tsc": "bin/tsc",
40+ "tsserver": "bin/tsserver"
41+ },
42+ "engines": {
43+ "node": ">=14.17"
44+ }
45+ },
46+ "node_modules/undici-types": {
47+ "version": "6.21.0",
48+ "resolved": "https://registry.npmjs.org/undici-types/-/undici-types-6.21.0.tgz",
49+ "integrity": "sha512-iwDZqg0QAGrg9Rav5H4n0M64c3mkR59cJ6wQp+7C4nI0gsmExaedaYLNO44eT4AtBBwjbTiGPMlt2Md0T9H9JQ==",
50+ "dev": true,
51+ "license": "MIT"
52+ }
53+ }
54+}
package.jsonadded+48−0View file
@@ -0,0 +1,48 @@
1+{
2+ "name": "proofery",
3+ "version": "0.1.0",
4+ "description": "A mathematical proof verifier written in TypeScript",
5+ "type": "module",
6+ "main": "dist/index.js",
7+ "types": "dist/index.d.ts",
8+ "bin": {
9+ "proofery": "./dist/cli.js"
10+ },
11+ "exports": {
12+ ".": {
13+ "types": "./dist/index.d.ts",
14+ "require": "./dist/index.js",
15+ "import": "./dist/index.js"
16+ },
17+ "./nodeParser": {
18+ "types": "./dist/nodeParser.d.ts",
19+ "require": "./dist/nodeParser.js",
20+ "import": "./dist/nodeParser.js"
21+ }
22+ },
23+ "files": [
24+ "dist",
25+ "README.md",
26+ "LICENSE"
27+ ],
28+ "scripts": {
29+ "build": "tsc",
30+ "start": "node dist/index.js",
31+ "dev": "tsc && node dist/index.js"
32+ },
33+ "keywords": [
34+ "proof",
35+ "verification",
36+ "mathematics",
37+ "theorem"
38+ ],
39+ "author": "Jeremy Magland",
40+ "license": "MIT",
41+ "devDependencies": {
42+ "@types/node": "^20.0.0",
43+ "typescript": "^5.3.0"
44+ },
45+ "engines": {
46+ "node": ">=18.0.0"
47+ }
48+}
src/block.tsadded+27−0View file
@@ -0,0 +1,27 @@
1+/**
2+ * Block representation for proof structure.
3+ */
4+
5+import { Expression } from './expression.js';
6+
7+/**
8+ * Represents a block in the proof tree.
9+ */
10+export class Block {
11+ constructor(
12+ public readonly lineNum: number,
13+ public readonly blockType: string,
14+ public readonly args: Expression[] = [],
15+ public children: Block[] = []
16+ ) {}
17+
18+ /**
19+ * String representation of the block.
20+ */
21+ toString(): string {
22+ const argsStr = this.args.length > 0
23+ ? ` ${this.args.map(a => a.toString()).join(' ')}`
24+ : '';
25+ return `${this.blockType}${argsStr}`;
26+ }
27+}
src/calculateVerifier.tsadded+304−0View file
@@ -0,0 +1,304 @@
1+/**
2+ * Verification logic for calculate blocks.
3+ */
4+
5+import { Block } from './block.js';
6+import { Expression } from './expression.js';
7+import { Context } from './context.js';
8+import { VerificationError } from './errors.js';
9+import { simplify } from './simplifier.js';
10+
11+/**
12+ * Verify a calculate block and return true if goal is resolved.
13+ */
14+export function verifyCalculate(
15+ step: Block,
16+ context: Context,
17+ axiomsAndTheorems: Map<string, Block>
18+): boolean {
19+ // 1. Validate that the goal is an equality
20+ if (context.goal === null) {
21+ throw new VerificationError(`Line ${step.lineNum}: No goal for calculate`);
22+ }
23+
24+ if (context.goal.name !== 'eq' || context.goal.children.length !== 2) {
25+ throw new VerificationError(
26+ `Line ${step.lineNum}: Goal must be eq(a, b), got ${context.goal}`
27+ );
28+ }
29+
30+ const initialExpr = context.goal.children[0];
31+ const finalExpr = context.goal.children[1];
32+
33+ // 2. Validate calculate structure
34+ if (step.args.length !== 1) {
35+ throw new VerificationError(
36+ `Line ${step.lineNum}: 'calculate' must have exactly one argument (initial expression)`
37+ );
38+ }
39+
40+ const calcInitial = step.args[0];
41+ if (!calcInitial.equals(initialExpr)) {
42+ throw new VerificationError(
43+ `Line ${step.lineNum}: Calculate initial expression ${calcInitial} does not match goal LHS ${initialExpr}`
44+ );
45+ }
46+
47+ if (step.children.length === 0) {
48+ throw new VerificationError(
49+ `Line ${step.lineNum}: Calculate block must have at least one step`
50+ );
51+ }
52+
53+ // 3. Process each calculation step
54+ let currentExpr = initialExpr;
55+
56+ for (const child of step.children) {
57+ if (child.blockType !== '=') {
58+ throw new VerificationError(
59+ `Line ${child.lineNum}: Calculate children must be '=' blocks, got '${child.blockType}'`
60+ );
61+ }
62+
63+ currentExpr = verifyCalcStep(child, currentExpr, context, axiomsAndTheorems);
64+ }
65+
66+ // 4. Final check: current expression should equal goal's RHS
67+ if (!currentExpr.equals(finalExpr)) {
68+ throw new VerificationError(
69+ `Line ${step.lineNum}: Calculate final expression ${currentExpr} does not match goal RHS ${finalExpr}`
70+ );
71+ }
72+
73+ return true; // Goal resolved
74+}
75+
76+/**
77+ * Verify a single calculation step and return the new expression.
78+ */
79+function verifyCalcStep(
80+ step: Block,
81+ prevExpr: Expression,
82+ context: Context,
83+ axiomsAndTheorems: Map<string, Block>
84+): Expression {
85+ if (step.args.length < 2) {
86+ throw new VerificationError(
87+ `Line ${step.lineNum}: '=' must have at least 2 arguments (new_expr and justification)`
88+ );
89+ }
90+
91+ const newExpr = step.args[0];
92+ const justificationType = step.args[1].name;
93+
94+ if (step.args[1].children.length > 0) {
95+ throw new VerificationError(
96+ `Line ${step.lineNum}: Justification type must be a simple identifier (by-lhs or by-rhs)`
97+ );
98+ }
99+
100+ // Get the equation (lhs, rhs) based on justification
101+ const remainingArgs = step.args.slice(2);
102+ let lhs: Expression, rhs: Expression;
103+
104+ if (justificationType === 'by-lhs') {
105+ [lhs, rhs] = getEquationForJustification(step, context, axiomsAndTheorems, remainingArgs);
106+ // by-lhs: verify that prevExpr can be transformed to newExpr by replacing lhs with rhs where needed
107+ if (!verifyTransformation(prevExpr, newExpr, lhs, rhs)) {
108+ throw new VerificationError(
109+ `Line ${step.lineNum}: Cannot transform ${prevExpr} to ${newExpr} using by-lhs ${lhs} = ${rhs}`
110+ );
111+ }
112+ } else if (justificationType === 'by-rhs') {
113+ [lhs, rhs] = getEquationForJustification(step, context, axiomsAndTheorems, remainingArgs);
114+ // by-rhs: verify that prevExpr can be transformed to newExpr by replacing rhs with lhs where needed
115+ if (!verifyTransformation(prevExpr, newExpr, rhs, lhs)) {
116+ throw new VerificationError(
117+ `Line ${step.lineNum}: Cannot transform ${prevExpr} to ${newExpr} using by-rhs ${lhs} = ${rhs}`
118+ );
119+ }
120+ } else {
121+ throw new VerificationError(
122+ `Line ${step.lineNum}: Unknown justification type '${justificationType}', expected 'by-lhs' or 'by-rhs'`
123+ );
124+ }
125+
126+ return newExpr;
127+}
128+
129+/**
130+ * Get the (lhs, rhs) equation from either a variable or axiom/theorem.
131+ */
132+function getEquationForJustification(
133+ step: Block,
134+ context: Context,
135+ axiomsAndTheorems: Map<string, Block>,
136+ args: Expression[]
137+): [Expression, Expression] {
138+ if (args.length === 0) {
139+ throw new VerificationError(
140+ `Line ${step.lineNum}: Justification requires at least one argument`
141+ );
142+ }
143+
144+ const firstArg = args[0];
145+
146+ // First argument must be a simple identifier
147+ if (firstArg.children.length > 0) {
148+ throw new VerificationError(
149+ `Line ${step.lineNum}: First justification argument must be a simple identifier (variable or axiom name)`
150+ );
151+ }
152+
153+ const name = firstArg.name;
154+
155+ // Check if it's a variable in context (with only one arg total)
156+ if (args.length === 1 && context.hasVariable(name)) {
157+ // This is a variable reference
158+ return getEquationFromVariable(step, name, context);
159+ }
160+
161+ // Otherwise, treat it as an axiom/theorem
162+ const axiomArgs = args.slice(1); // Remaining args are the axiom arguments
163+ return getEquationFromAxiom(step, name, axiomArgs, context, axiomsAndTheorems);
164+}
165+
166+/**
167+ * Extract (lhs, rhs) from a variable with type eq(lhs, rhs).
168+ */
169+function getEquationFromVariable(
170+ step: Block,
171+ varName: string,
172+ context: Context
173+): [Expression, Expression] {
174+ if (!context.hasVariable(varName)) {
175+ throw new VerificationError(
176+ `Line ${step.lineNum}: Variable '${varName}' not in context`
177+ );
178+ }
179+
180+ const varType = context.getVariableType(varName)!;
181+
182+ if (varType.name !== 'eq' || varType.children.length !== 2) {
183+ throw new VerificationError(
184+ `Line ${step.lineNum}: Variable '${varName}' must have type eq(a, b), got ${varType}`
185+ );
186+ }
187+
188+ return [varType.children[0], varType.children[1]];
189+}
190+
191+/**
192+ * Extract (lhs, rhs) from an axiom/theorem after substituting arguments.
193+ */
194+function getEquationFromAxiom(
195+ step: Block,
196+ axiomName: string,
197+ args: Expression[],
198+ context: Context,
199+ axiomsAndTheorems: Map<string, Block>
200+): [Expression, Expression] {
201+ if (!axiomsAndTheorems.has(axiomName)) {
202+ throw new VerificationError(
203+ `Line ${step.lineNum}: Axiom or theorem '${axiomName}' not found`
204+ );
205+ }
206+
207+ const axiomBlock = axiomsAndTheorems.get(axiomName)!;
208+
209+ // Extract suppose blocks
210+ const supposeBlocks: Block[] = [];
211+ let concludeBlock: Block | null = null;
212+
213+ for (const child of axiomBlock.children) {
214+ if (child.blockType === 'suppose') {
215+ supposeBlocks.push(child);
216+ } else if (child.blockType === 'conclude') {
217+ concludeBlock = child;
218+ }
219+ }
220+
221+ if (concludeBlock === null) {
222+ throw new VerificationError(
223+ `Line ${step.lineNum}: Axiom '${axiomName}' has no conclude block`
224+ );
225+ }
226+
227+ // Verify number of arguments matches
228+ if (args.length !== supposeBlocks.length) {
229+ throw new VerificationError(
230+ `Line ${step.lineNum}: Axiom '${axiomName}' expects ${supposeBlocks.length} arguments, got ${args.length}`
231+ );
232+ }
233+
234+ // Build substitution map
235+ const substitutions = new Map<string, Expression>();
236+
237+ for (let i = 0; i < supposeBlocks.length; i++) {
238+ const suppose = supposeBlocks[i];
239+ const arg = args[i];
240+
241+ // Parse suppose: suppose name : type
242+ if (suppose.args.length !== 1) {
243+ throw new VerificationError(
244+ `Line ${step.lineNum}: Invalid suppose block in axiom '${axiomName}'`
245+ );
246+ }
247+
248+ const supposeArg = suppose.args[0];
249+ if (supposeArg.name !== 'var' || supposeArg.children.length !== 2) {
250+ throw new VerificationError(
251+ `Line ${step.lineNum}: Invalid suppose format in axiom '${axiomName}'`
252+ );
253+ }
254+
255+ const varName = supposeArg.children[0].name;
256+ substitutions.set(varName, arg);
257+ }
258+
259+ // Get the conclusion and verify it's an equation
260+ let conclusion = concludeBlock.args[0];
261+
262+ // Apply substitutions to the conclusion
263+ for (const [varName, argExpr] of substitutions) {
264+ conclusion = conclusion.substitute(varName, argExpr);
265+ }
266+
267+ if (conclusion.name !== 'eq' || conclusion.children.length !== 2) {
268+ throw new VerificationError(
269+ `Line ${step.lineNum}: Axiom '${axiomName}' conclusion must be eq(a, b), got ${conclusion}`
270+ );
271+ }
272+
273+ return [conclusion.children[0], conclusion.children[1]];
274+}
275+
276+/**
277+ * Verify that prevExpr can be transformed to targetExpr by replacing fromExpr with toExpr where needed.
278+ */
279+function verifyTransformation(
280+ prevExpr: Expression,
281+ targetExpr: Expression,
282+ fromExpr: Expression,
283+ toExpr: Expression
284+): boolean {
285+ // If they're already equal, no substitution needed
286+ if (prevExpr.equals(targetExpr)) {
287+ return true;
288+ }
289+
290+ // Try substituting at the root level
291+ if (prevExpr.equals(fromExpr)) {
292+ return toExpr.equals(targetExpr);
293+ }
294+
295+ // If names don't match or different number of children, can't transform
296+ if (prevExpr.name !== targetExpr.name || prevExpr.children.length !== targetExpr.children.length) {
297+ return false;
298+ }
299+
300+ // Recursively check all children
301+ return prevExpr.children.every((pc, i) =>
302+ verifyTransformation(pc, targetExpr.children[i], fromExpr, toExpr)
303+ );
304+}
src/cli.tsadded+101−0View file
@@ -0,0 +1,101 @@
1+#!/usr/bin/env node
2+/**
3+ * Command-line interface for proofery.
4+ */
5+
6+import * as fs from 'fs';
7+import { parseFileSync } from './nodeParser.js';
8+import { verifyFile } from './verifier.js';
9+import { VerificationError, ParseError } from './errors.js';
10+
11+function main(): void {
12+ const args = process.argv.slice(2);
13+
14+ // Parse command line arguments
15+ let verbose = false;
16+ let filepath: string | null = null;
17+
18+ for (let i = 0; i < args.length; i++) {
19+ const arg = args[i];
20+ if (arg === '--verbose' || arg === '-v') {
21+ verbose = true;
22+ } else if (arg === '--help' || arg === '-h') {
23+ printHelp();
24+ process.exit(0);
25+ } else if (!arg.startsWith('-')) {
26+ filepath = arg;
27+ } else {
28+ console.error(`Unknown option: ${arg}`);
29+ printHelp();
30+ process.exit(1);
31+ }
32+ }
33+
34+ if (!filepath) {
35+ console.error('Error: No file specified');
36+ printHelp();
37+ process.exit(1);
38+ }
39+
40+ try {
41+ // Check if file exists
42+ if (!fs.existsSync(filepath)) {
43+ console.error(`Error: File '${filepath}' not found`);
44+ process.exit(1);
45+ }
46+
47+ // Parse the file
48+ if (verbose) {
49+ console.log(`Parsing ${filepath}...`);
50+ }
51+
52+ const blocks = parseFileSync(filepath);
53+
54+ if (verbose) {
55+ console.log(`Parsed ${blocks.length} top-level blocks\n`);
56+ }
57+
58+ // Verify the proofs
59+ verifyFile(blocks, verbose);
60+
61+ if (verbose) {
62+ console.log('\n✓ All proofs verified successfully!');
63+ }
64+
65+ process.exit(0);
66+ } catch (error) {
67+ if (error instanceof VerificationError || error instanceof ParseError || error instanceof SyntaxError) {
68+ console.error(`Error: ${error.message}`);
69+ process.exit(1);
70+ } else if (error instanceof Error) {
71+ console.error(`Unexpected error: ${error.message}`);
72+ if (verbose && error.stack) {
73+ console.error(error.stack);
74+ }
75+ process.exit(1);
76+ } else {
77+ console.error(`Unexpected error: ${error}`);
78+ process.exit(1);
79+ }
80+ }
81+}
82+
83+function printHelp(): void {
84+ console.log(`
85+proofery - A mathematical proof verifier
86+
87+Usage: proofery [options] <file>
88+
89+Arguments:
90+ <file> Path to the .prf file to verify
91+
92+Options:
93+ -v, --verbose Enable verbose output
94+ -h, --help Show this help message
95+
96+Example:
97+ proofery --verbose example.prf
98+`);
99+}
100+
101+main();
src/context.tsadded+60−0View file
@@ -0,0 +1,60 @@
1+/**
2+ * Context tracking for proof verification.
3+ */
4+
5+import { Expression } from './expression.js';
6+
7+/**
8+ * Context holds variables and their types, plus the current goal.
9+ */
10+export class Context {
11+ private variables: Map<string, Expression>;
12+ public goal: Expression | null;
13+
14+ constructor() {
15+ this.variables = new Map();
16+ this.goal = null;
17+ }
18+
19+ /**
20+ * Add a variable with its type to the context.
21+ */
22+ addVariable(name: string, varType: Expression): void {
23+ this.variables.set(name, varType);
24+ }
25+
26+ /**
27+ * Check if a variable exists in the context.
28+ */
29+ hasVariable(name: string): boolean {
30+ return this.variables.has(name);
31+ }
32+
33+ /**
34+ * Get the type of a variable.
35+ */
36+ getVariableType(name: string): Expression | undefined {
37+ return this.variables.get(name);
38+ }
39+
40+ /**
41+ * Create a deep copy of this context.
42+ */
43+ copy(): Context {
44+ const newContext = new Context();
45+ newContext.variables = new Map(this.variables);
46+ newContext.goal = this.goal ? this.goal.copy() : null;
47+ return newContext;
48+ }
49+
50+ /**
51+ * String representation of the context.
52+ */
53+ toString(): string {
54+ const vars = Array.from(this.variables.entries())
55+ .map(([name, type]) => `${name}: ${type.toString()}`)
56+ .join(', ');
57+ const goalStr = this.goal ? this.goal.toString() : 'None';
58+ return `Context(vars=[${vars}], goal=${goalStr})`;
59+ }
60+}
src/errors.tsadded+17−0View file
@@ -0,0 +1,17 @@
1+/**
2+ * Custom error classes for proofery.
3+ */
4+
5+export class VerificationError extends Error {
6+ constructor(message: string) {
7+ super(message);
8+ this.name = 'VerificationError';
9+ }
10+}
11+
12+export class ParseError extends SyntaxError {
13+ constructor(message: string) {
14+ super(message);
15+ this.name = 'ParseError';
16+ }
17+}
src/expression.tsadded+142−0View file
@@ -0,0 +1,142 @@
1+/**
2+ * Expression tree representation and parsing.
3+ */
4+
5+import { ParseError } from './errors.js';
6+
7+/**
8+ * Represents a prefix-notation expression tree.
9+ */
10+export class Expression {
11+ constructor(
12+ public readonly name: string,
13+ public readonly children: Expression[] = []
14+ ) {}
15+
16+ /**
17+ * Check structural equality of expressions.
18+ */
19+ equals(other: Expression): boolean {
20+ if (this.name !== other.name) {
21+ return false;
22+ }
23+ if (this.children.length !== other.children.length) {
24+ return false;
25+ }
26+ return this.children.every((child, i) => child.equals(other.children[i]));
27+ }
28+
29+ /**
30+ * Create a deep copy of this expression.
31+ */
32+ copy(): Expression {
33+ return new Expression(
34+ this.name,
35+ this.children.map(c => c.copy())
36+ );
37+ }
38+
39+ /**
40+ * Substitute all occurrences of varName with replacement.
41+ */
42+ substitute(varName: string, replacement: Expression): Expression {
43+ if (this.name === varName && this.children.length === 0) {
44+ return replacement.copy();
45+ }
46+ return new Expression(
47+ this.name,
48+ this.children.map(c => c.substitute(varName, replacement))
49+ );
50+ }
51+
52+ /**
53+ * String representation of the expression.
54+ */
55+ toString(): string {
56+ if (this.children.length === 0) {
57+ return this.name;
58+ }
59+ const childrenStr = this.children.map(c => c.toString()).join(', ');
60+ return `${this.name}(${childrenStr})`;
61+ }
62+}
63+
64+/**
65+ * Parse a prefix notation expression, handling 'a : b' as var(a, b).
66+ */
67+export function parseExpression(text: string, lineNum: number): Expression {
68+ text = text.trim();
69+
70+ // Handle special case: "a : b" -> "var(a, b)"
71+ if (text.includes(':')) {
72+ // Find the colon that's not inside parentheses
73+ let depth = 0;
74+ let colonPos = -1;
75+ for (let i = 0; i < text.length; i++) {
76+ const ch = text[i];
77+ if (ch === '(') {
78+ depth++;
79+ } else if (ch === ')') {
80+ depth--;
81+ } else if (ch === ':' && depth === 0) {
82+ colonPos = i;
83+ break;
84+ }
85+ }
86+
87+ if (colonPos > 0) {
88+ const varName = text.substring(0, colonPos).trim();
89+ const varType = text.substring(colonPos + 1).trim();
90+ // Recursively parse to handle nested colons
91+ const typeExpr = parseExpression(varType, lineNum);
92+ return new Expression('var', [new Expression(varName), typeExpr]);
93+ }
94+ }
95+
96+ // Find the opening parenthesis
97+ const parenPos = text.indexOf('(');
98+
99+ if (parenPos === -1) {
100+ // Simple identifier with no children
101+ return new Expression(text);
102+ }
103+
104+ // Extract name and arguments
105+ const exprName = text.substring(0, parenPos).trim();
106+
107+ // Find matching closing parenthesis
108+ if (!text.endsWith(')')) {
109+ throw new ParseError(`Line ${lineNum}: Mismatched parentheses in expression: ${text}`);
110+ }
111+
112+ const argsText = text.substring(parenPos + 1, text.length - 1).trim();
113+
114+ // Parse comma-separated arguments (respecting nested parentheses)
115+ const args: string[] = [];
116+ if (argsText) {
117+ let currentArg = '';
118+ let depth = 0;
119+ for (const ch of argsText) {
120+ if (ch === ',' && depth === 0) {
121+ args.push(currentArg.trim());
122+ currentArg = '';
123+ } else {
124+ if (ch === '(') {
125+ depth++;
126+ } else if (ch === ')') {
127+ depth--;
128+ }
129+ currentArg += ch;
130+ }
131+ }
132+
133+ if (currentArg) {
134+ args.push(currentArg.trim());
135+ }
136+ }
137+
138+ // Recursively parse each argument
139+ const children = args.map(arg => parseExpression(arg, lineNum));
140+
141+ return new Expression(exprName, children);
142+}
src/index.tsadded+36−0View file
@@ -0,0 +1,36 @@
1+/**
2+ * Proofery - A mathematical proof verifier
3+ *
4+ * This module provides the main library API for parsing and verifying
5+ * mathematical proofs written in .prf format.
6+ *
7+ * @example
8+ * ```typescript
9+ * import { parseContent, verifyFile } from 'proofery';
10+ *
11+ * const prfContent = `
12+ * axiom my_axiom
13+ * conclude eq(1, 1)
14+ * `;
15+ *
16+ * const blocks = parseContent(prfContent);
17+ * verifyFile(blocks, false);
18+ * ```
19+ */
20+
21+// Export parser functions (browser-safe)
22+export { parseContent } from './parser.js';
23+
24+// Note: For Node.js file parsing (parseFile, parseFileSync),
25+// import directly from 'proofery/nodeParser' instead
26+
27+// Export verifier functions
28+export { verifyFile } from './verifier.js';
29+
30+// Export types
31+export { Block } from './block.js';
32+export { Expression } from './expression.js';
33+export { Context } from './context.js';
34+
35+// Export error classes
36+export { VerificationError, ParseError } from './errors.js';
src/nodeParser.tsadded+26−0View file
@@ -0,0 +1,26 @@
1+/**
2+ * Node.js-specific parser functions that use the fs module.
3+ * These functions are not available in browser environments.
4+ */
5+
6+import * as fs from 'fs';
7+import { parseContent } from './parser.js';
8+import type { Block } from './block.js';
9+
10+/**
11+ * Parse a .prf file from the filesystem and return a list of top-level blocks.
12+ * This function is only available in Node.js environments.
13+ */
14+export function parseFileSync(filepath: string): Block[] {
15+ const content = fs.readFileSync(filepath, 'utf-8');
16+ return parseContent(content);
17+}
18+
19+/**
20+ * Async version of parseFileSync.
21+ * This function is only available in Node.js environments.
22+ */
23+export async function parseFile(filepath: string): Promise<Block[]> {
24+ const content = fs.readFileSync(filepath, 'utf-8');
25+ return parseContent(content);
26+}
src/parser.tsadded+191−0View file
@@ -0,0 +1,191 @@
1+/**
2+ * Parser for .prf files.
3+ */
4+
5+import { Block } from './block.js';
6+import { Expression, parseExpression } from './expression.js';
7+import { ParseError } from './errors.js';
8+
9+interface ParsedLine {
10+ lineNum: number;
11+ level: number;
12+ text: string;
13+}
14+
15+/**
16+ * Parse .prf content and return a list of top-level blocks.
17+ * This is the main parsing function that works in both browser and Node.js.
18+ */
19+export function parseContent(content: string): Block[] {
20+ const lines = content.split('\n');
21+
22+ // Parse lines with their indentation levels
23+ const parsedLines: ParsedLine[] = [];
24+ let indentUnit: string | null = null;
25+
26+ for (let i = 0; i < lines.length; i++) {
27+ const lineNum = i + 1;
28+ let line = lines[i];
29+
30+ // Remove trailing newline/carriage return
31+ line = line.replace(/\r?\n?$/, '');
32+
33+ // Skip empty lines and comments
34+ if (!line.trim() || line.trim().startsWith('#')) {
35+ continue;
36+ }
37+
38+ // Detect indentation
39+ let indentLevel = 0;
40+ const stripped = line.trimStart();
41+ const indentStr = line.substring(0, line.length - stripped.length);
42+
43+ if (indentStr) {
44+ // Detect indent unit from first indented line
45+ if (indentUnit === null) {
46+ indentUnit = indentStr;
47+ indentLevel = 1;
48+ } else {
49+ // Check if indentation is consistent
50+ if (indentStr.length % indentUnit.length !== 0) {
51+ throw new ParseError(`Line ${lineNum}: Inconsistent indentation`);
52+ }
53+ indentLevel = indentStr.length / indentUnit.length;
54+ }
55+ }
56+
57+ parsedLines.push({ lineNum, level: indentLevel, text: stripped });
58+ }
59+
60+ // Build block tree
61+ return buildBlocks(parsedLines, 0, 0).blocks;
62+}
63+
64+interface BuildResult {
65+ blocks: Block[];
66+ nextIdx: number;
67+}
68+
69+/**
70+ * Recursively build block tree from parsed lines.
71+ */
72+function buildBlocks(parsedLines: ParsedLine[], startIdx: number, expectedLevel: number): BuildResult {
73+ const blocks: Block[] = [];
74+ let idx = startIdx;
75+
76+ while (idx < parsedLines.length) {
77+ const { lineNum, level, text } = parsedLines[idx];
78+
79+ // If we've gone back to a lower level, return to parent
80+ if (level < expectedLevel) {
81+ break;
82+ }
83+
84+ // Skip lines at deeper levels (they'll be processed as children)
85+ if (level > expectedLevel) {
86+ throw new ParseError(`Line ${lineNum}: Unexpected indentation`);
87+ }
88+
89+ // Parse the block
90+ const block = parseBlock(lineNum, text);
91+
92+ // Process children at the next level
93+ if (idx + 1 < parsedLines.length) {
94+ const nextLevel = parsedLines[idx + 1].level;
95+ if (nextLevel > level) {
96+ const result = buildBlocks(parsedLines, idx + 1, level + 1);
97+ block.children = result.blocks;
98+ blocks.push(block);
99+ idx = result.nextIdx;
100+ continue;
101+ }
102+ }
103+
104+ blocks.push(block);
105+ idx++;
106+ }
107+
108+ return { blocks, nextIdx: idx };
109+}
110+
111+/**
112+ * Parse a single block line into a Block object.
113+ */
114+function parseBlock(lineNum: number, lineText: string): Block {
115+ // Split the line into tokens
116+ const tokens = tokenize(lineText, lineNum);
117+
118+ if (tokens.length === 0) {
119+ throw new ParseError(`Line ${lineNum}: Empty block`);
120+ }
121+
122+ const blockType = tokens[0];
123+ const remainingTokens = tokens.slice(1);
124+
125+ // Handle blocks with "name : type" pattern at the argument level
126+ // For suppose, assert, define, we-have, case: expect 3 tokens (name, :, type)
127+ let args: Expression[];
128+ if (['suppose', 'assert', 'define', 'we-have', 'case'].includes(blockType)) {
129+ if (remainingTokens.length === 3 && remainingTokens[1] === ':') {
130+ const varName = remainingTokens[0];
131+ const varTypeText = remainingTokens[2];
132+ const varType = parseExpression(varTypeText, lineNum);
133+ args = [new Expression('var', [new Expression(varName), varType])];
134+ } else {
135+ throw new ParseError(`Line ${lineNum}: '${blockType}' must have format 'name : type'`);
136+ }
137+ } else {
138+ // Parse the remaining tokens as expressions
139+ args = remainingTokens.map(token => parseExpression(token, lineNum));
140+ }
141+
142+ return new Block(lineNum, blockType, args);
143+}
144+
145+/**
146+ * Tokenize a line, respecting parentheses and colons.
147+ */
148+function tokenize(line: string, lineNum: number): string[] {
149+ const tokens: string[] = [];
150+ let currentToken = '';
151+ let depth = 0;
152+
153+ for (const ch of line) {
154+ if (ch === '(' && depth === 0) {
155+ // Start of arguments
156+ currentToken += ch;
157+ depth++;
158+ } else if (ch === '(') {
159+ currentToken += ch;
160+ depth++;
161+ } else if (ch === ')') {
162+ currentToken += ch;
163+ depth--;
164+ } else if (ch === ':' && depth === 0) {
165+ // Colon outside parentheses - token separator and also a token
166+ if (currentToken.trim()) {
167+ tokens.push(currentToken.trim());
168+ currentToken = '';
169+ }
170+ tokens.push(':');
171+ } else if (ch === ' ' && depth === 0) {
172+ // Space outside parentheses - token separator
173+ if (currentToken.trim()) {
174+ tokens.push(currentToken.trim());
175+ currentToken = '';
176+ }
177+ } else {
178+ currentToken += ch;
179+ }
180+ }
181+
182+ if (currentToken.trim()) {
183+ tokens.push(currentToken.trim());
184+ }
185+
186+ if (depth !== 0) {
187+ throw new ParseError(`Line ${lineNum}: Mismatched parentheses`);
188+ }
189+
190+ return tokens.filter(t => t.length > 0);
191+}
src/simplifier.tsadded+64−0View file
@@ -0,0 +1,64 @@
1+/**
2+ * Expression simplification based on context.
3+ */
4+
5+import { Expression } from './expression.js';
6+import { Context } from './context.js';
7+
8+/**
9+ * Simplify an expression based on the context.
10+ */
11+export function simplify(expr: Expression, context: Context): Expression {
12+ let current = expr;
13+ let previous: Expression | null = null;
14+
15+ // Keep applying simplification rules until no more changes
16+ while (previous === null || !current.equals(previous)) {
17+ previous = current;
18+ current = applySimplificationRules(current, context);
19+ }
20+
21+ return current;
22+}
23+
24+/**
25+ * Apply simplification rules once.
26+ */
27+function applySimplificationRules(expr: Expression, context: Context): Expression {
28+ // Rule: left(h) → a if h has type and(a, b)
29+ if (expr.name === 'left' && expr.children.length === 1) {
30+ const arg = expr.children[0];
31+ const argType = getTypeOfExpr(arg, context);
32+ if (argType && argType.name === 'and' && argType.children.length === 2) {
33+ return argType.children[0];
34+ }
35+ }
36+
37+ // Rule: right(h) → b if h has type and(a, b)
38+ if (expr.name === 'right' && expr.children.length === 1) {
39+ const arg = expr.children[0];
40+ const argType = getTypeOfExpr(arg, context);
41+ if (argType && argType.name === 'and' && argType.children.length === 2) {
42+ return argType.children[1];
43+ }
44+ }
45+
46+ // Recursively simplify children
47+ const simplifiedChildren = expr.children.map(child =>
48+ applySimplificationRules(child, context)
49+ );
50+
51+ return new Expression(expr.name, simplifiedChildren);
52+}
53+
54+/**
55+ * Get the type of an expression from the context.
56+ */
57+function getTypeOfExpr(expr: Expression, context: Context): Expression | null {
58+ // Simple case: variable name lookup
59+ if (expr.children.length === 0) {
60+ return context.getVariableType(expr.name) || null;
61+ }
62+
63+ return null;
64+}
src/verifier.tsadded+721−0View file
@@ -0,0 +1,721 @@
1+/**
2+ * Proof verification logic.
3+ */
4+
5+import { Block } from './block.js';
6+import { Expression } from './expression.js';
7+import { Context } from './context.js';
8+import { VerificationError } from './errors.js';
9+import { simplify } from './simplifier.js';
10+import { verifyCalculate } from './calculateVerifier.js';
11+
12+/**
13+ * Verify all axioms and theorems in a file.
14+ */
15+export function verifyFile(blocks: Block[], verbose: boolean = false): void {
16+ // First pass: collect all axioms and theorems
17+ const axiomsAndTheorems = new Map<string, Block>();
18+
19+ for (const block of blocks) {
20+ if (block.blockType === 'axiom' || block.blockType === 'theorem') {
21+ if (block.args.length !== 1) {
22+ throw new VerificationError(
23+ `Line ${block.lineNum}: ${block.blockType} must have exactly one argument (the name)`
24+ );
25+ }
26+
27+ const name = block.args[0].name;
28+ if (block.args[0].children.length > 0) {
29+ throw new VerificationError(
30+ `Line ${block.lineNum}: ${block.blockType} name must be a simple identifier`
31+ );
32+ }
33+
34+ axiomsAndTheorems.set(name, block);
35+
36+ if (verbose) {
37+ console.log(`Found ${block.blockType}: ${name}`);
38+ }
39+ } else {
40+ throw new VerificationError(
41+ `Line ${block.lineNum}: Top-level blocks must be 'axiom' or 'theorem', got '${block.blockType}'`
42+ );
43+ }
44+ }
45+
46+ // Second pass: verify theorems
47+ for (const block of blocks) {
48+ if (block.blockType === 'theorem') {
49+ const name = block.args[0].name;
50+ if (verbose) {
51+ console.log(`\nVerifying theorem: ${name}`);
52+ }
53+ verifyTheorem(block, axiomsAndTheorems, verbose);
54+ if (verbose) {
55+ console.log(`✓ Theorem ${name} verified`);
56+ }
57+ }
58+ }
59+}
60+
61+/**
62+ * Verify a single theorem.
63+ */
64+function verifyTheorem(theoremBlock: Block, axiomsAndTheorems: Map<string, Block>, verbose: boolean): void {
65+ // Create initial context from suppose blocks
66+ const context = new Context();
67+
68+ const supposeBlocks: Block[] = [];
69+ let concludeBlock: Block | null = null;
70+ let proofBlock: Block | null = null;
71+
72+ // Parse structure: suppose* conclude proof
73+ for (const child of theoremBlock.children) {
74+ if (child.blockType === 'suppose') {
75+ supposeBlocks.push(child);
76+ } else if (child.blockType === 'conclude') {
77+ if (concludeBlock !== null) {
78+ throw new VerificationError(`Line ${child.lineNum}: Multiple 'conclude' blocks in theorem`);
79+ }
80+ concludeBlock = child;
81+ } else if (child.blockType === 'proof') {
82+ if (proofBlock !== null) {
83+ throw new VerificationError(`Line ${child.lineNum}: Multiple 'proof' blocks in theorem`);
84+ }
85+ proofBlock = child;
86+ } else {
87+ throw new VerificationError(
88+ `Line ${child.lineNum}: Invalid block type '${child.blockType}' in theorem`
89+ );
90+ }
91+ }
92+
93+ if (concludeBlock === null) {
94+ throw new VerificationError(`Line ${theoremBlock.lineNum}: Theorem missing 'conclude' block`);
95+ }
96+
97+ if (proofBlock === null) {
98+ throw new VerificationError(`Line ${theoremBlock.lineNum}: Theorem missing 'proof' block`);
99+ }
100+
101+ // Process suppose blocks
102+ for (const suppose of supposeBlocks) {
103+ processSuppose(suppose, context);
104+ }
105+
106+ // Process conclude block
107+ processConclude(concludeBlock, context);
108+
109+ // Verify the proof
110+ const goalResolved = verifyProof(proofBlock, context, axiomsAndTheorems, verbose);
111+
112+ if (!goalResolved) {
113+ throw new VerificationError(`Line ${proofBlock.lineNum}: Proof does not resolve the goal`);
114+ }
115+}
116+
117+/**
118+ * Process a suppose block: suppose name : type
119+ */
120+function processSuppose(supposeBlock: Block, context: Context): void {
121+ if (supposeBlock.args.length !== 1) {
122+ throw new VerificationError(`Line ${supposeBlock.lineNum}: 'suppose' must have exactly one argument`);
123+ }
124+
125+ const arg = supposeBlock.args[0];
126+ if (arg.name !== 'var' || arg.children.length !== 2) {
127+ throw new VerificationError(
128+ `Line ${supposeBlock.lineNum}: 'suppose' argument must be of form 'name : type'`
129+ );
130+ }
131+
132+ const varName = arg.children[0].name;
133+ const varType = arg.children[1];
134+
135+ if (arg.children[0].children.length > 0) {
136+ throw new VerificationError(`Line ${supposeBlock.lineNum}: Variable name must be a simple identifier`);
137+ }
138+
139+ context.addVariable(varName, varType);
140+}
141+
142+/**
143+ * Process a conclude block: conclude type
144+ */
145+function processConclude(concludeBlock: Block, context: Context): void {
146+ if (concludeBlock.args.length !== 1) {
147+ throw new VerificationError(`Line ${concludeBlock.lineNum}: 'conclude' must have exactly one argument`);
148+ }
149+
150+ context.goal = concludeBlock.args[0];
151+}
152+
153+/**
154+ * Verify a proof block and return whether the goal was resolved.
155+ */
156+function verifyProof(proofBlock: Block, context: Context, axiomsAndTheorems: Map<string, Block>, verbose: boolean): boolean {
157+ let goalResolved = false;
158+
159+ for (const child of proofBlock.children) {
160+ const result = verifyProofStep(child, context, axiomsAndTheorems, verbose);
161+ if (result) {
162+ goalResolved = true;
163+ }
164+ }
165+
166+ return goalResolved;
167+}
168+
169+/**
170+ * Verify a single proof step. Returns true if the goal was resolved.
171+ */
172+function verifyProofStep(step: Block, context: Context, axiomsAndTheorems: Map<string, Block>, verbose: boolean): boolean {
173+ switch (step.blockType) {
174+ case 'unpack-and':
175+ return verifyUnpackAnd(step, context, axiomsAndTheorems, verbose);
176+ case 'cases':
177+ return verifyCases(step, context, axiomsAndTheorems, verbose);
178+ case 'witness':
179+ return verifyWitness(step, context);
180+ case 'assert-goal':
181+ return verifyAssertGoal(step, context);
182+ case 'exact':
183+ return verifyExact(step, context);
184+ case 'calculate':
185+ return verifyCalculate(step, context, axiomsAndTheorems);
186+ case 'assert':
187+ return verifyAssert(step, context);
188+ case 'define':
189+ return verifyDefine(step, context);
190+ case 'consider':
191+ return verifyConsider(step, context);
192+ case 'forall-apply':
193+ return verifyForallApply(step, context);
194+ case 'deconstruct-exists':
195+ return verifyDeconstructExists(step, context);
196+ case 'we-have':
197+ return verifyWeHave(step, context, axiomsAndTheorems, verbose);
198+ case 'focus-or':
199+ return verifyFocusOr(step, context);
200+ default:
201+ throw new VerificationError(`Line ${step.lineNum}: Unknown proof step type '${step.blockType}'`);
202+ }
203+}
204+
205+/**
206+ * Verify unpack-and: goal must be and(a, b), requires two goal children.
207+ */
208+function verifyUnpackAnd(step: Block, context: Context, axiomsAndTheorems: Map<string, Block>, verbose: boolean): boolean {
209+ if (step.args.length !== 0) {
210+ throw new VerificationError(`Line ${step.lineNum}: 'unpack-and' takes no arguments`);
211+ }
212+
213+ if (context.goal === null) {
214+ throw new VerificationError(`Line ${step.lineNum}: No goal to unpack`);
215+ }
216+
217+ if (context.goal.name !== 'and' || context.goal.children.length !== 2) {
218+ throw new VerificationError(`Line ${step.lineNum}: Goal must be and(a, b), got ${context.goal}`);
219+ }
220+
221+ if (step.children.length !== 2) {
222+ throw new VerificationError(`Line ${step.lineNum}: 'unpack-and' requires exactly 2 children`);
223+ }
224+
225+ // Verify both children are goal blocks
226+ for (let i = 0; i < step.children.length; i++) {
227+ const child = step.children[i];
228+ if (child.blockType !== 'goal') {
229+ throw new VerificationError(`Line ${child.lineNum}: 'unpack-and' children must be 'goal' blocks`);
230+ }
231+
232+ if (child.args.length !== 1) {
233+ throw new VerificationError(`Line ${child.lineNum}: 'goal' must have exactly one argument`);
234+ }
235+
236+ const expectedGoal = context.goal.children[i];
237+ if (!child.args[0].equals(expectedGoal)) {
238+ throw new VerificationError(
239+ `Line ${child.lineNum}: Expected goal ${expectedGoal}, got ${child.args[0]}`
240+ );
241+ }
242+
243+ // Each goal must have one proof child
244+ if (child.children.length !== 1 || child.children[0].blockType !== 'proof') {
245+ throw new VerificationError(`Line ${child.lineNum}: 'goal' must have exactly one 'proof' child`);
246+ }
247+
248+ // Verify the proof with the subgoal
249+ const subContext = context.copy();
250+ subContext.goal = expectedGoal;
251+ const resolved = verifyProof(child.children[0], subContext, axiomsAndTheorems, verbose);
252+
253+ if (!resolved) {
254+ throw new VerificationError(`Line ${child.lineNum}: Proof does not resolve goal ${expectedGoal}`);
255+ }
256+ }
257+
258+ return true; // Goal resolved
259+}
260+
261+/**
262+ * Verify cases: variable must have type or(a, b), requires two case children.
263+ */
264+function verifyCases(step: Block, context: Context, axiomsAndTheorems: Map<string, Block>, verbose: boolean): boolean {
265+ if (step.args.length !== 1) {
266+ throw new VerificationError(`Line ${step.lineNum}: 'cases' takes exactly one argument (variable name)`);
267+ }
268+
269+ const varName = step.args[0].name;
270+ if (step.args[0].children.length > 0) {
271+ throw new VerificationError(`Line ${step.lineNum}: 'cases' argument must be a simple variable name`);
272+ }
273+
274+ if (!context.hasVariable(varName)) {
275+ throw new VerificationError(`Line ${step.lineNum}: Variable '${varName}' not in context`);
276+ }
277+
278+ const varType = context.getVariableType(varName)!;
279+ if (varType.name !== 'or' || varType.children.length !== 2) {
280+ throw new VerificationError(
281+ `Line ${step.lineNum}: Variable '${varName}' must have type or(a, b), got ${varType}`
282+ );
283+ }
284+
285+ if (step.children.length !== 2) {
286+ throw new VerificationError(`Line ${step.lineNum}: 'cases' requires exactly 2 'case' children`);
287+ }
288+
289+ // Verify both case children
290+ for (let i = 0; i < step.children.length; i++) {
291+ const child = step.children[i];
292+ if (child.blockType !== 'case') {
293+ throw new VerificationError(`Line ${child.lineNum}: 'cases' children must be 'case' blocks`);
294+ }
295+
296+ if (child.args.length !== 1) {
297+ throw new VerificationError(`Line ${child.lineNum}: 'case' must have exactly one argument`);
298+ }
299+
300+ const arg = child.args[0];
301+ if (arg.name !== 'var' || arg.children.length !== 2) {
302+ throw new VerificationError(`Line ${child.lineNum}: 'case' argument must be of form 'name : type'`);
303+ }
304+
305+ const caseVarName = arg.children[0].name;
306+ const caseType = arg.children[1];
307+
308+ const expectedType = varType.children[i];
309+ if (!caseType.equals(expectedType)) {
310+ throw new VerificationError(
311+ `Line ${child.lineNum}: Expected case type ${expectedType}, got ${caseType}`
312+ );
313+ }
314+
315+ // Verify proof with added case variable
316+ const caseContext = context.copy();
317+ caseContext.addVariable(caseVarName, caseType);
318+
319+ // Each case needs a proof
320+ if (child.children.length !== 1 || child.children[0].blockType !== 'proof') {
321+ throw new VerificationError(`Line ${child.lineNum}: 'case' must have exactly one 'proof' child`);
322+ }
323+
324+ const resolved = verifyProof(child.children[0], caseContext, axiomsAndTheorems, verbose);
325+ if (!resolved) {
326+ throw new VerificationError(`Line ${child.lineNum}: Proof in case does not resolve goal`);
327+ }
328+ }
329+
330+ return true; // Goal resolved
331+}
332+
333+/**
334+ * Verify witness: goal must be exists(var(name, type), body), modifies goal.
335+ */
336+function verifyWitness(step: Block, context: Context): boolean {
337+ if (step.args.length !== 1) {
338+ throw new VerificationError(`Line ${step.lineNum}: 'witness' takes exactly one argument`);
339+ }
340+
341+ const witnessName = step.args[0].name;
342+ if (step.args[0].children.length > 0) {
343+ throw new VerificationError(`Line ${step.lineNum}: 'witness' argument must be a simple identifier`);
344+ }
345+
346+ if (context.goal === null) {
347+ throw new VerificationError(`Line ${step.lineNum}: No goal for witness`);
348+ }
349+
350+ if (context.goal.name !== 'exists' || context.goal.children.length !== 2) {
351+ throw new VerificationError(
352+ `Line ${step.lineNum}: Goal must be exists(var(name, type), body), got ${context.goal}`
353+ );
354+ }
355+
356+ const varExpr = context.goal.children[0];
357+ if (varExpr.name !== 'var' || varExpr.children.length !== 2) {
358+ throw new VerificationError(
359+ `Line ${step.lineNum}: exists must have var(name, type) as first argument`
360+ );
361+ }
362+
363+ const boundVarName = varExpr.children[0].name;
364+ const body = context.goal.children[1];
365+
366+ // Substitute witness into body
367+ context.goal = body.substitute(boundVarName, new Expression(witnessName));
368+
369+ return false; // Does not resolve goal
370+}
371+
372+/**
373+ * Verify assert-goal: expression must match current goal.
374+ */
375+function verifyAssertGoal(step: Block, context: Context): boolean {
376+ if (step.args.length !== 1) {
377+ throw new VerificationError(`Line ${step.lineNum}: 'assert-goal' takes exactly one argument`);
378+ }
379+
380+ const expectedGoal = step.args[0];
381+
382+ if (context.goal === null) {
383+ throw new VerificationError(`Line ${step.lineNum}: No current goal`);
384+ }
385+
386+ if (!context.goal.equals(expectedGoal)) {
387+ throw new VerificationError(
388+ `Line ${step.lineNum}: Expected goal ${expectedGoal}, but current goal is ${context.goal}`
389+ );
390+ }
391+
392+ return false; // Does not resolve goal
393+}
394+
395+/**
396+ * Verify exact: two variants - variable name or expression after simplification.
397+ */
398+function verifyExact(step: Block, context: Context): boolean {
399+ if (step.args.length !== 1) {
400+ throw new VerificationError(`Line ${step.lineNum}: 'exact' takes exactly one argument`);
401+ }
402+
403+ const arg = step.args[0];
404+
405+ if (context.goal === null) {
406+ throw new VerificationError(`Line ${step.lineNum}: No goal to resolve`);
407+ }
408+
409+ // Variant 1: Simple variable name
410+ if (arg.children.length === 0 && context.hasVariable(arg.name)) {
411+ const varType = context.getVariableType(arg.name)!;
412+ if (!varType.equals(context.goal)) {
413+ throw new VerificationError(
414+ `Line ${step.lineNum}: Variable '${arg.name}' has type ${varType}, but goal is ${context.goal}`
415+ );
416+ }
417+ return true; // Goal resolved
418+ }
419+
420+ // Variant 2: Expression after simplification
421+ const simplified = simplify(arg, context);
422+ if (!simplified.equals(context.goal)) {
423+ throw new VerificationError(
424+ `Line ${step.lineNum}: Expression ${arg} simplifies to ${simplified}, but goal is ${context.goal}`
425+ );
426+ }
427+
428+ return true; // Goal resolved
429+}
430+
431+/**
432+ * Verify assert: assert name : type.
433+ */
434+function verifyAssert(step: Block, context: Context): boolean {
435+ if (step.args.length !== 1) {
436+ throw new VerificationError(`Line ${step.lineNum}: 'assert' must have exactly one argument`);
437+ }
438+
439+ const arg = step.args[0];
440+ if (arg.name !== 'var' || arg.children.length !== 2) {
441+ throw new VerificationError(`Line ${step.lineNum}: 'assert' argument must be of form 'name : type'`);
442+ }
443+
444+ const varName = arg.children[0].name;
445+ const expectedType = arg.children[1];
446+
447+ if (!context.hasVariable(varName)) {
448+ throw new VerificationError(`Line ${step.lineNum}: Variable '${varName}' not in context`);
449+ }
450+
451+ const actualType = context.getVariableType(varName)!;
452+ if (!actualType.equals(expectedType)) {
453+ throw new VerificationError(
454+ `Line ${step.lineNum}: Variable '${varName}' has type ${actualType}, expected ${expectedType}`
455+ );
456+ }
457+
458+ return false; // Does not resolve goal
459+}
460+
461+/**
462+ * Verify define: define name : eq(lhs, rhs).
463+ */
464+function verifyDefine(step: Block, context: Context): boolean {
465+ if (step.args.length !== 1) {
466+ throw new VerificationError(`Line ${step.lineNum}: 'define' must have exactly one argument`);
467+ }
468+
469+ const arg = step.args[0];
470+ if (arg.name !== 'var' || arg.children.length !== 2) {
471+ throw new VerificationError(`Line ${step.lineNum}: 'define' argument must be of form 'name : type'`);
472+ }
473+
474+ const varName = arg.children[0].name;
475+ const varType = arg.children[1];
476+
477+ if (context.hasVariable(varName)) {
478+ throw new VerificationError(`Line ${step.lineNum}: Variable '${varName}' already in context`);
479+ }
480+
481+ // Check that type is an eq expression
482+ if (varType.name !== 'eq' || varType.children.length !== 2) {
483+ throw new VerificationError(`Line ${step.lineNum}: 'define' type must be eq(lhs, rhs)`);
484+ }
485+
486+ context.addVariable(varName, varType);
487+
488+ return false; // Does not resolve goal
489+}
490+
491+/**
492+ * Verify consider: goal must be forall(var(name, type), body).
493+ */
494+function verifyConsider(step: Block, context: Context): boolean {
495+ if (step.args.length !== 1) {
496+ throw new VerificationError(`Line ${step.lineNum}: 'consider' takes exactly one argument`);
497+ }
498+
499+ const varName = step.args[0].name;
500+ if (step.args[0].children.length > 0) {
501+ throw new VerificationError(`Line ${step.lineNum}: 'consider' argument must be a simple identifier`);
502+ }
503+
504+ if (context.goal === null) {
505+ throw new VerificationError(`Line ${step.lineNum}: No goal for consider`);
506+ }
507+
508+ if (context.goal.name !== 'forall' || context.goal.children.length !== 2) {
509+ throw new VerificationError(
510+ `Line ${step.lineNum}: Goal must be forall(var(name, type), body), got ${context.goal}`
511+ );
512+ }
513+
514+ const varExpr = context.goal.children[0];
515+ if (varExpr.name !== 'var' || varExpr.children.length !== 2) {
516+ throw new VerificationError(
517+ `Line ${step.lineNum}: forall must have var(name, type) as first argument`
518+ );
519+ }
520+
521+ const boundVarName = varExpr.children[0].name;
522+ const varType = varExpr.children[1];
523+ const body = context.goal.children[1];
524+
525+ if (boundVarName !== varName) {
526+ throw new VerificationError(
527+ `Line ${step.lineNum}: Expected variable '${boundVarName}', got '${varName}'`
528+ );
529+ }
530+
531+ context.addVariable(varName, varType);
532+ context.goal = body;
533+
534+ return false; // Does not resolve goal
535+}
536+
537+/**
538+ * Verify forall-apply: apply forall to an argument.
539+ */
540+function verifyForallApply(step: Block, context: Context): boolean {
541+ if (step.args.length !== 3) {
542+ throw new VerificationError(`Line ${step.lineNum}: 'forall-apply' takes exactly 3 arguments`);
543+ }
544+
545+ const forallVar = step.args[0].name;
546+ const argVar = step.args[1].name;
547+ const resultVar = step.args[2].name;
548+
549+ if (step.args[0].children.length > 0 || step.args[1].children.length > 0 || step.args[2].children.length > 0) {
550+ throw new VerificationError(
551+ `Line ${step.lineNum}: 'forall-apply' arguments must be simple identifiers`
552+ );
553+ }
554+
555+ if (!context.hasVariable(forallVar)) {
556+ throw new VerificationError(`Line ${step.lineNum}: Variable '${forallVar}' not in context`);
557+ }
558+
559+ if (!context.hasVariable(argVar)) {
560+ throw new VerificationError(`Line ${step.lineNum}: Variable '${argVar}' not in context`);
561+ }
562+
563+ if (context.hasVariable(resultVar)) {
564+ throw new VerificationError(`Line ${step.lineNum}: Variable '${resultVar}' already in context`);
565+ }
566+
567+ const forallType = context.getVariableType(forallVar)!;
568+ if (forallType.name !== 'forall' || forallType.children.length !== 2) {
569+ throw new VerificationError(
570+ `Line ${step.lineNum}: Variable '${forallVar}' must have type forall(var(name, type), body)`
571+ );
572+ }
573+
574+ const varExpr = forallType.children[0];
575+ if (varExpr.name !== 'var' || varExpr.children.length !== 2) {
576+ throw new VerificationError(
577+ `Line ${step.lineNum}: forall must have var(name, type) as first argument`
578+ );
579+ }
580+
581+ const boundVarName = varExpr.children[0].name;
582+ const expectedArgType = varExpr.children[1];
583+ const body = forallType.children[1];
584+
585+ const argType = context.getVariableType(argVar)!;
586+ if (!argType.equals(expectedArgType)) {
587+ throw new VerificationError(
588+ `Line ${step.lineNum}: Argument '${argVar}' has type ${argType}, expected ${expectedArgType}`
589+ );
590+ }
591+
592+ // Substitute argVar for boundVarName in body
593+ const resultType = body.substitute(boundVarName, new Expression(argVar));
594+ context.addVariable(resultVar, resultType);
595+
596+ return false; // Does not resolve goal
597+}
598+
599+/**
600+ * Verify deconstruct-exists: extract witness and hypothesis from exists.
601+ */
602+function verifyDeconstructExists(step: Block, context: Context): boolean {
603+ if (step.args.length !== 3) {
604+ throw new VerificationError(`Line ${step.lineNum}: 'deconstruct-exists' takes exactly 3 arguments`);
605+ }
606+
607+ const existsVar = step.args[0].name;
608+ const witnessVar = step.args[1].name;
609+ const hypVar = step.args[2].name;
610+
611+ if (step.args[0].children.length > 0 || step.args[1].children.length > 0 || step.args[2].children.length > 0) {
612+ throw new VerificationError(
613+ `Line ${step.lineNum}: 'deconstruct-exists' arguments must be simple identifiers`
614+ );
615+ }
616+
617+ if (!context.hasVariable(existsVar)) {
618+ throw new VerificationError(`Line ${step.lineNum}: Variable '${existsVar}' not in context`);
619+ }
620+
621+ if (context.hasVariable(witnessVar)) {
622+ throw new VerificationError(`Line ${step.lineNum}: Variable '${witnessVar}' already in context`);
623+ }
624+
625+ if (context.hasVariable(hypVar)) {
626+ throw new VerificationError(`Line ${step.lineNum}: Variable '${hypVar}' already in context`);
627+ }
628+
629+ const existsType = context.getVariableType(existsVar)!;
630+ if (existsType.name !== 'exists' || existsType.children.length !== 2) {
631+ throw new VerificationError(
632+ `Line ${step.lineNum}: Variable '${existsVar}' must have type exists(var(name, type), body)`
633+ );
634+ }
635+
636+ const varExpr = existsType.children[0];
637+ if (varExpr.name !== 'var' || varExpr.children.length !== 2) {
638+ throw new VerificationError(
639+ `Line ${step.lineNum}: exists must have var(name, type) as first argument`
640+ );
641+ }
642+
643+ const boundVarName = varExpr.children[0].name;
644+ const witnessType = varExpr.children[1];
645+ const body = existsType.children[1];
646+
647+ // Add witness variable and hypothesis variable
648+ context.addVariable(witnessVar, witnessType);
649+ const hypType = body.substitute(boundVarName, new Expression(witnessVar));
650+ context.addVariable(hypVar, hypType);
651+
652+ return false; // Does not resolve goal
653+}
654+
655+/**
656+ * Verify we-have: prove intermediate result.
657+ */
658+function verifyWeHave(step: Block, context: Context, axiomsAndTheorems: Map<string, Block>, verbose: boolean): boolean {
659+ if (step.args.length !== 1) {
660+ throw new VerificationError(`Line ${step.lineNum}: 'we-have' must have exactly one argument`);
661+ }
662+
663+ const arg = step.args[0];
664+ if (arg.name !== 'var' || arg.children.length !== 2) {
665+ throw new VerificationError(`Line ${step.lineNum}: 'we-have' argument must be of form 'name : type'`);
666+ }
667+
668+ const varName = arg.children[0].name;
669+ const varType = arg.children[1];
670+
671+ if (context.hasVariable(varName)) {
672+ throw new VerificationError(`Line ${step.lineNum}: Variable '${varName}' already in context`);
673+ }
674+
675+ if (step.children.length !== 1 || step.children[0].blockType !== 'proof') {
676+ throw new VerificationError(`Line ${step.lineNum}: 'we-have' must have exactly one 'proof' child`);
677+ }
678+
679+ // Verify the proof with the new goal
680+ const subContext = context.copy();
681+ subContext.goal = varType;
682+ const resolved = verifyProof(step.children[0], subContext, axiomsAndTheorems, verbose);
683+
684+ if (!resolved) {
685+ throw new VerificationError(`Line ${step.lineNum}: Proof does not establish ${varType}`);
686+ }
687+
688+ context.addVariable(varName, varType);
689+
690+ return false; // Does not resolve goal
691+}
692+
693+/**
694+ * Verify focus-or: goal must be or(a, b), focus on left or right.
695+ */
696+function verifyFocusOr(step: Block, context: Context): boolean {
697+ if (step.args.length !== 1) {
698+ throw new VerificationError(`Line ${step.lineNum}: 'focus-or' takes exactly one argument`);
699+ }
700+
701+ const direction = step.args[0].name;
702+ if (step.args[0].children.length > 0 || (direction !== 'left' && direction !== 'right')) {
703+ throw new VerificationError(`Line ${step.lineNum}: 'focus-or' argument must be 'left' or 'right'`);
704+ }
705+
706+ if (context.goal === null) {
707+ throw new VerificationError(`Line ${step.lineNum}: No goal for focus-or`);
708+ }
709+
710+ if (context.goal.name !== 'or' || context.goal.children.length !== 2) {
711+ throw new VerificationError(`Line ${step.lineNum}: Goal must be or(a, b), got ${context.goal}`);
712+ }
713+
714+ if (direction === 'left') {
715+ context.goal = context.goal.children[0];
716+ } else {
717+ context.goal = context.goal.children[1];
718+ }
719+
720+ return false; // Does not resolve goal
721+}
tsconfig.jsonadded+20−0View file
@@ -0,0 +1,20 @@
1+{
2+ "compilerOptions": {
3+ "target": "ES2020",
4+ "module": "ES2020",
5+ "lib": ["ES2020"],
6+ "outDir": "./dist",
7+ "rootDir": "./src",
8+ "strict": true,
9+ "esModuleInterop": true,
10+ "skipLibCheck": true,
11+ "forceConsistentCasingInFileNames": true,
12+ "resolveJsonModule": true,
13+ "declaration": true,
14+ "declarationMap": true,
15+ "sourceMap": true,
16+ "moduleResolution": "node"
17+ },
18+ "include": ["src/**/*"],
19+ "exclude": ["node_modules", "dist"]
20+}