Metadata-Version: 2.4
Name: py-prop-logic-kernel
Version: 0.0.6
Requires-Python: >=3.10
Description-Content-Type: text/markdown

# PROP-LOGIC-KERNEL

This project is a small proposition-logic tactic kernel in Lean, exposed through a line-based REPL.

## LEAN MODULE

- `PropLogicKernel/Basic.lean`: proposition syntax, tactics, goals, and state
- `PropLogicKernel/Parser.lean`: parser for propositions and tactic commands (written by cursor)
- `PropLogicKernel/Resolver.lean`: operational semantics for tactics
- `PropLogicKernel/Printer.lean`: rendering of propositions, tactics, and goals
- `PropLogicKernel/REPL.lean`: REPL-level state, status lines, and exit-code policy
- `REPL/REPL.lean`: generic line-based REPL loop
- `Main.lean`: executable entrypoint

## PROPOSITION SPECIFICATION

A proposition `P` is one of:

- `⊥`
- atom
- `A ∧ B`
- `A ∨ B`
- `A → B`

Associativity follows the parser/printer implementation:

- `∧`, `∨`, and `→` are parsed right-associatively
- parentheses may be used explicitly

## PARSER SPECIFICATION

`PropLogicKernel/Parser.lean` uppercases proposition input before parsing.

After uppercasing, proposition input is rejected unless every character is one of:

- whitespace
- `(`, `)`
- `∧`, `∨`, `→`, `⊥`
- uppercase letters `A-Z`
- digits `0-9`
- underscore `_`

Atom names are maximal nonempty strings over:

- uppercase letters `A-Z`
- digits `0-9`
- underscore `_`

Examples of valid atom names:

- `A`
- `P1`
- `HELLO_WORLD`
- `X_2`

## GOAL/STATE MODEL

A goal consists of:

- a set of hypotheses
- a target proposition

The state tracks:

- a list of goals
- `varCount`
- `newCount`
- `sorrCount`

## TACTIC

These are the kernel rules implemented by `PropLogicKernel/Resolver.lean`.

- `intro`
  - If goal is `A → B`, add a fresh hypothesis `A` and replace the goal with `B`.
- `apply n`
  - If hypothesis `n` is `A → B` and current goal is `B`, replace the goal with `A`.
- `exact n`
  - If hypothesis `n` exactly matches the current goal, solve the goal.
- `constructor`
  - If goal is `A ∧ B`, split it into two goals.
- `left`
  - If goal is `A ∨ B`, replace the goal with `A`.
- `right`
  - If goal is `A ∨ B`, replace the goal with `B`.
- `cases n`
  - If hypothesis `n` is `A ∨ B`, branch into two goals.
  - If hypothesis `n` is `A ∧ B`, add both parts as fresh hypotheses.
  - If hypothesis `n` is `⊥`, solve the goal immediately.

### CLASSICAL LOGIC

- `lem P`
  - Classical only.
  - Adds hypothesis `(P → ⊥) ∨ P`.
- `refine n`
  - Classical only.
  - If hypothesis `n` is `A1 → B1` and goal is `B`, replace the current goal with goals `B1 → B` and `A1`.

### APPLICATION LEVEL COMMANDS

- `sorry`
  - Solves the current goal unconditionally and increments `sorrCount`.
- `new P`
  - Pushes a fresh goal `P` and increments `newCount`.

## FAILURE BEHAVIOR

- Parse failures return `parse error`.
- Resolution failures return an error message and keep the previous state.
- `lem` and `refine` fail if classical logic is disabled.
- Any tactic other than `new` fails on an empty goal stack.

## REPL protocol

The executable built by `lake build` runs `REPL.run` from `REPL/REPL.lean`.

For each step:

- write zero or more status/error lines to `stderr`
- write zero or more output lines to `stdout`
- write the prompt `> ` to `stderr` with no trailing newline
- read exactly one newline-terminated line from `stdin`
- transition to the next state

Status lines are prefixed by `-- `.

Typical status line:

- `-- new_count 1 sorry_count 0 goals_remaining 2`

Success marker:

- `-- all goals accomplished!`

That success marker is emitted iff:

- at least one goal was successfully introduced via `new`
- no `sorry` was used
- all goals are solved

## EXIT CODE POLICY

At EOF, `REPL.run` returns the previous step's `code`.

`PropLogicKernel/REPL.lean` sets exit code `0` iff (same with `all goals accomplished!`):

- at least one goal was successfully introduced via `new`
- no `sorry` was used
- all goals are solved

Otherwise exit code is `1`.

Parse/resolution errors do not automatically force exit code `1`; they preserve the previous state. So if the kernel is already in a success state, a later failing command can still leave final exit code `0`.


## DISCLAIMER: AI GENERATED CODE

The following files were written by Cursor:

- `README.md`
- All Python code in this repo (for example: `py_prop_logic_kernel/`)
- `PropLogicKernel/Parser.lean`