Ricardo (Nov 15 2022 at 03:18): 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?
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: Feb 08 2023 at 04:04 UTC