git @ Cat's Eye Technologies Maxixe / 6a5439c
Allow hole in Universal Generalization to be plugged. Chris Pressey 8 years ago
2 changed file(s) with 36 addition(s) and 1 deletion(s). Raw diff Collapse all Expand all
337337 ===> ok
338338
339339 The problem is that you should only be able to lift *arbitrary* (that is, *non* local)
340 variables into a forall. So we'll need something like `X{nonlocal}` in the UI.
340 variables into a forall. So let's try to fix that by adding `X{nonlocal}` in the UG.
341
342 given
343 Simplification_Right = and(P, Q) |- Q
344 Tautology = P |- P
345
346 UG = P ; X{nonlocal term} ; V{atom} |- forall(V, P[X -> V])
347 UI = forall(X, P) ; V{term} |- P[X -> V]
348 EG = P ; X{term} ; V{atom} |- exists(V, P[X -> V])
349 block EI
350 Let = exists(X, P) ; V{unique local atom} |- P[X -> V]
351 end
352
353 Premise = |- exists(x, and(man(x), socrates(x)))
354 show
355 forall(x, socrates(x))
356 proof
357 Step_1 = exists(x, and(man(x), socrates(x))) by Premise
358 block EI
359 Step_2 = and(man(k), socrates(k)) by Let with Step_1, k
360 Step_3 = socrates(k) by Simplification_Right with Step_2
361 Step_4 = forall(x, socrates(x)) by UG with Step_3, k, x
362 end
363 Step_5 = forall(x, socrates(x)) by Tautology with Step_4
364 qed
365 ???> must not contain local atom 'k'
366
367 Better.
341368
342369 Equational Reasoning
343370 --------------------
8686 elif hypothesis.has_attribute('term'):
8787 hypothesis.term.match(with_, unifier)
8888 with_term = with_
89 if hypothesis.has_attribute('nonlocal'):
90 atoms = set()
91 with_term.collect_atoms(atoms)
92 for atom in self.local_atoms:
93 if atom in atoms:
94 self.step_error("argument '%s' to hypothesis '%s' must not contain local atom '%s'" % (
95 with_, hypothesis, atom
96 ))
8997 else:
9098 with_step, from_block = self.proof.find_step_and_block(with_.name)
9199 if from_block.level > block.level: