CC @erikmd

Dear @mrhaandi, thanks for the question. Indeed, the issue you observe comes from the fact rewrite (surjective_pairing a) (in your second example) unexpectedly rewrites the hidden evar, which subsequently prevents the over tactic to instantiate it:

Lemma fails (A: list (nat * nat)) (f: nat -> nat): 
  map (fun (a: nat * nat) => fst (let '(x, y) := a in (f x, f y))) A = map (fun (a: nat * nat) => f (fst a)) A.
Proof.
under map_ext.
  move=> a.

  Set Printing All.
  (* @Under_eq nat (…) (?Goal a) *)

  rewrite (surjective_pairing a).
  (*  @Under_eq nat (…) (?Goal (@pair nat nat (@fst nat nat a) (@snd nat nat a))) *)

So to fix you proof script, I'll suggest you just do

under map_ext.
  move=> a. rewrite {1}(surjective_pairing a). over.

or more succinctly:

under map_ext => a.
  by rewrite {1}(surjective_pairing a) over.

I see, thank you @erikmd .
However, for more complex examples it is tedious to figure out the particular occurrences.
For now, I have a workaround (see below) based on the contextual pattern in Under_eq _ that seems to select the right occurrences.

Lemma workaround (A: list (nat * nat)) (f: nat -> nat): 
  map (fun (a: nat * nat) => fst (let '(x, y) := a in (f x, f y))) A = map (fun (a: nat * nat) => f (fst a)) A.
Proof.
  under map_ext.
    move=> a. rewrite [in Under_eq _] (surjective_pairing a). over.
  done.
Qed.

Since Under_eq itself is supposed to be hidden, this workaround still feels hacky.

Erik, I don't get why the evar that was touched by rewrite cannot be instantiated. Isn't it a weakness of reflexivity (unification)?

I don't mind hardwiring in the pattern selection algorithm a blacklist for the last argument of under_eq, I think it is a feature of more general interest, but I want to understand what fails precisely.

In the meantime I suggest you use the pattern, you can also do as for LHS, see bigop.v, to define a shorthand. If you are consistent then porting your scripts to a fixed version of SSR can be done with a simple search/replace.

@mrhaandi

Since Under_eq itself is supposed to be hidden, this workaround still feels hacky.

Yes, and BTW Under_eq will be replaced with Under_rel in the upcoming 8.11, cf. #10022

@gares

Erik, I don't get why the evar that was touched by rewrite cannot be instantiated. Isn't it a weakness of reflexivity (unification)?

No, this occurs precisely because the lemma that is rewritten here falls in the following corner case:
it has type a = (a.1, a.2), so it applies to all occurrences of bound variable a, including (?Goal a) … and this rewrite is precisely what we wouldn't want in practice.

I don't mind hardwiring in the pattern selection algorithm a blacklist for the last argument of Under_eq, I think it is a feature of more general interest,

Sounds a good idea 👍 (I don't see other solutions apart from that and the use of an occurrence selector / contextual pattern)

Hi @gares

I don't mind hardwiring in the pattern selection algorithm a blacklist for the last argument of under_eq,

IINM that blacklisting for Under_rel should be implemented in plugins/ssrmatching/ssrmatching.ml…

can you have a look in the upcoming days? (I'd be willing to help if need be, but I am not familiar with the pattern selection algo implemented in that file;
and I don't know if it should be kept possible to bypass that hardwired blacklisting for Under_eq/Under_rel, e.g. by doing rewrite [in X in @Under_eq _ _ X]lem?)

(reminder: Under_eq is the "tag" for Coq 8.10, and Under_rel for Coq 8.11)

I'm sorry but I'm a bit busy. What I had in mind is to have in ssrmatching.v a transparent polymorphic identity function called nomatch, Registered as ssr.nomatch and have the first two terms to which it is applied be ignored by these pieces of code:

Then under generates the goal Under_rel T LHS (nomatch T RHS) and that is all.

the first two terms

This is to deal with the corner case nomatch (T1 -> T2) f t that should not protect t. Such a term can be, in principle, obtained by applying other tactics if we start using nomatch elsewhere. It should not happen in the case of under I believe.

FTR, this feature should be documented next to lock, since it is serves similar purposes, but has no logical effect (while lock t =/= t, and indeed one can use lock to decorate the head of an application, so that matching does not recognize it, but it does not prevent matching to recurse under it).

Thanks @gares for your comments!

A question on a detail:

this feature should be documented next to lock

you seem to suggest here to add the nomatch function in ssreflect.v, but as this change deals with ssrmatching.ml, shouldn't this be added to ssrmatching.v ?

Sure, I think I'd be fine with a See also...