git @ Cat's Eye Technologies Maxixe / 23c984b
Enforcing a final rule in a block-case is now optional. Chris Pressey 8 years ago
4 changed file(s) with 47 addition(s) and 31 deletion(s). Raw diff Collapse all Expand all
+16
-25
doc/Examples.md less more
9494 block Disjunction
9595 case
9696 Disj_Elim_Left = or(P, Q) |- P
97 Disj_Conc_Left = P |- P
9897 end
9998 case
10099 Disj_Elim_Right = or(P, Q) |- Q
101 Disj_Conc_Right = P |- P
102100 end
103101 end
104102 Tautology = P |- P
111109 case
112110 Step_2 = a by Disj_Elim_Left with Step_1
113111 Step_3 = or(b, a) by Disj_Intro_Left with Step_2, b
114 Step_4 = or(b, a) by Disj_Conc_Left with Step_3
115 end
116 case
117 Step_5 = b by Disj_Elim_Right with Step_1
118 Step_6 = or(b, a) by Disj_Intro_Right with Step_5, a
119 Step_7 = or(b, a) by Disj_Conc_Right with Step_6
120 end
121 end
122 Step_8 = or(b, a) by Tautology with Step_7
112 end
113 case
114 Step_4 = b by Disj_Elim_Right with Step_1
115 Step_5 = or(b, a) by Disj_Intro_Right with Step_4, a
116 end
117 end
118 Step_6 = or(b, a) by Tautology with Step_5
123119 qed
124120 ===> ok
125121
244240 block Existential_Instantiation
245241 case
246242 Let = exists(X, P) ; V{unique local atom} |- P[X -> V]
247 Then = P |- P
248243 end
249244 end
250245
264259 Step_8 = socrates(k) by Simplification_Right with Step_4
265260 Step_9 = and(mortal(k), socrates(k)) by Conjunction with Step_7, Step_8
266261 Step_10 = exists(y, and(mortal(y), socrates(y))) by Existential_Generalization with Step_9, k, y
267 Step_11 = exists(y, and(mortal(y), socrates(y))) by Then with Step_10
268 end
269 end
270 Step_12 = exists(y, and(mortal(y), socrates(y))) by Tautology with Step_11
262 end
263 end
264 Step_11 = exists(y, and(mortal(y), socrates(y))) by Tautology with Step_10
271265 qed
272266 ===> ok
273267
280274 block EI
281275 case
282276 Let = exists(X, P) ; V{unique local atom} |- P[X -> V]
283 Then = P |- P
284277 end
285278 end
286279
328321 block EI
329322 case
330323 Let = exists(X, P) ; V{unique local atom} |- P[X -> V]
331 Then = P |- P
332324 end
333325 end
334326
370362 Step_11 = biimpl(even(add(x, c(1))), exists(m, eq(add(x, c(1)), add(m, m)))) by UI with Step_10, add(x, c(1))
371363 Step_12 = impl(exists(m, eq(add(x, c(1)), add(m, m))), even(add(x, c(1)))) by Reverse_Weakening with Step_11
372364 Step_13 = even(add(x, c(1))) by Modus_Ponens with Step_9, Step_12
373 Step_14 = even(add(x, c(1))) by Then with Step_13
374365 end
375366 end
376 Step_15 = impl(odd(x), even(add(x, c(1)))) by Conclusion with Step_1, Step_14
377 end
378 end
379 Step_16 = forall(y, impl(odd(y), even(add(y, c(1))))) by UG with Step_15, x, y
380 qed
381 ===> ok
367 Step_14 = impl(odd(x), even(add(x, c(1)))) by Conclusion with Step_1, Step_13
368 end
369 end
370 Step_15 = forall(y, impl(odd(y), even(add(y, c(1))))) by UG with Step_14, x, y
371 qed
372 ===> ok
+26
-3
doc/Maxixe.md less more
382382 instantiating a specially-declared _block rule_. The structure of a block rule determines
383383 rules determine the structure of the block.
384384
385 A block rule (and thus a block) consists of one or more _cases_. Each case contains two
386 non-block rules. The first rule must be used in the first step of the case, and the second
387 rule must be used in the final step of the case.
385 A block rule (and thus a block) consists of one or more _cases_. Each case contains one
386 or two non-block rules. The first rule must be used in the first step of the case, and
387 the second rule, if given, must be used in the final step of the case.
388388
389389 given
390390 A = |- a
394394 C = b |- c
395395 end
396396 end
397 D = c |- d
398 show
399 d
400 proof
401 S1 = a by A
402 block Subproof
403 case
404 S2 = b by B with S1
405 S3 = c by C with S2
406 end
407 end
408 S4 = d by D with S3
409 qed
410 ===> ok
411
412 given
413 A = |- a
414 block Subproof
415 case
416 B = a |- b
417 end
418 end
419 C = b |- c
397420 D = c |- d
398421 show
399422 d
+1
-1
src/maxixe/checker.py less more
4141 raise ValueError("initial step of case %s of %s must use rule %s" %
4242 (case_num, self.current_block.name, block_rule_case.initial.var.name)
4343 )
44 if case.steps[-1].by.name != block_rule_case.final.var.name:
44 if block_rule_case.final is not None and case.steps[-1].by.name != block_rule_case.final.var.name:
4545 raise ValueError("final step of case %s of %s must use rule %s" %
4646 (case_num, self.current_block.name, block_rule_case.final.var.name)
4747 )
+4
-2
src/maxixe/parser.py less more
77 # Proof ::= "given" {Rule | BlockRule} "show" Term "proof" {Step | Block} "qed".
88 # Rule ::= Var Attributes "=" [Hyp {";" Hyp}] "|-" Term ["[" Subst {"," Subst} "]"].
99 # BlockRule ::= "block" Var {BlockRuleCase} "end".
10 # BlockRuleCase ::= "case" Rule Rule "end".
10 # BlockRuleCase ::= "case" Rule [Rule] "end".
1111 # Hyp ::= Term Attributes.
1212 # Attributes ::= ["{" {Atom} "}"].
1313 # Subst ::= Term "->" Term.
8888 cases = []
8989 self.scanner.expect('case')
9090 initial = self.rule()
91 final = self.rule()
91 final = None
92 if not self.scanner.on('end'):
93 final = self.rule()
9294 self.scanner.expect('end')
9395 return BlockRuleCase(initial=initial, final=final)
9496