## Stream: math-comp users

### Topic: Set preimage proof

#### Julin Shaji (Apr 08 2024 at 10:23):

I got a goal like this which says given a set {set A+B} in which all elements are value like inr _, the set given by inl @^-1 would be empty.

From mathcomp Require Import all_ssreflect.

Goal forall {A B: finType} (b: {set B}),
(* inl @^-1: ((inr (A:=A)) @: b) = set0. *)
inl @^-1: [set (inr (A:=A)) x | x in b] = set0.
Proof.
move => A B b.
(*
1 subgoal

A, B : finType
b : {set B}

========================= (1 / 1)

inl @^-1: [set inr x | x in b] = set0
*)
Search (_ @^-1: _).


How can we proceed from here?

Couldn't figure out a suitable lemma with the Search.

#### Reynald Affeldt (Apr 08 2024 at 10:33):

to show that two sets are equal, you can use apply/setP.

#### Julin Shaji (Apr 08 2024 at 10:45):

Thanks. Made some progress with it:

  Lemma foo1: forall {A B: finType} (b: {set B}),
inl @^-1: ((inr (A:=A)) @: b) = set0.
(* inl @^-1: [set (inr (A:=A)) x | x in b] = set0. *)
Proof.
move => A B b.
apply/setP => //= x.
rewrite !in_set.
(*
1 subgoal

A, B : finType
b : {set B}
x : A

========================= (1 / 1)

(inl x \in [set inr x | x in b]) = false
*)
Search (_ \in _).


Rewriting with unfold_in reduces it to [set inr x | x in b] (inl x) = false but was not sure if that's the way to go..

#### Reynald Affeldt (Apr 08 2024 at 11:12):

apply/negbTE changes the goal with better notations

#### Reynald Affeldt (Apr 08 2024 at 11:13):

and then you want to look at imsetP because you are dealing with the image of a set

#### Julin Shaji (Apr 08 2024 at 11:26):

Could do it!
Not sure if I'm doing it in a proper way, though..

  Lemma bar: forall {A B: Type} (a: A) (b: B),
inl (B:=B) a = inr (A:=A) b -> False.
Proof.
move => A B a b.
move => H.
inversion H.
Qed.

Lemma foo1: forall {A B: finType} (b: {set B}),
inl @^-1: ((inr (A:=A)) @: b) = set0.
Proof.
move => A B b.
apply/setP => //= x.
rewrite !in_set.
apply/negbTE/imsetP => [[eb]] => _.
by apply: bar.
Qed.


Is use of inversion more of a non-ssreflect style?

#### Reynald Affeldt (Apr 08 2024 at 11:30):

From mathcomp Require Import all_ssreflect.

Goal forall {A B: finType} (b: {set B}),
(* inl @^-1: ((inr (A:=A)) @: b) = set0. *)
inl @^-1: [set (inr (A:=A)) x | x in b] = set0.
Proof.
move => A B b.
apply/setP => x.
rewrite !inE.
apply/negbTE.
apply/imsetP.
by case.
Qed.


#### Reynald Affeldt (Apr 08 2024 at 11:31):

you don't need no inversion because the "inl = inr" hypo is already contradictory

#### Julin Shaji (Apr 08 2024 at 11:41):

Thanks!. Hadn't realized it can figure out the inl _ = inr _ being a contradiction by itself.
Did it separately because once I need to derive a=b from inl a = inl b. It didn't seem able to figure it out by itself then (or more likely, I didn't use some ssreflect feature).

#### Julin Shaji (Apr 08 2024 at 11:42):

I had also been trying to prove this:

  Lemma foo2: forall {A B: finType} (a: {set B}),
(* a = inl @^-1: ((inl (B:=B)) @: a). *)
a = inl @^-1: [set (inl (B:=B)) x | x in a].
Proof.
move => A B a.
apply/setP => //= x.
rewrite inE.
(*
1 subgoal

A, B : finType
a : {set B}
x : B

========================= (1 / 1)

(x \in a) = (inl x \in [set inl x0 | x0 in a])
*)


Is there some lemma that can help? I did a few Search-es, but couldn't spot any.

#### Quentin VERMANDE (Apr 08 2024 at 12:55):

Maybe mem_imset (found with Search imset mem, or more easily with Search (_ _ \in imset _ _) but that requires knowing what the notation hides).

#### Julin Shaji (Apr 08 2024 at 17:01):

mem_imset helped!

But I kind of ended up doing things a bit 'manually'..

  Lemma inl_inj {A B: Type}: injective (rT:=A+B) inl.
Proof.  by rewrite /injective => ? ?; case.  Qed.

Lemma foo2: forall {A B: finType} (a: {set A}),
a = inl @^-1: [set (inl (B:=B)) x | x in a].
Proof.
move => A B a.
apply/setP => //= x.
rewrite finset.inE.
symmetry.
exact: (mem_imset (aT:=A) (rT:=A+B)%type inl a x inl_inj).
Qed.


Could there be a better way to do this?

#### Quentin VERMANDE (Apr 08 2024 at 18:12):

You should not have to write finset., and you should be able to rewrite mem_imset just after inE.

Last updated: Jul 25 2024 at 15:02 UTC