<jupyter_start><jupyter_text>$\newcommand{\Suc}{\operatorname{Suc}}$<jupyter_code>import os
os.chdir('..')
from kernel.type import TFun, NatType, BoolType
from kernel.term import Var, Forall, Exists, And, Implies, Inst, Eq
from kernel.thm import Thm
from kernel import theory
from kernel.proofterm import ProofTerm, refl, TacticException
from data.nat import Suc
from logic import basic
from logic.tactic import Tactic, intros_tac, rule_tac, elim_tac, intro_forall_tac, intro_imp_tac, \
    assumption, conj_elim_tac
from logic.conv import top_sweep_conv, rewr_conv, beta_norm_conv, top_conv, bottom_conv, arg_conv
from syntax.settings import settings

basic.load_theory('nat')
settings.unicode = True<jupyter_output><empty_output><jupyter_text>Tactics for predicate logic In this section, we introduce more tactics: those for predicate logic, for rewriting, and for induction.To reason in predicate logic, we need tactics for introducing and eliminating forall and exists quantification. Introduction of forall quantification is already implemented as `intro_forall_tac` in the previous section. The other three tactics can be easily implemented using what we already have.We begin with elimination of forall quantification. This corresponds to instantiating a forall assumption on some term. It uses the following theorem:<jupyter_code>theory.print_theorem('allE')<jupyter_output>allE: ⊢ (∀x1. P x1) ⟶ (P x ⟶ R) ⟶ R<jupyter_text>Here the free variable $x$ in the second assumption is the term used to substitute for the bound variable in the forall quantification. We package this up as a tactic that accepts $x$ as an argument:<jupyter_code>class forall_elim_tac(Tactic):
    def __init__(self, t):
        self.t = t

    def get_proof_term(self, goal):
        return ProofTerm.sorry(goal).tacs(
            elim_tac('allE', inst=Inst(x=self.t)),
            intro_imp_tac())<jupyter_output><empty_output><jupyter_text>We test the use of this tactic on the theorem $(\forall x.\,P(x)\wedge Q(x)) \to (\forall x.\,P(x)) \wedge (\forall x.\,Q(x))$. We first show the point at which elimination of forall is needed:<jupyter_code>x = Var('x', NatType)
P = Var('P', TFun(NatType, BoolType))
Q = Var('Q', TFun(NatType, BoolType))

goal = Implies(Forall(x, And(P(x), Q(x))), And(Forall(x, P(x)), Forall(x, Q(x))))
pt = ProofTerm.sorry(Thm([], goal))

print(pt.tacs(intros_tac, rule_tac('conjI'), intro_forall_tac('x')))<jupyter_output>ProofTerm(⊢ (∀x. P x ∧ Q x) ⟶ (∀x. P x) ∧ (∀x. Q x))
Gaps: ∀x. P x ∧ Q x ⊢ P x
      ∀x. P x ∧ Q x ⊢ ∀x. Q x<jupyter_text>We instantiate $\forall x.\,P(x)\wedge Q(x)$ with the term $x$, the result is:<jupyter_code>print(pt.tacs(intros_tac, rule_tac('conjI'), intro_forall_tac('x'), forall_elim_tac(x)))<jupyter_output>ProofTerm(⊢ (∀x. P x ∧ Q x) ⟶ (∀x. P x) ∧ (∀x. Q x))
