[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] using TCCs in proofs
Is there a facility or recommended way to deal with the following.
I define a function f which involves some complicated dependent types and
generates TCCs that aren't proved by the built-in strategies.
Now I do a proof involving f and thus get similar TCCs. Having discharged
the TCCs for f, I can now use them in this proof. But I'm doing it by
hand: look at the obligation, find f's TCC with similar consequent, and
(then (use "f_TCC_number_whatever") (grind))
It works but it's tedious.
I haven't tried it, but a quick look at the Prover Guide's chapter on
strategies suggests I can easily define a strategy that tries the above
for each of f's TCCs. But there are several such f so I'd prefer to
generate the strategy automatically.