Stream: math-comp users

Topic: under rewriting


view this post on Zulip Florent Hivert (Sep 16 2021 at 17:55):

Reading the source, I just discovered the under / over tactical. This is brilliant ! Being able to write

 under eq_bigr do rewrite expr0.

is so handy ! Just one question: In the interactive mode, after the over. I end up with goal such as:

\sum_(i <- ...) (fun i 0=> a + i0) i

I need to rewrite /= to get

\sum_(i <- ...) a + i

I tried over => /= or over; rewrite /= but it doesn't work. It seems that what follows over is simply ignored. Is it the case ? Is it on purpose ?

view this post on Zulip Enrico Tassi (Sep 16 2021 at 19:50):

I would be surprised if (under ....) => /= was not working (in a one liner), but I can see the pain point... CC @Erik Martin-Dorel

view this post on Zulip Enrico Tassi (Sep 16 2021 at 19:56):

Usually, Coq beta-iota reduces goals, so it would not be too ad-hoc imo to systematically reduce that beta-redex (without even requiring a /=) at over time.

view this post on Zulip Erik Martin-Dorel (Sep 16 2021 at 22:04):

Hi, thanks @Enrico Tassi for the ping.
@Florent Hivert I didn't take a close look at your example (but feel free to post a complete, minimal lemma example if need be) but I'd suspect you just hit the following known issue (a minor limitation of the under tactic):
https://github.com/coq/coq/issues/11118

view this post on Zulip Erik Martin-Dorel (Sep 16 2021 at 22:09):

Roughly speaking, this limitation is due to the fact some too-aggressive rewrites (or maybe just a simpl) could impact the underlying evar (that is hidden by the notation); so if your example is also related to this issue, the standard workaround would be to guard the rewrite with a contextual pattern…

view this post on Zulip Erik Martin-Dorel (Sep 16 2021 at 22:12):

Ah sorry @Florent Hivert, I think I read your question too fast.
Indeed, the behavior you describe is fairly normal, and documented in the manual: https://coq.github.io/doc/master/refman/proof-engine/ssreflect-proof-language.html?highlight=under#one-liner-mode

view this post on Zulip Erik Martin-Dorel (Sep 16 2021 at 22:20):

To sum up, there is a small difference regarding beta-iota-reduction of the goals between the interactive mode of under (without do …) and the one-liner mode of under (with a do … clause), and this difference shows up typically when using bigops, given they are defined in a way that naturally builds beta-redexes from the general term.
Keeping or removing these beta redexes should have no impact on the proof term, so you could just as well do over. simpl. temporarily and remove the simpl. after completing the proof… but feel free to open an issue in the bug tracker if you want: indeed I agree with @Enrico Tassi that we may try to extendover with some "beta-iota-reduction post-processing" (albeit it would not be fully straightforward because this post-processing step should not be done on the current goal, but on all other goals… does this make sense, Enrico?)

view this post on Zulip Florent Hivert (Sep 16 2021 at 22:32):

@Erik Martin-Dorel Thanks for your detailed answer.

Sorry if my question wasn't clear. Here is an example. After:

Lemma bla K i (s : seq nat) : K = \sum_(j <- s) (i + j).
Proof.
under [RHS]eq_bigr => j _.
  rewrite addnC.
over.

I get the goal

  K = \sum_(j <- s) (addn^~ i) j

instead of

  K = \sum_(j <- s) (j + i)

I understand that this is expected. What surprise me is that

Lemma bla K i (s : seq nat) : K = \sum_(j <- s) (i + j).
Proof.
under [RHS]eq_bigr => j _.
  rewrite addnC.
over; rewrite A_lemma_that_even_doesnt_exists.

doesn't complain. I would expect it to raise an error and that

...
over; rewrite /=.

simplifies the goal and that

view this post on Zulip Florent Hivert (Sep 16 2021 at 22:35):

Of course replacing the ; by a . after over shows the expected behavior.

view this post on Zulip Erik Martin-Dorel (Sep 16 2021 at 22:43):

