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
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
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
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
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 extend
over 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
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
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
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
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:
or the demo that was presented at the Coq Workshop 2019:
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: Jan 29 2023 at 18:03 UTC