proofs.py

""" (c) This file is part of the course
    Mathematical Logic through Programming
    by Gonczarowski and Nisan.
    File name: code/propositions/proofs.py """

from functools import reduce
from propositions.syntax import *
from copy import deepcopy



class InferenceRule:
    """ An inference rule, i.e., a list of zero or more assumed formulae, and
        a conclusion formula """

    def __init__(self, assumptions, conclusion):
        assert type(conclusion) == Formula
        for assumption in assumptions:
            assert type(assumption) == Formula
        self.assumptions = assumptions
        self.conclusion = conclusion

    def __eq__(self, other):
        if (len(self.assumptions) != len(other.assumptions)):
            return False
        if self.conclusion != other.conclusion:
            return False
        for assumption1, assumption2 in zip(self.assumptions, other.assumptions):
            if assumption1 != assumption2:
                return False
        return True

    def __ne__(self, other):
        return not self == other
        
    def __repr__(self):
        return str([assumption.infix() for assumption in self.assumptions]) + \
               ' ==> ' + self.conclusion.infix()

    def variables(self):
        """ Return the set of atomic propositions (variables) used in the
            assumptions and in the conclusion of self. """
        # Task 4.1

        if len(self.assumptions) == 0:
            top = set()
        else:
            top = reduce(lambda x,y: x.union(y.variables()),
                       [set()] + self.assumptions)
        return top.union(self.conclusion.variables())
        
    def is_instance_of(self, rule, instantiation_map=None):
        """ Return whether there exist formulae f1,...,fn and variables
            v1,...,vn such that self is obtained by simultaneously substituting
            each occurrence of f1 with v1, each occurrence of f2 with v2, ...,
            in all of the assumptions of rule as well as in its conclusion.
            If so, and if instantiation_map is given, then it is (cleared and)
            populated with the mapping from each vi to the corresponding fi """
        # Task 4.4
        if instantiation_map is None:
            instantiation_map = dict()
        if len(self.assumptions) == 0 and len(rule.assumptions) == 0:
            assumptions = True
        else:
            if len(self.assumptions) != len(rule.assumptions):
                return False
            assumptions = False not in [InferenceRule._update_instantiation_map(
                x,y, instantiation_map)
                          for (x,y) in zip(self.assumptions, rule.assumptions)]
        con = InferenceRule._update_instantiation_map(self.conclusion,
                                                      rule.conclusion, instantiation_map)
        answer = con and assumptions
        if not answer:
            instantiation_map.clear()
        return answer



    @staticmethod
    def _update_instantiation_map(formula, template, instantiation_map):
        """ Return whether the given formula can be obtained from the given
            template formula by simultaneously and consistantly substituting,
            for every variable in the given template formula, every occurrence
            of this variable with some formula, while respecting the
            correspondence already in instantiation_map (which maps from
            variables to formulae). If so, then instantiation_map is updated
            with any additional substitutions dictated by this matching. If
            not, then instantiation_map may be modified arbitrarily """
        # Task 4.4
        if is_variable(template.root):
            if formula is None:
                return False
            if template.root in instantiation_map:
                return formula == instantiation_map[template.root]
            else:
                instantiation_map[template.root] = formula
                return True
        elif template.root != formula.root:
            return False
        if is_unary(template.root):
            return InferenceRule._update_instantiation_map(formula.first,
                                                           template.first,
                                                         instantiation_map)
        elif is_binary(template.root):
            return InferenceRule._update_instantiation_map(formula.first,
                    template.first, instantiation_map) and \
                   InferenceRule._update_instantiation_map(formula.second,
                                                           template.second, instantiation_map)
        elif is_trinary(template.root):
            return InferenceRule._update_instantiation_map(formula.first, template.first,
                                             instantiation_map) and \
                   InferenceRule._update_instantiation_map(formula.second, template.second,
                                             instantiation_map) and \
                   InferenceRule._update_instantiation_map(formula.third, template.third,
                                             instantiation_map)

    def to_formula(self):
        """ Translates this Inference Rule into a Formula by anding the assumptions
        and -> to the conclusion """
        if len(self.assumptions) == 0:
            assumptions = Formula('T')
        elif len(self.assumptions) == 1:
            assumptions = self.assumptions[0]
        else:
            assumptions = reduce(lambda x,y: Formula('&', x, y), self.assumptions)
        return Formula('->', assumptions, self.conclusion)