Thanks @Florent Hivert for providing a complete example!

Actually, no bug expected here: as over is a terminator and it succeeds alone, any syntactically correct tactic over; some_tactic. succeeds as well, even if some_tactic would fail alone on a goal.
Think of, for example, the toy example tactic admit; fail.

view this post on Zulip Erik Martin-Dorel (Sep 16 2021 at 22:44):

And regarding the over tactic itself and simpl, note that over; simpl. couldn't work for your use case, because you'd like that simpl. impacts the other subgoals, which is not what the semantics of ; could provide.

view this post on Zulip Erik Martin-Dorel (Sep 16 2021 at 22:53):

(If one really wants a single tactic to do this (with the current version of over), one might think of all: over || simpl. but it's somewhat-ugly… and longer to type than over. simpl. :)

view this post on Zulip Enrico Tassi (Sep 17 2021 at 07:41):

I think the subtlety is that in interactive mode when Coq decides to simplify the goal it is too early, only when the evar gets assigned the beta redex materializes. So I was proposing to make over act on two goals (at the ml level it should be doable) and beta reduce the second one.

view this post on Zulip Erik Martin-Dorel (Sep 17 2021 at 07:57):

OK!, but what should happen if the user types 2: over. ?

view this post on Zulip Erik Martin-Dorel (Sep 17 2021 at 07:58):

I just mean, maybe it's tricky to implement the enhancement you are suggesting...

view this post on Zulip Florent Hivert (Sep 17 2021 at 08:55):

While we are speaking about under. I just hit the following problem: when I write

Lemma under_big_pair (s : seq (nat * nat)) : \sum_(p <- s) (p.1 + p.2) = 0.
Proof.
under eq_bigr.
  case => [u v] _.
  by rewrite over.

Coq fails with

Error: No applicable tactic.

is it the same problem as the aforementioned issue https://github.com/coq/coq/issues/11118 ? I'm not expert enough about Coq's internal to understand what is happening. Compared to the issue, I haven't done any rewriting, but in both cases, there is a sequence of pair.

view this post on Zulip Pierre Roux (Sep 17 2021 at 11:41):

under does not accept destructing the "index" variable, so you have to keep the pair p intact. IINM that's because this variable is used internally by the tactic, so if you destruct it, it is missing at the end and over cannot do its job.

view this post on Zulip Florent Hivert (Sep 17 2021 at 12:45):

@Pierre Roux Thanks for the answer. I can't find any reference to that in the documentation. Is there any ? Or is it something you have deduced ?

view this post on Zulip Pierre Roux (Sep 17 2021 at 13:03):

This is indeed probably missing in the doc. I mostly deduced it from running into similar issues to yours and getting confirmation from the author of the tactic (@Erik Martin-Dorel ). Similarly, you should avoid anything that could rewrite that instance of the index variables (which might not be obvious because that particular instance is hidden below the big Under notation).

view this post on Zulip Erik Martin-Dorel (Sep 17 2021 at 13:28):

Hi! indeed… and an extra remark in the Coq manual about this could be useful…

view this post on Zulip Erik Martin-Dorel (Sep 17 2021 at 13:30):

BTW @Florent Hivert, beyond the Sphinx-based doc, you might want to browse the test file dedicated to under, if you want to see more examples of use:
https://github.com/coq/coq/blob/d2ded49fa464b9c898b4bb1e6532a4411e393807/test-suite/ssr/under.v
or the demo that was presented at the Coq Workshop 2019:
https://www.irit.fr/~Erik.Martin-Dorel/exposes/coq10_demo_under.v
https://www.irit.fr/~Erik.Martin-Dorel/exposes/2019_coq10_ssr.pdf

view this post on Zulip Florent Hivert (Sep 17 2021 at 14:43):

Thanks for all those precision and pointers.

view this post on Zulip Florent Hivert (Sep 17 2021 at 14:45):

The test files seems indeed to be full of good examples ! As always, there is no better doc than the sources and the tests :wink:


Last updated: Mar 29 2024 at 13:01 UTC