## Stream: math-comp users

### Topic: view to transform nested [forall x, forall y, ...]

#### Ricardo (Nov 15 2022 at 03:18):

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

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`?

#### Julien Puydt (Nov 15 2022 at 06:25):

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!

#### Cyril Cohen (Nov 15 2022 at 09:27):

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

#### Julien Puydt (Nov 15 2022 at 09:40):

@Cyril Cohen , oh indeed then `by apply: (iffP 'forall_forallP).` is a one-liner.

#### Ricardo (Nov 15 2022 at 21:43):

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!

#### Paolo Giarrusso (Nov 16 2022 at 00:30):

so `'forall_forallP` is really parsed as `'forall_ forallP`? :-|

#### Ricardo (Nov 16 2022 at 00:56):

Yes, I think so.

Last updated: Jul 23 2024 at 20:01 UTC