macro to expand "by rewrite A B C ... ."

[chdoc]

A commonly used idiom in the mathematical components library (and many libraries building on top of mathcomp) is to use somthing like by rewrite A !B /= C D // E to close a goal. During code maintenance, one often finds onself in a situation where one of the rewrites in the chain fails.

Currently, examining the intermediate proof stats of such a rewrite chain requires: (1) removing the by, (2) inserting a dot, and (3) stepping to the dot. It would be nice if there was a macro to "expand" the rewrite chain.

For example, consider the following lemma (from mathcomp.ssreflect.ssrnat.v)

Lemma leq_exp2l m n1 n2 : 1 < m -> (m ^ n1 <= m ^ n2) = (n1 <= n2).
Proof.
move=> m_gt1; elim: n1 n2 => [|n1 IHn] [|n2] //; last 1 first.
- by rewrite !expnS leq_pmul2l ?IHn // ltnW.
- by rewrite expn_gt0 ltnW.
by rewrite leqNgt (leq_trans m_gt1) // expnS leq_pmulr // expn_gt0 ltnW. 
Qed.

It would be nice if there was a macro to expand the last line automatically into this (presumably) equivalent sequence of tactics:

  { rewrite leqNgt.
    all: rewrite (leq_trans m_gt1).
    all: rewrite //.
    all: rewrite expnS.
    all: rewrite leq_pmulr.
    all: rewrite //.
    all: rewrite expn_gt0.
    all: rewrite ltnW.
    all: done. }

This would allow examining, step by step, what is happening. Of course, a macro undoing this expansion would facilitate editing the rewrite chain.

This is for the rewrite from ssr. The default rewrite tactic (where rules are separated by ,), has a slightly different semantics where subsequent rules are only applied to the "main" and not to those generated by rules with premises.

(Doing this with Coq-side support may be desirable, but it might be a while before the Coq document model has matured to the point where this can easily be supported)

[erikmd]

Hi @chdoc, thanks for suggesting this! sounds like a neat feature to have for ssreflect proofs indeed.

would you already have further suggestions to refine that part of the feature you mention?:

a macro undoing this expansion would facilitate editing the rewrite chain.

(e.g., maybe the inserted expanded line should be partly locked for editing, e.g. the all: rewrite substrings? other ideas?)

[chdoc]

I would be happy to have a bare-bones implementation that I can play around with sooner rather than later. Unfortunately, I'm not very good at elisp. But now that you ask, here are some ideas:

1. handle the case with and without an initial by / final all: done
2. add a macro for "new line beginning with all:rewrite" (along the lines of "new item" in auctex)

I'm neutral about the locking for rewriting. But if "marking" the all:rewrite makes it easier to do the folding, I'd be fine with that. Although that would require using a macro to insert steps in between. Also, folding should probably be robust with regard rewrite with multiple rules, as to not force people to add another "all:rewrite" line just to insert a rule.

[erikmd]

Hi @chdoc

idea: add a macro for "new line beginning with all:rewrite" − I'm neutral about the locking for rewriting

indeed, the "lock" seems unneeded, provided it is easy to add "another line" and the "folding" is robust.

