Stream: math-comp users

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


view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Nov 15 2021 at 08:49):

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

view this post on Zulip 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.

view this post on Zulip Christian Doczkal (Nov 15 2021 at 08:53):

Try Search {in _, _}.

view this post on Zulip 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!

view this post on Zulip Notification Bot (Nov 15 2021 at 09:09):

Andrey Klaus has marked this topic as resolved.

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Nov 15 2021 at 09:12):

CC @Erik Martin-Dorel

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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. ^^

view this post on Zulip 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:


Last updated: Jan 29 2023 at 19:02 UTC