class DeductiveProof:
    """ A deductive proof, i.e., a statement of an inference rule, a list of
        assumed inference rules, and a list of lines that prove the former from
        the latter """
    
    class Line:
        """ A line, i.e., a formula, the index of the inference rule whose
            instance justifies the formula from previous lines, and the list
            of indices of these previous lines """
        def __init__(self, conclusion, rule=None, justification=None):
            self.conclusion = conclusion
            self.rule = rule
            self.justification = justification

        def __repr__(self):
            if (self.rule is None):
                return self.conclusion.infix()
            r = self.conclusion.infix() + ' (Inference Rule ' + str(self.rule)
            sep = ';'
            for i in range(len(self.justification)):
                r += sep + ' Assumption ' + str(i) + ': Line ' + \
                     str(self.justification[i])
                sep = ','
            r += '.)' if len(self.justification) > 0 else ')'
            return r

    def __init__(self, statement, rules, lines):
        self.statement = statement
        self.rules = rules
        self.lines = lines

    def __repr__(self):
        r = 'Proof for ' + str(self.statement) + ':\n'
        for i in range(len(self.rules)):
            r += 'Inference Rule ' + str(i) + ': ' + str(self.rules[i]) + '\n'
        for i in range(len(self.lines)):
            r += str(i) + ') ' + str(self.lines[i]) + '\n'
        return r

    def instance_for_line(self, line):
        """ Return the instantiated inference rule that corresponds to the
            given line number """
        # Task 4.5
        real_line = self.lines[line]
        assumptions = [self.lines[i].conclusion for i in
                       real_line.justification]
        return InferenceRule(assumptions, real_line.conclusion)


        
    def is_valid(self):
        """ Return whether lines are a valid proof of statement from rules """
        # Task 4.6
        for i,line in enumerate(self.lines):
            # If it doesn't have a rule, we assume it  is an assumption
            if line.rule is None:
                continue
            rule = self.rules[line.rule]
            if not self.instance_for_line(i).is_instance_of(rule):
                return False
            if False in [i > x for x in line.justification]:
                return False
        return self.instance_for_line(len(self.lines) - 1).conclusion.infix()\
               == self.statement.conclusion.infix()


def instantiate(formula, instantiation_map):
    """ Return a formula obtained from the given formula by simultaneously
        substituting, for each variable v that is a key of instantiation_map,
        each occurrence v with the formula instantiation_map[v] """
    # Task 5.2.1
    return _instantiate_helper(formula, instantiation_map)

def _instantiate_helper(formula, instantiation_map):
    """ Instantiate without copying"""
    if is_variable(formula.root):
        return instantiation_map[formula.root]
    if is_unary(formula.root):
        return Formula(formula.root,
                       _instantiate_helper(formula.first, instantiation_map)
                       )
    elif is_binary(formula.root):
        return Formula(formula.root,
                       _instantiate_helper(formula.first, instantiation_map),
                       _instantiate_helper(formula.second, instantiation_map)
                       )
    elif is_trinary(formula.root):
        return Formula(formula.root,
                       _instantiate_helper(formula.first, instantiation_map),
                       _instantiate_helper(formula.second, instantiation_map),
                       _instantiate_helper(formula.third, instantiation_map)
                       )

def prove_instance(proof, instance):
    """ Return a proof of the given instance of the inference rule that proof
        proves, via the same inference rules used by proof """
    # Task 5.2.1
    instantiation_map = dict()
    if not instance.is_instance_of(proof.statement, instantiation_map):
        return None
    my_lines = []
    for line in proof.lines:
        my_lines.append(
            DeductiveProof.Line(
                instantiate(line.conclusion, instantiation_map),
                line.rule, line.justification)
        )
    return DeductiveProof(instance, proof.rules, my_lines)

