Stream: math-comp users

Topic: Generating rewrite directives out of ring or field tactic...


view this post on Zulip Kazuhiko Sakaguchi (Oct 21 2021 at 07:50):

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.

view this post on Zulip Enrico Tassi (Oct 21 2021 at 09:16):

Do you mean like ring_simplify?

view this post on Zulip Kazuhiko Sakaguchi (Oct 21 2021 at 09:25):

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.

view this post on Zulip Kazuhiko Sakaguchi (Oct 21 2021 at 09:27):

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 (_ + _) + (_ + _).

view this post on Zulip Enrico Tassi (Oct 21 2021 at 09:45):

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.

view this post on Zulip Assia Mahboubi (Oct 21 2021 at 13:33):

Kazuhiko Sakaguchi said:

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.

Which use case do you have in mind for such a feature?

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 13:35):

@Kazuhiko Sakaguchi ‘s idea would (for one) help replacing the potentially fragile have -> : (a + b) - (c + d) = … by ring. step with a short rewrite

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 13:37):

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.

view this post on Zulip Kazuhiko Sakaguchi (Oct 21 2021 at 13:44):

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

view this post on Zulip Kazuhiko Sakaguchi (Oct 21 2021 at 13:45):

Indeed, the actual ring tactic performs normalization. We need another mechanism to produce rewriting steps.

view this post on Zulip Paolo Giarrusso (Oct 21 2021 at 13:46):

(right, that kind of fragility won’t apply to maths as much as to program verification)

view this post on Zulip Kazuhiko Sakaguchi (Oct 21 2021 at 13:46):

I think it is also useful to clean up the proof of Apéry's theorem ;)

view this post on Zulip Laurent Théry (Oct 21 2021 at 14:02):

maybe you can instrument SMTcoq to find automatically these "elementary" rewriting step proofs.

view this post on Zulip Assia Mahboubi (Oct 21 2021 at 14:13):

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?

view this post on Zulip Enrico Tassi (Oct 21 2021 at 14:15):

@Cyril Cohen please fork off this sub thread

view this post on Zulip Assia Mahboubi (Oct 21 2021 at 15:21):

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.

view this post on Zulip Assia Mahboubi (Oct 21 2021 at 15:22):

I understand that you want to generate them, but I do not yet see the gain in this case.

view this post on Zulip Assia Mahboubi (Oct 21 2021 at 15:23):

Would something like a pattern selection for ring_simplifybe helpful for what you have in mind?


Last updated: Feb 02 2023 at 15:04 UTC