Checkpoint fixing subst to support checking Socks and Shoes
Chris Pressey
2 years ago
| 6 | 6 | inv(mul(A, B)) = mul(inv(B), inv(A)) |
| 7 | 7 | proof |
| 8 | 8 | e = e |
| 9 | mul(A, inv(A)) = e [by #inv on LHS] | |
| 9 | mul(A, inv(A)) = e | |
| 10 | 10 | mul(mul(A, B), inv(mul(A, B))) = e [by substitution of mul(A, B) into A] |
| 11 | mul(mul(A, B), inv(mul(A, B))) = mul(A, inv(A)) [by #inv on RHS] | |
| 11 | mul(mul(A, B), inv(mul(A, B))) = mul(A, inv(A)) | |
| 12 | mul(mul(A, B), inv(mul(A, B))) = mul(mul(A, e), inv(A)) | |
| 12 | 13 | |
| 13 | // s4 = check (invIntroR "a" [2] s3) "((a*b)*~(a*b))=(a*~a)" | |
| 14 | // s5 = check (identIntroR [2,1] s4) "((a*b)*~(a*b))=((a*e)*~a)" | |
| 15 | 14 | // s6 = check (invIntroR "b" [2,1,2] s5) "((a*b)*~(a*b))=((a*(b*~b))*~a)" |
| 16 | 15 | // s7 = check (assocR [2,1] s6) "((a*b)*~(a*b))=(((a*b)*~b)*~a)" |
| 17 | 16 | // s8 = check (assocL [2] s7) "((a*b)*~(a*b))=((a*b)*(~b*~a))" |
| 86 | 86 | raise NotImplementedError(str(term)) |
| 87 | 87 | |
| 88 | 88 | |
| 89 | def subst_at_index(term, unifier, index): | |
| 90 | if not unifier.success: | |
| 91 | return term | |
| 92 | if not index: | |
| 93 | return subst(term, unifier) | |
| 94 | if len(index) and isinstance(term, Term): | |
| 95 | position = index[0] | |
| 96 | new_subterm = subst_at_index(term.subterms[position], unifier, index[1:]) | |
| 97 | subterms = term.subterms[:] | |
| 98 | subterms[position] = new_subterm | |
| 99 | return Term(term.ctor, subterms) | |
| 100 | else: | |
| 101 | raise NotImplementedError('{} at {}'.format(str(term), index)) | |
| 102 | ||
| 103 | ||
| 89 | 104 | def replace(term, target, replacement): |
| 90 | 105 | if term == target: |
| 91 | 106 | return replacement |
| 0 | 0 | # TODO: these should probably come from a "eqthy.hints" module |
| 1 | 1 | from eqthy.parser import Substitution, Congruence |
| 2 | from eqthy.terms import Eqn, all_matches, subst, render, RewriteRule, replace | |
| 2 | from eqthy.terms import Eqn, all_matches, subst, subst_at_index, render, RewriteRule, replace | |
| 3 | 3 | |
| 4 | 4 | |
| 5 | 5 | class DerivationError(Exception): |
| 93 | 93 | |
| 94 | 94 | self.log(" Trying to rewrite rhs {} with {}", render(prev.eqn.rhs), render(rule)) |
| 95 | 95 | for rewritten_rhs in self.all_rewrites(rule, prev.eqn.rhs): |
| 96 | self.log(" Using {}, rewrote {} to {}", render(rule), render(prev.eqn.rhs), render(rewritten_rhs)) | |
| 96 | 97 | rewritten_eqn = Eqn(prev.eqn.lhs, rewritten_rhs) |
| 97 | 98 | if step.eqn == rewritten_eqn: |
| 98 | 99 | self.log(" Can rewrite rhs to obtain: {}", render(rewritten_eqn)) |
| 102 | 103 | matches = all_matches(rule.pattern, term) |
| 103 | 104 | rewrites = [] |
| 104 | 105 | for (index, unifier) in matches: |
| 105 | rewrites.append(subst(rule.substitution, unifier)) | |
| 106 | rewrites.append(subst_at_index(rule.substitution, unifier, index)) | |
| 106 | 107 | return rewrites |