Stream: math-comp users

Topic: ✔ working with `{in _ _}`

Andrey Klaus (Nov 15 2021 at 07:57):

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.

1. 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 ->...)
2. How to query Locate about this {in}? Locate "{in _, _}" and Locate "{in _}" didnt help.

Enrico Tassi (Nov 15 2021 at 08:49):

You probably need to Locate "{ in _ }" (with a space)

Enrico Tassi (Nov 15 2021 at 08:52):

I would look for a lemma linking all and cat to operate on the conclusion, but I did not try.

Christian Doczkal (Nov 15 2021 at 08:53):

Try Search {in _, _}.

Andrey Klaus (Nov 15 2021 at 09:08):

@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!

Notification Bot (Nov 15 2021 at 09:09):

Andrey Klaus has marked this topic as resolved.

Christian Doczkal (Nov 15 2021 at 09:09):

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?

Enrico Tassi (Nov 15 2021 at 09:12):

CC @Erik Martin-Dorel

Andrey Klaus (Nov 15 2021 at 09:12):

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

Erik Martin-Dorel (Nov 16 2021 at 22:23):

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.

Christian Doczkal (Nov 16 2021 at 22:38):

@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.

Christian Doczkal (Nov 17 2021 at 15:35):

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. ^^

Erik Martin-Dorel (Nov 18 2021 at 01:06):

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: Jan 29 2023 at 19:02 UTC