Closed cbuschardt closed 1 year ago
The hypotheses are not subject to premise selection: all of them are always passed to the ATPs. So you can achieve the effect you want by just adding the lemmas to the context:
Lemma Z_div_step:
forall u v k,
v > 0 -> u / v = (u + v * k) / v - k.
Proof.
pose proof Z.add_cancel_r.
pose proof Z.sub_add.
hammer.
Whether the ATPs will be able to make use of the translated hypotheses is a different matter.
The prediction algorithm doesn't always identify the critical lemmas for the problem space. I'd love a way to manually add entries to merge with the result of "predict".
Lemma Z_div_step: forall u v k, v > 0 -> u / v = (u + v * k) / v - k. Proof. hammer AdditionalPredictions: Z.add_cancel_r, Z.sub_add.
The intent is to compose this into tactics related to specific problem domains.