		Search-engine friendly clone of the ACL2 documentation.

Semantics-deeply-embedded

Exec-proof-tree

Execute a proof tree.

Signature
(exec-proof-tree ptree defs p) → outcome
Arguments: ptree — Guard (proof-treep ptree).; defs — Guard (definition-listp defs).; p — Guard (primep p).
Returns: outcome — Type (proof-outcomep outcome).

Executing a proof tree means checking if it provides a valid proof, and in that case computing the assertion it proves. If the proof is invalid, a failure indication is returned (this could be extended to include more information in the future). If some error occurs during the course of the execution of the proof, e.g. a variable is not found in an assignment, an error indication is returned; this should never happen under suitable well-formedness conditions, which we plan to formally specify and prove. Note the difference between a failure outcome, where no error occurs but the proof tree is invalid, and an error outcome, where some error occurs that prevents the establishment of whether the proof tree is valid or not.

Besides a proof tree, we need a list of definitions, which provides a context in which the constraints are checked.

We also need a prime, which defines the prime field with respect to which the constraints are checked.

To execute a proof tree for an equality constraint, we simply evaluate the constraint.

To execute a proof tree for a relation application, we first evaluate the argument expressions, propagating any errors. Then we look up the relation in the list of definitions, returning an error if absent. Then we execute the proof subtrees, propagating errors and failures. If the proof subtrees all succeed, they yield a list of assertions. We ensure that they all have the same assignment, specifically the one that is obtained by extending, with the assignment asgfree that is the component of the proof tree, the assignment asgpara that assigns the values of the argument expressions to the relation's formal parameters. We require asgfree to have as keys exactly the free variables of the relation; this implies that the keys are disjoint from asgpara. We ensure that the constraints are the ones that form the body of the named relation. In other words, the subtrees must prove that it is possible to extend the assignment of arguments to parameters in a way that all the constraints of the relation are satisfied. This corresponds to the existential quantification discussed in semantics-deeply-embedded, in some suitable sense. We allow relations with an empty body (i.e. no constraints) to be proved by an empty list of subtrees; note that in this case there is no use of asgfree (which may just be nil), because the subtrees do not prove any assertions in this case.

Theorem: return-type-of-exec-proof-tree.outcome

(defthm return-type-of-exec-proof-tree.outcome
  (b* ((?outcome (exec-proof-tree ptree defs p)))
    (proof-outcomep outcome))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-proof-tree-list.outcome

(defthm return-type-of-exec-proof-tree-list.outcome
  (b* ((?outcome (exec-proof-tree-list ptrees defs p)))
    (proof-list-outcomep outcome))
  :rule-classes :rewrite)

Theorem: len-of-exec-proof-tree-list

(defthm len-of-exec-proof-tree-list
 (b* ((?outcome (exec-proof-tree-list ptrees defs p)))
  (implies (proof-list-outcome-case outcome :assertions)
           (equal (len (proof-list-outcome-assertions->get outcome))
                  (len ptrees)))))

Theorem: exec-proof-tree-of-proof-tree-fix-ptree

(defthm exec-proof-tree-of-proof-tree-fix-ptree
  (equal (exec-proof-tree (proof-tree-fix ptree)
                          defs p)
         (exec-proof-tree ptree defs p)))

Theorem: exec-proof-tree-of-definition-list-fix-defs

(defthm exec-proof-tree-of-definition-list-fix-defs
  (equal (exec-proof-tree ptree (definition-list-fix defs)
                          p)
         (exec-proof-tree ptree defs p)))

Theorem: exec-proof-tree-list-of-proof-tree-list-fix-ptrees

(defthm exec-proof-tree-list-of-proof-tree-list-fix-ptrees
  (equal (exec-proof-tree-list (proof-tree-list-fix ptrees)
                               defs p)
         (exec-proof-tree-list ptrees defs p)))

Theorem: exec-proof-tree-list-of-definition-list-fix-defs

(defthm exec-proof-tree-list-of-definition-list-fix-defs
  (equal (exec-proof-tree-list ptrees (definition-list-fix defs)
                               p)
         (exec-proof-tree-list ptrees defs p)))

Theorem: exec-proof-tree-proof-tree-equiv-congruence-on-ptree

(defthm exec-proof-tree-proof-tree-equiv-congruence-on-ptree
  (implies (proof-tree-equiv ptree ptree-equiv)
           (equal (exec-proof-tree ptree defs p)
                  (exec-proof-tree ptree-equiv defs p)))
  :rule-classes :congruence)

Theorem: exec-proof-tree-definition-list-equiv-congruence-on-defs

(defthm exec-proof-tree-definition-list-equiv-congruence-on-defs
  (implies (definition-list-equiv defs defs-equiv)
           (equal (exec-proof-tree ptree defs p)
                  (exec-proof-tree ptree defs-equiv p)))
  :rule-classes :congruence)

Theorem: exec-proof-tree-list-proof-tree-list-equiv-congruence-on-ptrees

(defthm
    exec-proof-tree-list-proof-tree-list-equiv-congruence-on-ptrees
  (implies (proof-tree-list-equiv ptrees ptrees-equiv)
           (equal (exec-proof-tree-list ptrees defs p)
                  (exec-proof-tree-list ptrees-equiv defs p)))
  :rule-classes :congruence)

Theorem: exec-proof-tree-list-definition-list-equiv-congruence-on-defs

(defthm
      exec-proof-tree-list-definition-list-equiv-congruence-on-defs
  (implies (definition-list-equiv defs defs-equiv)
           (equal (exec-proof-tree-list ptrees defs p)
                  (exec-proof-tree-list ptrees defs-equiv p)))
  :rule-classes :congruence)

Theorem: proof-tree-equal-assignment-is-assertion-assignment

(defthm proof-tree-equal-assignment-is-assertion-assignment
 (implies
  (proof-tree-case ptree :equal)
  (b* ((outcome (exec-proof-tree ptree defs p)))
   (implies
      (proof-outcome-case outcome :assertion)
      (equal (assertion->asg (proof-outcome-assertion->get outcome))
             (proof-tree-equal->asg ptree))))))

Theorem: proof-tree-relation-assignment-is-assertion-assignment

(defthm proof-tree-relation-assignment-is-assertion-assignment
 (implies
  (proof-tree-case ptree :relation)
  (b* ((outcome (exec-proof-tree ptree defs p)))
   (implies
      (proof-outcome-case outcome :assertion)
      (equal (assertion->asg (proof-outcome-assertion->get outcome))
             (proof-tree-relation->asg ptree))))))

Subtopics

Exec-proof-tree-list