[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
invoke

   (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.