<jupyter_start><jupyter_text>$\newcommand{\To}{\Rightarrow}$<jupyter_code>import os
os.chdir('..')
from kernel.type import TFun, NatType, BoolType
from kernel.term import Var, Nat, Lambda, Abs, Bound, plus, Eq
from kernel.proofterm import ProofTerm, refl
from logic.conv import Conv, fun_conv, arg_conv, arg1_conv, rewr_conv, try_conv, binop_conv, beta_conv
from logic import basic
from syntax.settings import settings
from util import name

basic.load_theory('nat')
settings.unicode = True<jupyter_output><empty_output><jupyter_text>Rewriting on abstraction In this section, we cover some further material on conversions. We begin where we left off in the last section: rewriting inside a $\lambda$-term. The conversion `abs_conv` takes a conversion as input, and applies the conversion to the body of a $\lambda$-term. It can be implemented as follows:<jupyter_code>class abs_conv(Conv):
    def __init__(self, cv):
        self.cv = cv
        
    def get_proof_term(self, t):
        var_names = [v.name for v in t.body.get_vars()]
        nm = name.get_variant_name(t.var_name, var_names)
        v = Var(nm, t.var_T)
        body = t.subst_bound(v)
        
        return self.cv.get_proof_term(body).abstraction(v)<jupyter_output><empty_output><jupyter_text>In line 1 of `get_proof_term`, we find the list of names of variables already in `t.body` using the `get_vars()` function. Note this only finds names of free variables, not the bound variable. On line 2, we use `name.get_variant_name` to find a fresh name for replacing the bound variable. Here `t.var_name` is the "suggested" name of the bound variable. The new variable $v$ is constructed in line 3, where `t.var_T` is the type of the bound variable. Finally, the body with bound variable replaced by $v$ is constructed on line 4.Let's test the conversion on some examples.<jupyter_code>x = Var('x', NatType)
t = Lambda(x, x + 2)
print('t: ', t)
pt = abs_conv(rewr_conv('add_comm')).get_proof_term(t)
print('pt:', pt)<jupyter_output>t:  λx::nat. x + 2
pt: ProofTerm(⊢ (λx::nat. x + 2) = (λx. 2 + x))<jupyter_text>The pattern in lines 1-4 of `abs_conv` occurs commonly, so it is implemented in the `dest_abs` function. We show some examples here:<jupyter_code>t = Lambda(x, x + 2)
v, body = t.dest_abs()
print('t:', t)
print('v:', v)
print('body:', body)<jupyter_output>t: λx::nat. x + 2
v: x
body: x + 2<jupyter_text>We show another example with a name conflict:<jupyter_code>t = Abs('x', NatType, plus(NatType)(x, Bound(0)))
v, body = t.dest_abs()
print('t:', t)
print('v:', v)
print('body:', body)<jupyter_output>t: λx1. x + x1
v: x1
body: x + x1<jupyter_text>Note how a fresh name `x1` is used both for printing and for the variable constructed by `dest_abs`. We now use `dest_abs` to simplify the implementation of `abs_conv`:<jupyter_code>class abs_conv(Conv):
    def __init__(self, cv):
        self.cv = cv
        
    def get_proof_term(self, t):
        v, body = t.dest_abs()
        return self.cv.get_proof_term(body).abstraction(v)
t = Lambda(x, x + 2)
print(abs_conv(rewr_conv('add_comm')).get_proof_term(t))<jupyter_output>ProofTerm(⊢ (λx::nat. x + 2) = (λx. 2 + x))<jupyter_text>Applying conversions to proof term So far, we describe the usual API for implementing and using conversions in functional programming. In holpy, a different API is available, based on modifying proof terms using `on_prop` and `on_rhs` methods of class `ProofTerm`. We demonstrate this API below.The `on_prop` method takes a conversion as input, and rewrites the proposition of the proof term using that conversion. For example:<jupyter_code>P = Var('P', TFun(NatType, BoolType))
n = Var('n', NatType)

pt = ProofTerm.assume(P(n + 2))
pt2 = pt.on_prop(arg_conv(rewr_conv('add_comm')))
print('pt: ', pt)
print('pt2:', pt2)<jupyter_output>pt:  ProofTerm(P (n + 2) ⊢ P (n + 2))
pt2: ProofTerm(P (n + 2) ⊢ P (2 + n))<jupyter_text>It is important to note that calling `on_prop` on a proof term `pt` does *not* modify `pt`. Proof terms are immutable objects. Instead, the function returns a new proof term which is the result.The `on_rhs` method applies the conversion to the right side of an equality. This is especially useful for composing conversions.<jupyter_code>x = Var('x', NatType)
y = Var('y', NatType)
z = Var('z', NatType)