Gaps: P x ∧ Q x, ∀x. P x ∧ Q x ⊢ P x
      ∀x. P x ∧ Q x ⊢ ∀x. Q x<jupyter_text>The proof can be finished as follows:<jupyter_code>print(pt.tacs(intros_tac, rule_tac('conjI'),
              intro_forall_tac('x'), forall_elim_tac(x), conj_elim_tac(), assumption(),
              intro_forall_tac('x'), forall_elim_tac(x), conj_elim_tac(), assumption()))<jupyter_output>ProofTerm(⊢ (∀x. P x ∧ Q x) ⟶ (∀x. P x) ∧ (∀x. Q x))<jupyter_text>Eliminating of an existence assumption corresponds to using $\exists x.\,P(x)$ to create a fresh variable $x$ satisfying $P(x)$. It uses the theorem `exE`. We package this up as a tactic which accepts the suggested name of the new variable:<jupyter_code>class ex_elim_tac(Tactic):
    def __init__(self, var_name=None):
        self.var_name = var_name
        
    def get_proof_term(self, goal):
        return ProofTerm.sorry(goal).tacs(
            elim_tac('exE'), intro_forall_tac(self.var_name), intro_imp_tac())<jupyter_output><empty_output><jupyter_text>Introducing an existence assumption corresponds to reducing the goal $\exists a.\,P(a)$ to showing $P(a)$ for some term $a$. It involves applying `rule_tac` on the following theorem:<jupyter_code>theory.print_theorem('exI')<jupyter_output>exI: ⊢ P a ⟶ (∃a1. P a1)<jupyter_text>We package this up in the following tactic. It accepts a parameter $s$ which is the candidate term for showing existence:<jupyter_code>class ex_intro_tac(Tactic):
    def __init__(self, s):
        self.s = s
        
    def get_proof_term(self, goal):
        return ProofTerm.sorry(goal).tac(rule_tac('exI', inst=Inst(a=self.s)))<jupyter_output><empty_output><jupyter_text>We test the above two tactics on the theorem $(\exists x.\,P(x)\wedge Q(x)) \to (\exists x.\,P(x)) \wedge (\forall x.\,Q(x))$. (Hint: if viewing interactively, remove a suffix of the sequence of tactics to see an intermediate state.)<jupyter_code>goal = Implies(Exists(x, And(P(x), Q(x))), And(Exists(x, P(x)), Exists(x, Q(x))))

pt = ProofTerm.sorry(Thm([], goal))
print(pt.tacs(intros_tac, rule_tac('conjI'),
              ex_elim_tac('x'), ex_intro_tac(x), conj_elim_tac(), assumption(),
              ex_elim_tac('x'), ex_intro_tac(x), conj_elim_tac(), assumption()))<jupyter_output>ProofTerm(⊢ (∃x. P x ∧ Q x) ⟶ (∃x. P x) ∧ (∃x. Q x))<jupyter_text>Finally, we show the proof of the theorem $(\exists x.\,\forall y.\,R(x,y)) \to (\forall y.\,\exists x.\,R(x,y))$. The whole proof can be done in five tactic applications, which is much simpler than the approach of composing proof rules from before:<jupyter_code>x = Var('x', NatType)
y = Var('y', NatType)
R = Var('R', TFun(NatType, NatType, BoolType))

goal = Implies(Exists(x, Forall(y, R(x, y))), Forall(y, Exists(x, R(x, y))))

pt = ProofTerm.sorry(Thm([], goal))
print(pt.tacs(intros_tac, ex_elim_tac('x'), forall_elim_tac(y), ex_intro_tac(x), assumption()))<jupyter_output>ProofTerm(⊢ (∃x. ∀y. R x y) ⟶ (∀y. ∃x. R x y))<jupyter_text>Rewriting and induction In this section, we show how to prove the basic theorems in Peano arithmetic using tactics. In particular, we show how to implement tactics for performing induction and for rewriting. Our goal is to prove the theorem $n+0=n$:<jupyter_code>n = Var('n', NatType)
goal = Eq(n + 0, n)
print(goal)

