Ssreflect Users Discussion List

[Georges Gonthier <>]

Hi,

  As a rule, the new library provides a "reflection" lemma stating the 
extensionality of all collection types such as tuples, finfuns, finsets, 
permutations, polynomials and matrices. In this case you want to use
  setP : forall (T : finType) (A B : {set T}), A =i B <-> A = B.
Since your goal is a comparison (==) you first need to turn it into an 
equation (=) using eqP; after you've introduced an arbitrary element u,
you can use in_set to expand the membership comprehension, so the line you're 
looking for might be
  apply/eqP; apply/setP=> u; rewrite !in_set /=.
This would leave you with the goal
  (u \in V_of G) &&  (((u, v) \in E_of G) || ((v, u) \in E_of G))
 = (u \in V_of G') && (((u, v') \in E_of G') || ((v', u) \in E_of G'))
which is as far as I can go without further information on G and G';
if G' = G you can pop the assumption VGu : u \in V_of G with the line
  case VGu: (u \in _) => //=.
Note that there are many other ways of dealing with the boolean equation 
subgoal produced by setP; I often use the double-reflection form of apply to 
reduce it to two implications, e.g., in your case I might write
  apply/setIdP/setIdP=> [[VGu] | [VG'u]].
The documentation for the new library is still under construction, and we 
will probably be releasing the library before it is complete; note however 
that many files have extended headers summarizing their contents.

    Georges Gonthier

-----Original Message-----
From: Filou Vincent []
Sent: 15 April 2009 13:51
To: 
Subject: equality of sets defined by comprehension

Hi all,

I'm stuck in a proof at the following subgoal:
[set u \in V_of G | ((u, v) \in E_of G) || ((v, u) \in E_of G)] == [set
u \in V_of G' | ((u, v') \in E_of G') || ((v', u) \in E_of G')]

Is there a way to transform it to something like

forall u, u \in V_of G ->(((u, v) \in E_of G) || ((v, u) \in E_of G)) ==
(((u, v') \in E_of G') || ((v', u) \in E_of G'))

?

And by the way, where can I find some documentation about the ssreflect
library?

Thanks,
Vincent