Why does PVS generate quotient_remainder_TCC2 subtype TCC
when type checking quotient_remainder recursive function
The answer is that the LET resulting form, in the case where n≥d, must have the expected (qr?(n, d)) type. Since the LET form refers to quotient_remainder function, which is under definition, the proof obligation (which is generated before) cannot refer to quotient_remainder function (not yet defined): hence the use of v template, which mimics quotient_remainder, in the expression of the TCC.
The TCC can be rewritten into the more understandable form:
where the type assumed for v clearly resembles that of quotient_remainder. We actually have:
The only difference is that the domain of v is smaller than the domain of quotient_remainder for two reasons:
Finally, the meaning of the TCC is the following: assuming that the result (q, r) of the recursive call satisfies the output type specification (qr?(n-d, d)), then prove that the LET form itself yields a result of the desired type (qr?(n, d)). In other words, the TCC is essentially equivalent to:
Indeed, when we look at the actual proof of the TCC, we see that the reference to v is soon replaced with a (q, r) pair.