pt = ProofTerm.sorry(Thm([], goal))<jupyter_output>n + 0 = n<jupyter_text>The first step is to perform induction on $n$. Recall the theorem for induction on natural numbers:<jupyter_code>theory.print_theorem('nat_induct')<jupyter_output>nat_induct: ⊢ P 0 ⟶ (∀n. P n ⟶ P (Suc n)) ⟶ P x<jupyter_text>To apply this theorem, we need to find instantiations for the predicate $P$ and variable $x$. We assume $x$ corresponds to a variable in the goal, then as long as $x$ is fixed, $P$ can be found by abstracting the goal over $x$. The following tactic implements this functionality. It accepts two parameters: name of the induction theorem and optionally a variable. If no variable is provided, then the tactic tries to find a variable of the same type in the goal statement, and succeeds only if there is exactly one such variable. The tactic is named `var_induct_tac` as we are performing structural induction on a variable, and there are several other kinds of inductions.<jupyter_code>class var_induct_tac(Tactic):
    def __init__(self, th_name, var=None):
        self.th_name = th_name
        self.var = var
        
    def get_proof_term(self, goal):
        th = theory.get_theorem(self.th_name)
        P, args = th.concl.strip_comb()
        if len(args) != 1 or not args[0].is_svar():
            raise TacticException('var_induct: wrong form of induction rule')
        arg = args[0]

        if self.var is None:
            goal_vars = [v for v in goal.prop.get_vars() if v.T == arg.T]
            if len(goal_vars) != 1:
                raise TacticException('var_induct: cannot find unique induction variable')
            var = goal_vars[0]
        else:
            var = self.var
            
        return ProofTerm.sorry(goal).tac(rule_tac(self.th_name, inst=Inst({arg.name: var})))<jupyter_output><empty_output><jupyter_text>We test this tactic by starting the induction proof as follows:<jupyter_code>print(pt.tac(var_induct_tac('nat_induct')))<jupyter_output>ProofTerm(⊢ n + 0 = n)
Gaps: ⊢ (0::nat) + 0 = 0
      ⊢ ∀n. n + 0 = n ⟶ Suc n + 0 = Suc n<jupyter_text>Next, we need to apply the rewriting rules `nat_plus_def_1` and `nat_plus_def_2`:<jupyter_code>theory.print_theorem('nat_plus_def_1', 'nat_plus_def_2')<jupyter_output>nat_plus_def_1: ⊢ 0 + n = n
nat_plus_def_2: ⊢ Suc m + n = Suc (m + n)<jupyter_text>This requires a tactic to rewrite (subterms) of the goal using a theorem. It can be implemented as follows. The tactic takes the name of the theorem, and an optional strategy parameter, that determines whether the rewriting is top-down (`top`), bottom-up (`bottom`), or top-down stopping at any subterms that is rewritten (`top_sweep`). The third option `top_sweep` is appropriate when the right side of the equality theorem contains a subterm that matches the left side (avoids infinite loops).<jupyter_code>class rewr_tac(Tactic):
    def __init__(self, th_name, *, strategy='top'):
        self.th_name = th_name
        if strategy == 'top':
            self.cv = top_conv
        elif strategy == 'bottom':
            self.cv = bottom_conv
        elif strategy == 'top_sweep':
            self.cv = top_sweep_conv
        else:
            raise AssertionError('unknown strategy')
        
    def get_proof_term(self, goal):
        eq_pt = refl(goal.prop).on_rhs(self.cv(rewr_conv(self.th_name)), beta_norm_conv())
        new_goal = ProofTerm.sorry(Thm(goal.hyps, eq_pt.rhs))
        return eq_pt.symmetric().equal_elim(new_goal)<jupyter_output><empty_output><jupyter_text>Two other tactics will be useful in the rest of the proof, and we introduce them at the same time. The first tactic is `reflexive_tac`, which simply resolves a goal that is a reflexive equality:<jupyter_code>class reflexive_tac(Tactic):
    def get_proof_term(self, goal):
        if not goal.is_reflexive():
            raise TacticException('reflexive')
            
        return ProofTerm.reflexive(goal.lhs)<jupyter_output><empty_output><jupyter_text>The other tactic rewrites the goal using the equalities in the assumptions:<jupyter_code>class rewr_prev_tac(Tactic):
    def get_proof_term(self, goal):
        eq_pt = refl(goal.prop)
        for hyp in goal.hyps:
            if hyp.is_equals():
                eq_pt = eq_pt.on_rhs(top_sweep_conv(rewr_conv(ProofTerm.assume(hyp))), beta_norm_conv())
        new_goal = ProofTerm.sorry(Thm(goal.hyps, eq_pt.rhs))
        return eq_pt.symmetric().equal_elim(new_goal)<jupyter_output><empty_output><jupyter_text>With these tactics, the proof of $n + 0 = n$ can be completed as follows:<jupyter_code>n = Var('n', NatType)
