I would like to proof

```
Goal forall (T : eqType) (s1 s2 : seq T) P, all P (undup (s1 ++ s2)) -> all P s1 && all P s2.
move/allP.
```

```
T : eqType
P : pred T
s1, s2 : seq T
============================
{in undup (s1 ++ s2), forall x : T, P x} -> all P s1 && all P s2
```

Questions.

- Should I use induction or there is another way? I tryed to rewrite mem_undup, but with no success (I think it is because this
`{in }`

is kind of notation for`forall x, x \in s1 ->...`

) - How to query
`Locate`

about this`{in}`

?`Locate "{in _, _}"`

and`Locate "{in _}"`

didnt help.

You probably need to `Locate "{ in _ }"`

(with a space)

I would look for a lemma linking `all`

and `cat`

to operate on the conclusion, but I did not try.

Try `Search {in _, _}.`

@Enrico Tassi , thanks for the point , `Locate "{ in _ , _ }".`

worked right. `all_cat`

worked great too, thanks for the idea!

@Christian Doczkal , thanks for pointing to Search, I didnt try, it just works. Great!

Andrey Klaus has marked this topic as resolved.

Sometimes it's more convenient to reason about `all`

using it's own lemmas rather than using the view for Prop. Try:

```
under eq_all_r => x do rewrite mem_undup //.
by rewrite all_cat.
```

@Enrico Tassi , Why do I need to add the //, shouldn't `over`

close the goal?

CC @Erik Martin-Dorel

@Christian Doczkal , great example, it is just what I wanted to find already a couple days! Lucky day :) Thank you.

Thanks @Enrico Tassi for the ping,

Regarding @Christian Doczkal's question:

`under eq_all_r => x do tac.`

is essentially equivalent to:

`(under eq_all_r) => [x | ]; [ tac; over | cbv beta iota ].`

and over is defined by:

`Ltac over := by [ apply: under_rel_done | rewrite over ]`

**But**, if you only use the interactive mode (without the "do") on this example, I've noticed we get:

```
Goal forall (T : eqType) (s1 s2 : seq T) P, all P (undup (s1 ++ s2)) -> all P s1 && all P s2.
move=> T s1 s2 P.
under eq_all_r.
↓
- T : eqType
- s1, s2 : seq T
- P : pred T
============================
forall x : T, (x \in undup (s1 ++ s2)) = (x \in ?Goal)
subgoal 2 (ID 7724) is:
all P ?Goal -> all P s1 && all P s2
```

i.e. **there is no 'Under[ _ ] notation** for capturing the evar (and enabling the proper feature of over).

On the other hand, look at what we'd get with this script:

```
Lemma ex_map l : head 0 (map (fun m => m - m) l) = 0.
under eq_map.
↓
- l : seq nat
============================
forall x : nat, 'Under[ x - x ]
subgoal 2 (ID 7703) is:
head 0 [seq ?Goal i | i <- l] = 0
```

So I guess there's a small bug here (or at least some room for improvement), certainly due to the specific form of the extensionality lemma `eq_all_r`

.

I don't have the time to dive into this right now, but you might want to file an issue in the Coq bug tracker.

@Erik Martin-Dorel , indeed I hadn't spotted that the `'Under [ _ ]`

notation was missing. I'll try to do a (plain) Coq example tomorrow and put it in the bug tracker.

I'm just circling around to this and I'm starting to think that this is not a bug, in the sense that there is no obvious (safe) way in which things should work. My understanding is that for `under _ => x`

to work reliably, the (hidden) RHS must be of the form `?Goal x`

. In the case of `eq_all_r`

it is of a more specific shape and, indeed, one can easily do rewrites on the LHS that make unification fail (e.g. `mem_cat`

). But it is interesting to know that one can temporarily violate the shape restriction and do things like this:

```
Goal forall (T : eqType) (s1 s2 : seq T) P,
all P (undup (s1 ++ s2)) -> all P s1 && all P s2.
move=> T s1 s2 P.
under eq_all_r => x.
by rewrite mem_undup mem_cat orbC -mem_cat.
```

Whether this is code that I would like to see in the mathcomp libraries is an entirely different matter. ^^

Hi @Christian Doczkal, yes I agree that this is not a bug.

This is indeed related to the fact `under`

's automatic extensional-side-conditions-detector only handles `=1`

like quantified equalities, of kind `forall x, f x = ?Goal x`

.

So e.g. `under eq_all => x.`

is supported for now.

Anyway, even if we don't see an obvious generalization of all quantified side-conditions that are involved here,

I believe it should be at least possible to extend the tactic so that `=i`

is supported as well. So feel free to open a feature request if you agree :)

Regarding your last remark, I don't have a strong opinion, but one could either say:

- that it's possible to use "under" in this case as a kind of "erewrite";
- or more conservatively, saying that using
`under`

now with`=i`

side-conditions (that are not "protected" with the`'Under[ _ ]`

goals, and discharged without over) is not recommended.

Last updated: Jul 23 2024 at 20:01 UTC