Stream: math-comp users

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


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

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

view this post on Zulip Cyril Cohen (Nov 15 2022 at 09:27):

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

view this post on Zulip Julien Puydt (Nov 15 2022 at 09:40):

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

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

view this post on Zulip Paolo Giarrusso (Nov 16 2022 at 00:30):

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

view this post on Zulip Ricardo (Nov 16 2022 at 00:56):

Yes, I think so.


Last updated: Feb 08 2023 at 04:04 UTC