def _combine_IRS(main_proof, lemma_proof):
    """Combines the two IRS"""
    new_irs = []
    # add all rules of main proof that are not instance of lemma
    for rule in main_proof.rules:
        if not rule.is_instance_of(lemma_proof.statement):
            new_irs.append(rule)
    # add all rules of lemma that are not already in the list
    for rule in lemma_proof.rules:
        add = True
        for new_rule in new_irs:
            if rule.is_instance_of(new_rule):
                add = False
                break
        if add:
            new_irs.append(rule)
    return new_irs

def _create_lemma_rule_LUT(new_irs, lemma_proof):
    """Creates a LUT for the new IRS"""
    lemma_rule_LUT = [] # LUT for indicies of lemma IRS
    for rule in lemma_proof.rules:
        for i, proof_rule in enumerate(new_irs):
            if rule.is_instance_of(proof_rule):
                lemma_rule_LUT.append(i)
                break
    return lemma_rule_LUT

def _create_non_lemma_rule_LUT(new_irs, main_proof, lemma_statement):
    """Creates a LUT for the new IRS"""
    non_lemma_rule_LUT = [] # LUT for indicies of lemma IRS
    for rule in main_proof.rules:
        if rule.is_instance_of(lemma_statement):
            non_lemma_rule_LUT.append(-1)
            continue
        for i, proof_rule in enumerate(new_irs):
            if rule.is_instance_of(proof_rule):
                non_lemma_rule_LUT.append(i)
                break
    return non_lemma_rule_LUT

def _update_justifications(line, my_lines, proof):
    """Updates a line justifications to the new lines"""
    for i, justi in enumerate(line.justification):
        for j in range(len(my_lines)):
            if proof.lines[justi].conclusion == my_lines[j].conclusion:
                line.justification[i] = j
                break


def inline_proof(main_proof, lemma_proof):
    """ Return a proof of the inference rule that main_proof proves, via the
        inference rules used in main_proof except for the one proven by
        lemma_proof, as well as via the inference rules used in lemma_proof
        (with duplicates removed) """
    # Task 5.2.2

    # IRs
    lemma_rule = lemma_proof.statement
    new_irs = _combine_IRS(main_proof, lemma_proof)
    lemma_rule_LUT = _create_lemma_rule_LUT(new_irs, lemma_proof)
    non_lemma_LUT = _create_non_lemma_rule_LUT(new_irs, main_proof, lemma_proof.statement)
    my_lines = []
    my_p = DeductiveProof(deepcopy(main_proof.statement), new_irs, my_lines) # My proof
    lines_added = 0
    # lines
    for line_num, line in enumerate(deepcopy(main_proof.lines)):
        if line.rule is None:
            my_lines.append(line)
            continue
        if not main_proof.rules[line.rule].is_instance_of(lemma_rule):
            _update_justifications(line, my_lines, main_proof)
            line.rule = non_lemma_LUT[line.rule]
            # for j in range(len(line.justification)):
            #     line.justification[j] = line.justification[j] + lines_added
            my_lines.append(line)
            continue
        line_instance = main_proof.instance_for_line(line_num)
        line_proof = prove_instance(lemma_proof, line_instance)
        assert line_proof is not None  # None if it can't proveide valid proof
        for l_p_line in deepcopy(line_proof.lines): # line proof line
            if l_p_line.rule is None: # it is an assumption, uneeded.
                continue
           # non-assumption should  have justifications
            assert l_p_line.justification is not None
            # update justifications
            for i, justi in enumerate(l_p_line.justification):
                for j in range(len(my_lines)):
                    if line_proof.lines[justi].conclusion == my_lines[j].conclusion:
                        l_p_line.justification[i] = j
                        break
            l_p_line.rule = lemma_rule_LUT[l_p_line.rule]
            my_lines.append(l_p_line)
            lines_added += 1 # add every lemma line
        lines_added -= 1 # 'remove' the line we replaced

        #####################################################
    return my_p