I'd like to get your help on the following code.

```
From mathcomp Require Import ssreflect ssrbool ssrnat ssrfun eqtype choice fintype seq finfun finmap.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Definition symb (T : finType) (R : rel T) :=
[forall x, forall y, R x y == R y x].
Definition symmetric (T : Type) (R : rel T) :=
forall x y, R x y == R y x.
Lemma symP (T : finType) (R : rel T) :
reflect (symmetric R) (symb R).
Proof.
rewrite /symmetric /symb. apply: (iffP idP).
move=> /forallP H x y.
Admitted.
```

I have the feeling there's an ssreflect idiomatic way to transform the nested `[forall x, forall y, ...]`

into `forall x y, ...`

directly. Is that correct?

Also, would it be more idiomatic to write `symmetric`

as `forall x y, R x y = R y x`

?

I found what you need by digging in matrix.v, where I was sure to find such double quantifications ; and got this out:

```
Lemma symP (T : finType) (R : rel T) :
reflect (symmetric R) (symb R).
Proof.
apply: (iffP idP).
by move=> /'forall_forallP H x y.
move=> H.
by apply/'forall_forallP.
Qed.
```

From the look of it, `'forall_`

is a prefix to apply results within a `[forall ]`

, but I have no clue how it works precisely!

You can even do `apply: (iffP 'forall_forallP).`

to begin with

@Cyril Cohen , oh indeed then `by apply: (iffP 'forall_forallP).`

is a one-liner.

Nice! I had seen that notation here

```
Notation "'forall_ view" := (forallPP (fun _ => view))
(at level 4, right associativity, format "''forall_' view").
```

But didn't notice the `'`

at the beginning and was trying with `/forall_forallP`

which wasn't working. Thank you both!

so `'forall_forallP`

is really parsed as `'forall_ forallP`

? :-|

Yes, I think so.

Last updated: Jul 23 2024 at 20:01 UTC