Add requires annotation (Req) to simp

[myreen]

It is often helpful if a proof that needs maintenance breaks as early as something goes wrong. In a proof that consists mostly of rewrites being applied, new breakage can be hard to track down because calls to simp, fs, rw etc do not stop even if the supplied theorems fail to be used.

This issue is about adding a new theorem annotation Req which causes simp/fs/rw to fail in case the annotated theorem isn't successfully applied as a rewrite.

Example:

simp [Req vital_thm]

would fail with a HOL_ERR in case vital_thm isn't successfully used at least once on the current goal.

This issue was discussed on slack, where @konrad-slind mentioned:

BTW: the rewrite tracking stuff is in https://github.com/HOL-Theorem-Prover/HOL/blob/master/src/simp/src/Cond_rewr.sml. Look for track_rewrites and used_rewrites. It's very simplistic, but accumulates every rewrite made into a ref list. Checking that an instance of a given, required, rewrite actually appears in the used_rewrites list would need a bit more work. If the required instance didn't appear, then the conversion would have to fail, and that would be even more work.

[konrad-slind]

Note. Req is just Once except that there is a check at the end of rewriting that its count equals zero.

…

On Fri, Mar 22, 2019 at 4:47 AM myreen ***@***.***> wrote: It is often helpful if a proof that needs maintenance breaks as early as something goes wrong. In a proof that consists mostly of rewrites being applied, new breakage can be hard to track down because calls to simp, fs, rw etc do not stop even if the supplied theorems fail to be used. This issue is about adding a new theorem annotation Req which causes simp/ fs/rw to fail in case the annotated theorem isn't successfully applied as a rewrite. *Example:* simp [Req vital_thm] would fail with a HOL_ERR in case vital_thm isn't successfully used at least once on the current goal. This issue was discussed on slack, where @konrad-slind <https://github.com/konrad-slind> mentioned: BTW: the rewrite tracking stuff is in https://github.com/HOL-Theorem-Prover/HOL/blob/master/src/simp/src/Cond_rewr.sml. Look for track_rewrites and used_rewrites. It's very simplistic, but accumulates every rewrite made into a ref list. Checking that an instance of a given, required, rewrite actually appears in the used_rewrites list would need a bit more work. If the required instance didn't appear, then the conversion would have to fail, and that would be even more work. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#680>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABDgDy1oQ4BEqqODmb_Pg82d5ExSk-c7ks5vZKafgaJpZM4cDMTc> .

[mn200]

Hmm. The “Req = Once+check” approach is not quite as easy as it sounds. The annotated theorems only pick up their references deep in the bowels of the simplifier. Getting those out to the surface so that the SIMP_CONV implementation can check that they've become non-zero is highly non-trivial.

I think I prefer something that scans the goal before and after looking for instances of the required left-hand sides, and complaining if the count has not decreased. You'd wrap

  require_useof mytheorem (simp[mytheorem, myothertheorem])

or similar.

[mn200]

This (nice, functional) approach underneath could be targeted by use of theorem-tags such as Req0 (count of LHS instances must be zero afterwards), and ReqDec (count of LHS instances must have decreased), so that simp[Req0 rwt] would still work.