pt = refl(x * (y + z))
pt2 = pt.on_rhs(rewr_conv('distrib_l'))
pt3 = pt2.on_rhs(arg1_conv(rewr_conv('mult_comm')))
pt4 = pt3.on_rhs(arg_conv(rewr_conv('mult_comm')))
print('pt: ', pt)
print('pt2:', pt2)
print('pt3:', pt3)
print('pt4:', pt4)<jupyter_output>pt:  ProofTerm(⊢ x * (y + z) = x * (y + z))
pt2: ProofTerm(⊢ x * (y + z) = x * y + x * z)
pt3: ProofTerm(⊢ x * (y + z) = y * x + x * z)
pt4: ProofTerm(⊢ x * (y + z) = y * x + z * x)<jupyter_text>Multiple rewrites on the right side appears commonly, so we allow it to be done more conveniently by providing the conversions in sequence to the `on_rhs` function. This can replace most of the uses of `then_conv` and `every_conv`.<jupyter_code>pt = refl(x * (y + z))
pt2 = pt.on_rhs(rewr_conv('distrib_l'), arg1_conv(rewr_conv('mult_comm')), arg_conv(rewr_conv('mult_comm')))
print('pt: ', pt)
print('pt2:', pt2)<jupyter_output>pt:  ProofTerm(⊢ x * (y + z) = x * (y + z))
pt2: ProofTerm(⊢ x * (y + z) = y * x + z * x)<jupyter_text>Incidentally, the function `binop_conv` can be used when we want to apply the same conversion to the two sides of a binary operator:<jupyter_code>print(pt.on_rhs(rewr_conv('distrib_l'), binop_conv(rewr_conv('mult_comm'))))<jupyter_output>ProofTerm(⊢ x * (y + z) = y * x + z * x)<jupyter_text>We now apply these ideas to re-implement the `swap_cv` function. Recall the purpose of this conversion is to rewrite an expression of the form $(a + b) + c$ to $(a + c) + b$.<jupyter_code>class swap_cv(Conv):
    def get_proof_term(self, t):
        return refl(t).on_rhs(
            rewr_conv('add_assoc'),
            arg_conv(rewr_conv('add_comm')),
            rewr_conv('add_assoc', sym=True))
t = (x + y) + 2
print('t: ', t)
print('pt:', refl(t).on_rhs(swap_cv()))<jupyter_output>t:  x + y + 2
pt: ProofTerm(⊢ x + y + 2 = x + 2 + y)<jupyter_text>This style of invoking conversions results in a more procedural code, better suited to the Python language.  `top_conv` revisited In the previous section on conversions, we implemented `top_conv` in the functional style. In this part, we re-implement the conversion in a more procedural style, also including rewriting on abstractions.<jupyter_code>class top_conv(Conv):
    def __init__(self, cv):
        self.cv = cv
        
    def get_proof_term(self, t):
        pt = refl(t).on_rhs(try_conv(self.cv))
        if pt.rhs.is_comb():
            return pt.on_rhs(fun_conv(self), arg_conv(self))
        elif pt.rhs.is_abs():
            return pt.on_rhs(abs_conv(self))
        else:
            return pt<jupyter_output><empty_output><jupyter_text>The function first tries to call `cv` on the current term. Next, if the result is not atomic (is either a combination or an abstraction), it calls `cv` on the subterms. Let's test the function on some examples.<jupyter_code>x = Var('x', NatType)
y = Var('y', NatType)
z = Var('z', NatType)

t = Lambda(x, y, x * (3 * y + z + 1))
pt = refl(t).on_rhs(top_conv(rewr_conv('distrib_l')))
print('t: ', t)
print('pt:', pt)<jupyter_output>t:  λx. λy. x * (3 * y + z + 1)
pt: ProofTerm(⊢ (λx. λy. x * (3 * y + z + 1)) = (λx. λy. x * (3 * y) + x * z + x * 1))<jupyter_text>Likewise the class `bottom_conv` can be implemented as follows:<jupyter_code>class bottom_conv(Conv):
    def __init__(self, cv):
        self.cv = cv
        
    def get_proof_term(self, t):
        pt = refl(t)
        if t.is_comb():
            return pt.on_rhs(fun_conv(self), arg_conv(self), try_conv(self.cv))
        elif t.is_abs():
            return pt.on_rhs(abs_conv(self), try_conv(self.cv))
        else:
            return pt.on_rhs(try_conv(self.cv))<jupyter_output><empty_output><jupyter_text>Let's test it on the $\beta$-reduction example from before:<jupyter_code>x = Var('x', NatType)
y = Var('y', NatType)
t = Lambda(x, y, x + y)(Nat(2), Nat(3))
print(refl(t).on_rhs(bottom_conv(beta_conv())))<jupyter_output>ProofTerm(⊢ (λx::nat. λy. x + y) 2 3 = 2 + 3)
{'fraction_non_alphanumeric': 0.1371713729308666, 'fraction_numerical': 0.008519961051606621, 'mean_word_length': 4.243777919591576, 'pattern_counts': {'":': 0, '<': 50, '<?xml version=': 0, '>': 50, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 1, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '15', 'dir': 'jupyter-structured-clean-dedup', 'id': '190620', 'license': 'BSD-3-Clause', 'n_tokens_mistral': 3099, 'n_tokens_neox': 3014, 'n_words': 939, 'path': 'tutorial/conversions2.ipynb', 'repo_name': 'crisperdue/holpy', 'size': '8216'}