Is it possible to convert a term like `l \in [pred l0 | size l0 == 2]`

to `(fun l0 => size l0 == 2) l`

?

I was looking for a way to do a rewriting to replace the `size l0`

part in the `\in`

version.

```
From mathcomp Require Import all_ssreflect.
Definition l: seq nat := [:: 0; 1].
Check l \in [pred l0 | size l0 == 2].
Check (fun l0 => size l0 == 2) l.
```

And how can we search for definitions involving `[pred .. ]`

?

To find definition name, `Locate "[pred _]".`

gave nothing.

Then try something less specific like `Locate "pred".`

Note that your two terms are convertible

```
Goal l \in [pred l0 | size l0 == 2] = (fun l0 => size l0 == 2) l.
Proof.
(* rewrite inE. *) (* gives (size l == 2) == (size l == 2) *)
reflexivity.
Qed.
```

Yeah, I was trying to figure out a way to convert from one form to the other. Couldn't find a way to rewrite `size l0`

when `l0`

is not even an assumption.

I mean, without having to prove a separate lemma.

Maybe there is some extensionality lemma that can be used with the `under`

tactic, like `eq_bigr`

for bigops.

I'm not (yet) familiar with `under`

.

But for now, I think I can work with this (though I'm not sure if I'm treading in the right track):

```
Goal forall (A: Type) (l:seq A) (bexp: bool),
l \in [pred l0 | bexp] = (fun l0 => bexp) l.
Proof. by []. Qed.
```

Or not.. I can't get it to work. I guess I better dig through `under`

.

Last updated: Jul 25 2024 at 16:02 UTC