Stream: math-comp users

Topic: Converting `rel` to set function

Julin Shaji (Apr 12 2024 at 06:40):

I have a relation R : rel T where T : finType.

So, R would be like T -> T -> bool, right?

I wish to use this R to make a function f: {set T} -> {set T} such
that for f X,

• x ∈ X -> ∀y ∈ T, R x y -> y ∈ f X

ie, f kind of 'gathers together' info from R.

Is this a good way of doing this and proving it correct?

From mathcomp Require Import all_ssreflect.

Section Foo.
  Context {T: finType} (a b: T).
  Context (R: rel T) (X: {set T}).

  Definition funify := [set y | x in X, y in T & R x y].

  Goal forall x y: T,
    x \in X ->
    y \in funify ->
    R x y.
  Proof.
    move => x y.
    rewrite /funify /=.
  Abort.

  Goal forall x y: T,
    R x y ->
    x \in X ->
    y \in funify.
  Proof.
    rewrite /funify /= => x y.
  Abort.
End Foo.

Julin Shaji (Apr 12 2024 at 10:08):

Saw finset.equivalence_partition, but that's not what's needed in this case, right?

Emilio Jesús Gallego Arias (Apr 18 2024 at 12:40):

Umm, I don't see how the first goal could be true. For example take R = eq , T = 2 and X = {1,2} , then funify X = {1,2}, however 1 \in X 2 \in funify, however R 1 2 = false ?

Julin Shaji (Apr 19 2024 at 10:53):

Oh.. yeah.. Thanks.
Dunno what I was thinking.

Julin Shaji (Apr 19 2024 at 10:53):

I'm taking only y and I can't expect x to be there always.

Emilio Jesús Gallego Arias (Apr 22 2024 at 11:50):

I get the feeling that you may be thinking about some relation R with some more particular properties, for example the relation could be functional, or surjective, etc...

Last updated: Oct 13 2024 at 01:02 UTC