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 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
```

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: Jan 29 2023 at 18:03 UTC