It is probably a bit out of scope, but I wish that tactics like ring
and field
will be able to produce proofs in the form of the rewrite
tactic.
Do you mean like ring_simplify
?
For example, the ring
tactic can solve (a + b) - (c + d) = (a - c) + (b - d)
, but it would also be nice if the system can suggest a reasonably short proof such as rewrite opprD addrACA
.
From the initial goal, I think it is quite difficult to find that opprD
and addrACA
are lemmas I need, even if I can find addrACA
from the pattern (_ + _) + (_ + _)
.
Under the disclaimer that I don't know the internals of ring, I suspect that the (reflexive) proof ring does is not the nice one from which rewrite lemmas can be found, it probably puts expressions in a normal form (possibly doing unneeded simplifications). Here you want the closest common "reduct".
I did work in the past to such a feature, in Matita, starting from the proof found by a paramodulation theorem prover, and that was the case.
I mean, nobody prevents the prover or ring to apply addrC here and there in their proof.
Kazuhiko Sakaguchi said:
It is probably a bit out of scope, but I wish that tactics like
ring
andfield
will be able to produce proofs in the form of therewrite
tactic.
Which use case do you have in mind for such a feature?
@Kazuhiko Sakaguchi ‘s idea would (for one) help replacing the potentially fragile have -> : (a + b) - (c + d) = … by ring.
step with a short rewrite
not sure if it’s their goal, but I often dislike those steps because they duplicate “internal proof state” (so is fragile) and it’s less concise.
I don't think that is fragile, but if the proof can be done by short rewriting steps, I don't want to leave that kind of assertion (have -> : ...
) in my proof script (for performance reasons for example).
Indeed, the actual ring
tactic performs normalization. We need another mechanism to produce rewriting steps.
(right, that kind of fragility won’t apply to maths as much as to program verification)
I think it is also useful to clean up the proof of Apéry's theorem ;)
maybe you can instrument SMTcoq
to find automatically these "elementary" rewriting step proofs.
Kazuhiko Sakaguchi said:
the proof can be done by short rewriting steps, I don't want to leave that kind of assertion (
have -> : ...
) in my proof script (for performance reasons for example).
Isn't that a bit orthogonal? I mean, having the explicit cut in the goal and the proof script you leave for this step?
@Cyril Cohen please fork off this sub thread
Kazuhiko Sakaguchi said:
I think it is also useful to clean up the proof of Apéry's theorem ;)
Interesting. While developing this proof I had the feeling that more automation (e.g., as provided by algebra-tactics
) would have helped. As medium to long chains of explicit low level rewrite rules tend to be fragile at refactoring time.
I understand that you want to generate them, but I do not yet see the gain in this case.
Would something like a pattern selection for ring_simplify
be helpful for what you have in mind?
Last updated: Oct 13 2024 at 01:02 UTC