Commit 595b263f10167ba7cbbc82f3e4f4905998b0ec13 - Eqthy

Demonstrate multiple theorems in a single document. Chris Pressey 2 years ago

3 changed file(s) with 57 addition(s) and 3 deletion(s). Raw diff Collapse all Expand all

-2

README.md less more

46	46	----
47	47
48	48	* Handle "on LHS", "on RHS" in hints.
49		* Demonstrate multiple theorems, and that previous theorems can be used
50		as justifications in proof steps.
	49	* Demonstrate that previous theorems can be used as justifications in
	50	proof steps.
51	51	* Show the step number or line number in the error message when
52	52	there is a derivation error.
53	53	* Allow rules to be instantiated with variable names other than the
54	54	ones that are specified in the rule.
	55	* Decide what happens when multiple files are given on the command line.
	56	Simply concatenating them does not play well with a grammar where
	57	axioms cannot follow theorems. Ideally we would want to trace the
	58	source file name for error reporting too.

+50

-0

doc/Eqthy.md less more

138	138	qed
139	139	===> ok
140	140
	141	A document may contain more than one theorem.
	142
	143	axiom mul(A, e) = A
	144	axiom mul(e, A) = A
	145	axiom mul(A, mul(B, C)) = mul(mul(A, B), C)
	146	theorem
	147	mul(A, e) = mul(e, A)
	148	proof
	149	A = A
	150	mul(A, e) = A
	151	mul(A, e) = mul(e, A)
	152	qed
	153	theorem
	154	mul(e, A) = mul(A, e)
	155	proof
	156	A = A
	157	A = mul(A, e)
	158	mul(e, A) = mul(A, e)
	159	qed
	160	===> ok
	161
141	162	Any variable name you like can be used in a theorem.
142	163
143	164	axiom mul(A, e) = A

177	198	mul(A, e) = A
178	199	qed
179	200	???> DerivationError: No step in proof showed mul(A, e) = mul(A, A)
	201
	202	Typically, all theorems that are given in the document are checked,
	203	and are checked in sequence, and checking stops at the first failure.
	204
	205	axiom mul(A, e) = A
	206	axiom mul(e, A) = A
	207	axiom mul(A, mul(B, C)) = mul(mul(A, B), C)
	208	theorem
	209	mul(A, e) = mul(e, A)
	210	proof
	211	A = A
	212	mul(A, e) = A
	213	mul(A, e) = mul(e, A)
	214	qed
	215	theorem
	216	mul(e, A) = mul(A, e)
	217	proof
	218	A = A
	219	A = mul(A, e)
	220	mul(e, A) = mul(A, A)
	221	qed
	222	theorem
	223	mul(e, A) = mul(A, e)
	224	proof
	225	A = A
	226	A = mul(A, e)
	227	mul(e, A) = mul(e, A)
	228	qed
	229	???> DerivationError: Could not derive mul(e, A) = mul(A, A) from A = mul(A, e)
180	230
181	231	This proof requires rewrites on the right-hand side of the equation.
182	232

-1

src/eqthy/main.py less more

34	34	text = ''
35	35	for filename in options.input_files:
36	36	with codecs.open(filename, 'r', encoding='UTF-8') as f:
37		text += f.read()
	37	text += f.read() + '\n'
38	38
39	39	p = Parser(text, filename)
40	40	ast = p.document()