## Tree @master (Download .tar.gz)

# Eqthy

*Version 0.1* | *See also:* Philomath
∘ LCF-style-ND

**Eqthy** is a formalized language for equational proofs. Its design attempts to
reconcile *simplicity of implementation on a machine* with *human usability*
(more on this below). It supports an elementary linear
style, where each line gives a step which is derived from the step on the previous
line, and may optionally state the justification for the derivation in that step.
Here is an example:

```
axiom (idright) mul(A, e) = A
axiom (idleft) mul(e, A) = A
axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
theorem (idcomm)
mul(A, e) = mul(e, A)
proof
A = A
mul(A, e) = A [by idright]
mul(A, e) = mul(e, A) [by idleft]
qed
```

For improved human usability, Eqthy is usually embedded within Markdown documents. This allows proofs to be written in a more "literate" style, with interspersed explanatory prose and references in the form of hyperlinks.

For a fuller description of the language, including a set of Falderal
tests, see **doc/Eqthy.md**.

A number of proofs have been written in Eqthy to date. These can be found in
the **eg/** directory. In particular, there are worked-out proofs:

- of the Socks and Shoes theorem in group theory
- in Propositional Algebra

with hopefully more to come in the future.

The Eqthy language is still at an early stage and is subject to change. However, since the idea is to accumulate a database of proofs which can be built upon, it is unlikely that the format of the language will change radically.

### Design Principles

Probably the language that Eqthy most resembles, in spirit, is Metamath; but its underlying mechanics are rather different. Eqthy is based on equational logic, so each step is an equation.

Eqthy's design attempts to reconcile simplicity of implementation on a machine with human usability. It should be understood that this is a balancing act; adding features to the language which improve usability will generally be detrimental to simplicity, and vice versa.

It has been implemented in Python in about 550 lines of code; the core verifier module is less than 200 lines of code. For more details, see the Implementations section below.

It is also possible for a human to write Eqthy documents by hand, and to read them, without much specialized knowledge. The base logic is equational logic, which has only 5 rules of inference, and these rules are particularly widely understood; "replace equals with equals" is a standard part of the high-school algebra cirriculum.

(In comparison, `mmverifier.py`

, a Python implementation of a Metamath
checker, is 360 lines of code; and while it is undoubtedly simple, the
Metamath language is not widely regarded as being easy to write or read.)

### Implementations

While the language does not prescribe any specific application for proofs written in Eqthy, it is reasonable to expect that one of the main reasons one would want a computer to read one would be for it to check it for validity.

This distribution contains such a proof checker, written in Python 3.
The source code for it can be found in the **src/** directory.

The core module that does proof checking,
**eqthy.verifier**, is less than 200 lines in length,
despite having many logging statements (which both act as comments, and provide a
trace to help the user understand the execution of the verifier on any given
document).

The desire is to make reading the code and understanding its behaviour as un-intimidating as possible.

## TODO

- Handle "on LHS", "on RHS" in hints.
- Show the step number or line number in the error message when there is a derivation error.
- Allow rules to be instantiated with variable names other than the ones that are specified in the rule.
- Allow context accumulated when verifying one document to be carried over and used when verifying the next documnet.
- Allow the first line of a proof to be an axiom.
- Arity checking? Would prevent some silly errors in axioms.

##
Commit History
@master
`git clone https://git.catseye.tc/Eqthy/`

- Merge pull request #1 from catseye/develop-0.1 Chris Pressey (commit: GitHub) 4 days ago
- Finish the Propositional Algebra proof! Such yay, much rejoicing Chris Pressey 5 days ago
- Modus ponens! After fixing a silly error in an axiom definition. Chris Pressey 5 days ago
- Checkpoint propositional algebra proof (take different tack on MP.) Chris Pressey 5 days ago
- Checkpoint working out the propositional algebra proof. Chris Pressey 12 days ago
- Add the hints given in the book. Chris Pressey 12 days ago
- Pick a proof for this and start working it out. Chris Pressey 12 days ago
- Rename example file again, to get it right this time. Chris Pressey 12 days ago
- Tidy up some of the example proofs a bit. Chris Pressey 12 days ago
- Rename example proof which is actually embedded in Markdown. Chris Pressey 12 days ago