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`

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?

@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: Feb 02 2023 at 15:04 UTC