prove

/z-spec:prove - Generate Lean 4 Proof Obligations

Translate a Z specification into Lean 4 proof obligations that formalize the key correctness properties: initialization establishes the state invariant, and every operation preserves it.

Input

Arguments: $ARGUMENTS

Parse arguments:

• First positional argument: Z specification file (default: search docs/*.tex)
• --obligations=all|init|preserve - which proof obligations to generate (default: all)
• --no-mathlib - generate standalone Lean without Mathlib dependency (simpler but fewer tactics)

Process

0. Prerequisites

Verify Lean 4 and Lake are installed:

which lean >/dev/null 2>&1 || echo "LEAN_NOT_FOUND"
which lake >/dev/null 2>&1 || echo "LAKE_NOT_FOUND"

If lean or lake not found: Stop and tell the user:

Lean 4 is not installed. Run /z-spec:setup lean to install the Lean 4 toolchain via elan.

Verify version compatibility:

lean --version 2>&1

The output should show Lean 4.x. If it shows Lean 3.x or an error, advise the user to update via elan update.

The Z specification should already exist and have been type-checked (via /z-spec:check). If the user has not done this, suggest it but do not block — the translation can still proceed from a syntactically valid spec.

1. Locate the Specification

If a file path is provided, use it directly.

If no file specified:

• Look in docs/ for .tex files containing Z specifications
• If multiple found, ask user to specify

Read the specification file.

2. Parse the Specification

Scan the specification and extract the following constructs. Each subsection describes what to look for and what to record.

2a. Given Sets

Look for given set declarations in \begin{zed} blocks:

\begin{zed}
[USERID, SESSIONID]
\end{zed}

Record each name. These become opaque types in Lean.

2b. Free Types

Look for free type definitions in \begin{zed} blocks:

\begin{zed}
Status ::= pending | active | suspended | closed
\end{zed}