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 ?
I would be surprised if (under ....) => /=
was not working (in a one liner), but I can see the pain point... CC @Erik Martin-Dorel
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.
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
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…
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
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?)
@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
Of course replacing the ;
by a .
after over
shows the expected behavior.
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.
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.
(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.
:)
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.
OK!, but what should happen if the user types 2: over. ?
I just mean, maybe it's tricky to implement the enhancement you are suggesting...
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.
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.
@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 ?
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).
Hi! indeed… and an extra remark in the Coq manual about this could be useful…
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
Thanks for all those precision and pointers.
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: Oct 13 2024 at 01:02 UTC