Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add requires annotation (Req) to simp #680

Closed
myreen opened this issue Mar 22, 2019 · 3 comments

Comments

@myreen
Copy link
Contributor

commented Mar 22, 2019

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

This comment has been minimized.

Copy link
Contributor

commented Mar 22, 2019

@mn200 mn200 added this to the Kananaskis-13 milestone Apr 29, 2019

@mn200

This comment has been minimized.

Copy link
Member

commented Apr 29, 2019

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 comment has been minimized.

Copy link
Member

commented Apr 29, 2019

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.

mn200 added a commit that referenced this issue Apr 30, 2019
Implement machinery to check that tactic results change acceptably
Used to implement checks that h.o. redexes don't remain, or have
decreased in count.

This is progress towards implementation of github issue #680.

@mn200 mn200 closed this in f49eec5 May 1, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
3 participants
You can’t perform that action at this time.