I believe there had been a thread on the ssreflect mailing list a long time ago, on a related topic (?) Cc @gares @CohenCyril @amahboubi @ggonthier @ybertot, would you have some specific comments/remarks/suggestions regarding this feature proposal? (hopefully I didn't forgot mentioning someone among the math-comp dev-team using emacs; otherwise sorry for that…)

BTW we should double-check from which Coq version the all: _ goal selector is available… And we should also decide which keybinding would be OK for the three steps involved (expansion; new line; folding) − below is the current list of keybindings FYI

C-c C-b		proof-process-buffer
C-c C-c		proof-interrupt-process
C-c C-d		proof-tree-external-display-toggle
C-c C-f		proof-find-theorems
C-c TAB		proof-query-identifier
C-c C-l		proof-layout-windows
C-c RET		proof-goto-point
C-c <C-return>  proof-goto-point
C-c C-n		proof-assert-next-command-interactive
C-c C-o		proof-display-some-buffers
C-c C-p		proof-prf
C-c C-r		proof-retract-buffer
C-c C-s		proof-toggle-active-scripting
C-c C-t		proof-ctxt
C-c C-u		proof-undo-last-successful-command
C-c C-v		proof-minibuffer-cmd
C-c C-w		pg-response-clear-displays
C-c C-x		proof-shell-exit
C-c C-z		proof-frob-locked-end
C-c >		proof-autosend-toggle
C-c `		proof-next-error
C-c b		proof-toolbar-toggle
C-c v		pg-toggle-visibility
C-c C-S-h	proof-help
C-c C-.		proof-goto-end-of-locked
C-c C-;		pg-insert-last-output-as-comment
C-c <C-backspace>		proof-undo-and-delete-last-successful-command

C-M-a		proof-goto-command-start
C-M-e		proof-goto-command-end
M-a		proof-backward-command
M-e		proof-forward-command
M-n		pg-next-matching-input-from-input
M-p		pg-previous-matching-input-from-input

C-M-q		prog-indent-sexp

C-c C-a C-a	coq-Search
C-c C-a C-b	coq-About
C-c C-a C-c	coq-Check
C-c C-a TAB	coq-insert-intros
C-c C-a C-l	coq-LocateConstant
C-c C-a RET	coq-insert-match
C-c C-a C-n	coq-LocateNotation
C-c C-a C-o	coq-SearchIsos
C-c C-a C-p	coq-Print
C-c C-a C-q	coq-query
C-c C-a C-r	coq-insert-requires
C-c C-a C-s	coq-Show
C-c C-a C-t	coq-insert-tactic
C-c C-a C-w	coq-ask-adapt-printing-width-and-show
C-c C-a !	coq-insert-solve-tactic
C-c C-a [	coq-insert-as-in-next-command
C-c C-a g	proof-store-goals-win
C-c C-a h	coq-PrintHint
C-c C-a r	proof-store-response-win
C-c C-a t	coq-insert-tactical
C-c C-a C-SPC	coq-insert-term
C-c C-a C-(	coq-insert-section-or-module
C-c C-a C-)	coq-end-Section
C-c C-a <C-return>		coq-insert-command

[CohenCyril]

I like this feature.

[chdoc]

And we should also decide which keybinding would be OK for the three steps involved

In my setup (PG + company-coq) C-c r is unbound. How about:

• C-c r x : coq-ssr-rewrite-expand
• C-c r i : coq-ssr-rewrite-insert-rule
• C-c r f : coq-ssr-rewrite-fold

(with C-x r ... are the register commands, but I don't think that's a problem)

If there is ever to be a corresponding set of macros for the default rewrite tactic, we may need a setting to disambiguate. But I'm not sure long rewrite chains are all that common outside of mathcomp.

[erikmd]

Hi @chdoc

And we should also decide which keybinding would be OK for the three steps involved

In my setup (PG + company-coq) C-c r is unbound.

even if most prover commands start with C-c C-a …, C-c r LGTM at first sight.

How about:

* `C-c r x` : `coq-ssr-rewrite-expand`

I'd rather suggest C-c r e maybe, as e is the initial of expand (and edit).

* `C-c r i` : `coq-ssr-rewrite-insert-rule`

yes, why not. otherwise C-c r RET maybe ?

* `C-c r f` : `coq-ssr-rewrite-fold`

:+1:

(with C-x r ... are the register commands, but I don't think that's a problem)

Indeed C-c and C-x are really independent.

If there is ever to be a corresponding set of macros for the default rewrite tactic, we may need a setting to disambiguate. But I'm not sure long rewrite chains are all that common outside of mathcomp.

if need be, we might later add a prefix (C-u C-c r e) to separate the versions, or simply auto-detect if the current file has Required ssreflect, a bit like how @CyrilAnac has implemented PR #480.

Cc @ProofGeneral/core, what is your opinion on these keybindings? C-c r e, C-c r i (or C-c r RET), C-c r f

[Matafou]

I think this feature goes beyong ssreflect. I have been thinking about something like this for the ; tactical. Debuging foo;bar;rab;oof boils down to the same mechanics really.

My 2 cents for now:

• Going back to a one-liner from the expanded and modified thing seems difficult, but storing the initial command in a comment is easy. And what you want is probably:

1. expand
2. experiment
3. go back to initial, modify it a bit, se what happens
4. expand the new command again and so on

• No opinion on the shortcuts. I am quite fed up with C-C C-a myself. I think contextual menu (with shortcuts displayed) would be nice.

[chdoc]

I think this feature goes beyong ssreflect. I have been thinking about something like this for the ; tactical. Debuging foo;bar;rab;oof boils down to the same mechanics really.

You are right. However, the difference is that by rewrite requires two edits at different places (the initial by and an intermediate . to see what's happening. For simple chains of ;, one can just do one local edit. So, while a minor nuisance, it's a lot less annoying. And in mathcomp by rewrite is everywhere.

Going back to a one-liner from the expanded and modified thing seems difficult, but storing the initial command in a comment is easy. And what you want is probably:

1. expand
2. experiment
3. go back to initial, modify it a bit, se what happens
4. expand the new command again and so on

I'm not sure I agree. For the rewrite case, going back basically amounts to removing intervening .\n all:rewrite (plus white space) and turning a potential final all:done into a by prefix. It the expansion the content of the {...} does not conform to the structure of an expanded rewrite, it would be okay to raise an error. And I do want an "expand, edit, fold" workflow.

The main thing that is keeping me from trying to implement this myself is that I'm not sure how to "tokenize" the rewrite rules, in particular in the presence of pattern selection and parentheses (e.g., rewrite [[set x in A | _ ]](some_lemma arg1 arg2))

[erikmd]

I think this feature goes beyong ssreflect. I have been thinking about something like this for the ; tactical. Debuging foo;bar;rab;oof boils down to the same mechanics really. … Going back to a one-liner from the expanded and modified thing seems difficult

actually I believe the difficulty is the other way around:

1. going back from the expanded script to a one-liner is OK if each line is prepended by all:, namely

{ rewrite lem1.
  all: rewrite lem2.
  all: try tac3.
  all: done }

could be replaced with by rewrite lem1 lem2; try tac3.

2. while I'm unsure whether one-liners could be expanded in a systematic way, in the presence of ssreflect proof selectors such as first and last. Namely, what would be the expansion of this one-liner?

by rewrite lem1 lem2; last apply: lem3.

Should the expansion macro fail in this case? or just expand by rewrite lem1 lem2 and keep ; last apply: lem3. somewhere e.g. in a comment? other ideas?

The main thing that is keeping me from trying to implement this myself is that I'm not sure how to "tokenize" the rewrite rules, in particular in the presence of pattern selection and parentheses (e.g., rewrite [[set x in A | _ ]](some_lemma arg1 arg2))

IINM the only solution for "tokenizing" your example would see [[set x in A | _ ]](some_lemma arg1 arg2) as an atom (a rstep to borrow the naming of the ssreflect refman) and that should be feasible to implement this by taking advantage of the fact that brackets are balanced.

[Matafou]

@chdoc, @erikmd good points.

This complex parsing of commands is probably much easier and safer to code on the ocaml side. @chdoc I don't understand your remark about the document model. I don't know if the coq team has time for this but it would be nice.

Maybe someone should fill a feature request for a command like:

Show SSR Rewrite Expansion <cmd>. Show THEN Expansion <cmd>.

Show SSR Rewrite Contraction <cmd>. Show THEN Contraction <cmd>.

I would also ask for this:

Show Tactic Expansion <tac>

That would play the role of the old "Info" tactical that is not yet reborn.

[gares]

Something along these lines can be surely implemented, I'm just wondering which is the best strategy. For example, as a first step one could just implement expansion, and have the UI do something like

(* begin expansion: original line *)
expanded code
(* end expansion *)

so that one could play with expanded code, then fix the original line, and finally discard the expanded code and restore the (updated) original line.

Propagating back changes done to multiple lines is, to me, much harder to implement on the Coq side since it cannot be done at the tactic level, but only at the document manager level (where all lines are visible, at the tactic level only one line is).

As a "concrete" syntax I would propose an attribute #[expand] that is ignored by "lines" for which the system does not know how to compute an expansion, while it would generate some specific printing (in addition to executing the line) for lines supporting expansion. So PG could silently sneak in a #[expand] attribute in front of commands when the user requires it and see if a more "expanded" version can be printed.

Expansion request could be iterated, in the sense that one may not want to have a long line be exploded into tiny fragments. Eg move: H1 H2; rewrite foo ?bar // =>x /fooP could first unfold to 3 steps (move:, rewrite and move=>). This seems also simpler to implement, since expansion instruction has not to be threaded deeply in the code (or across code that does not understand the flag). Imagine that Coq knows how to expand ; and rewrite, but not move:. This strategy would still work, while a more global one may not.

[gares]

Note that generating

(* begin expansion: original line *)
original line
(* end expansion *)

could be useful even if no expansion was provided. One can still break down the line by hand and while keeping the original one up there and have a keybinding to discard his manual expansion in favor of the line in the comment when he is finished.

[erikmd]

Hi @gares, thanks for your comments.

That's good if you think something is feasible (in a more "semantic" way) from the coq/ocaml side for the "expansion". But as I had mentioned in another comment, do you think by rewrite lem1 lem2; last apply: lem3. would admit a proper expansion?

Regarding the final folding, I believe this is actually easier to do in a syntactic way (e.g., from PG) so I'm not too worried about that.

And maybe the folding feature could actually be useful independently of the "expansion-folding" workflow? (indeed when developing ssreflect proof scripts, I think it is very common to compress rewrite/apply/… consecutive lines to get one-liners or so (while preserving the 80-char limit of course); however the lines at stake to compress won't start with all: …, so maybe I'm too optimistic here)

[chdoc]

As a "concrete" syntax I would propose an attribute #[expand] that is ignored by "lines" for which the system does not know how to compute an expansion, while it would generate some specific printing (in addition to executing the line) for lines supporting expansion. So PG could silently sneak in a #[expand] attribute in front of commands when the user requires it and see if a more "expanded" version can be printed.

Why execute the line when an expansion is requested? Presumably, if a user wants to expand a line, he does not want to execute the line as a whole. So the interface would likely undo the tactic execution immediately. Another question is whether one wants to enable expanding tactics that are not the next tactic to be executed. Though that may not be useful enough to warrant complicating the implementation.

[erikmd]

FYI I just posted a related question on zulip.

[Matafou]

But as I had mentioned in another comment, do you think by rewrite lem1 lem2; last apply: lem3. would admit a proper expansion?

Maybe something like:

{ all: rewrite lem1.
  all: rewrite lem2.
  -1: apply lem3. }

or if -1: does not work (does it?) then:

{ all: rewrite lem1.
  all: rewrite lem2.
  all: cycle -1.
  1: apply lem3. }

[erikmd]

Hi @Matafou, thanks for you comment!

indeed,

{ all: rewrite lem1.
  all: rewrite lem2.
  all: cycle -1.
  1: apply lem3. }

is a working workaround (while -1: is not supported but parsed as - (bullet) then 1:)

meanwhile, thanks to the Ltac Coq refman I found another possible solution, a bit verbose albeit not requiring goal permutation:

{ all: rewrite lem1.
  all: rewrite lem2.
  all: [> .. | apply: lem3]. }

all things put together, maybe there is enough material along these lines, to implement a PoC (when we'll find the time for that) handling most ssr one-liners idioms − assuming we fallback to "no-op" if the phrasing of the one-liner is not supported.

[chdoc]

Well, I would be happy with a prototype that handles only the [by] rewrite from ssreflect. The reason for this is that there is a plan to remove occurrence selectors in favor of pattern selectors in mathcomp. There are many occurrence selectors and they often occur in the middle of long rewrites. This was my motivation for this feature request.

[Matafou]

I guess we won't work on a poc until summer holidays.

By the way, looking back at the first example of this feature wish:.

by rewrite leqNgt (leq_trans m_gt1) // expnS leq_pmulr // expn_gt0 ltnW. 

being transformed into:  

  { rewrite leqNgt.
    all: rewrite (leq_trans m_gt1).
    all: rewrite //.
    all: rewrite expnS.
    all: rewrite leq_pmulr.
    all: rewrite //.
    all: rewrite expn_gt0.
    all: rewrite ltnW.
    all: done. }

I have a naive question: why not having the latter in the source and have IDE fold it and show a compacted version more or less like the former when not editing it?

I have always been very displeased with this long combinations: hard to write, extend and debug. Same for the long series of ;.

Especially if we could do something like this (which is not the case currently I think):

all:{
   1: rewrite leqNgt.
   rewrite (leq_trans m_gt1).
   rewrite //.
   rewrite expnS.
   rewrite leq_pmulr.
   rewrite //.
   rewrite expn_gt0.
   rewrite ltnW.
   done. }

[CohenCyril]

I have a naive question: why not having the latter in the source and have IDE fold it and show a compacted version more or less like the former when not editing it?

Believe it or not :wink: but

• I do read most ssreflect scripts without relying on an editor (only the ones that are tidied up and not only mine) and would be annoyed that the source is expanded by default.
• I often write full lines of rewrite scripts in one go (when you are used to it you know exactly what should go after what) and I would be pretty annoyed that the editor auto expands it.

[gares]

I'm not really convinced, what you propose @Matafou is like asking ML programs to be written in administrative normal form. Sure, it would ease the work of a small step debugger, but it is not what an experienced programmer likes to read/write.