goal = Eq(n + 0, n)
pt = ProofTerm.sorry(Thm([], goal))

pt.tacs(var_induct_tac('nat_induct'),
        rewr_tac('nat_plus_def_1'), reflexive_tac(),
        intros_tac, rewr_tac('nat_plus_def_2'), rewr_prev_tac(), reflexive_tac())<jupyter_output><empty_output><jupyter_text>We now show proofs of some other theorems in Peano arithmetic. First, $n * 0 = 0$:<jupyter_code>goal = Eq(n * 0, 0)

pt = ProofTerm.sorry(Thm([], goal))
pt.tacs(var_induct_tac('nat_induct'),
        rewr_tac('nat_times_def_1'), reflexive_tac(),
        intros_tac, rewr_tac('nat_times_def_2'), rewr_tac('nat_plus_def_1'), assumption())<jupyter_output><empty_output><jupyter_text>Associativity of addition $(x + y) + z = x + (y + z)$:<jupyter_code>x = Var('x', NatType)
y = Var('y', NatType)
z = Var('z', NatType)

goal = Eq((x + y) + z, x + (y + z))
pt = ProofTerm.sorry(Thm([], goal))

pt.tacs(var_induct_tac('nat_induct', x),
        rewr_tac('nat_plus_def_1'), reflexive_tac(),
        intro_forall_tac('x'), intro_imp_tac(), rewr_tac('nat_plus_def_2', strategy='bottom'),
        rewr_prev_tac(), reflexive_tac())<jupyter_output><empty_output><jupyter_text>Commutativity of addition $x + y = y + x$. This requires proving the lemma $x + \Suc y = \Suc (x + y)$ (recorded in the library as `add_Suc_right`, as well as the theorem `add_0_right` proved above.<jupyter_code>goal = Eq(x + Suc(y), Suc(x + y))

pt = ProofTerm.sorry(Thm([], goal))
pt.tacs(var_induct_tac('nat_induct', x),
        rewr_tac('nat_plus_def_1'), reflexive_tac(),
        intro_forall_tac('x'), intro_imp_tac(), rewr_tac('nat_plus_def_2'),
        rewr_prev_tac(), reflexive_tac())
goal = Eq(x + y, y + x)

pt = ProofTerm.sorry(Thm([], goal))
pt.tacs(var_induct_tac('nat_induct', x),
        rewr_tac('nat_plus_def_1'), rewr_tac('add_0_right'), reflexive_tac(),
        intro_forall_tac('x'), intro_imp_tac(), rewr_tac('nat_plus_def_2'),
        rewr_tac('add_Suc_right'), rewr_prev_tac(), reflexive_tac())<jupyter_output><empty_output><jupyter_text>Distributivity of multiplication over addition is still not so easy prove, we start the proof here:<jupyter_code>goal = Eq(x * (y + z), x * y + x * z)
pt = ProofTerm.sorry(Thm([], goal))

pt2 = pt.tacs(var_induct_tac('nat_induct', x),
              rewr_tac('nat_times_def_1'), rewr_tac('nat_plus_def_1'), reflexive_tac(),
              intro_forall_tac('x'), intro_imp_tac(), rewr_tac('nat_times_def_2'),
              rewr_prev_tac())
print(pt2)<jupyter_output>ProofTerm(⊢ x * (y + z) = x * y + x * z)
Gaps: x * (y + z) = x * y + x * z ⊢ y + z + (x * y + x * z) = y + x * y + (z + x * z)
{'fraction_non_alphanumeric': 0.1318789159809768, 'fraction_numerical': 0.0037744394957348834, 'mean_word_length': 4.339782345828295, 'pattern_counts': {'":': 0, '<': 85, '<?xml version=': 0, '>': 85, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '24', 'dir': 'jupyter-structured-clean-dedup', 'id': '635927', 'license': 'BSD-3-Clause', 'n_tokens_mistral': 5093, 'n_tokens_neox': 4844, 'n_words': 1362, 'path': 'tutorial/tactics2.ipynb', 'repo_name': 'crisperdue/holpy', 'size': '13247'}