Commit 8940f8d8d1bb4195cc8c957a948762416d6e46b3 - Eqthy

Small formatting updates and fixes. Chris Pressey 1 year, 4 months ago

2 changed file(s) with 13 addition(s) and 11 deletion(s). Raw diff Collapse all Expand all

-5

README.md less more

61	61	adding features to the language which improve usability will generally be
62	62	detrimental to simplicity, and vice versa.
63	63
64		It has been implemented in Python in about 550 lines of code; the core
65		verifier module is less than 200 lines of code. For more details, see
	64	It has been implemented in Python 3 in about 720 lines of code; the core
	65	verifier module is less than 150 lines of code. For more details, see
66	66	the [Implementations](#implementations) section below.
67	67
68	68	It is also possible for a human to write Eqthy documents by hand, and

71	71	rules are particularly widely understood; "replace equals with equals" is
72	72	a standard part of the high-school algebra cirriculum.
73	73
74		(In comparison, `mmverifier.py`, a Python implementation of a Metamath
75		checker, is 360 lines of code; and while it is undoubtedly simple, the
	74	(In comparison, [mmverify.py][], a Python implementation of a Metamath
	75	checker, is about 360 lines of code; and while it is undoubtedly simple, the
76	76	Metamath language is not widely regarded as being easy to write or read.)
77	77
78	78	### Implementations

100	100
101	101	* Handle "on LHS", "on RHS" in hints.
102	102	* Allow context accumulated when verifying one document to be
103		carried over and used when verifying the next documnet.
	103	carried over and used when verifying the next document.
104	104	* Allow the first line of a proof to be an axiom.
105	105	* Scanner should report correct line number in errors
106	106	when Eqthy document is embedded in Markdown.

175	175	one language, which is only a modest superset of Eqthy.
176	176
177	177	[Metamath]: https://us.metamath.org/
	178	[mmverify.py]: https://github.com/david-a-wheeler/mmverify.py
178	179	[equational logic]: doc/Equational-Logic.md

-6

eg/boolean-algebra.eqthy.md less more

138	138	> infer
139	139	> not(and(A, B)) = or(not(A), not(B))
140	140
141		is not expressible in equational logic, so can't directly be written in Eqthy. At least, not the general version of it:
	141	is not expressible in equational logic, so can't directly be written in Eqthy.
	142	At least, not the general version of it:
	143
142	144	> From
143	145	> and(X, Y) = 0
144	146	> and
145	147	> or(X, Y) = 1
146	148	> infer
147	149	> not(X) = Y
148
149	150
150	151	But, we can still express the specific instance of it:
151	152

216	217	or(not(not(A)), not(B)) = not(and(not(A), B)) [by substitution of not(A) into A]
217	218	or(not(not(A)), not(not(B))) = not(and(not(A), not(B))) [by substitution of not(B) into B]
218	219	not(or(not(not(A)), not(not(B)))) = not(not(and(not(A), not(B)))) [by congruence of C and not(C)]
219		not(or(not(not(A)), not(not(B)))) = and(not(A), not(B))
220		not(or(A, not(not(B)))) = and(not(A), not(B))
221		not(or(A, B)) = and(not(A), not(B))
222		qed
	220	not(or(not(not(A)), not(not(B)))) = and(not(A), not(B))
	221	not(or(A, not(not(B)))) = and(not(A), not(B))
	222	not(or(A, B)) = and(not(A), not(B))
	223	qed