git @ Cat's Eye Technologies Eqthy / e5205a7
Refactor documentation. Chris Pressey 2 years ago
4 changed file(s) with 364 addition(s) and 326 deletion(s). Raw diff Collapse all Expand all
+19
-84
README.md less more
00 Eqthy
11 =====
22
3 **Eqthy** is a language for equational proofs. It's similar to, but
4 different from, the "calculational style" developed and popularized by
5 Dijkstra et al.
3 **Eqthy** is a language for equational proofs, designed to be both
4 machine-readable and human-usable. It strongly resembles equational
5 styles of proof as they are often found in introductory textbooks,
6 where each line follows from the previous line.
67
7 This document is a sketch. It describes the language. It mentions some
8 things a processor of the language might be expected to do.
8 Here is an example of what an Eqthy proof looks like:
99
10 An Eqthy document consists of any number of axioms and theorems. Each
11 axiom is an equation. An equation equates two terms. Terms consist of
12 constructors (also called function symbols) and variables. Variables begin
13 with uppercase letters. Constructors begin with lowercase letters are
14 followed by a list of zero or more subterms, enclosed in parentheses. If a
15 term has no subterms, it is called an "atom" and the parentheses may be
16 omitted.
17
18 Each axiom may optionally by named. Here are some example axioms:
19
20 axiom (#id-right) mul(A, e) = A
21 axiom (#id-left) mul(e, A) = A
22 axiom (#assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
23
24 A theorem gives an equation, followed by a sequence of equations that shows
25 that the equation can be derived using the available means. The available
26 means are:
27
28 * the axioms that have been previously defined
29 * the theorems that have been previously proved
30 * the rules of inference of equational logic, which are
31 * Reflexivity (A=A)
32 * Transitivity (if A=B and B=C then A=C)
33 * Substitution (if x(A)=y(A) then x(B)=y(B))
34 * Congruence (if A=B then x(A)=x(B))
35
36 The sequence of equations following a theorem is a proof. Each equation in
37 the proof is optionally annotated with a hint that follows it, indicating what
38 axiom, theorem, or rule of inference was used to derive it.
39
40 theorem (#id-comm)
10 axiom (id-right) mul(A, e) = A
11 axiom (id-left) mul(e, A) = A
12 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
13 theorem (id-comm)
4114 mul(A, e) = mul(e, A)
4215 proof
43 A = A [by reflexivity]
44 mul(A, e) = A [by #id-right on LHS]
45 mul(A, e) = mul(e, A) [by #id-left on RHS]
16 A = A
17 mul(A, e) = A [by id-right]
18 mul(A, e) = mul(e, A) [by id-left]
4619 qed
4720
48 Each step in a theorem can be checked for validity by a processor. The processor
49 may be a computer program. During this checking, the processor has access to all
50 the axioms and all the theories previously given in this Eqthy document
51 (and possibly from shared libraries). The checking process ensures that the first
52 step can be obtained from an axiom or previously proved theory, that each step
53 can be derived from the previous step, and that the equation being proved matches
54 the last step. Once a theorem has been checked, the equation that was provded
55 is available for use in subsequent theorems.
21 For a fuller description of the language, including a set of Falderal
22 tests, see [doc/Eqthy.md](doc/Eqthy.md).
5623
57 The hint on each step is optional. If omitted, it is assumed that the processor will do
58 what it can to search for what rule might have been applied, to derive this step from the previous
59 step. It is also assumed that the processor may have limitations in this regard, so in
60 practice, the hint might not be optional on steps for which necessarily involve more searching.
24 The language does not prescribe any specific usage but it is expected
25 that one of the main reasons for a computer to read a proof written
26 in Eqthy would be to check it for validity.
6127
62 Eqthy itself makes no assumption about the power of any particular processor to
63 search for derivations in the absence of hints. A processor may not be able to
64 derive anything without hints, or it may not require any hints at all. What is
65 required of a processor is that it does not allow a chain of steps which is invalid
66 to be reported as valid and subsequently used in other proofs.
67
68 In the above theorem, if we omit the hints, the processor must deduce by itself that:
69
70 * `A = A` is an instance of reflexivity. This is easy to see, because the LHS and RHS are
71 identical.
72 * `mul(A, e) = A` is an application of `#id-right` on the LHS. This can be seen
73 by searching through the available axioms and previously-proved theorem steps,
74 to see which rewrite of `A = A` would result in `mul(A, e) = A`.
75 * The third step is similar to the second.
76
77 Additionally, if the step `B = A` appears immediately after `A = B`, it can infer that
78 the rule of symmetry was invoked.
79
80 The rules of substitution and congruence may also be invoked; they may require a hint,
81 as it is sometimes not obvious what is being substituted where.
82
83 e = e [by reflexivity]
84 mul(C, inv(C)) = e [by #inverse on LHS]
85 mul(mul(A, B), inv(mul(A, B))) = e [by substitution of mul(A, B) for C]
86 mul(A, mul(mul(A, B), inv(mul(A, B)))) = mul(A, e) [by congruence of B and mul(A, B)]
87
88 Once the processor has resolved what rules were applies and checked that the proof is
89 valid, it can _pretty-print_ an _annotated_ version of the input Eqthy document, one which
90 includes all of the hints that it inferred. This pretty-printed document can be checked
91 again in the future, and more efficiently, as all the searches for hints have been
92 already performed.
28 This distribution contains such a proof checker, written in Python 3.
29 The source code for it can be found in the [src/](src/) directory.
9330
9431 TODO
9532 ----
9633
97 * Describe the supplied implementation(s)
9834 * `[by previous_theorem]`
9935 * Document the Syntax for Comments
100 * Document status of `#` in names
10136 * impl: show step number or line number when cannot derive next step
+344
-0
doc/Eqthy.md less more
0 Eqthy
1 =====
2
3 Description of the Language
4 ---------------------------
5
6 An Eqthy document consists of any number of axioms and theorems. Each
7 axiom is an equation. An equation equates two terms. Terms consist of
8 constructors (also called function symbols) and variables. Variables begin
9 with uppercase letters. Constructors begin with lowercase letters are
10 followed by a list of zero or more subterms, enclosed in parentheses. If a
11 term has no subterms, it is called an "atom" and the parentheses may be
12 omitted.
13
14 Each axiom may optionally by named. Here are some example axioms:
15
16 axiom (#id-right) mul(A, e) = A
17 axiom (#id-left) mul(e, A) = A
18 axiom (#assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
19
20 A theorem gives an equation, followed by a sequence of equations that shows
21 that the equation can be derived using the available means. The available
22 means are:
23
24 * the axioms that have been previously defined
25 * the theorems that have been previously proved
26 * the rules of inference of equational logic, which are
27 * Reflexivity (A=A)
28 * Transitivity (if A=B and B=C then A=C)
29 * Substitution (if x(A)=y(A) then x(B)=y(B))
30 * Congruence (if A=B then x(A)=x(B))
31
32 The sequence of equations following a theorem is a proof. Each equation in
33 the proof is optionally annotated with a hint that follows it, indicating what
34 axiom, theorem, or rule of inference was used to derive it.
35
36 theorem (#id-comm)
37 mul(A, e) = mul(e, A)
38 proof
39 A = A [by reflexivity]
40 mul(A, e) = A [by #id-right on LHS]
41 mul(A, e) = mul(e, A) [by #id-left on RHS]
42 qed
43
44 Each step in a theorem can be checked for validity by a processor. The processor
45 may be a computer program. During this checking, the processor has access to all
46 the axioms and all the theories previously given in this Eqthy document
47 (and possibly from shared libraries). The checking process ensures that the first
48 step can be obtained from an axiom or previously proved theory, that each step
49 can be derived from the previous step, and that the equation being proved matches
50 the last step. Once a theorem has been checked, the equation that was provded
51 is available for use in subsequent theorems.
52
53 The hint on each step is optional. If omitted, it is assumed that the processor will do
54 what it can to search for what rule might have been applied, to derive this step from the previous
55 step. It is also assumed that the processor may have limitations in this regard, so in
56 practice, the hint might not be optional on steps for which necessarily involve more searching.
57
58 Eqthy itself makes no assumption about the power of any particular processor to
59 search for derivations in the absence of hints. A processor may not be able to
60 derive anything without hints, or it may not require any hints at all. What is
61 required of a processor is that it does not allow a chain of steps which is invalid
62 to be reported as valid and subsequently used in other proofs.
63
64 In the above theorem, if we omit the hints, the processor must deduce by itself that:
65
66 * `A = A` is an instance of reflexivity. This is easy to see, because the LHS and RHS are
67 identical.
68 * `mul(A, e) = A` is an application of `#id-right` on the LHS. This can be seen
69 by searching through the available axioms and previously-proved theorem steps,
70 to see which rewrite of `A = A` would result in `mul(A, e) = A`.
71 * The third step is similar to the second.
72
73 Additionally, if the step `B = A` appears immediately after `A = B`, it can infer that
74 the rule of symmetry was invoked.
75
76 The rules of substitution and congruence may also be invoked; they may require a hint,
77 as it is sometimes not obvious what is being substituted where.
78
79 e = e [by reflexivity]
80 mul(C, inv(C)) = e [by #inverse on LHS]
81 mul(mul(A, B), inv(mul(A, B))) = e [by substitution of mul(A, B) for C]
82 mul(A, mul(mul(A, B), inv(mul(A, B)))) = mul(A, e) [by congruence of B and mul(A, B)]
83
84 Once the processor has resolved what rules were applies and checked that the proof is
85 valid, it can _pretty-print_ an _annotated_ version of the input Eqthy document, one which
86 includes all of the hints that it inferred. This pretty-printed document can be checked
87 again in the future, and more efficiently, as all the searches for hints have been
88 already performed.
89
90 Prescriptive Examples
91 ---------------------
92
93 We now present a number of example Eqthy documents in
94 Falderal format, in the hopes that they will help clarify
95 the semantics of the language.
96
97 -> Functionality "Parse Eqthy Document" is implemented by shell command
98 -> "python3 bin/eqthy --dump-ast %(test-body-file)"
99
100 ### Parse Eqthy Document
101
102 -> Tests for functionality "Parse Eqthy Document"
103
104 This document is well-formed. It will parse.
105
106 axiom inv(A) = A
107 ===> Development(axioms=[Axiom(name=None, eqn=Eqn(lhs=Term(ctor='inv', subterms=[Variable(name='A')]), rhs=Variable(name='A')))], theorems=[])
108
109 This document is not well-formed. It will not parse.
110
111 axiom inv(A) .
112 ???> Expected '=', but found '.'
113
114 ### Check Eqthy Document
115
116 -> Functionality "Check Eqthy Document" is implemented by shell command
117 -> "python3 bin/eqthy %(test-body-file) && echo 'ok'"
118
119 -> Tests for functionality "Check Eqthy Document"
120
121 This document consists of some axioms and a theorem.
122
123 axiom mul(A, e) = A
124 axiom mul(e, A) = A
125 axiom mul(A, mul(B, C)) = mul(mul(A, B), C)
126 theorem
127 mul(A, e) = A
128 proof
129 A = A
130 mul(A, e) = A
131 qed
132 ===> ok
133
134 Any variable name you like can be used in a theorem.
135
136 axiom mul(A, e) = A
137 axiom mul(e, A) = A
138 axiom mul(A, mul(B, C)) = mul(mul(A, B), C)
139 theorem
140 mul(Z, e) = Z
141 proof
142 Z = Z
143 mul(Z, e) = Z
144 qed
145 ===> ok
146
147 This "proof" contains a misstep.
148
149 axiom mul(A, e) = A
150 axiom mul(e, A) = A
151 axiom mul(A, mul(B, C)) = mul(mul(A, B), C)
152 theorem
153 mul(A, e) = mul(foo, mul(e, A))
154 proof
155 A = A
156 mul(A, e) = A
157 mul(A, e) = mul(foo, mul(e, A))
158 qed
159 ???> DerivationError: Could not derive mul(A, e) = mul(foo, mul(e, A)) from mul(A, e) = A
160
161 This theorem does not prove what it says it proves.
162
163 axiom mul(A, e) = A
164 axiom mul(e, A) = A
165 axiom mul(A, mul(B, C)) = mul(mul(A, B), C)
166 theorem
167 mul(A, e) = mul(A, A)
168 proof
169 A = A
170 mul(A, e) = A
171 qed
172 ???> DerivationError: No step in proof showed mul(A, e) = mul(A, A)
173
174 This proof requires rewrites on the right-hand side of the equation.
175
176 axiom mul(A, e) = A
177 axiom mul(e, A) = A
178 axiom mul(A, mul(B, C)) = mul(mul(A, B), C)
179 theorem
180 mul(A, e) = mul(e, A)
181 proof
182 A = A
183 mul(A, e) = A
184 mul(A, e) = mul(e, A)
185 qed
186 ===> ok
187
188 Axioms and theorems can be named.
189
190 axiom (idright) mul(A, e) = A
191 axiom (idleft) mul(e, A) = A
192 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
193 theorem (idcomm)
194 mul(A, e) = mul(e, A)
195 proof
196 A = A
197 mul(A, e) = A
198 mul(A, e) = mul(e, A)
199 qed
200 ===> ok
201
202 Names of axioms and theorems can begin with a `#` symbol
203 and contain `-` symbols.
204
205 axiom (#id-right) mul(A, e) = A
206 axiom (#id-left) mul(e, A) = A
207 axiom (#assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
208 theorem (#id-comm)
209 mul(A, e) = mul(e, A)
210 proof
211 A = A
212 mul(A, e) = A [by #id-right]
213 mul(A, e) = mul(e, A)
214 qed
215 ===> ok
216
217 #### Hints
218
219 Proof steps can name the axiom being used in a hint written next to
220 the step.
221
222 axiom (idright) mul(A, e) = A
223 axiom (idleft) mul(e, A) = A
224 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
225 theorem
226 A = mul(A, e)
227 proof
228 A = A
229 A = mul(A, e) [by idright]
230 qed
231 ===> ok
232
233 Naming an axiom in a hint when the axiom used was not actually used there
234 is incorrect. It is reasonable to (at least) warn the user of this mistake.
235
236 axiom (idright) mul(A, e) = A
237 axiom (idleft) mul(e, A) = A
238 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
239 theorem
240 A = mul(A, e)
241 proof
242 A = A
243 A = mul(A, e) [by idleft]
244 qed
245 ???> waaaaa
246
247 Using the reflexivity hint when the rule used was not actually reflexivity
248 is incorrect. It is reasonable to (at least) warn the user of this mistake.
249
250 axiom (idright) mul(A, e) = A
251 axiom (idleft) mul(e, A) = A
252 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
253 theorem
254 A = mul(A, e)
255 proof
256 A = A
257 A = mul(A, e) [by reflexivity]
258 qed
259 ???> Reflexivity
260
261 Proof steps can use the "substitution" hint.
262
263 axiom (idright) mul(A, e) = A
264 axiom (idleft) mul(e, A) = A
265 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
266 theorem
267 mul(mul(e, B), e) = mul(e, B)
268 proof
269 A = A
270 mul(A, e) = A
271 mul(mul(e, B), e) = mul(e, B) [by substitution of mul(e, B) into A]
272 qed
273 ===> ok
274
275 In a substitution hint, the "into" part must name a variable.
276
277 axiom (idright) mul(A, e) = A
278 axiom (idleft) mul(e, A) = A
279 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
280 theorem
281 mul(mul(e, B), e) = mul(e, B)
282 proof
283 A = A
284 mul(A, e) = A
285 mul(mul(e, B), e) = mul(e, B) [by substitution of mul(e, B) into mul(e, e)]
286 qed
287 ???> Expected variable
288
289 Using the substitution hint when the rule used was not actually substitution
290 is incorrect. It is reasonable to (at least) warn the user of this mistake.
291
292 axiom (idright) mul(A, e) = A
293 axiom (idleft) mul(e, A) = A
294 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
295 theorem
296 mul(A, e) = A
297 proof
298 A = A
299 mul(A, e) = A [by substitution of mul(A, e) into A]
300 qed
301 ???> Substitution
302
303 Proof steps can use the "congruence" hint.
304
305 axiom (idright) mul(A, e) = A
306 axiom (idleft) mul(e, A) = A
307 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
308 theorem
309 mul(B, mul(A, e)) = mul(B, A)
310 proof
311 A = A
312 mul(A, e) = A
313 mul(B, mul(A, e)) = mul(B, A) [by congruence of A and mul(B, A)]
314 qed
315 ===> ok
316
317 In a congruence hint, the first part must name a variable.
318
319 axiom (idright) mul(A, e) = A
320 axiom (idleft) mul(e, A) = A
321 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
322 theorem
323 mul(B, mul(A, e)) = mul(B, A)
324 proof
325 A = A
326 mul(A, e) = A
327 mul(B, mul(A, e)) = mul(B, A) [by congruence of mul(B, A) and A]
328 qed
329 ???> Expected variable
330
331 Using the congruence hint when the rule used was not actually substitution
332 is incorrect. It is reasonable to (at least) warn the user of this mistake.
333
334 axiom (idright) mul(A, e) = A
335 axiom (idleft) mul(e, A) = A
336 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
337 theorem
338 mul(A, e) = A
339 proof
340 A = A
341 mul(A, e) = A [by congruence of A and mul(A, e)]
342 qed
343 ???> Congruence
+1
-2
test.sh less more
00 #!/bin/sh
11
2 falderal tests/*.md || exit 1
3
2 falderal doc/*.md || exit 1
+0
-240
tests/Eqthy.md less more
0 Eqthy
1 =====
2
3 This document provides a number of example Eqthy document in
4 Falderal format, in the hopes that they will help clarify
5 the semantics of the language.
6 For an overview of the language, see the README file.
7
8 -> Functionality "Parse Eqthy Document" is implemented by shell command
9 -> "python3 bin/eqthy --dump-ast %(test-body-file)"
10
11 ### Parse Eqthy Document
12
13 -> Tests for functionality "Parse Eqthy Document"
14
15 This document is well-formed. It will parse.
16
17 axiom inv(A) = A
18 ===> Development(axioms=[Axiom(name=None, eqn=Eqn(lhs=Term(ctor='inv', subterms=[Variable(name='A')]), rhs=Variable(name='A')))], theorems=[])
19
20 This document is not well-formed. It will not parse.
21
22 axiom inv(A) .
23 ???> Expected '=', but found '.'
24
25 ### Check Eqthy Document
26
27 -> Functionality "Check Eqthy Document" is implemented by shell command
28 -> "python3 bin/eqthy %(test-body-file) && echo 'ok'"
29
30 -> Tests for functionality "Check Eqthy Document"
31
32 This document consists of some axioms and a theorem.
33
34 axiom mul(A, e) = A
35 axiom mul(e, A) = A
36 axiom mul(A, mul(B, C)) = mul(mul(A, B), C)
37 theorem
38 mul(A, e) = A
39 proof
40 A = A
41 mul(A, e) = A
42 qed
43 ===> ok
44
45 Any variable name you like can be used in a theorem.
46
47 axiom mul(A, e) = A
48 axiom mul(e, A) = A
49 axiom mul(A, mul(B, C)) = mul(mul(A, B), C)
50 theorem
51 mul(Z, e) = Z
52 proof
53 Z = Z
54 mul(Z, e) = Z
55 qed
56 ===> ok
57
58 This "proof" contains a misstep.
59
60 axiom mul(A, e) = A
61 axiom mul(e, A) = A
62 axiom mul(A, mul(B, C)) = mul(mul(A, B), C)
63 theorem
64 mul(A, e) = mul(foo, mul(e, A))
65 proof
66 A = A
67 mul(A, e) = A
68 mul(A, e) = mul(foo, mul(e, A))
69 qed
70 ???> DerivationError: Could not derive mul(A, e) = mul(foo, mul(e, A)) from mul(A, e) = A
71
72 This theorem does not prove what it says it proves.
73
74 axiom mul(A, e) = A
75 axiom mul(e, A) = A
76 axiom mul(A, mul(B, C)) = mul(mul(A, B), C)
77 theorem
78 mul(A, e) = mul(A, A)
79 proof
80 A = A
81 mul(A, e) = A
82 qed
83 ???> DerivationError: No step in proof showed mul(A, e) = mul(A, A)
84
85 This proof requires rewrites on the right-hand side of the equation.
86
87 axiom mul(A, e) = A
88 axiom mul(e, A) = A
89 axiom mul(A, mul(B, C)) = mul(mul(A, B), C)
90 theorem
91 mul(A, e) = mul(e, A)
92 proof
93 A = A
94 mul(A, e) = A
95 mul(A, e) = mul(e, A)
96 qed
97 ===> ok
98
99 Axioms and theorems can be named.
100
101 axiom (idright) mul(A, e) = A
102 axiom (idleft) mul(e, A) = A
103 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
104 theorem (idcomm)
105 mul(A, e) = mul(e, A)
106 proof
107 A = A
108 mul(A, e) = A
109 mul(A, e) = mul(e, A)
110 qed
111 ===> ok
112
113 #### Hints
114
115 Proof steps can name the axiom being used in a hint written next to
116 the step.
117
118 axiom (idright) mul(A, e) = A
119 axiom (idleft) mul(e, A) = A
120 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
121 theorem
122 A = mul(A, e)
123 proof
124 A = A
125 A = mul(A, e) [by idright]
126 qed
127 ===> ok
128
129 Naming an axiom in a hint when the axiom used was not actually used there
130 is incorrect. It is reasonable to (at least) warn the user of this mistake.
131
132 axiom (idright) mul(A, e) = A
133 axiom (idleft) mul(e, A) = A
134 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
135 theorem
136 A = mul(A, e)
137 proof
138 A = A
139 A = mul(A, e) [by idleft]
140 qed
141 ???> waaaaa
142
143 Using the reflexivity hint when the rule used was not actually reflexivity
144 is incorrect. It is reasonable to (at least) warn the user of this mistake.
145
146 axiom (idright) mul(A, e) = A
147 axiom (idleft) mul(e, A) = A
148 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
149 theorem
150 A = mul(A, e)
151 proof
152 A = A
153 A = mul(A, e) [by reflexivity]
154 qed
155 ???> Reflexivity
156
157 Proof steps can use the "substitution" hint.
158
159 axiom (idright) mul(A, e) = A
160 axiom (idleft) mul(e, A) = A
161 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
162 theorem
163 mul(mul(e, B), e) = mul(e, B)
164 proof
165 A = A
166 mul(A, e) = A
167 mul(mul(e, B), e) = mul(e, B) [by substitution of mul(e, B) into A]
168 qed
169 ===> ok
170
171 In a substitution hint, the "into" part must name a variable.
172
173 axiom (idright) mul(A, e) = A
174 axiom (idleft) mul(e, A) = A
175 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
176 theorem
177 mul(mul(e, B), e) = mul(e, B)
178 proof
179 A = A
180 mul(A, e) = A
181 mul(mul(e, B), e) = mul(e, B) [by substitution of mul(e, B) into mul(e, e)]
182 qed
183 ???> Expected variable
184
185 Using the substitution hint when the rule used was not actually substitution
186 is incorrect. It is reasonable to (at least) warn the user of this mistake.
187
188 axiom (idright) mul(A, e) = A
189 axiom (idleft) mul(e, A) = A
190 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
191 theorem
192 mul(A, e) = A
193 proof
194 A = A
195 mul(A, e) = A [by substitution of mul(A, e) into A]
196 qed
197 ???> Substitution
198
199 Proof steps can use the "congruence" hint.
200
201 axiom (idright) mul(A, e) = A
202 axiom (idleft) mul(e, A) = A
203 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
204 theorem
205 mul(B, mul(A, e)) = mul(B, A)
206 proof
207 A = A
208 mul(A, e) = A
209 mul(B, mul(A, e)) = mul(B, A) [by congruence of A and mul(B, A)]
210 qed
211 ===> ok
212
213 In a congruence hint, the first part must name a variable.
214
215 axiom (idright) mul(A, e) = A
216 axiom (idleft) mul(e, A) = A
217 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
218 theorem
219 mul(B, mul(A, e)) = mul(B, A)
220 proof
221 A = A
222 mul(A, e) = A
223 mul(B, mul(A, e)) = mul(B, A) [by congruence of mul(B, A) and A]
224 qed
225 ???> Expected variable
226
227 Using the congruence hint when the rule used was not actually substitution
228 is incorrect. It is reasonable to (at least) warn the user of this mistake.
229
230 axiom (idright) mul(A, e) = A
231 axiom (idleft) mul(e, A) = A
232 axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
233 theorem
234 mul(A, e) = A
235 proof
236 A = A
237 mul(A, e) = A [by congruence of A and mul(A, e)]
238 qed
239 ???> Congruence