bind_let rule

This rule already appears in elaborated proofs output by Carcara.

@bandreotti writes: bind_let: Akin to "congruence for lets"

This rule (or an alternative formulation that Carcara can use instead) should be added to the standard. @bandreotti has more information about the formal description of the rule.

assigned to @hbarbosa, @hjsc, and @bandreotti

To clarify, here is an example of how Carcara currently uses this rule:

(anchor :step t1 :args ((x Int)))
...
(step t1.t1 (cl (= phi psi)) :rule hole)
(step t1 (cl (= (let ((x t)) phi) (let ((x t)) psi))) :rule bind_let)

This rule is necessary for elaboration in Carcara when we are removing the implicit reordering of equalities. For instance, consider the case where in the SMT-LIB problem file we have (assert (let ((x 1)) (= x 0))), but in the Alethe proof we have (assume h1 (let ((x 1)) (= 0 x))) (note how the equality (= x 0) was implicitly flipped). To make this transformation explicit, we would need to show that the two let terms are equivalent, and we do this by first showing that the inner terms are equal, and then using bind_let to wrap them in a let binder:

(anchor :step t1 :args ((x Int)))
(step t1.t1 (cl (= (= x 0) (= 0 x))) :rule eq_symmetric)
(step t1 (cl (= (let ((x 1)) (= x 0)) (let ((x 1)) (= 0 x)))) :rule bind_let)

Carcara also has to handle the case where implicit equality reordering is applied to the variable values in the let binding. In this case, we add steps inside the subproof to show that the two values are equivalent, and then pass these steps as premises to the bind_let step. Here is an example, in which step t1.t1 is used to show that the two different values for the bound variable x are equivalent:

(anchor :step t1 :args ((p Bool)))
(step t1.t1 (cl (= (= 0 1) (= 1 0))) :rule eq_symmetric)
(step t1.t2 (cl (= (= p false) (= false p))) :rule eq_symmetric)
(step t1 (cl (= (let ((p (= 0 1))) (= p false)) (let ((p (= 1 0))) (= false p))))
    :rule bind_let :premises (t1.t1))

While of course we don't need a rule with this exact semantics to be added to the specification, it would be good if the rule that is eventually added is powerful enough to model this.

added CarcaraElaborationRule label

added todo-Isabelle todo-specification labels

Question here: shouldn't t1.t1 come before the anchor? if it's conclusion contains a variable bound by the let it should be handled by the context of the let itself, but by the surrounding context.

The reasoning behind t1.t1 being inside the anchor is in case the variable values use other variables from earlier in the let binding. For instance:

(anchor :step t1 :args ((p Int) (q Int)))
(step t1.t1 (cl (= (+ 0 p) (+ p 0))) :rule hole)
(step t1.t2 (cl (= phi psi)) :rule hole)
(step t1 (cl (=
    (let ((p 0) (q (+ 0 p))) phi)
    (let ((p 0) (q (+ p 0))) psi)))
    :rule bind_let :premises (t1.t1))

In this case, t1.t1 needs to prove that (= (+ 0 p) (+ p 0)), so it needs to be inside the subproof, where p is in the context.

This is not right, because the semantics of let is that it is parallel, i.e., it defines a simultaneous substitution. Therefore if there is a variable in the RHS of a let assignment, that variable must be bound from outside the let (see page 29 of the standard). So I agree with @hjsc that the steps relative to rewriting the RHS of the assignments should be done outside the anchor with the variables of the LHS of the assignments.

Ah, I see, I was confused about the let semantics. In this case I agree, these steps should be outside the anchor. I will change Carcara to use this rule correctly.

mentioned in merge request !14 (merged)

removed todo-specification label